[STATEMENT]
lemma (in Ring) zero_ideal:"ideal R {\<zero>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R {\<zero>}
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aGroup R \<Longrightarrow> ideal R {\<zero>}
[PROOF STEP]
apply (rule ideal_condition1)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. aGroup R \<Longrightarrow> {\<zero>} \<subseteq> carrier R
 2. aGroup R \<Longrightarrow> {\<zero>} \<noteq> {}
 3. aGroup R \<Longrightarrow> \<forall>x\<in>{\<zero>}. \<forall>y\<in>{\<zero>}. x \<plusminus> y \<in> {\<zero>}
 4. aGroup R \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>{\<zero>}. r \<cdot>\<^sub>r x \<in> {\<zero>}
[PROOF STEP]
apply (simp add:ring_zero)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. aGroup R \<Longrightarrow> {\<zero>} \<noteq> {}
 2. aGroup R \<Longrightarrow> \<forall>x\<in>{\<zero>}. \<forall>y\<in>{\<zero>}. x \<plusminus> y \<in> {\<zero>}
 3. aGroup R \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>{\<zero>}. r \<cdot>\<^sub>r x \<in> {\<zero>}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. aGroup R \<Longrightarrow> \<forall>x\<in>{\<zero>}. \<forall>y\<in>{\<zero>}. x \<plusminus> y \<in> {\<zero>}
 2. aGroup R \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>{\<zero>}. r \<cdot>\<^sub>r x \<in> {\<zero>}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. aGroup R \<Longrightarrow> \<zero> \<plusminus> \<zero> = \<zero>
 2. aGroup R \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>{\<zero>}. r \<cdot>\<^sub>r x \<in> {\<zero>}
[PROOF STEP]
apply (cut_tac ring_zero, simp add:aGroup.ag_l_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aGroup R \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>{\<zero>}. r \<cdot>\<^sub>r x \<in> {\<zero>}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aGroup R \<Longrightarrow> \<forall>r\<in>carrier R. r \<cdot>\<^sub>r \<zero> = \<zero>
[PROOF STEP]
apply (rule ballI, simp add:ring_times_x_0)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) whole_ideal:"ideal R (carrier R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R (carrier R)
[PROOF STEP]
apply (rule ideal_condition1)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. carrier R \<subseteq> carrier R
 2. carrier R \<noteq> {}
 3. \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<plusminus> y \<in> carrier R
 4. \<forall>r\<in>carrier R. \<forall>x\<in>carrier R. r \<cdot>\<^sub>r x \<in> carrier R
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. carrier R \<noteq> {}
 2. \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<plusminus> y \<in> carrier R
 3. \<forall>r\<in>carrier R. \<forall>x\<in>carrier R. r \<cdot>\<^sub>r x \<in> carrier R
[PROOF STEP]
apply (cut_tac ring_zero, blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<plusminus> y \<in> carrier R
 2. \<forall>r\<in>carrier R. \<forall>x\<in>carrier R. r \<cdot>\<^sub>r x \<in> carrier R
[PROOF STEP]
apply (cut_tac ring_is_ag,
        simp add:aGroup.ag_pOp_closed,
        simp add:ring_tOp_closed)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_inc_one:"\<lbrakk>ideal R I; 1\<^sub>r \<in> I \<rbrakk> \<Longrightarrow> I = carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; 1\<^sub>r \<in> I\<rbrakk> \<Longrightarrow> I = carrier R
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; 1\<^sub>r \<in> I\<rbrakk> \<Longrightarrow> I \<subseteq> carrier R
 2. \<lbrakk>ideal R I; 1\<^sub>r \<in> I\<rbrakk> \<Longrightarrow> carrier R \<subseteq> I
[PROOF STEP]
apply (simp add:ideal_subset1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; 1\<^sub>r \<in> I\<rbrakk> \<Longrightarrow> carrier R \<subseteq> I
[PROOF STEP]
apply (rule subsetI,
       frule_tac r = x in ideal_ring_multiple[of "I" "1\<^sub>r"], assumption+,
       simp add:ring_r_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_inc_one1:"ideal R I \<Longrightarrow>
                              (1\<^sub>r \<in> I) = (I = carrier R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> (1\<^sub>r \<in> I) = (I = carrier R)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; 1\<^sub>r \<in> I\<rbrakk> \<Longrightarrow> I = carrier R
 2. \<lbrakk>ideal R I; I = carrier R\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> I
[PROOF STEP]
apply (simp add:ideal_inc_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; I = carrier R\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> I
[PROOF STEP]
apply (frule sym, thin_tac "I = carrier R",
        cut_tac ring_one, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_inc_unit:"\<lbrakk>ideal R I; a \<in> I; Unit R a\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> I; Unit R a\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> I
[PROOF STEP]
by (simp add:Unit_def, erule conjE, erule bexE,
       frule_tac r = b in ideal_ring_multiple1[of "I" "a"], assumption+,
       simp)


[STATEMENT]
lemma (in Ring) proper_ideal:"\<lbrakk>ideal R I; 1\<^sub>r \<notin> I\<rbrakk> \<Longrightarrow> I \<noteq> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; 1\<^sub>r \<notin> I\<rbrakk> \<Longrightarrow> I \<noteq> carrier R
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R (carrier R); 1\<^sub>r \<notin> carrier R; I = carrier R\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add: ring_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_inc_unit1:"\<lbrakk>a \<in> carrier R; Unit R a; ideal R I; a \<in> I\<rbrakk>
                        \<Longrightarrow> I = carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; Unit R a; ideal R I; a \<in> I\<rbrakk> \<Longrightarrow> I = carrier R
[PROOF STEP]
apply (frule ideal_inc_unit[of "I" "a"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; Unit R a; ideal R I; a \<in> I; 1\<^sub>r \<in> I\<rbrakk> \<Longrightarrow> I = carrier R
[PROOF STEP]
apply (rule ideal_inc_one[of "I"], assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) int_ideal:"\<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> ideal R (I \<inter> J)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> ideal R (I \<inter> J)
[PROOF STEP]
apply (rule ideal_condition1)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> I \<inter> J \<subseteq> carrier R
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> I \<inter> J \<noteq> {}
 3. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>x\<in>I \<inter> J. \<forall>y\<in>I \<inter> J. x \<plusminus> y \<in> I \<inter> J
 4. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I \<inter> J. r \<cdot>\<^sub>r x \<in> I \<inter> J
[PROOF STEP]
apply (frule ideal_subset1[of "I"], frule ideal_subset1[of "J"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ideal R I; ideal R J; I \<subseteq> carrier R; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> I \<inter> J \<subseteq> carrier R
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> I \<inter> J \<noteq> {}
 3. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>x\<in>I \<inter> J. \<forall>y\<in>I \<inter> J. x \<plusminus> y \<in> I \<inter> J
 4. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I \<inter> J. r \<cdot>\<^sub>r x \<in> I \<inter> J
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> I \<inter> J \<noteq> {}
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>x\<in>I \<inter> J. \<forall>y\<in>I \<inter> J. x \<plusminus> y \<in> I \<inter> J
 3. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I \<inter> J. r \<cdot>\<^sub>r x \<in> I \<inter> J
[PROOF STEP]
apply (frule ideal_zero[of "I"], frule ideal_zero[of "J"], blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>x\<in>I \<inter> J. \<forall>y\<in>I \<inter> J. x \<plusminus> y \<in> I \<inter> J
 2. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I \<inter> J. r \<cdot>\<^sub>r x \<in> I \<inter> J
[PROOF STEP]
apply ((rule ballI)+, simp, (erule conjE)+,
         simp add:ideal_pOp_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; ideal R J\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I \<inter> J. r \<cdot>\<^sub>r x \<in> I \<inter> J
[PROOF STEP]
apply ((rule ballI)+, simp, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x. \<lbrakk>ideal R I; ideal R J; r \<in> carrier R; x \<in> I; x \<in> J\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r x \<in> I \<and> r \<cdot>\<^sub>r x \<in> J
[PROOF STEP]
apply (simp add:ideal_ring_multiple)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) set_sum_mem:"\<lbrakk>a \<in> I; b \<in> J; I \<subseteq> carrier R; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow>
             a \<plusminus> b \<in> I \<minusplus> J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> I; b \<in> J; I \<subseteq> carrier R; J \<subseteq> carrier R\<rbrakk> \<Longrightarrow> a \<plusminus> b \<in> I \<minusplus> J
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> I; b \<in> J; I \<subseteq> carrier R; J \<subseteq> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<plusminus> b \<in> I \<minusplus> J
[PROOF STEP]
apply (simp add:aGroup.set_sum, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) sum_ideals:"\<lbrakk>ideal R I1; ideal R I2\<rbrakk> \<Longrightarrow> ideal R (I1 \<minusplus> I2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I1; ideal R I2\<rbrakk> \<Longrightarrow> ideal R (I1 \<minusplus> I2)
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I1; ideal R I2; aGroup R\<rbrakk> \<Longrightarrow> ideal R (I1 \<minusplus> I2)
[PROOF STEP]
apply (frule ideal_subset1[of "I1"], frule ideal_subset1[of "I2"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R\<rbrakk> \<Longrightarrow> ideal R (I1 \<minusplus> I2)
[PROOF STEP]
apply (rule ideal_condition1)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R\<rbrakk> \<Longrightarrow> I1 \<minusplus> I2 \<subseteq> carrier R
 2. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R\<rbrakk> \<Longrightarrow> I1 \<minusplus> I2 \<noteq> {}
 3. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R\<rbrakk> \<Longrightarrow> \<forall>x\<in>I1 \<minusplus> I2. \<forall>y\<in>I1 \<minusplus> I2. x \<plusminus> y \<in> I1 \<minusplus> I2
 4. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I1 \<minusplus> I2. r \<cdot>\<^sub>r x \<in> I1 \<minusplus> I2
[PROOF STEP]
apply (rule subsetI, simp add:aGroup.set_sum, (erule bexE)+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x h k. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R; h \<in> I1; k \<in> I2; x = h \<plusminus> k\<rbrakk> \<Longrightarrow> x \<in> carrier R
 2. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R\<rbrakk> \<Longrightarrow> I1 \<minusplus> I2 \<noteq> {}
 3. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R\<rbrakk> \<Longrightarrow> \<forall>x\<in>I1 \<minusplus> I2. \<forall>y\<in>I1 \<minusplus> I2. x \<plusminus> y \<in> I1 \<minusplus> I2
 4. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I1 \<minusplus> I2. r \<cdot>\<^sub>r x \<in> I1 \<minusplus> I2
[PROOF STEP]
apply (frule_tac h = h in ideal_subset[of "I1"], assumption+,
        frule_tac h = k in ideal_subset[of "I2"], assumption+,
        cut_tac ring_is_ag,
        simp add:aGroup.ag_pOp_closed)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R\<rbrakk> \<Longrightarrow> I1 \<minusplus> I2 \<noteq> {}
 2. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R\<rbrakk> \<Longrightarrow> \<forall>x\<in>I1 \<minusplus> I2. \<forall>y\<in>I1 \<minusplus> I2. x \<plusminus> y \<in> I1 \<minusplus> I2
 3. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I1 \<minusplus> I2. r \<cdot>\<^sub>r x \<in> I1 \<minusplus> I2
[PROOF STEP]
apply (frule ideal_zero[of "I1"], frule ideal_zero[of "I2"],
        frule set_sum_mem[of "\<zero>" "I1" "\<zero>" "I2"], assumption+, blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R\<rbrakk> \<Longrightarrow> \<forall>x\<in>I1 \<minusplus> I2. \<forall>y\<in>I1 \<minusplus> I2. x \<plusminus> y \<in> I1 \<minusplus> I2
 2. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I1 \<minusplus> I2. r \<cdot>\<^sub>r x \<in> I1 \<minusplus> I2
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R; x \<in> I1 \<minusplus> I2; y \<in> I1 \<minusplus> I2\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> I1 \<minusplus> I2
 2. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I1 \<minusplus> I2. r \<cdot>\<^sub>r x \<in> I1 \<minusplus> I2
[PROOF STEP]
apply (simp add:aGroup.set_sum, (erule bexE)+, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y h ha k ka. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R; h \<in> I1; ha \<in> I1; k \<in> I2; x = h \<plusminus> k; ka \<in> I2; y = ha \<plusminus> ka\<rbrakk> \<Longrightarrow> \<exists>hb\<in>I1. \<exists>kb\<in>I2. h \<plusminus> k \<plusminus> (ha \<plusminus> ka) = hb \<plusminus> kb
 2. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I1 \<minusplus> I2. r \<cdot>\<^sub>r x \<in> I1 \<minusplus> I2
[PROOF STEP]
apply (rename_tac x y i ia j ja)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y i ia j ja. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R; i \<in> I1; ia \<in> I1; j \<in> I2; x = i \<plusminus> j; ja \<in> I2; y = ia \<plusminus> ja\<rbrakk> \<Longrightarrow> \<exists>h\<in>I1. \<exists>k\<in>I2. i \<plusminus> j \<plusminus> (ia \<plusminus> ja) = h \<plusminus> k
 2. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I1 \<minusplus> I2. r \<cdot>\<^sub>r x \<in> I1 \<minusplus> I2
[PROOF STEP]
apply (frule_tac h = i in ideal_subset[of "I1"], assumption+,
        frule_tac h = ia in ideal_subset[of "I1"], assumption+,
        frule_tac h = j in ideal_subset[of "I2"], assumption+,
        frule_tac h = ja in ideal_subset[of "I2"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y i ia j ja. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R; i \<in> I1; ia \<in> I1; j \<in> I2; x = i \<plusminus> j; ja \<in> I2; y = ia \<plusminus> ja; i \<in> carrier R; ia \<in> carrier R; j \<in> carrier R; ja \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>h\<in>I1. \<exists>k\<in>I2. i \<plusminus> j \<plusminus> (ia \<plusminus> ja) = h \<plusminus> k
 2. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I1 \<minusplus> I2. r \<cdot>\<^sub>r x \<in> I1 \<minusplus> I2
[PROOF STEP]
apply (subst aGroup.pOp_assocTr43, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y i ia j ja. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R; i \<in> I1; ia \<in> I1; j \<in> I2; x = i \<plusminus> j; ja \<in> I2; y = ia \<plusminus> ja; i \<in> carrier R; ia \<in> carrier R; j \<in> carrier R; ja \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>h\<in>I1. \<exists>k\<in>I2. i \<plusminus> (j \<plusminus> ia) \<plusminus> ja = h \<plusminus> k
 2. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I1 \<minusplus> I2. r \<cdot>\<^sub>r x \<in> I1 \<minusplus> I2
[PROOF STEP]
apply (frule_tac x = j and y = ia in aGroup.ag_pOp_commute[of "R"],
          assumption+, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y i ia j ja. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R; i \<in> I1; ia \<in> I1; j \<in> I2; x = i \<plusminus> j; ja \<in> I2; y = ia \<plusminus> ja; i \<in> carrier R; ia \<in> carrier R; j \<in> carrier R; ja \<in> carrier R; j \<plusminus> ia = ia \<plusminus> j\<rbrakk> \<Longrightarrow> \<exists>h\<in>I1. \<exists>k\<in>I2. i \<plusminus> (ia \<plusminus> j) \<plusminus> ja = h \<plusminus> k
 2. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I1 \<minusplus> I2. r \<cdot>\<^sub>r x \<in> I1 \<minusplus> I2
[PROOF STEP]
apply (subst aGroup.pOp_assocTr43[THEN sym], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y i ia j ja. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R; i \<in> I1; ia \<in> I1; j \<in> I2; x = i \<plusminus> j; ja \<in> I2; y = ia \<plusminus> ja; i \<in> carrier R; ia \<in> carrier R; j \<in> carrier R; ja \<in> carrier R; j \<plusminus> ia = ia \<plusminus> j\<rbrakk> \<Longrightarrow> \<exists>h\<in>I1. \<exists>k\<in>I2. i \<plusminus> ia \<plusminus> (j \<plusminus> ja) = h \<plusminus> k
 2. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I1 \<minusplus> I2. r \<cdot>\<^sub>r x \<in> I1 \<minusplus> I2
[PROOF STEP]
apply (frule_tac x = i and y = ia in ideal_pOp_closed[of "I1"], assumption+,
        frule_tac x = j and y = ja in ideal_pOp_closed[of "I2"], assumption+,
        blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I1 \<minusplus> I2. r \<cdot>\<^sub>r x \<in> I1 \<minusplus> I2
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R; r \<in> carrier R; x \<in> I1 \<minusplus> I2\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r x \<in> I1 \<minusplus> I2
[PROOF STEP]
apply (simp add:aGroup.set_sum, (erule bexE)+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x h k. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R; r \<in> carrier R; h \<in> I1; k \<in> I2; x = h \<plusminus> k\<rbrakk> \<Longrightarrow> \<exists>ha\<in>I1. \<exists>ka\<in>I2. r \<cdot>\<^sub>r (h \<plusminus> k) = ha \<plusminus> ka
[PROOF STEP]
apply (rename_tac r x i j)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x i j. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R; r \<in> carrier R; i \<in> I1; j \<in> I2; x = i \<plusminus> j\<rbrakk> \<Longrightarrow> \<exists>h\<in>I1. \<exists>k\<in>I2. r \<cdot>\<^sub>r (i \<plusminus> j) = h \<plusminus> k
[PROOF STEP]
apply (frule_tac h = i in ideal_subset[of "I1"], assumption+,
        frule_tac h = j in ideal_subset[of "I2"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x i j. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R; r \<in> carrier R; i \<in> I1; j \<in> I2; x = i \<plusminus> j; i \<in> carrier R; j \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>h\<in>I1. \<exists>k\<in>I2. r \<cdot>\<^sub>r (i \<plusminus> j) = h \<plusminus> k
[PROOF STEP]
apply (simp add:ring_distrib1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x i j. \<lbrakk>ideal R I1; ideal R I2; aGroup R; I1 \<subseteq> carrier R; I2 \<subseteq> carrier R; r \<in> carrier R; i \<in> I1; j \<in> I2; x = i \<plusminus> j; i \<in> carrier R; j \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>h\<in>I1. \<exists>k\<in>I2. r \<cdot>\<^sub>r i \<plusminus> r \<cdot>\<^sub>r j = h \<plusminus> k
[PROOF STEP]
apply (frule_tac x = i and r = r in ideal_ring_multiple[of "I1"], assumption+,
        frule_tac x = j and r = r in ideal_ring_multiple[of "I2"], assumption+,
        blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) sum_ideals_la1:"\<lbrakk>ideal R I1; ideal R I2\<rbrakk> \<Longrightarrow> I1 \<subseteq> (I1 \<minusplus> I2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I1; ideal R I2\<rbrakk> \<Longrightarrow> I1 \<subseteq> I1 \<minusplus> I2
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I1; ideal R I2; aGroup R\<rbrakk> \<Longrightarrow> I1 \<subseteq> I1 \<minusplus> I2
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal R I1; ideal R I2; aGroup R; x \<in> I1\<rbrakk> \<Longrightarrow> x \<in> I1 \<minusplus> I2
[PROOF STEP]
apply (frule ideal_zero[of "I2"],
       frule_tac h = x in ideal_subset[of "I1"], assumption+,
       frule_tac x = x in aGroup.ag_r_zero[of "R"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal R I1; ideal R I2; aGroup R; x \<in> I1; \<zero> \<in> I2; x \<in> carrier R; x \<plusminus> \<zero> = x\<rbrakk> \<Longrightarrow> x \<in> I1 \<minusplus> I2
[PROOF STEP]
apply (subst aGroup.set_sum, assumption,
       simp add:ideal_subset1, simp add:ideal_subset1, simp,
       frule sym, thin_tac "x \<plusminus> \<zero> = x", blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) sum_ideals_la2:"\<lbrakk>ideal R I1; ideal R I2 \<rbrakk> \<Longrightarrow> I2 \<subseteq> (I1 \<minusplus> I2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I1; ideal R I2\<rbrakk> \<Longrightarrow> I2 \<subseteq> I1 \<minusplus> I2
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I1; ideal R I2; aGroup R\<rbrakk> \<Longrightarrow> I2 \<subseteq> I1 \<minusplus> I2
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal R I1; ideal R I2; aGroup R; x \<in> I2\<rbrakk> \<Longrightarrow> x \<in> I1 \<minusplus> I2
[PROOF STEP]
apply (frule ideal_zero[of "I1"],
       frule_tac h = x in ideal_subset[of "I2"], assumption+,
       frule_tac x = x in aGroup.ag_l_zero[of "R"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal R I1; ideal R I2; aGroup R; x \<in> I2; \<zero> \<in> I1; x \<in> carrier R; \<zero> \<plusminus> x = x\<rbrakk> \<Longrightarrow> x \<in> I1 \<minusplus> I2
[PROOF STEP]
apply (subst aGroup.set_sum, assumption,
       simp add:ideal_subset1, simp add:ideal_subset1, simp,
       frule sym, thin_tac "\<zero> \<plusminus> x = x", blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) sum_ideals_cont:"\<lbrakk>ideal R I;  A \<subseteq> I; B \<subseteq> I \<rbrakk> \<Longrightarrow> A \<minusplus> B \<subseteq> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; A \<subseteq> I; B \<subseteq> I\<rbrakk> \<Longrightarrow> A \<minusplus> B \<subseteq> I
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; A \<subseteq> I; B \<subseteq> I; aGroup R\<rbrakk> \<Longrightarrow> A \<minusplus> B \<subseteq> I
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal R I; A \<subseteq> I; B \<subseteq> I; aGroup R; x \<in> A \<minusplus> B\<rbrakk> \<Longrightarrow> x \<in> I
[PROOF STEP]
apply (frule ideal_subset1[of I],
        frule subset_trans[of A I "carrier R"], assumption+,
        frule subset_trans[of B I "carrier R"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal R I; A \<subseteq> I; B \<subseteq> I; aGroup R; x \<in> A \<minusplus> B; I \<subseteq> carrier R; A \<subseteq> carrier R; B \<subseteq> carrier R\<rbrakk> \<Longrightarrow> x \<in> I
[PROOF STEP]
apply (simp add:aGroup.set_sum[of R], (erule bexE)+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x h k. \<lbrakk>ideal R I; A \<subseteq> I; B \<subseteq> I; aGroup R; I \<subseteq> carrier R; A \<subseteq> carrier R; B \<subseteq> carrier R; h \<in> A; k \<in> B; x = h \<plusminus> k\<rbrakk> \<Longrightarrow> h \<plusminus> k \<in> I
[PROOF STEP]
apply (frule_tac c = h in subsetD[of "A" "I"], assumption+,
        frule_tac c = k in subsetD[of "B" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x h k. \<lbrakk>ideal R I; A \<subseteq> I; B \<subseteq> I; aGroup R; I \<subseteq> carrier R; A \<subseteq> carrier R; B \<subseteq> carrier R; h \<in> A; k \<in> B; x = h \<plusminus> k; h \<in> I; k \<in> I\<rbrakk> \<Longrightarrow> h \<plusminus> k \<in> I
[PROOF STEP]
apply (simp add:ideal_pOp_closed)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideals_set_sum:"\<lbrakk>ideal R A; ideal R B; x \<in> A \<minusplus> B\<rbrakk> \<Longrightarrow>
             \<exists>h\<in>A. \<exists>k\<in>B. x = h \<plusminus> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R A; ideal R B; x \<in> A \<minusplus> B\<rbrakk> \<Longrightarrow> \<exists>h\<in>A. \<exists>k\<in>B. x = h \<plusminus> k
[PROOF STEP]
apply (frule ideal_subset1[of A],
       frule ideal_subset1[of B])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R A; ideal R B; x \<in> A \<minusplus> B; A \<subseteq> carrier R; B \<subseteq> carrier R\<rbrakk> \<Longrightarrow> \<exists>h\<in>A. \<exists>k\<in>B. x = h \<plusminus> k
[PROOF STEP]
apply (cut_tac ring_is_ag,
       simp add:aGroup.set_sum)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) a_in_principal:"a \<in> carrier R \<Longrightarrow> a \<in> Rxa R a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> carrier R \<Longrightarrow> a \<in> R \<diamondsuit>\<^sub>p a
[PROOF STEP]
apply (cut_tac ring_one,
       frule ring_l_one[THEN sym, of "a"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; 1\<^sub>r \<in> carrier R; a = 1\<^sub>r \<cdot>\<^sub>r a\<rbrakk> \<Longrightarrow> a \<in> R \<diamondsuit>\<^sub>p a
[PROOF STEP]
apply (simp add:Rxa_def, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) principal_ideal:"a \<in> carrier R \<Longrightarrow> ideal R (Rxa R a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> carrier R \<Longrightarrow> ideal R (R \<diamondsuit>\<^sub>p a)
[PROOF STEP]
apply (rule ideal_condition1)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. a \<in> carrier R \<Longrightarrow> R \<diamondsuit>\<^sub>p a \<subseteq> carrier R
 2. a \<in> carrier R \<Longrightarrow> R \<diamondsuit>\<^sub>p a \<noteq> {}
 3. a \<in> carrier R \<Longrightarrow> \<forall>x\<in>R \<diamondsuit>\<^sub>p a. \<forall>y\<in>R \<diamondsuit>\<^sub>p a. x \<plusminus> y \<in> R \<diamondsuit>\<^sub>p a
 4. a \<in> carrier R \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>R \<diamondsuit>\<^sub>p a. r \<cdot>\<^sub>r x \<in> R \<diamondsuit>\<^sub>p a
[PROOF STEP]
apply (rule subsetI,
         simp add:Rxa_def, erule bexE, simp add:ring_tOp_closed)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. a \<in> carrier R \<Longrightarrow> R \<diamondsuit>\<^sub>p a \<noteq> {}
 2. a \<in> carrier R \<Longrightarrow> \<forall>x\<in>R \<diamondsuit>\<^sub>p a. \<forall>y\<in>R \<diamondsuit>\<^sub>p a. x \<plusminus> y \<in> R \<diamondsuit>\<^sub>p a
 3. a \<in> carrier R \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>R \<diamondsuit>\<^sub>p a. r \<cdot>\<^sub>r x \<in> R \<diamondsuit>\<^sub>p a
[PROOF STEP]
apply (frule a_in_principal[of "a"], blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<in> carrier R \<Longrightarrow> \<forall>x\<in>R \<diamondsuit>\<^sub>p a. \<forall>y\<in>R \<diamondsuit>\<^sub>p a. x \<plusminus> y \<in> R \<diamondsuit>\<^sub>p a
 2. a \<in> carrier R \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>R \<diamondsuit>\<^sub>p a. r \<cdot>\<^sub>r x \<in> R \<diamondsuit>\<^sub>p a
[PROOF STEP]
apply ((rule ballI)+,
        simp add:Rxa_def, (erule bexE)+, simp,
        subst ring_distrib2[THEN sym], assumption+,
        cut_tac ring_is_ag,
        frule_tac x = r and y = ra in aGroup.ag_pOp_closed, assumption+,
        blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> carrier R \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>R \<diamondsuit>\<^sub>p a. r \<cdot>\<^sub>r x \<in> R \<diamondsuit>\<^sub>p a
[PROOF STEP]
apply ((rule ballI)+,
        simp add:Rxa_def, (erule bexE)+, simp,
        simp add:ring_tOp_assoc[THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x ra. \<lbrakk>a \<in> carrier R; r \<in> carrier R; ra \<in> carrier R; x = ra \<cdot>\<^sub>r a\<rbrakk> \<Longrightarrow> \<exists>rb\<in>carrier R. r \<cdot>\<^sub>r ra \<cdot>\<^sub>r a = rb \<cdot>\<^sub>r a
[PROOF STEP]
apply (frule_tac x = r and y = ra in ring_tOp_closed, assumption, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) rxa_in_Rxa:"\<lbrakk>a \<in> carrier R; r \<in> carrier R\<rbrakk> \<Longrightarrow>
                                     r \<cdot>\<^sub>r a \<in> Rxa R a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; r \<in> carrier R\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r a \<in> R \<diamondsuit>\<^sub>p a
[PROOF STEP]
by (simp add:Rxa_def, blast)


[STATEMENT]
lemma (in Ring) Rxa_one:"Rxa R 1\<^sub>r = carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<diamondsuit>\<^sub>p 1\<^sub>r = carrier R
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. R \<diamondsuit>\<^sub>p 1\<^sub>r \<subseteq> carrier R
 2. carrier R \<subseteq> R \<diamondsuit>\<^sub>p 1\<^sub>r
[PROOF STEP]
apply (rule subsetI, simp add:Rxa_def, erule bexE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x r. \<lbrakk>r \<in> carrier R; x = r \<cdot>\<^sub>r 1\<^sub>r\<rbrakk> \<Longrightarrow> x \<in> carrier R
 2. carrier R \<subseteq> R \<diamondsuit>\<^sub>p 1\<^sub>r
[PROOF STEP]
apply (simp add:ring_r_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. carrier R \<subseteq> R \<diamondsuit>\<^sub>p 1\<^sub>r
[PROOF STEP]
apply (rule subsetI, simp add:Rxa_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> carrier R \<Longrightarrow> \<exists>r\<in>carrier R. x = r \<cdot>\<^sub>r 1\<^sub>r
[PROOF STEP]
apply (frule_tac t = x in ring_r_one[THEN sym], blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) Rxa_zero:"Rxa R \<zero> = {\<zero>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<diamondsuit>\<^sub>p \<zero> = {\<zero>}
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. R \<diamondsuit>\<^sub>p \<zero> \<subseteq> {\<zero>}
 2. {\<zero>} \<subseteq> R \<diamondsuit>\<^sub>p \<zero>
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> R \<diamondsuit>\<^sub>p \<zero> \<Longrightarrow> x \<in> {\<zero>}
 2. {\<zero>} \<subseteq> R \<diamondsuit>\<^sub>p \<zero>
[PROOF STEP]
apply (simp add:Rxa_def, erule bexE, simp add:ring_times_x_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {\<zero>} \<subseteq> R \<diamondsuit>\<^sub>p \<zero>
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {\<zero>} \<Longrightarrow> x \<in> R \<diamondsuit>\<^sub>p \<zero>
[PROOF STEP]
apply (simp add:Rxa_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r\<in>carrier R. \<zero> = r \<cdot>\<^sub>r \<zero>
[PROOF STEP]
apply (cut_tac ring_zero,
        frule ring_times_x_0[THEN sym, of "\<zero>"], blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) Rxa_nonzero:"\<lbrakk>a \<in> carrier R; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> Rxa R a \<noteq> {\<zero>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; a \<noteq> \<zero>\<rbrakk> \<Longrightarrow> R \<diamondsuit>\<^sub>p a \<noteq> {\<zero>}
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; a \<noteq> \<zero>; R \<diamondsuit>\<^sub>p a = {\<zero>}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule a_in_principal[of "a"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; a \<noteq> \<zero>; R \<diamondsuit>\<^sub>p a = {\<zero>}; a \<in> R \<diamondsuit>\<^sub>p a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_cont_Rxa:"\<lbrakk>ideal R I; a \<in> I\<rbrakk> \<Longrightarrow> Rxa R a \<subseteq> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> I\<rbrakk> \<Longrightarrow> R \<diamondsuit>\<^sub>p a \<subseteq> I
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal R I; a \<in> I; x \<in> R \<diamondsuit>\<^sub>p a\<rbrakk> \<Longrightarrow> x \<in> I
[PROOF STEP]
apply (simp add:Rxa_def, erule bexE, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x r. \<lbrakk>ideal R I; a \<in> I; r \<in> carrier R; x = r \<cdot>\<^sub>r a\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r a \<in> I
[PROOF STEP]
apply (simp add:ideal_ring_multiple)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) Rxa_mult_smaller:"\<lbrakk> a \<in> carrier R; b \<in> carrier R\<rbrakk> \<Longrightarrow>
                    Rxa R (a \<cdot>\<^sub>r b) \<subseteq> Rxa R b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R\<rbrakk> \<Longrightarrow> R \<diamondsuit>\<^sub>p (a \<cdot>\<^sub>r b) \<subseteq> R \<diamondsuit>\<^sub>p b
[PROOF STEP]
apply (frule rxa_in_Rxa[of b a], assumption,
       frule principal_ideal[of b])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<cdot>\<^sub>r b \<in> R \<diamondsuit>\<^sub>p b; ideal R (R \<diamondsuit>\<^sub>p b)\<rbrakk> \<Longrightarrow> R \<diamondsuit>\<^sub>p (a \<cdot>\<^sub>r b) \<subseteq> R \<diamondsuit>\<^sub>p b
[PROOF STEP]
apply (rule ideal_cont_Rxa[of "R \<diamondsuit>\<^sub>p b" "a \<cdot>\<^sub>r b"], assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) id_ideal_psub_sum:"\<lbrakk>ideal R I; a \<in> carrier R; a \<notin> I\<rbrakk> \<Longrightarrow>
                                             I \<subset> I \<minusplus> Rxa R a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; a \<notin> I\<rbrakk> \<Longrightarrow> I \<subset> I \<minusplus> R \<diamondsuit>\<^sub>p a
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; a \<notin> I; aGroup R\<rbrakk> \<Longrightarrow> I \<subset> I \<minusplus> R \<diamondsuit>\<^sub>p a
[PROOF STEP]
apply (simp add:psubset_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; a \<notin> I; aGroup R\<rbrakk> \<Longrightarrow> I \<subseteq> I \<minusplus> R \<diamondsuit>\<^sub>p a \<and> I \<noteq> I \<minusplus> R \<diamondsuit>\<^sub>p a
[PROOF STEP]
apply (frule principal_ideal)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; a \<notin> I; aGroup R; ideal R (R \<diamondsuit>\<^sub>p a)\<rbrakk> \<Longrightarrow> I \<subseteq> I \<minusplus> R \<diamondsuit>\<^sub>p a \<and> I \<noteq> I \<minusplus> R \<diamondsuit>\<^sub>p a
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; a \<in> carrier R; a \<notin> I; aGroup R; ideal R (R \<diamondsuit>\<^sub>p a)\<rbrakk> \<Longrightarrow> I \<subseteq> I \<minusplus> R \<diamondsuit>\<^sub>p a
 2. \<lbrakk>ideal R I; a \<in> carrier R; a \<notin> I; aGroup R; ideal R (R \<diamondsuit>\<^sub>p a)\<rbrakk> \<Longrightarrow> I \<noteq> I \<minusplus> R \<diamondsuit>\<^sub>p a
[PROOF STEP]
apply (rule sum_ideals_la1, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; a \<notin> I; aGroup R; ideal R (R \<diamondsuit>\<^sub>p a)\<rbrakk> \<Longrightarrow> I \<noteq> I \<minusplus> R \<diamondsuit>\<^sub>p a
[PROOF STEP]
apply (rule contrapos_pp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; a \<in> carrier R; a \<notin> I; aGroup R; ideal R (R \<diamondsuit>\<^sub>p a)\<rbrakk> \<Longrightarrow> ?Q9
 2. \<lbrakk>ideal R I; a \<in> carrier R; a \<notin> I; aGroup R; ideal R (R \<diamondsuit>\<^sub>p a); \<not> I \<noteq> I \<minusplus> R \<diamondsuit>\<^sub>p a\<rbrakk> \<Longrightarrow> \<not> ?Q9
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; a \<notin> I; aGroup R; ideal R (R \<diamondsuit>\<^sub>p a); I = I \<minusplus> R \<diamondsuit>\<^sub>p a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule sum_ideals_la2[of "I" "Rxa R a"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; a \<notin> I; aGroup R; ideal R (R \<diamondsuit>\<^sub>p a); I = I \<minusplus> R \<diamondsuit>\<^sub>p a; R \<diamondsuit>\<^sub>p a \<subseteq> I \<minusplus> R \<diamondsuit>\<^sub>p a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule a_in_principal[of "a"],
       frule subsetD[of "Rxa R a" "I \<minusplus> Rxa R a" "a"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; a \<notin> I; aGroup R; ideal R (R \<diamondsuit>\<^sub>p a); I = I \<minusplus> R \<diamondsuit>\<^sub>p a; R \<diamondsuit>\<^sub>p a \<subseteq> I \<minusplus> R \<diamondsuit>\<^sub>p a; a \<in> R \<diamondsuit>\<^sub>p a; a \<in> I \<minusplus> R \<diamondsuit>\<^sub>p a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) mul_two_principal_idealsTr:"\<lbrakk>a \<in> carrier R; b \<in> carrier R;
         x \<in> Rxa R a; y \<in> Rxa R b\<rbrakk> \<Longrightarrow> \<exists>r\<in>carrier R. x \<cdot>\<^sub>r y = r \<cdot>\<^sub>r (a \<cdot>\<^sub>r b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; b \<in> carrier R; x \<in> R \<diamondsuit>\<^sub>p a; y \<in> R \<diamondsuit>\<^sub>p b\<rbrakk> \<Longrightarrow> \<exists>r\<in>carrier R. x \<cdot>\<^sub>r y = r \<cdot>\<^sub>r (a \<cdot>\<^sub>r b)
[PROOF STEP]
apply (simp add:Rxa_def, (erule bexE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r ra. \<lbrakk>a \<in> carrier R; b \<in> carrier R; r \<in> carrier R; x = r \<cdot>\<^sub>r a; ra \<in> carrier R; y = ra \<cdot>\<^sub>r b\<rbrakk> \<Longrightarrow> \<exists>r\<in>carrier R. x \<cdot>\<^sub>r y = r \<cdot>\<^sub>r (a \<cdot>\<^sub>r b)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r ra. \<lbrakk>a \<in> carrier R; b \<in> carrier R; r \<in> carrier R; x = r \<cdot>\<^sub>r a; ra \<in> carrier R; y = ra \<cdot>\<^sub>r b\<rbrakk> \<Longrightarrow> \<exists>rb\<in>carrier R. r \<cdot>\<^sub>r a \<cdot>\<^sub>r (ra \<cdot>\<^sub>r b) = rb \<cdot>\<^sub>r (a \<cdot>\<^sub>r b)
[PROOF STEP]
apply (frule_tac x = ra and y = b in ring_tOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r ra. \<lbrakk>a \<in> carrier R; b \<in> carrier R; r \<in> carrier R; x = r \<cdot>\<^sub>r a; ra \<in> carrier R; y = ra \<cdot>\<^sub>r b; ra \<cdot>\<^sub>r b \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>rb\<in>carrier R. r \<cdot>\<^sub>r a \<cdot>\<^sub>r (ra \<cdot>\<^sub>r b) = rb \<cdot>\<^sub>r (a \<cdot>\<^sub>r b)
[PROOF STEP]
apply (simp add:ring_tOp_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r ra. \<lbrakk>a \<in> carrier R; b \<in> carrier R; r \<in> carrier R; x = r \<cdot>\<^sub>r a; ra \<in> carrier R; y = ra \<cdot>\<^sub>r b; ra \<cdot>\<^sub>r b \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>rb\<in>carrier R. r \<cdot>\<^sub>r (a \<cdot>\<^sub>r (ra \<cdot>\<^sub>r b)) = rb \<cdot>\<^sub>r (a \<cdot>\<^sub>r b)
[PROOF STEP]
apply (simp add:ring_tOp_assoc[THEN sym, of a _ b])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r ra. \<lbrakk>a \<in> carrier R; b \<in> carrier R; r \<in> carrier R; x = r \<cdot>\<^sub>r a; ra \<in> carrier R; y = ra \<cdot>\<^sub>r b; ra \<cdot>\<^sub>r b \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>rb\<in>carrier R. r \<cdot>\<^sub>r (a \<cdot>\<^sub>r ra \<cdot>\<^sub>r b) = rb \<cdot>\<^sub>r (a \<cdot>\<^sub>r b)
[PROOF STEP]
apply (simp add:ring_tOp_commute[of a], simp add:ring_tOp_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r ra. \<lbrakk>a \<in> carrier R; b \<in> carrier R; r \<in> carrier R; x = r \<cdot>\<^sub>r a; ra \<in> carrier R; y = ra \<cdot>\<^sub>r b; ra \<cdot>\<^sub>r b \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>rb\<in>carrier R. r \<cdot>\<^sub>r (ra \<cdot>\<^sub>r (a \<cdot>\<^sub>r b)) = rb \<cdot>\<^sub>r (b \<cdot>\<^sub>r a)
[PROOF STEP]
apply (frule_tac x = a and y = b in ring_tOp_closed, assumption+,
       thin_tac "ra \<cdot>\<^sub>r b \<in> carrier R",
       simp add:ring_tOp_assoc[THEN sym, of _ _ "a \<cdot>\<^sub>r b"],
       frule_tac x = r and y = ra in ring_tOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r ra. \<lbrakk>a \<in> carrier R; b \<in> carrier R; r \<in> carrier R; x = r \<cdot>\<^sub>r a; ra \<in> carrier R; y = ra \<cdot>\<^sub>r b; a \<cdot>\<^sub>r b \<in> carrier R; r \<cdot>\<^sub>r ra \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>rb\<in>carrier R. r \<cdot>\<^sub>r ra \<cdot>\<^sub>r (a \<cdot>\<^sub>r b) = rb \<cdot>\<^sub>r (b \<cdot>\<^sub>r a)
[PROOF STEP]
apply (simp add:ring_tOp_commute[of b a])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r ra. \<lbrakk>a \<in> carrier R; b \<in> carrier R; r \<in> carrier R; x = r \<cdot>\<^sub>r a; ra \<in> carrier R; y = ra \<cdot>\<^sub>r b; a \<cdot>\<^sub>r b \<in> carrier R; r \<cdot>\<^sub>r ra \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>rb\<in>carrier R. r \<cdot>\<^sub>r ra \<cdot>\<^sub>r (a \<cdot>\<^sub>r b) = rb \<cdot>\<^sub>r (a \<cdot>\<^sub>r b)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) sum_of_prideals0:
      "\<forall>f. (\<forall>l \<le> n. f l \<in> carrier R) \<longrightarrow> ideal R (sum_pr_ideals R f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<longrightarrow> ideal R (sum_pr_ideals R f n)
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>f. (\<forall>l\<le>0. f l \<in> carrier R) \<longrightarrow> ideal R (sum_pr_ideals R f 0)
 2. \<And>n. \<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<longrightarrow> ideal R (sum_pr_ideals R f n) \<Longrightarrow> \<forall>f. (\<forall>l\<le>Suc n. f l \<in> carrier R) \<longrightarrow> ideal R (sum_pr_ideals R f (Suc n))
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. (\<forall>l\<le>0. f l \<in> carrier R) \<longrightarrow> ideal R (sum_pr_ideals R f 0)
 2. \<And>n. \<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<longrightarrow> ideal R (sum_pr_ideals R f n) \<Longrightarrow> \<forall>f. (\<forall>l\<le>Suc n. f l \<in> carrier R) \<longrightarrow> ideal R (sum_pr_ideals R f (Suc n))
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. \<forall>l\<le>0. f l \<in> carrier R \<Longrightarrow> ideal R (sum_pr_ideals R f 0)
 2. \<And>n. \<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<longrightarrow> ideal R (sum_pr_ideals R f n) \<Longrightarrow> \<forall>f. (\<forall>l\<le>Suc n. f l \<in> carrier R) \<longrightarrow> ideal R (sum_pr_ideals R f (Suc n))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. f 0 \<in> carrier R \<Longrightarrow> ideal R (R \<diamondsuit>\<^sub>p f 0)
 2. \<And>n. \<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<longrightarrow> ideal R (sum_pr_ideals R f n) \<Longrightarrow> \<forall>f. (\<forall>l\<le>Suc n. f l \<in> carrier R) \<longrightarrow> ideal R (sum_pr_ideals R f (Suc n))
[PROOF STEP]
apply (rule Ring.principal_ideal, rule Ring_axioms, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<longrightarrow> ideal R (sum_pr_ideals R f n) \<Longrightarrow> \<forall>f. (\<forall>l\<le>Suc n. f l \<in> carrier R) \<longrightarrow> ideal R (sum_pr_ideals R f (Suc n))
[PROOF STEP]
(** case n **)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<longrightarrow> ideal R (sum_pr_ideals R f n) \<Longrightarrow> \<forall>f. (\<forall>l\<le>Suc n. f l \<in> carrier R) \<longrightarrow> ideal R (sum_pr_ideals R f (Suc n))
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<longrightarrow> ideal R (sum_pr_ideals R f n); \<forall>l\<le>Suc n. f l \<in> carrier R\<rbrakk> \<Longrightarrow> ideal R (sum_pr_ideals R f (Suc n))
[PROOF STEP]
apply (frule_tac x = f in spec,
        thin_tac "\<forall>f. (\<forall>l \<le> n. f l \<in> carrier R) \<longrightarrow>
               ideal R (sum_pr_ideals R f n)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<forall>l\<le>Suc n. f l \<in> carrier R; (\<forall>l\<le>n. f l \<in> carrier R) \<longrightarrow> ideal R (sum_pr_ideals R f n)\<rbrakk> \<Longrightarrow> ideal R (sum_pr_ideals R f (Suc n))
[PROOF STEP]
apply (cut_tac n = n in Nsetn_sub_mem1, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<forall>l\<le>Suc n. f l \<in> carrier R; ideal R (sum_pr_ideals R f n)\<rbrakk> \<Longrightarrow> ideal R (R \<diamondsuit>\<^sub>p f (Suc n) \<minusplus> sum_pr_ideals R f n)
[PROOF STEP]
apply (cut_tac a = "f (Suc n)" in  principal_ideal,
       simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<forall>l\<le>Suc n. f l \<in> carrier R; ideal R (sum_pr_ideals R f n); ideal R (R \<diamondsuit>\<^sub>p f (Suc n))\<rbrakk> \<Longrightarrow> ideal R (R \<diamondsuit>\<^sub>p f (Suc n) \<minusplus> sum_pr_ideals R f n)
[PROOF STEP]
apply (rule_tac ?I1.0 = "Rxa R (f (Suc n))" and
        ?I2.0 = "sum_pr_ideals R f n" in Ring.sum_ideals, rule Ring_axioms, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) sum_of_prideals:"\<lbrakk>\<forall>l \<le> n. f l \<in> carrier R\<rbrakk> \<Longrightarrow>
                      ideal R (sum_pr_ideals R f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l\<le>n. f l \<in> carrier R \<Longrightarrow> ideal R (sum_pr_ideals R f n)
[PROOF STEP]
apply (simp add:sum_of_prideals0)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) sum_of_prideals1:"\<forall>f. (\<forall>l \<le> n. f l \<in> carrier R) \<longrightarrow>
                                    f ` {i. i \<le> n} \<subseteq> (sum_pr_ideals R f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<longrightarrow> f ` {i. i \<le> n} \<subseteq> sum_pr_ideals R f n
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>f. (\<forall>l\<le>0. f l \<in> carrier R) \<longrightarrow> f ` {i. i \<le> 0} \<subseteq> sum_pr_ideals R f 0
 2. \<And>n. \<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<longrightarrow> f ` {i. i \<le> n} \<subseteq> sum_pr_ideals R f n \<Longrightarrow> \<forall>f. (\<forall>l\<le>Suc n. f l \<in> carrier R) \<longrightarrow> f ` {i. i \<le> Suc n} \<subseteq> sum_pr_ideals R f (Suc n)
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. \<forall>l\<le>0. f l \<in> carrier R \<Longrightarrow> f ` {i. i \<le> 0} \<subseteq> sum_pr_ideals R f 0
 2. \<And>n. \<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<longrightarrow> f ` {i. i \<le> n} \<subseteq> sum_pr_ideals R f n \<Longrightarrow> \<forall>f. (\<forall>l\<le>Suc n. f l \<in> carrier R) \<longrightarrow> f ` {i. i \<le> Suc n} \<subseteq> sum_pr_ideals R f (Suc n)
[PROOF STEP]
apply (simp, simp add:a_in_principal)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<longrightarrow> f ` {i. i \<le> n} \<subseteq> sum_pr_ideals R f n \<Longrightarrow> \<forall>f. (\<forall>l\<le>Suc n. f l \<in> carrier R) \<longrightarrow> f ` {i. i \<le> Suc n} \<subseteq> sum_pr_ideals R f (Suc n)
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<longrightarrow> f ` {i. i \<le> n} \<subseteq> sum_pr_ideals R f n; \<forall>l\<le>Suc n. f l \<in> carrier R\<rbrakk> \<Longrightarrow> f ` {i. i \<le> Suc n} \<subseteq> sum_pr_ideals R f (Suc n)
[PROOF STEP]
apply (frule_tac a = f in forall_spec,
        thin_tac "\<forall>f. (\<forall>l \<le> n. f l \<in> carrier R) \<longrightarrow>
               f ` {i. i \<le> n} \<subseteq> sum_pr_ideals R f n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n f. \<forall>l\<le>Suc n. f l \<in> carrier R \<Longrightarrow> \<forall>l\<le>n. f l \<in> carrier R
 2. \<And>n f. \<lbrakk>\<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<longrightarrow> f ` {i. i \<le> n} \<subseteq> sum_pr_ideals R f n; \<forall>l\<le>Suc n. f l \<in> carrier R; f ` {i. i \<le> n} \<subseteq> sum_pr_ideals R f n\<rbrakk> \<Longrightarrow> f ` {i. i \<le> Suc n} \<subseteq> sum_pr_ideals R f (Suc n)
[PROOF STEP]
apply (rule allI, cut_tac n = n in Nset_un, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<longrightarrow> f ` {i. i \<le> n} \<subseteq> sum_pr_ideals R f n; \<forall>l\<le>Suc n. f l \<in> carrier R; f ` {i. i \<le> n} \<subseteq> sum_pr_ideals R f n\<rbrakk> \<Longrightarrow> f ` {i. i \<le> Suc n} \<subseteq> sum_pr_ideals R f (Suc n)
[PROOF STEP]
apply (subst Nset_un)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<longrightarrow> f ` {i. i \<le> n} \<subseteq> sum_pr_ideals R f n; \<forall>l\<le>Suc n. f l \<in> carrier R; f ` {i. i \<le> n} \<subseteq> sum_pr_ideals R f n\<rbrakk> \<Longrightarrow> f ` ({j. j \<le> n} \<union> {Suc n}) \<subseteq> sum_pr_ideals R f (Suc n)
[PROOF STEP]
apply (cut_tac A = "{i. i \<le> (Suc n)}" and f = f and B = "carrier R" and
        ?A1.0 = "{i. i \<le> n}" and ?A2.0 = "{Suc n}" in im_set_un1,
        simp, rule Nset_un)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<longrightarrow> f ` {i. i \<le> n} \<subseteq> sum_pr_ideals R f n; \<forall>l\<le>Suc n. f l \<in> carrier R; f ` {i. i \<le> n} \<subseteq> sum_pr_ideals R f n; f ` ({i. i \<le> n} \<union> {Suc n}) = f ` {i. i \<le> n} \<union> f ` {Suc n}\<rbrakk> \<Longrightarrow> f ` ({j. j \<le> n} \<union> {Suc n}) \<subseteq> sum_pr_ideals R f (Suc n)
[PROOF STEP]
apply (thin_tac "\<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<longrightarrow>
               f ` {i. i \<le> n} \<subseteq> sum_pr_ideals R f n",
        simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<forall>l\<le>Suc n. f l \<in> carrier R; f ` {i. i \<le> n} \<subseteq> sum_pr_ideals R f n\<rbrakk> \<Longrightarrow> f (Suc n) \<in> R \<diamondsuit>\<^sub>p f (Suc n) \<minusplus> sum_pr_ideals R f n \<and> f ` {j. j \<le> n} \<subseteq> R \<diamondsuit>\<^sub>p f (Suc n) \<minusplus> sum_pr_ideals R f n
[PROOF STEP]
apply (cut_tac n = n and f = f in sum_of_prideals,
        cut_tac n = n in Nsetn_sub_mem1, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<forall>l\<le>Suc n. f l \<in> carrier R; f ` {i. i \<le> n} \<subseteq> sum_pr_ideals R f n; ideal R (sum_pr_ideals R f n)\<rbrakk> \<Longrightarrow> f (Suc n) \<in> R \<diamondsuit>\<^sub>p f (Suc n) \<minusplus> sum_pr_ideals R f n \<and> f ` {j. j \<le> n} \<subseteq> R \<diamondsuit>\<^sub>p f (Suc n) \<minusplus> sum_pr_ideals R f n
[PROOF STEP]
apply (cut_tac a = "f (Suc n)" in principal_ideal, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<forall>l\<le>Suc n. f l \<in> carrier R; f ` {i. i \<le> n} \<subseteq> sum_pr_ideals R f n; ideal R (sum_pr_ideals R f n); ideal R (R \<diamondsuit>\<^sub>p f (Suc n))\<rbrakk> \<Longrightarrow> f (Suc n) \<in> R \<diamondsuit>\<^sub>p f (Suc n) \<minusplus> sum_pr_ideals R f n \<and> f ` {j. j \<le> n} \<subseteq> R \<diamondsuit>\<^sub>p f (Suc n) \<minusplus> sum_pr_ideals R f n
[PROOF STEP]
apply (frule_tac ?I1.0 = "Rxa R (f (Suc n))" and ?I2.0 = "sum_pr_ideals R f n"
                 in sum_ideals_la1, assumption+,
        cut_tac a = "f (Suc n)" in a_in_principal, simp,
        frule_tac A = "R \<diamondsuit>\<^sub>p f (Suc n)" and
         B = "R \<diamondsuit>\<^sub>p f (Suc n) \<minusplus> sum_pr_ideals R f n" and c = "f (Suc n)" in
         subsetD, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<forall>l\<le>Suc n. f l \<in> carrier R; f ` {i. i \<le> n} \<subseteq> sum_pr_ideals R f n; ideal R (sum_pr_ideals R f n); ideal R (R \<diamondsuit>\<^sub>p f (Suc n)); R \<diamondsuit>\<^sub>p f (Suc n) \<subseteq> R \<diamondsuit>\<^sub>p f (Suc n) \<minusplus> sum_pr_ideals R f n; f (Suc n) \<in> R \<diamondsuit>\<^sub>p f (Suc n); f (Suc n) \<in> R \<diamondsuit>\<^sub>p f (Suc n) \<minusplus> sum_pr_ideals R f n\<rbrakk> \<Longrightarrow> f ` {j. j \<le> n} \<subseteq> R \<diamondsuit>\<^sub>p f (Suc n) \<minusplus> sum_pr_ideals R f n
[PROOF STEP]
apply (frule_tac ?I1.0 = "Rxa R (f (Suc n))" and
         ?I2.0 = "sum_pr_ideals R f n" in sum_ideals_la2, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<forall>l\<le>Suc n. f l \<in> carrier R; f ` {i. i \<le> n} \<subseteq> sum_pr_ideals R f n; ideal R (sum_pr_ideals R f n); ideal R (R \<diamondsuit>\<^sub>p f (Suc n)); R \<diamondsuit>\<^sub>p f (Suc n) \<subseteq> R \<diamondsuit>\<^sub>p f (Suc n) \<minusplus> sum_pr_ideals R f n; f (Suc n) \<in> R \<diamondsuit>\<^sub>p f (Suc n); f (Suc n) \<in> R \<diamondsuit>\<^sub>p f (Suc n) \<minusplus> sum_pr_ideals R f n; sum_pr_ideals R f n \<subseteq> R \<diamondsuit>\<^sub>p f (Suc n) \<minusplus> sum_pr_ideals R f n\<rbrakk> \<Longrightarrow> f ` {j. j \<le> n} \<subseteq> R \<diamondsuit>\<^sub>p f (Suc n) \<minusplus> sum_pr_ideals R f n
[PROOF STEP]
apply (rule_tac A = "f ` {j. j \<le> n}" and B = "sum_pr_ideals R f n" and
         C = "Rxa R (f (Suc n)) \<minusplus> sum_pr_ideals R f n" in subset_trans,
         assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) sum_of_prideals2:"\<forall>l \<le> n. f l \<in> carrier R
               \<Longrightarrow>  f ` {i. i \<le> n} \<subseteq> (sum_pr_ideals R f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l\<le>n. f l \<in> carrier R \<Longrightarrow> f ` {i. i \<le> n} \<subseteq> sum_pr_ideals R f n
[PROOF STEP]
apply (simp add:sum_of_prideals1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) sum_of_prideals3:"ideal R I \<Longrightarrow>
      \<forall>f. (\<forall>l \<le> n. f l \<in> carrier R) \<and> (f ` {i. i \<le> n} \<subseteq> I) \<longrightarrow>
          (sum_pr_ideals R f n \<subseteq> I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> \<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<and> f ` {i. i \<le> n} \<subseteq> I \<longrightarrow> sum_pr_ideals R f n \<subseteq> I
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ideal R I \<Longrightarrow> \<forall>f. (\<forall>l\<le>0. f l \<in> carrier R) \<and> f ` {i. i \<le> 0} \<subseteq> I \<longrightarrow> sum_pr_ideals R f 0 \<subseteq> I
 2. \<And>n. \<lbrakk>ideal R I; \<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<and> f ` {i. i \<le> n} \<subseteq> I \<longrightarrow> sum_pr_ideals R f n \<subseteq> I\<rbrakk> \<Longrightarrow> \<forall>f. (\<forall>l\<le>Suc n. f l \<in> carrier R) \<and> f ` {i. i \<le> Suc n} \<subseteq> I \<longrightarrow> sum_pr_ideals R f (Suc n) \<subseteq> I
[PROOF STEP]
apply (rule allI, rule impI, erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>ideal R I; \<forall>l\<le>0. f l \<in> carrier R; f ` {i. i \<le> 0} \<subseteq> I\<rbrakk> \<Longrightarrow> sum_pr_ideals R f 0 \<subseteq> I
 2. \<And>n. \<lbrakk>ideal R I; \<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<and> f ` {i. i \<le> n} \<subseteq> I \<longrightarrow> sum_pr_ideals R f n \<subseteq> I\<rbrakk> \<Longrightarrow> \<forall>f. (\<forall>l\<le>Suc n. f l \<in> carrier R) \<and> f ` {i. i \<le> Suc n} \<subseteq> I \<longrightarrow> sum_pr_ideals R f (Suc n) \<subseteq> I
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>ideal R I; f 0 \<in> carrier R; f 0 \<in> I\<rbrakk> \<Longrightarrow> R \<diamondsuit>\<^sub>p f 0 \<subseteq> I
 2. \<And>n. \<lbrakk>ideal R I; \<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<and> f ` {i. i \<le> n} \<subseteq> I \<longrightarrow> sum_pr_ideals R f n \<subseteq> I\<rbrakk> \<Longrightarrow> \<forall>f. (\<forall>l\<le>Suc n. f l \<in> carrier R) \<and> f ` {i. i \<le> Suc n} \<subseteq> I \<longrightarrow> sum_pr_ideals R f (Suc n) \<subseteq> I
[PROOF STEP]
apply (rule ideal_cont_Rxa[of I], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>ideal R I; \<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<and> f ` {i. i \<le> n} \<subseteq> I \<longrightarrow> sum_pr_ideals R f n \<subseteq> I\<rbrakk> \<Longrightarrow> \<forall>f. (\<forall>l\<le>Suc n. f l \<in> carrier R) \<and> f ` {i. i \<le> Suc n} \<subseteq> I \<longrightarrow> sum_pr_ideals R f (Suc n) \<subseteq> I
[PROOF STEP]
apply (rule allI, rule impI, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>ideal R I; \<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<and> f ` {i. i \<le> n} \<subseteq> I \<longrightarrow> sum_pr_ideals R f n \<subseteq> I; \<forall>l\<le>Suc n. f l \<in> carrier R; f ` {i. i \<le> Suc n} \<subseteq> I\<rbrakk> \<Longrightarrow> sum_pr_ideals R f (Suc n) \<subseteq> I
[PROOF STEP]
apply (frule_tac a = f in forall_spec,
        thin_tac "\<forall>f. (\<forall>l \<le> n. f l \<in> carrier R) \<and> f `{i. i \<le> n} \<subseteq> I \<longrightarrow>
               sum_pr_ideals R f n \<subseteq> I")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n f. \<lbrakk>ideal R I; \<forall>l\<le>Suc n. f l \<in> carrier R; f ` {i. i \<le> Suc n} \<subseteq> I\<rbrakk> \<Longrightarrow> (\<forall>l\<le>n. f l \<in> carrier R) \<and> f ` {i. i \<le> n} \<subseteq> I
 2. \<And>n f. \<lbrakk>ideal R I; \<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<and> f ` {i. i \<le> n} \<subseteq> I \<longrightarrow> sum_pr_ideals R f n \<subseteq> I; \<forall>l\<le>Suc n. f l \<in> carrier R; f ` {i. i \<le> Suc n} \<subseteq> I; sum_pr_ideals R f n \<subseteq> I\<rbrakk> \<Longrightarrow> sum_pr_ideals R f (Suc n) \<subseteq> I
[PROOF STEP]
apply (simp add:Nset_un)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>ideal R I; \<forall>f. (\<forall>l\<le>n. f l \<in> carrier R) \<and> f ` {i. i \<le> n} \<subseteq> I \<longrightarrow> sum_pr_ideals R f n \<subseteq> I; \<forall>l\<le>Suc n. f l \<in> carrier R; f ` {i. i \<le> Suc n} \<subseteq> I; sum_pr_ideals R f n \<subseteq> I\<rbrakk> \<Longrightarrow> sum_pr_ideals R f (Suc n) \<subseteq> I
[PROOF STEP]
apply (thin_tac "\<forall>f. (\<forall>l \<le> n. f l \<in> carrier R) \<and> f ` {i. i \<le> n} \<subseteq> I \<longrightarrow>
               sum_pr_ideals R f n \<subseteq> I")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>ideal R I; \<forall>l\<le>Suc n. f l \<in> carrier R; f ` {i. i \<le> Suc n} \<subseteq> I; sum_pr_ideals R f n \<subseteq> I\<rbrakk> \<Longrightarrow> sum_pr_ideals R f (Suc n) \<subseteq> I
[PROOF STEP]
apply (frule_tac x = "Suc n" in spec,
        thin_tac "\<forall>l \<le> (Suc n). f l \<in> carrier R", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>ideal R I; f ` {i. i \<le> Suc n} \<subseteq> I; sum_pr_ideals R f n \<subseteq> I; f (Suc n) \<in> carrier R\<rbrakk> \<Longrightarrow> R \<diamondsuit>\<^sub>p f (Suc n) \<minusplus> sum_pr_ideals R f n \<subseteq> I
[PROOF STEP]
apply (cut_tac a = "Suc n" and A = "{i. i \<le> Suc n}" and
          f = f in mem_in_image2, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>ideal R I; f ` {i. i \<le> Suc n} \<subseteq> I; sum_pr_ideals R f n \<subseteq> I; f (Suc n) \<in> carrier R; f (Suc n) \<in> f ` {i. i \<le> Suc n}\<rbrakk> \<Longrightarrow> R \<diamondsuit>\<^sub>p f (Suc n) \<minusplus> sum_pr_ideals R f n \<subseteq> I
[PROOF STEP]
apply (frule_tac A = "f ` {i. i \<le> Suc n}" and B = I and c = "f (Suc n)" in
          subsetD,  assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>ideal R I; f ` {i. i \<le> Suc n} \<subseteq> I; sum_pr_ideals R f n \<subseteq> I; f (Suc n) \<in> carrier R; f (Suc n) \<in> f ` {i. i \<le> Suc n}; f (Suc n) \<in> I\<rbrakk> \<Longrightarrow> R \<diamondsuit>\<^sub>p f (Suc n) \<minusplus> sum_pr_ideals R f n \<subseteq> I
[PROOF STEP]
apply (rule_tac A = "Rxa R  (f (Suc n))" and B = "sum_pr_ideals R f n" in
        sum_ideals_cont[of I], assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n f. \<lbrakk>ideal R I; f ` {i. i \<le> Suc n} \<subseteq> I; sum_pr_ideals R f n \<subseteq> I; f (Suc n) \<in> carrier R; f (Suc n) \<in> f ` {i. i \<le> Suc n}; f (Suc n) \<in> I\<rbrakk> \<Longrightarrow> R \<diamondsuit>\<^sub>p f (Suc n) \<subseteq> I
 2. \<And>n f. \<lbrakk>ideal R I; f ` {i. i \<le> Suc n} \<subseteq> I; sum_pr_ideals R f n \<subseteq> I; f (Suc n) \<in> carrier R; f (Suc n) \<in> f ` {i. i \<le> Suc n}; f (Suc n) \<in> I\<rbrakk> \<Longrightarrow> sum_pr_ideals R f n \<subseteq> I
[PROOF STEP]
apply (rule ideal_cont_Rxa[of I], assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) sum_of_prideals4:"\<lbrakk>ideal R I; \<forall>l \<le> n. f l \<in> carrier R;
       (f ` {i. i \<le> n} \<subseteq> I)\<rbrakk> \<Longrightarrow> sum_pr_ideals R f n \<subseteq> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; \<forall>l\<le>n. f l \<in> carrier R; f ` {i. i \<le> n} \<subseteq> I\<rbrakk> \<Longrightarrow> sum_pr_ideals R f n \<subseteq> I
[PROOF STEP]
apply (simp add:sum_of_prideals3)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ker_ideal:"\<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> ideal A (ker\<^bsub>A,R\<^esub> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> ideal A (ker\<^bsub>A,R\<^esub> f)
[PROOF STEP]
apply (frule Ring.ring_is_ag[of "A"], frule Ring.ring_is_ag[of "R"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> ideal A (ker\<^bsub>A,R\<^esub> f)
[PROOF STEP]
apply (rule Ring.ideal_condition1, assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> ker\<^bsub>A,R\<^esub> f \<subseteq> carrier A
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> ker\<^bsub>A,R\<^esub> f \<noteq> {}
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> \<forall>x\<in>ker\<^bsub>A,R\<^esub> f. \<forall>y\<in>ker\<^bsub>A,R\<^esub> f. x \<plusminus>\<^bsub>A\<^esub> y \<in> ker\<^bsub>A,R\<^esub> f
 4. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier A. \<forall>x\<in>ker\<^bsub>A,R\<^esub> f. r \<cdot>\<^sub>r\<^bsub>A\<^esub> x \<in> ker\<^bsub>A,R\<^esub> f
[PROOF STEP]
apply (rule subsetI,
       simp add:ker_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> ker\<^bsub>A,R\<^esub> f \<noteq> {}
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> \<forall>x\<in>ker\<^bsub>A,R\<^esub> f. \<forall>y\<in>ker\<^bsub>A,R\<^esub> f. x \<plusminus>\<^bsub>A\<^esub> y \<in> ker\<^bsub>A,R\<^esub> f
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier A. \<forall>x\<in>ker\<^bsub>A,R\<^esub> f. r \<cdot>\<^sub>r\<^bsub>A\<^esub> x \<in> ker\<^bsub>A,R\<^esub> f
[PROOF STEP]
apply (simp add:rHom_def, frule conjunct1)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> aHom A R \<and> (\<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y) \<and> f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>; aGroup A; aGroup R; f \<in> aHom A R\<rbrakk> \<Longrightarrow> ker\<^bsub>A,R\<^esub> f \<noteq> {}
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> \<forall>x\<in>ker\<^bsub>A,R\<^esub> f. \<forall>y\<in>ker\<^bsub>A,R\<^esub> f. x \<plusminus>\<^bsub>A\<^esub> y \<in> ker\<^bsub>A,R\<^esub> f
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier A. \<forall>x\<in>ker\<^bsub>A,R\<^esub> f. r \<cdot>\<^sub>r\<^bsub>A\<^esub> x \<in> ker\<^bsub>A,R\<^esub> f
[PROOF STEP]
apply (frule ker_inc_zero[of "A" "R" "f"], assumption+, blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> \<forall>x\<in>ker\<^bsub>A,R\<^esub> f. \<forall>y\<in>ker\<^bsub>A,R\<^esub> f. x \<plusminus>\<^bsub>A\<^esub> y \<in> ker\<^bsub>A,R\<^esub> f
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier A. \<forall>x\<in>ker\<^bsub>A,R\<^esub> f. r \<cdot>\<^sub>r\<^bsub>A\<^esub> x \<in> ker\<^bsub>A,R\<^esub> f
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R; x \<in> ker\<^bsub>A,R\<^esub> f; y \<in> ker\<^bsub>A,R\<^esub> f\<rbrakk> \<Longrightarrow> x \<plusminus>\<^bsub>A\<^esub> y \<in> ker\<^bsub>A,R\<^esub> f
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier A. \<forall>x\<in>ker\<^bsub>A,R\<^esub> f. r \<cdot>\<^sub>r\<^bsub>A\<^esub> x \<in> ker\<^bsub>A,R\<^esub> f
[PROOF STEP]
apply (simp add:ker_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R; x \<in> carrier A; f x = \<zero>\<^bsub>R\<^esub>; y \<in> carrier A; f y = \<zero>\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> x \<plusminus>\<^bsub>A\<^esub> y \<in> carrier A \<and> f (x \<plusminus>\<^bsub>A\<^esub> y) = \<zero>\<^bsub>R\<^esub>
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier A. \<forall>x\<in>ker\<^bsub>A,R\<^esub> f. r \<cdot>\<^sub>r\<^bsub>A\<^esub> x \<in> ker\<^bsub>A,R\<^esub> f
[PROOF STEP]
apply (simp add:aGroup.ag_pOp_closed)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R; x \<in> carrier A; f x = \<zero>\<^bsub>R\<^esub>; y \<in> carrier A; f y = \<zero>\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> f (x \<plusminus>\<^bsub>A\<^esub> y) = \<zero>\<^bsub>R\<^esub>
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier A. \<forall>x\<in>ker\<^bsub>A,R\<^esub> f. r \<cdot>\<^sub>r\<^bsub>A\<^esub> x \<in> ker\<^bsub>A,R\<^esub> f
[PROOF STEP]
apply (simp add:rHom_def, frule conjunct1,
        simp add:aHom_add,
        frule Ring.ring_zero[of "R"],
        simp add:aGroup.ag_l_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier A. \<forall>x\<in>ker\<^bsub>A,R\<^esub> f. r \<cdot>\<^sub>r\<^bsub>A\<^esub> x \<in> ker\<^bsub>A,R\<^esub> f
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R; r \<in> carrier A; x \<in> ker\<^bsub>A,R\<^esub> f\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r\<^bsub>A\<^esub> x \<in> ker\<^bsub>A,R\<^esub> f
[PROOF STEP]
apply (simp add:ker_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R; r \<in> carrier A; x \<in> carrier A; f x = \<zero>\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r\<^bsub>A\<^esub> x \<in> carrier A \<and> f (r \<cdot>\<^sub>r\<^bsub>A\<^esub> x) = \<zero>\<^bsub>R\<^esub>
[PROOF STEP]
apply (simp add:Ring.ring_tOp_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R; r \<in> carrier A; x \<in> carrier A; f x = \<zero>\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> f (r \<cdot>\<^sub>r\<^bsub>A\<^esub> x) = \<zero>\<^bsub>R\<^esub>
[PROOF STEP]
apply (simp add:rHom_tOp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R; r \<in> carrier A; x \<in> carrier A; f x = \<zero>\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> f r \<cdot>\<^sub>r\<^bsub>R\<^esub> \<zero>\<^bsub>R\<^esub> = \<zero>\<^bsub>R\<^esub>
[PROOF STEP]
apply (frule_tac a = r in rHom_mem[of "f" "A" "R"], assumption+,
        simp add:Ring.ring_times_x_0)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done