[STATEMENT]
lemma (in Ring) qring_carrier:"ideal R I \<Longrightarrow>
              carrier (qring R I)  = {X. \<exists>a\<in> carrier R. a \<uplus>\<^bsub>R\<^esub> I = X}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> carrier (R /\<^sub>r I) = {X. \<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> I = X}
[PROOF STEP]
apply (simp add:carrier_qring1 set_ar_cos_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> {X. \<exists>a\<in>carrier R. X = a \<uplus>\<^bsub>R\<^esub> I} = {X. \<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> I = X}
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ideal R I \<Longrightarrow> {X. \<exists>a\<in>carrier R. X = a \<uplus>\<^bsub>R\<^esub> I} \<subseteq> {X. \<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> I = X}
 2. ideal R I \<Longrightarrow> {X. \<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> I = X} \<subseteq> {X. \<exists>a\<in>carrier R. X = a \<uplus>\<^bsub>R\<^esub> I}
[PROOF STEP]
apply (rule subsetI, simp, erule bexE, frule sym, thin_tac "x = a \<uplus>\<^bsub>R\<^esub> I",
        blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> {X. \<exists>a\<in>carrier R. a \<uplus>\<^bsub>R\<^esub> I = X} \<subseteq> {X. \<exists>a\<in>carrier R. X = a \<uplus>\<^bsub>R\<^esub> I}
[PROOF STEP]
apply (rule subsetI, simp, erule bexE, frule sym, thin_tac "a \<uplus>\<^bsub>R\<^esub> I = x",
       blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) qring_mem:"\<lbrakk>ideal R I; a \<in> carrier R\<rbrakk> \<Longrightarrow>
                                 a \<uplus>\<^bsub>R\<^esub> I \<in> carrier (qring R I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>R\<^esub> I \<in> carrier (R /\<^sub>r I)
[PROOF STEP]
apply (simp add:qring_carrier)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>aa\<in>carrier R. aa \<uplus>\<^bsub>R\<^esub> I = a \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) qring_pOp:"\<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R \<rbrakk>
 \<Longrightarrow> pop (qring R I) (a \<uplus>\<^bsub>R\<^esub> I) (b \<uplus>\<^bsub>R\<^esub> I) = (a \<plusminus> b) \<uplus>\<^bsub>R\<^esub> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>R\<^esub> I \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> b \<uplus>\<^bsub>R\<^esub> I = (a \<plusminus> b) \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
by (simp add:qring_def, simp add:ar_c_top)


[STATEMENT]
lemma (in Ring) qring_zero:"ideal R I \<Longrightarrow> zero (qring R I) = I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> = I
[PROOF STEP]
apply (simp add:qring_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) qring_zero_1:"\<lbrakk>a \<in> carrier R; ideal R I; a \<uplus>\<^bsub>R\<^esub> I = I\<rbrakk> \<Longrightarrow>
                                    a \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; ideal R I; a \<uplus>\<^bsub>R\<^esub> I = I\<rbrakk> \<Longrightarrow> a \<in> I
[PROOF STEP]
by (frule a_in_ar_coset [of "I" "a"], assumption+, simp)


[STATEMENT]
lemma (in Ring) Qring_fix1:"\<lbrakk>a \<in> carrier R; ideal R I; a \<in> I\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>R\<^esub> I = I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; ideal R I; a \<in> I\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>R\<^esub> I = I
[PROOF STEP]
apply (cut_tac ring_is_ag, frule aGroup.b_ag_group)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; ideal R I; a \<in> I; aGroup R; Group (b_ag R)\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>R\<^esub> I = I
[PROOF STEP]
apply (simp add:ar_coset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; ideal R I; a \<in> I; aGroup R; Group (b_ag R)\<rbrakk> \<Longrightarrow> I \<bullet>\<^bsub>b_ag R\<^esub> a = I
[PROOF STEP]
apply (frule ideal_asubg[of "I"], simp add:asubGroup_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; ideal R I; a \<in> I; aGroup R; Group (b_ag R); b_ag R \<guillemotright> I \<rbrakk> \<Longrightarrow> I \<bullet>\<^bsub>b_ag R\<^esub> a = I
[PROOF STEP]
apply (simp add:Group.rcs_fixed2[of "b_ag R" "I"])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ar_cos_same:"\<lbrakk>a \<in> carrier R; ideal R I; x \<in> a \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow>
                                x \<uplus>\<^bsub>R\<^esub> I = a \<uplus>\<^bsub>R\<^esub> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; ideal R I; x \<in> a \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> x \<uplus>\<^bsub>R\<^esub> I = a \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; ideal R I; x \<in> a \<uplus>\<^bsub>R\<^esub> I; aGroup R\<rbrakk> \<Longrightarrow> x \<uplus>\<^bsub>R\<^esub> I = a \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (rule ar_coset_same1[of "I" "x" "a"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>a \<in> carrier R; ideal R I; x \<in> a \<uplus>\<^bsub>R\<^esub> I; aGroup R\<rbrakk> \<Longrightarrow> x \<in> carrier R
 2. \<lbrakk>a \<in> carrier R; ideal R I; x \<in> a \<uplus>\<^bsub>R\<^esub> I; aGroup R\<rbrakk> \<Longrightarrow> a \<in> carrier R
 3. \<lbrakk>a \<in> carrier R; ideal R I; x \<in> a \<uplus>\<^bsub>R\<^esub> I; aGroup R\<rbrakk> \<Longrightarrow> a \<plusminus> -\<^sub>a x \<in> I
[PROOF STEP]
apply (rule ar_coset_subsetD[of "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; ideal R I; x \<in> a \<uplus>\<^bsub>R\<^esub> I; aGroup R\<rbrakk> \<Longrightarrow> a \<plusminus> -\<^sub>a x \<in> I
[PROOF STEP]
apply (frule ar_coset_mem2[of "I" "a" "x"], assumption+,
       erule bexE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. \<lbrakk>a \<in> carrier R; ideal R I; x \<in> a \<uplus>\<^bsub>R\<^esub> I; aGroup R; h \<in> I; x = a \<plusminus> h\<rbrakk> \<Longrightarrow> a \<plusminus> -\<^sub>a x \<in> I
[PROOF STEP]
apply (frule_tac h = h in ideal_subset[of "I"], assumption,
      simp add:aGroup.ag_p_inv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. \<lbrakk>a \<in> carrier R; ideal R I; a \<plusminus> h \<in> a \<uplus>\<^bsub>R\<^esub> I; aGroup R; h \<in> I; x = a \<plusminus> h; h \<in> carrier R\<rbrakk> \<Longrightarrow> a \<plusminus> (-\<^sub>a a \<plusminus> -\<^sub>a h) \<in> I
[PROOF STEP]
apply (frule_tac x = a in aGroup.ag_mOp_closed[of "R"], assumption+,
       frule_tac x = h in aGroup.ag_mOp_closed[of "R"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. \<lbrakk>a \<in> carrier R; ideal R I; a \<plusminus> h \<in> a \<uplus>\<^bsub>R\<^esub> I; aGroup R; h \<in> I; x = a \<plusminus> h; h \<in> carrier R; -\<^sub>a a \<in> carrier R; -\<^sub>a h \<in> carrier R\<rbrakk> \<Longrightarrow> a \<plusminus> (-\<^sub>a a \<plusminus> -\<^sub>a h) \<in> I
[PROOF STEP]
apply (simp add:aGroup.ag_pOp_assoc[THEN sym],
       simp add:aGroup.ag_r_inv1 aGroup.ag_l_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. \<lbrakk>a \<in> carrier R; ideal R I; a \<plusminus> h \<in> a \<uplus>\<^bsub>R\<^esub> I; aGroup R; h \<in> I; x = a \<plusminus> h; h \<in> carrier R; -\<^sub>a a \<in> carrier R; -\<^sub>a h \<in> carrier R\<rbrakk> \<Longrightarrow> -\<^sub>a h \<in> I
[PROOF STEP]
apply (simp add:ideal_inv1_closed)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) qring_tOp:"\<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R\<rbrakk> \<Longrightarrow>
                tp (qring R I) (a \<uplus>\<^bsub>R\<^esub> I) (b \<uplus>\<^bsub>R\<^esub> I) = (a \<cdot>\<^sub>r b) \<uplus>\<^bsub>R\<^esub> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R\<rbrakk> \<Longrightarrow> (a \<uplus>\<^bsub>R\<^esub> I) \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<uplus>\<^bsub>R\<^esub> I) = a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
by (simp add:qring_def, simp add:rcostOp)


[STATEMENT]
lemma rind_hom_well_def:"\<lbrakk>Ring A; Ring R; f \<in> rHom A R; a \<in> carrier A \<rbrakk> \<Longrightarrow>
                                   f a = (f\<degree>\<^bsub>A,R\<^esub>) (a \<uplus>\<^bsub>A\<^esub> (ker\<^bsub>A,R\<^esub> f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; a \<in> carrier A\<rbrakk> \<Longrightarrow> f a = (f\<degree>\<^bsub>A,R\<^esub>) (a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f)
[PROOF STEP]
apply (frule ker_ideal[of "A" "R" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; a \<in> carrier A; ideal A (ker\<^bsub>A,R\<^esub> f)\<rbrakk> \<Longrightarrow> f a = (f\<degree>\<^bsub>A,R\<^esub>) (a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f)
[PROOF STEP]
apply (frule Ring.mem_set_ar_cos[of "A" "ker\<^bsub>A,R\<^esub> f" "a"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; a \<in> carrier A; ideal A (ker\<^bsub>A,R\<^esub> f); a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f)\<rbrakk> \<Longrightarrow> f a = (f\<degree>\<^bsub>A,R\<^esub>) (a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f)
[PROOF STEP]
apply (simp add:rind_hom_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; a \<in> carrier A; ideal A (ker\<^bsub>A,R\<^esub> f); a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f)\<rbrakk> \<Longrightarrow> f a = f (SOME x. x \<in> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f)
[PROOF STEP]
apply (rule someI2_ex)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; a \<in> carrier A; ideal A (ker\<^bsub>A,R\<^esub> f); a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f)\<rbrakk> \<Longrightarrow> \<exists>aa. aa \<in> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f
 2. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; a \<in> carrier A; ideal A (ker\<^bsub>A,R\<^esub> f); a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f); x \<in> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f\<rbrakk> \<Longrightarrow> f a = f x
[PROOF STEP]
apply (frule Ring.a_in_ar_coset [of "A" "ker\<^bsub>A,R\<^esub> f" "a"], assumption+, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; a \<in> carrier A; ideal A (ker\<^bsub>A,R\<^esub> f); a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f); x \<in> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f\<rbrakk> \<Longrightarrow> f a = f x
[PROOF STEP]
apply (frule_tac x = x in Ring.ar_coset_mem2[of "A" "ker\<^bsub>A,R\<^esub> f" "a"],
           assumption+, erule bexE, simp,
        frule_tac h = h in Ring.ideal_subset[of "A" "ker\<^bsub>A,R\<^esub> f"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x h. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; a \<in> carrier A; ideal A (ker\<^bsub>A,R\<^esub> f); a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f); a \<plusminus>\<^bsub>A\<^esub> h \<in> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f; h \<in> ker\<^bsub>A,R\<^esub> f; x = a \<plusminus>\<^bsub>A\<^esub> h; h \<in> carrier A\<rbrakk> \<Longrightarrow> f a = f (a \<plusminus>\<^bsub>A\<^esub> h)
[PROOF STEP]
apply (frule_tac Ring.ring_is_ag[of "A"],
        frule_tac Ring.ring_is_ag[of "R"],
        simp add:rHom_def, frule conjunct1, simp add:aHom_add)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x h. \<lbrakk>Ring A; Ring R; (\<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>; a \<in> carrier A; ideal A (ker\<^bsub>A,R\<^esub> f); a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f); a \<plusminus>\<^bsub>A\<^esub> h \<in> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f; h \<in> ker\<^bsub>A,R\<^esub> f; x = a \<plusminus>\<^bsub>A\<^esub> h; h \<in> carrier A; aGroup A; aGroup R; f \<in> aHom A R\<rbrakk> \<Longrightarrow> f a = f a \<plusminus>\<^bsub>R\<^esub> f h
[PROOF STEP]
apply (simp add:ker_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x h. \<lbrakk>Ring A; Ring R; (\<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>; a \<in> carrier A; ideal A {a \<in> carrier A. f a = \<zero>\<^bsub>R\<^esub>}; a \<uplus>\<^bsub>A\<^esub> {a \<in> carrier A. f a = \<zero>\<^bsub>R\<^esub>} \<in> set_ar_cos A {a \<in> carrier A. f a = \<zero>\<^bsub>R\<^esub>}; a \<plusminus>\<^bsub>A\<^esub> h \<in> a \<uplus>\<^bsub>A\<^esub> {a \<in> carrier A. f a = \<zero>\<^bsub>R\<^esub>}; f h = \<zero>\<^bsub>R\<^esub>; x = a \<plusminus>\<^bsub>A\<^esub> h; h \<in> carrier A; aGroup A; aGroup R; f \<in> aHom A R\<rbrakk> \<Longrightarrow> f a = f a \<plusminus>\<^bsub>R\<^esub> \<zero>\<^bsub>R\<^esub>
[PROOF STEP]
apply (frule aHom_mem[of "A" "R" "f" "a"], assumption+,
        simp add:aGroup.ag_r_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) set_r_ar_cos:"ideal R I \<Longrightarrow>
                 set_rcs (b_ag R) I = set_ar_cos R I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> set_rcs (b_ag R) I = set_ar_cos R I
[PROOF STEP]
apply (simp add:set_ar_cos_def set_rcs_def ar_coset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> {C. \<exists>a\<in>carrier (b_ag R). C = I \<bullet>\<^bsub>b_ag R\<^esub> a} = {X. \<exists>a\<in>carrier R. X = I \<bullet>\<^bsub>b_ag R\<^esub> a}
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; aGroup R\<rbrakk> \<Longrightarrow> {C. \<exists>a\<in>carrier (b_ag R). C = I \<bullet>\<^bsub>b_ag R\<^esub> a} = {X. \<exists>a\<in>carrier R. X = I \<bullet>\<^bsub>b_ag R\<^esub> a}
[PROOF STEP]
apply (simp add:aGroup.ag_carrier_carrier)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma set_r_ar_cos_ker:"\<lbrakk>Ring A; Ring R; f \<in> rHom A R \<rbrakk> \<Longrightarrow>
                     set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f) = set_ar_cos 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> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f) = set_ar_cos A (ker\<^bsub>A,R\<^esub> f)
[PROOF STEP]
apply (frule ker_ideal[of "A" "R" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; ideal A (ker\<^bsub>A,R\<^esub> f)\<rbrakk> \<Longrightarrow> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f) = set_ar_cos A (ker\<^bsub>A,R\<^esub> f)
[PROOF STEP]
apply (simp add:Ring.carrier_qring[THEN sym],
        simp add:Ring.carrier_qring1[THEN sym])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ind_hom_rhom:"\<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow>
                                    (f\<degree>\<^bsub>A,R\<^esub>) \<in> rHom (qring A (ker\<^bsub>A,R\<^esub> f)) R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R
[PROOF STEP]
apply (simp add:rHom_def [of "qring A (ker\<^bsub>A,R\<^esub> f)" "R"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R \<and> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (simp add:aHom_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) \<rightarrow> carrier R \<and> f\<degree>\<^bsub>A,R\<^esub> \<in> extensional (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))) \<and> (\<forall>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>b\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (a \<plusminus>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b)
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) \<rightarrow> carrier R
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> extensional (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))) \<and> (\<forall>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>b\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (a \<plusminus>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b)
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (simp add:qring_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f) \<rightarrow> carrier R
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> extensional (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))) \<and> (\<forall>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>b\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (a \<plusminus>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b)
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (simp add:rind_hom_def extensional_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<lambda>X\<in>set_ar_cos A (ker\<^bsub>A,R\<^esub> f). f (SOME x. x \<in> X)) \<in> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f) \<rightarrow> carrier R
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> extensional (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))) \<and> (\<forall>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>b\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (a \<plusminus>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b)
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (rule Pi_I)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; x \<in> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f)\<rbrakk> \<Longrightarrow> (\<lambda>X\<in>set_ar_cos A (ker\<^bsub>A,R\<^esub> f). f (SOME x. x \<in> X)) x \<in> carrier R
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> extensional (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))) \<and> (\<forall>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>b\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (a \<plusminus>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b)
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (frule Ring.ring_is_ag [of "A"], frule Ring.ring_is_ag [of "R"],
        frule aGroup.b_ag_group [of "R"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; x \<in> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f); aGroup A; aGroup R; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<lambda>X\<in>set_ar_cos A (ker\<^bsub>A,R\<^esub> f). f (SOME x. x \<in> X)) x \<in> carrier R
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> extensional (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))) \<and> (\<forall>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>b\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (a \<plusminus>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b)
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (simp add:aGroup.ag_carrier_carrier [THEN sym])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; x \<in> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f); aGroup A; aGroup R; Group (b_ag R)\<rbrakk> \<Longrightarrow> (x \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f) \<longrightarrow> f (SOME xa. xa \<in> x) \<in> carrier (b_ag R)) \<and> (x \<notin> set_ar_cos A (ker\<^bsub>A,R\<^esub> f) \<longrightarrow> undefined \<in> carrier (b_ag R))
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> extensional (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))) \<and> (\<forall>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>b\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (a \<plusminus>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b)
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (simp add:set_ar_cos_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; x \<in> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f); aGroup A; aGroup R; Group (b_ag R)\<rbrakk> \<Longrightarrow> ((\<exists>a\<in>carrier A. x = a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) \<longrightarrow> f (SOME xa. xa \<in> x) \<in> carrier (b_ag R)) \<and> ((\<forall>a\<in>carrier A. x \<noteq> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) \<longrightarrow> undefined \<in> carrier (b_ag R))
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> extensional (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))) \<and> (\<forall>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>b\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (a \<plusminus>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b)
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; x \<in> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f); aGroup A; aGroup R; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<exists>a\<in>carrier A. x = a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) \<longrightarrow> f (SOME xa. xa \<in> x) \<in> carrier (b_ag R)
 2. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; x \<in> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f); aGroup A; aGroup R; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a\<in>carrier A. x \<noteq> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) \<longrightarrow> undefined \<in> carrier (b_ag R)
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> extensional (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))) \<and> (\<forall>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>b\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (a \<plusminus>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b)
 4. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; x \<in> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f); aGroup A; aGroup R; Group (b_ag R); \<exists>a\<in>carrier A. x = a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f\<rbrakk> \<Longrightarrow> f (SOME xa. xa \<in> x) \<in> carrier (b_ag R)
 2. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; x \<in> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f); aGroup A; aGroup R; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a\<in>carrier A. x \<noteq> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) \<longrightarrow> undefined \<in> carrier (b_ag R)
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> extensional (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))) \<and> (\<forall>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>b\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (a \<plusminus>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b)
 4. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (erule bexE, simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x a. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f \<in> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f); aGroup A; aGroup R; Group (b_ag R); a \<in> carrier A; x = a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f\<rbrakk> \<Longrightarrow> f (SOME x. x \<in> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) \<in> carrier (b_ag R)
 2. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; x \<in> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f); aGroup A; aGroup R; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a\<in>carrier A. x \<noteq> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) \<longrightarrow> undefined \<in> carrier (b_ag R)
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> extensional (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))) \<and> (\<forall>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>b\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (a \<plusminus>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b)
 4. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (frule ker_ideal [of "A" "R" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x a. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f \<in> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f); aGroup A; aGroup R; Group (b_ag R); a \<in> carrier A; x = a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f; ideal A (ker\<^bsub>A,R\<^esub> f)\<rbrakk> \<Longrightarrow> f (SOME x. x \<in> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) \<in> carrier (b_ag R)
 2. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; x \<in> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f); aGroup A; aGroup R; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a\<in>carrier A. x \<noteq> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) \<longrightarrow> undefined \<in> carrier (b_ag R)
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> extensional (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))) \<and> (\<forall>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>b\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (a \<plusminus>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b)
 4. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (frule_tac a = a in Ring.a_in_ar_coset [of "A" "ker\<^bsub>A,R\<^esub> f"],
        assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x a. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f \<in> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f); aGroup A; aGroup R; Group (b_ag R); a \<in> carrier A; x = a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f; ideal A (ker\<^bsub>A,R\<^esub> f); a \<in> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f\<rbrakk> \<Longrightarrow> f (SOME x. x \<in> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) \<in> carrier (b_ag R)
 2. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; x \<in> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f); aGroup A; aGroup R; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a\<in>carrier A. x \<noteq> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) \<longrightarrow> undefined \<in> carrier (b_ag R)
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> extensional (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))) \<and> (\<forall>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>b\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (a \<plusminus>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b)
 4. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (rule someI2_ex, blast)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x a xa. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f \<in> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f); aGroup A; aGroup R; Group (b_ag R); a \<in> carrier A; x = a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f; ideal A (ker\<^bsub>A,R\<^esub> f); a \<in> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f; xa \<in> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f\<rbrakk> \<Longrightarrow> f xa \<in> carrier (b_ag R)
 2. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; x \<in> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f); aGroup A; aGroup R; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a\<in>carrier A. x \<noteq> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) \<longrightarrow> undefined \<in> carrier (b_ag R)
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> extensional (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))) \<and> (\<forall>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>b\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (a \<plusminus>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b)
 4. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (frule_tac I = "ker\<^bsub>A,R\<^esub> f" and a = a and x = xa in
                   Ring.ar_coset_subsetD[of "A"], assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x a xa. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f \<in> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f); aGroup A; aGroup R; Group (b_ag R); a \<in> carrier A; x = a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f; ideal A (ker\<^bsub>A,R\<^esub> f); a \<in> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f; xa \<in> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f; xa \<in> carrier A\<rbrakk> \<Longrightarrow> f xa \<in> carrier (b_ag R)
 2. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; x \<in> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f); aGroup A; aGroup R; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a\<in>carrier A. x \<noteq> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) \<longrightarrow> undefined \<in> carrier (b_ag R)
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> extensional (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))) \<and> (\<forall>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>b\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (a \<plusminus>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b)
 4. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (simp add:aGroup.ag_carrier_carrier, simp add:rHom_mem)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; x \<in> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f); aGroup A; aGroup R; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a\<in>carrier A. x \<noteq> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) \<longrightarrow> undefined \<in> carrier (b_ag R)
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> extensional (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))) \<and> (\<forall>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>b\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (a \<plusminus>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b)
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (simp add:set_r_ar_cos_ker, simp add:set_ar_cos_def, rule impI, blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> extensional (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))) \<and> (\<forall>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>b\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (a \<plusminus>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b)
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> extensional (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)))
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>b\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (a \<plusminus>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (simp add:qring_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> extensional (set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f))
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>b\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (a \<plusminus>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (simp add:set_r_ar_cos_ker)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> extensional (set_ar_cos A (ker\<^bsub>A,R\<^esub> f))
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>b\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (a \<plusminus>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (simp add:rind_hom_def extensional_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>b\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (a \<plusminus>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; a \<in> carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)); b \<in> carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,R\<^esub>) (a \<plusminus>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (simp add:qring_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; a \<in> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f); b \<in> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f)\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,R\<^esub>) (c_top (b_ag A) (ker\<^bsub>A,R\<^esub> f) a b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (simp add:set_r_ar_cos_ker)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; a \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f); b \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f)\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,R\<^esub>) (c_top (b_ag A) (ker\<^bsub>A,R\<^esub> f) a b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (simp add:set_ar_cos_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; \<exists>aa\<in>carrier A. a = aa \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f; \<exists>a\<in>carrier A. b = a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,R\<^esub>) (c_top (b_ag A) (ker\<^bsub>A,R\<^esub> f) a b) = (f\<degree>\<^bsub>A,R\<^esub>) a \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) b
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply ((erule bexE)+, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ab. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aa \<in> carrier A; a = aa \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f; ab \<in> carrier A; b = ab \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,R\<^esub>) (c_top (b_ag A) (ker\<^bsub>A,R\<^esub> f) (aa \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) (ab \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f)) = (f\<degree>\<^bsub>A,R\<^esub>) (aa \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) (ab \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f)
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (frule ker_ideal[of "A" "R" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ab. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aa \<in> carrier A; a = aa \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f; ab \<in> carrier A; b = ab \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f; ideal A (ker\<^bsub>A,R\<^esub> f)\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,R\<^esub>) (c_top (b_ag A) (ker\<^bsub>A,R\<^esub> f) (aa \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) (ab \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f)) = (f\<degree>\<^bsub>A,R\<^esub>) (aa \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) (ab \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f)
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (simp add:Ring.ar_c_top)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ab. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aa \<in> carrier A; a = aa \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f; ab \<in> carrier A; b = ab \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f; ideal A (ker\<^bsub>A,R\<^esub> f)\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,R\<^esub>) ((aa \<plusminus>\<^bsub>A\<^esub> ab) \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) = (f\<degree>\<^bsub>A,R\<^esub>) (aa \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) (ab \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f)
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (frule Ring.ring_is_ag[of "A"],
        frule Ring.ring_is_ag[of "R"],
        frule_tac x = aa and y = ab in aGroup.ag_pOp_closed[of "A"],
        assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ab. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aa \<in> carrier A; a = aa \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f; ab \<in> carrier A; b = ab \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f; ideal A (ker\<^bsub>A,R\<^esub> f); aGroup A; aGroup R; aa \<plusminus>\<^bsub>A\<^esub> ab \<in> carrier A\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,R\<^esub>) ((aa \<plusminus>\<^bsub>A\<^esub> ab) \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) = (f\<degree>\<^bsub>A,R\<^esub>) (aa \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) \<plusminus>\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) (ab \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f)
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (simp add:rind_hom_well_def[THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ab. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aa \<in> carrier A; a = aa \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f; ab \<in> carrier A; b = ab \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f; ideal A (ker\<^bsub>A,R\<^esub> f); aGroup A; aGroup R; aa \<plusminus>\<^bsub>A\<^esub> ab \<in> carrier A\<rbrakk> \<Longrightarrow> f (aa \<plusminus>\<^bsub>A\<^esub> ab) = f aa \<plusminus>\<^bsub>R\<^esub> f ab
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (simp add:rHom_def, frule conjunct1, simp add:aHom_add)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y) \<and> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). \<forall>y\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[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; x \<in> carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)); y \<in> carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,R\<^esub>) (x \<cdot>\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> y) = (f\<degree>\<^bsub>A,R\<^esub>) x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) y
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (frule ker_ideal[of "A" "R" "f"], assumption+,
        simp add:Ring.carrier_qring1, simp add:set_ar_cos_def,
        (erule bexE)+, simp add:qring_def Ring.rcostOp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y a aa. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; ideal A (ker\<^bsub>A,R\<^esub> f); a \<in> carrier A; x = a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f; aa \<in> carrier A; y = aa \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,R\<^esub>) (a \<cdot>\<^sub>r\<^bsub>A\<^esub> aa \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) = (f\<degree>\<^bsub>A,R\<^esub>) (a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) (aa \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f)
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (frule Ring.ring_is_ag[of "A"],
         frule_tac x = a and y = aa in Ring.ring_tOp_closed[of "A"],
         assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y a aa. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; ideal A (ker\<^bsub>A,R\<^esub> f); a \<in> carrier A; x = a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f; aa \<in> carrier A; y = aa \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f; aGroup A; a \<cdot>\<^sub>r\<^bsub>A\<^esub> aa \<in> carrier A\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,R\<^esub>) (a \<cdot>\<^sub>r\<^bsub>A\<^esub> aa \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) = (f\<degree>\<^bsub>A,R\<^esub>) (a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) \<cdot>\<^sub>r\<^bsub>R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) (aa \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f)
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (simp add:rind_hom_well_def[THEN sym], simp add:rHom_tOp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,R\<^esub>) 1\<^sub>r\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (simp add:qring_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,R\<^esub>) (1\<^sub>r\<^bsub>A\<^esub> \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
apply (frule Ring.ring_one[of "A"],
        simp add:rind_hom_well_def[THEN sym],
        simp add:rHom_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ind_hom_injec:"\<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow>
                              injec\<^bsub>(qring A (ker\<^bsub>A,R\<^esub> f)),R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> injec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>)
[PROOF STEP]
apply (simp add:injec_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R \<and> ker\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) = {\<zero>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub>}
[PROOF STEP]
apply (frule ind_hom_rhom [of "A" "R" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R \<and> ker\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) = {\<zero>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub>}
[PROOF STEP]
apply (frule rHom_aHom[of "f\<degree>\<^bsub>A,R\<^esub>" "A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)" "R"], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R\<rbrakk> \<Longrightarrow> ker\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) = {\<zero>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub>}
[PROOF STEP]
apply (simp add:ker_def[of _ _ "f\<degree>\<^bsub>A,R\<^esub>"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R\<rbrakk> \<Longrightarrow> {a \<in> carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) a = \<zero>\<^bsub>R\<^esub>} = {\<zero>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub>}
[PROOF STEP]
apply ((subst qring_def)+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R\<rbrakk> \<Longrightarrow> {a \<in> set_rcs (b_ag A) (ker\<^bsub>A,R\<^esub> f). (f\<degree>\<^bsub>A,R\<^esub>) a = \<zero>\<^bsub>R\<^esub>} = {ker\<^bsub>A,R\<^esub> f}
[PROOF STEP]
apply (simp add:set_r_ar_cos_ker)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R\<rbrakk> \<Longrightarrow> {a \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f). (f\<degree>\<^bsub>A,R\<^esub>) a = \<zero>\<^bsub>R\<^esub>} = {ker\<^bsub>A,R\<^esub> f}
[PROOF STEP]
apply (frule Ring.ring_is_ag[of "A"],
       frule Ring.ring_is_ag[of "R"],
       frule ker_ideal[of "A" "R" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; aGroup A; aGroup R; ideal A (ker\<^bsub>A,R\<^esub> f)\<rbrakk> \<Longrightarrow> {a \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f). (f\<degree>\<^bsub>A,R\<^esub>) a = \<zero>\<^bsub>R\<^esub>} = {ker\<^bsub>A,R\<^esub> f}
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; aGroup A; aGroup R; ideal A (ker\<^bsub>A,R\<^esub> f)\<rbrakk> \<Longrightarrow> {a \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f). (f\<degree>\<^bsub>A,R\<^esub>) a = \<zero>\<^bsub>R\<^esub>} \<subseteq> {ker\<^bsub>A,R\<^esub> f}
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; aGroup A; aGroup R; ideal A (ker\<^bsub>A,R\<^esub> f)\<rbrakk> \<Longrightarrow> {ker\<^bsub>A,R\<^esub> f} \<subseteq> {a \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f). (f\<degree>\<^bsub>A,R\<^esub>) a = \<zero>\<^bsub>R\<^esub>}
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; aGroup A; aGroup R; ideal A (ker\<^bsub>A,R\<^esub> f); x \<in> {a \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f). (f\<degree>\<^bsub>A,R\<^esub>) a = \<zero>\<^bsub>R\<^esub>}\<rbrakk> \<Longrightarrow> x \<in> {ker\<^bsub>A,R\<^esub> f}
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; aGroup A; aGroup R; ideal A (ker\<^bsub>A,R\<^esub> f)\<rbrakk> \<Longrightarrow> {ker\<^bsub>A,R\<^esub> f} \<subseteq> {a \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f). (f\<degree>\<^bsub>A,R\<^esub>) a = \<zero>\<^bsub>R\<^esub>}
[PROOF STEP]
apply (simp, erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; aGroup A; aGroup R; ideal A (ker\<^bsub>A,R\<^esub> f); x \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f); (f\<degree>\<^bsub>A,R\<^esub>) x = \<zero>\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> x = ker\<^bsub>A,R\<^esub> f
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; aGroup A; aGroup R; ideal A (ker\<^bsub>A,R\<^esub> f)\<rbrakk> \<Longrightarrow> {ker\<^bsub>A,R\<^esub> f} \<subseteq> {a \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f). (f\<degree>\<^bsub>A,R\<^esub>) a = \<zero>\<^bsub>R\<^esub>}
[PROOF STEP]
apply (simp add:set_ar_cos_def, erule bexE, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x a. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; aGroup A; aGroup R; ideal A (ker\<^bsub>A,R\<^esub> f); (f\<degree>\<^bsub>A,R\<^esub>) (a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) = \<zero>\<^bsub>R\<^esub>; a \<in> carrier A; x = a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f = ker\<^bsub>A,R\<^esub> f
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; aGroup A; aGroup R; ideal A (ker\<^bsub>A,R\<^esub> f)\<rbrakk> \<Longrightarrow> {ker\<^bsub>A,R\<^esub> f} \<subseteq> {a \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f). (f\<degree>\<^bsub>A,R\<^esub>) a = \<zero>\<^bsub>R\<^esub>}
[PROOF STEP]
apply (simp add:rind_hom_well_def[THEN sym, of "A" "R" "f"],
        thin_tac "x = a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x a. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; aGroup A; aGroup R; ideal A (ker\<^bsub>A,R\<^esub> f); f a = \<zero>\<^bsub>R\<^esub>; a \<in> carrier A\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f = ker\<^bsub>A,R\<^esub> f
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; aGroup A; aGroup R; ideal A (ker\<^bsub>A,R\<^esub> f)\<rbrakk> \<Longrightarrow> {ker\<^bsub>A,R\<^esub> f} \<subseteq> {a \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f). (f\<degree>\<^bsub>A,R\<^esub>) a = \<zero>\<^bsub>R\<^esub>}
[PROOF STEP]
apply (rule_tac a = a in Ring.Qring_fix1[of "A" _ "ker\<^bsub>A,R\<^esub> f"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x a. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; aGroup A; aGroup R; ideal A (ker\<^bsub>A,R\<^esub> f); f a = \<zero>\<^bsub>R\<^esub>; a \<in> carrier A\<rbrakk> \<Longrightarrow> a \<in> ker\<^bsub>A,R\<^esub> f
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; aGroup A; aGroup R; ideal A (ker\<^bsub>A,R\<^esub> f)\<rbrakk> \<Longrightarrow> {ker\<^bsub>A,R\<^esub> f} \<subseteq> {a \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f). (f\<degree>\<^bsub>A,R\<^esub>) a = \<zero>\<^bsub>R\<^esub>}
[PROOF STEP]
apply (simp add:ker_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; aGroup A; aGroup R; ideal A (ker\<^bsub>A,R\<^esub> f)\<rbrakk> \<Longrightarrow> {ker\<^bsub>A,R\<^esub> f} \<subseteq> {a \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f). (f\<degree>\<^bsub>A,R\<^esub>) a = \<zero>\<^bsub>R\<^esub>}
[PROOF STEP]
apply (rule subsetI, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; aGroup A; aGroup R; ideal A (ker\<^bsub>A,R\<^esub> f); x = ker\<^bsub>A,R\<^esub> f\<rbrakk> \<Longrightarrow> ker\<^bsub>A,R\<^esub> f \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f) \<and> (f\<degree>\<^bsub>A,R\<^esub>) (ker\<^bsub>A,R\<^esub> f) = \<zero>\<^bsub>R\<^esub>
[PROOF STEP]
apply (simp add:Ring.I_in_set_ar_cos[of "A" "ker\<^bsub>A,R\<^esub> f"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; aGroup A; aGroup R; ideal A (ker\<^bsub>A,R\<^esub> f); x = ker\<^bsub>A,R\<^esub> f\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,R\<^esub>) (ker\<^bsub>A,R\<^esub> f) = \<zero>\<^bsub>R\<^esub>
[PROOF STEP]
apply (frule Ring.ideal_zero[of "A" "ker\<^bsub>A,R\<^esub> f"], assumption+,
        frule Ring.ring_zero[of "A"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; aGroup A; aGroup R; ideal A (ker\<^bsub>A,R\<^esub> f); x = ker\<^bsub>A,R\<^esub> f; \<zero>\<^bsub>A\<^esub> \<in> ker\<^bsub>A,R\<^esub> f; \<zero>\<^bsub>A\<^esub> \<in> carrier A\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,R\<^esub>) (ker\<^bsub>A,R\<^esub> f) = \<zero>\<^bsub>R\<^esub>
[PROOF STEP]
apply (frule Ring.ar_coset_same4[of "A" "ker\<^bsub>A,R\<^esub> f" "\<zero>\<^bsub>A\<^esub>"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; aGroup A; aGroup R; ideal A (ker\<^bsub>A,R\<^esub> f); x = ker\<^bsub>A,R\<^esub> f; \<zero>\<^bsub>A\<^esub> \<in> ker\<^bsub>A,R\<^esub> f; \<zero>\<^bsub>A\<^esub> \<in> carrier A; \<zero>\<^bsub>A\<^esub> \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f = ker\<^bsub>A,R\<^esub> f\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,R\<^esub>) (ker\<^bsub>A,R\<^esub> f) = \<zero>\<^bsub>R\<^esub>
[PROOF STEP]
apply (frule rind_hom_well_def[THEN sym, of "A" "R" "f" "\<zero>\<^bsub>A\<^esub>"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; aGroup A; aGroup R; ideal A (ker\<^bsub>A,R\<^esub> f); x = ker\<^bsub>A,R\<^esub> f; \<zero>\<^bsub>A\<^esub> \<in> ker\<^bsub>A,R\<^esub> f; \<zero>\<^bsub>A\<^esub> \<in> carrier A; \<zero>\<^bsub>A\<^esub> \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f = ker\<^bsub>A,R\<^esub> f; (f\<degree>\<^bsub>A,R\<^esub>) (\<zero>\<^bsub>A\<^esub> \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) = f \<zero>\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,R\<^esub>) (ker\<^bsub>A,R\<^esub> f) = \<zero>\<^bsub>R\<^esub>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; aGroup A; aGroup R; ideal A (ker\<^bsub>A,R\<^esub> f); x = ker\<^bsub>A,R\<^esub> f; \<zero>\<^bsub>A\<^esub> \<in> ker\<^bsub>A,R\<^esub> f; \<zero>\<^bsub>A\<^esub> \<in> carrier A; \<zero>\<^bsub>A\<^esub> \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f = ker\<^bsub>A,R\<^esub> f; (f\<degree>\<^bsub>A,R\<^esub>) (ker\<^bsub>A,R\<^esub> f) = f \<zero>\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> f \<zero>\<^bsub>A\<^esub> = \<zero>\<^bsub>R\<^esub>
[PROOF STEP]
apply (rule rHom_0_0, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rhom_to_rimg:"\<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow>
                                   f \<in> rHom A (rimg A R f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f \<in> rHom A (rimg A R 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> f \<in> rHom A (rimg A R f)
[PROOF STEP]
apply (subst rHom_def, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> f \<in> aHom A (rimg A R f) \<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>rimg A R f\<^esub> f y) \<and> f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>rimg A R f\<^esub>
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> f \<in> aHom A (rimg A R f)
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> (\<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>rimg A R f\<^esub> f y) \<and> f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>rimg A R f\<^esub>
[PROOF STEP]
apply (subst aHom_def, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> f \<in> carrier A \<rightarrow> carrier (rimg A R f) \<and> f \<in> extensional (carrier A) \<and> (\<forall>a\<in>carrier A. \<forall>b\<in>carrier A. f (a \<plusminus>\<^bsub>A\<^esub> b) = f a \<plusminus>\<^bsub>rimg A R f\<^esub> f b)
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> (\<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>rimg A R f\<^esub> f y) \<and> f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>rimg A R f\<^esub>
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> f \<in> carrier A \<rightarrow> carrier (rimg A R f)
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> f \<in> extensional (carrier A) \<and> (\<forall>a\<in>carrier A. \<forall>b\<in>carrier A. f (a \<plusminus>\<^bsub>A\<^esub> b) = f a \<plusminus>\<^bsub>rimg A R f\<^esub> f b)
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> (\<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>rimg A R f\<^esub> f y) \<and> f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>rimg A R f\<^esub>
[PROOF STEP]
apply (simp add:rimg_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> f \<in> extensional (carrier A) \<and> (\<forall>a\<in>carrier A. \<forall>b\<in>carrier A. f (a \<plusminus>\<^bsub>A\<^esub> b) = f a \<plusminus>\<^bsub>rimg A R f\<^esub> f b)
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> (\<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>rimg A R f\<^esub> f y) \<and> f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>rimg A R f\<^esub>
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> f \<in> extensional (carrier A)
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier A. \<forall>b\<in>carrier A. f (a \<plusminus>\<^bsub>A\<^esub> b) = f a \<plusminus>\<^bsub>rimg A R f\<^esub> f b
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> (\<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>rimg A R f\<^esub> f y) \<and> f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>rimg A R f\<^esub>
[PROOF STEP]
apply (simp add:rHom_def aHom_def)
[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>a\<in>carrier A. \<forall>b\<in>carrier A. f (a \<plusminus>\<^bsub>A\<^esub> b) = f a \<plusminus>\<^bsub>rimg A R f\<^esub> f b
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> (\<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>rimg A R f\<^esub> f y) \<and> f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>rimg A R f\<^esub>
[PROOF STEP]
apply ((rule ballI)+, simp add:rimg_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R; a \<in> carrier A; b \<in> carrier A\<rbrakk> \<Longrightarrow> f (a \<plusminus>\<^bsub>A\<^esub> b) = f a \<plusminus>\<^bsub>R\<^esub> f b
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> (\<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>rimg A R f\<^esub> f y) \<and> f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>rimg A R f\<^esub>
[PROOF STEP]
apply (rule aHom_add, assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R; a \<in> carrier A; b \<in> carrier A\<rbrakk> \<Longrightarrow> f \<in> aHom A R
 2. \<And>a b. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R; a \<in> carrier A; b \<in> carrier A\<rbrakk> \<Longrightarrow> a \<in> carrier A
 3. \<And>a b. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R; a \<in> carrier A; b \<in> carrier A\<rbrakk> \<Longrightarrow> b \<in> carrier A
 4. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> (\<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>rimg A R f\<^esub> f y) \<and> f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>rimg A R f\<^esub>
[PROOF STEP]
apply (simp add:rHom_aHom, assumption+)
[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>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> f y) \<and> f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>rimg A R f\<^esub>
[PROOF STEP]
apply (rule conjI)
[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>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> f y
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>rimg A R f\<^esub>
[PROOF STEP]
apply ((rule ballI)+, simp add:rimg_def, simp add:rHom_tOp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>rimg A R f\<^esub>
[PROOF STEP]
apply (simp add:rimg_def, simp add:rHom_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ker_to_rimg:"\<lbrakk>Ring A; Ring R; f \<in> rHom A R \<rbrakk> \<Longrightarrow>
                         ker\<^bsub>A,R\<^esub> f = ker\<^bsub>A,(rimg A R f)\<^esub> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> ker\<^bsub>A,R\<^esub> f = ker\<^bsub>A,rimg A R f\<^esub> f
[PROOF STEP]
apply (frule rhom_to_rimg [of "A" "R" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f \<in> rHom A (rimg A R f)\<rbrakk> \<Longrightarrow> ker\<^bsub>A,R\<^esub> f = ker\<^bsub>A,rimg A R f\<^esub> f
[PROOF STEP]
apply (simp add:ker_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f \<in> rHom A (rimg A R f)\<rbrakk> \<Longrightarrow> {a \<in> carrier A. f a = \<zero>\<^bsub>R\<^esub>} = {a \<in> carrier A. f a = \<zero>\<^bsub>rimg A R f\<^esub>}
[PROOF STEP]
apply (simp add:rimg_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma indhom_eq:"\<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,(rimg A R f)\<^esub> = f\<degree>\<^bsub>A,R\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>
[PROOF STEP]
apply (frule rimg_ring[of "A" "R" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; Ring (rimg A R f)\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>
[PROOF STEP]
apply (frule rhom_to_rimg[of "A" "R" "f"], assumption+,
       frule ind_hom_rhom[of "A" "rimg A R f"], assumption+,
       frule ind_hom_rhom[of "A" "R" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; Ring (rimg A R f); f \<in> rHom A (rimg A R f); f\<degree>\<^bsub>A,rimg A R f\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,rimg A R f\<^esub> f)) (rimg A R f); f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>
[PROOF STEP]
(** extensional **)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; Ring (rimg A R f); f \<in> rHom A (rimg A R f); f\<degree>\<^bsub>A,rimg A R f\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,rimg A R f\<^esub> f)) (rimg A R f); f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>
[PROOF STEP]
apply (rule funcset_eq[of "f\<degree>\<^bsub>A,rimg A R f\<^esub> " "carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))" "f\<degree>\<^bsub>A,R\<^esub>"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; Ring (rimg A R f); f \<in> rHom A (rimg A R f); f\<degree>\<^bsub>A,rimg A R f\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,rimg A R f\<^esub> f)) (rimg A R f); f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,rimg A R f\<^esub> \<in> extensional (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)))
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; Ring (rimg A R f); f \<in> rHom A (rimg A R f); f\<degree>\<^bsub>A,rimg A R f\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,rimg A R f\<^esub> f)) (rimg A R f); f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> extensional (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)))
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; Ring (rimg A R f); f \<in> rHom A (rimg A R f); f\<degree>\<^bsub>A,rimg A R f\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,rimg A R f\<^esub> f)) (rimg A R f); f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,rimg A R f\<^esub>) x = (f\<degree>\<^bsub>A,R\<^esub>) x
[PROOF STEP]
apply (simp add:ker_to_rimg[THEN sym],
        simp add:rHom_def[of _ "rimg A R f"] aHom_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; Ring (rimg A R f); f \<in> rHom A (rimg A R f); f\<degree>\<^bsub>A,rimg A R f\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,rimg A R f\<^esub> f)) (rimg A R f); f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> extensional (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)))
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; Ring (rimg A R f); f \<in> rHom A (rimg A R f); f\<degree>\<^bsub>A,rimg A R f\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,rimg A R f\<^esub> f)) (rimg A R f); f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,rimg A R f\<^esub>) x = (f\<degree>\<^bsub>A,R\<^esub>) x
[PROOF STEP]
apply (simp add:rHom_def[of _ "R"] aHom_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; Ring (rimg A R f); f \<in> rHom A (rimg A R f); f\<degree>\<^bsub>A,rimg A R f\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,rimg A R f\<^esub> f)) (rimg A R f); f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,rimg A R f\<^esub>) x = (f\<degree>\<^bsub>A,R\<^esub>) x
[PROOF STEP]
apply (simp add:ker_to_rimg[THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; Ring (rimg A R f); f \<in> rHom A (rimg A R f); f\<degree>\<^bsub>A,rimg A R f\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,rimg A R f\<^esub>) x = (f\<degree>\<^bsub>A,R\<^esub>) x
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; Ring (rimg A R f); f \<in> rHom A (rimg A R f); f\<degree>\<^bsub>A,rimg A R f\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; x \<in> carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,rimg A R f\<^esub>) x = (f\<degree>\<^bsub>A,R\<^esub>) x
[PROOF STEP]
apply (frule ker_ideal[of "A" "R" "f"], assumption+,
        simp add:Ring.carrier_qring1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; Ring (rimg A R f); f \<in> rHom A (rimg A R f); f\<degree>\<^bsub>A,rimg A R f\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; x \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f); ideal A (ker\<^bsub>A,R\<^esub> f)\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,rimg A R f\<^esub>) x = (f\<degree>\<^bsub>A,R\<^esub>) x
[PROOF STEP]
apply (simp add:set_ar_cos_def, erule bexE, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x a. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; Ring (rimg A R f); f \<in> rHom A (rimg A R f); f\<degree>\<^bsub>A,rimg A R f\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; ideal A (ker\<^bsub>A,R\<^esub> f); a \<in> carrier A; x = a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,rimg A R f\<^esub>) (a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) = (f\<degree>\<^bsub>A,R\<^esub>) (a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f)
[PROOF STEP]
apply (simp add:rind_hom_well_def[THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x a. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; Ring (rimg A R f); f \<in> rHom A (rimg A R f); f\<degree>\<^bsub>A,rimg A R f\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; ideal A (ker\<^bsub>A,R\<^esub> f); a \<in> carrier A; x = a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f\<rbrakk> \<Longrightarrow> (f\<degree>\<^bsub>A,rimg A R f\<^esub>) (a \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) = f a
[PROOF STEP]
apply (frule rind_hom_well_def[THEN sym, of "A" "rimg A R f" "f"],
         assumption+, simp add:ker_to_rimg[THEN sym])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done