[STATEMENT]
lemma indhom_bijec2_rimg:"\<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow>
                    bijec\<^bsub>(qring A (ker\<^bsub>A,R\<^esub> f)),(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> bijec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),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> bijec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),rimg A R f\<^esub> (f\<degree>\<^bsub>A,R\<^esub>)
[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; Ring (rimg A R f); f \<in> rHom A (rimg A R f)\<rbrakk> \<Longrightarrow> bijec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),rimg A R f\<^esub> (f\<degree>\<^bsub>A,R\<^esub>)
[PROOF STEP]
apply (frule ind_hom_rhom[of "A" "rimg A R f" "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)\<rbrakk> \<Longrightarrow> bijec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),rimg A R f\<^esub> (f\<degree>\<^bsub>A,R\<^esub>)
[PROOF STEP]
apply (frule ker_to_rimg[THEN sym, 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); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f\<rbrakk> \<Longrightarrow> bijec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),rimg A R f\<^esub> (f\<degree>\<^bsub>A,R\<^esub>)
[PROOF STEP]
apply (frule indhom_eq[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); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>\<rbrakk> \<Longrightarrow> bijec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),rimg A R f\<^esub> (f\<degree>\<^bsub>A,R\<^esub>)
[PROOF STEP]
apply simp
[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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>\<rbrakk> \<Longrightarrow> bijec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),rimg A R f\<^esub> (f\<degree>\<^bsub>A,R\<^esub>)
[PROOF STEP]
apply (simp add:bijec_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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>\<rbrakk> \<Longrightarrow> injec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),rimg A R f\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) \<and> surjec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),rimg A R f\<^esub> (f\<degree>\<^bsub>A,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; Ring (rimg A R f); f \<in> rHom A (rimg A R f); f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>\<rbrakk> \<Longrightarrow> injec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),rimg A R f\<^esub> (f\<degree>\<^bsub>A,R\<^esub>)
 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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>\<rbrakk> \<Longrightarrow> surjec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),rimg A R f\<^esub> (f\<degree>\<^bsub>A,R\<^esub>)
[PROOF STEP]
apply (simp add:injec_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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f) \<and> ker\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),rimg A R f\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) = {\<zero>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub>}
 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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>\<rbrakk> \<Longrightarrow> surjec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),rimg A R f\<^esub> (f\<degree>\<^bsub>A,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; Ring (rimg A R f); f \<in> rHom A (rimg A R f); f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R 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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>\<rbrakk> \<Longrightarrow> ker\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),rimg A R f\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) = {\<zero>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub>}
 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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>\<rbrakk> \<Longrightarrow> surjec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),rimg A R f\<^esub> (f\<degree>\<^bsub>A,R\<^esub>)
[PROOF STEP]
apply (simp add:rHom_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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>\<rbrakk> \<Longrightarrow> ker\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),rimg A R f\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) = {\<zero>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub>}
 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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>\<rbrakk> \<Longrightarrow> surjec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),rimg A R f\<^esub> (f\<degree>\<^bsub>A,R\<^esub>)
[PROOF STEP]
apply (frule ind_hom_injec [of "A" "R" "f"], assumption+)
[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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>; injec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>)\<rbrakk> \<Longrightarrow> ker\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),rimg A R f\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) = {\<zero>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub>}
 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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>\<rbrakk> \<Longrightarrow> surjec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),rimg A R f\<^esub> (f\<degree>\<^bsub>A,R\<^esub>)
[PROOF STEP]
apply (simp add:injec_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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>; 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>}\<rbrakk> \<Longrightarrow> ker\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),rimg A R f\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) = {\<zero>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub>}
 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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>\<rbrakk> \<Longrightarrow> surjec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),rimg A R f\<^esub> (f\<degree>\<^bsub>A,R\<^esub>)
[PROOF STEP]
apply (simp add:ker_def [of _ _ "f\<degree>\<^bsub>A,R\<^esub>"])
[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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>; f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R \<and> {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>}\<rbrakk> \<Longrightarrow> {a \<in> carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) a = \<zero>\<^bsub>rimg A R f\<^esub>} = {\<zero>\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)\<^esub>}
 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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>\<rbrakk> \<Longrightarrow> surjec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),rimg A R f\<^esub> (f\<degree>\<^bsub>A,R\<^esub>)
[PROOF STEP]
apply (simp add:rimg_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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>\<rbrakk> \<Longrightarrow> surjec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),rimg A R f\<^esub> (f\<degree>\<^bsub>A,R\<^esub>)
[PROOF STEP]
apply (simp add:surjec_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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f) \<and> surj_to (f\<degree>\<^bsub>A,R\<^esub>) (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))) (carrier (rimg A R f))
[PROOF STEP]
apply (rule conjI)
[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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> aHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R 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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>\<rbrakk> \<Longrightarrow> surj_to (f\<degree>\<^bsub>A,R\<^esub>) (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))) (carrier (rimg A R f))
[PROOF STEP]
apply (simp add:rHom_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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>\<rbrakk> \<Longrightarrow> surj_to (f\<degree>\<^bsub>A,R\<^esub>) (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))) (carrier (rimg A R f))
[PROOF STEP]
apply (rule surj_to_test)
[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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>\<rbrakk> \<Longrightarrow> f\<degree>\<^bsub>A,R\<^esub> \<in> carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) \<rightarrow> carrier (rimg A R 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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>\<rbrakk> \<Longrightarrow> \<forall>b\<in>carrier (rimg A R f). \<exists>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) a = b
[PROOF STEP]
apply (simp add:rHom_def 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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>\<rbrakk> \<Longrightarrow> \<forall>b\<in>carrier (rimg A R f). \<exists>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) a = b
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>; b \<in> carrier (rimg A R f)\<rbrakk> \<Longrightarrow> \<exists>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) a = b
[PROOF STEP]
apply (simp add:rimg_carrier)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>; b \<in> f ` carrier A\<rbrakk> \<Longrightarrow> \<exists>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) a = b
[PROOF STEP]
apply (simp add:image_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>; \<exists>x\<in>carrier A. b = f x\<rbrakk> \<Longrightarrow> \<exists>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) a = b
[PROOF STEP]
apply (erule bexE, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b 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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>; x \<in> carrier A; b = f x\<rbrakk> \<Longrightarrow> \<exists>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) a = f x
[PROOF STEP]
apply (frule_tac a1 = x in rind_hom_well_def[THEN sym, of "A" "R" "f"],
                   assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b 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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>; x \<in> carrier A; b = f x; (f\<degree>\<^bsub>A,R\<^esub>) (x \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) = f x\<rbrakk> \<Longrightarrow> \<exists>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) a = f x
[PROOF STEP]
apply (frule ker_ideal[of "A" "R" "f"], assumption+,
        simp add:Ring.carrier_qring1,
        frule_tac a = x in Ring.mem_set_ar_cos[of "A" "ker\<^bsub>A,R\<^esub> f"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b 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,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) (rimg A R f); ker\<^bsub>A,rimg A R f\<^esub> f = ker\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,rimg A R f\<^esub> = f\<degree>\<^bsub>A,R\<^esub>; x \<in> carrier A; b = f x; (f\<degree>\<^bsub>A,R\<^esub>) (x \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) = f x; ideal A (ker\<^bsub>A,R\<^esub> f); x \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f)\<rbrakk> \<Longrightarrow> \<exists>a\<in>set_ar_cos A (ker\<^bsub>A,R\<^esub> f). (f\<degree>\<^bsub>A,R\<^esub>) a = f x
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma surjec_ind_bijec:"\<lbrakk>Ring A; Ring R; f \<in> rHom A R; surjec\<^bsub>A,R\<^esub> f\<rbrakk> \<Longrightarrow>
     bijec\<^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; surjec\<^bsub>A,R\<^esub> f\<rbrakk> \<Longrightarrow> bijec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),R\<^esub> (f\<degree>\<^bsub>A,R\<^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; surjec\<^bsub>A,R\<^esub> f; f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R\<rbrakk> \<Longrightarrow> bijec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>)
[PROOF STEP]
apply (simp add:surjec_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f \<in> aHom A R \<and> surj_to f (carrier A) (carrier R); f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R\<rbrakk> \<Longrightarrow> bijec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>)
[PROOF STEP]
apply (simp add:bijec_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f \<in> aHom A R \<and> surj_to f (carrier A) (carrier R); f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R\<rbrakk> \<Longrightarrow> injec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>) \<and> surjec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>)
[PROOF STEP]
apply (simp add:ind_hom_injec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f \<in> aHom A R \<and> surj_to f (carrier A) (carrier R); f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R\<rbrakk> \<Longrightarrow> surjec\<^bsub>A /\<^sub>r (ker\<^bsub>A,R\<^esub> f),R\<^esub> (f\<degree>\<^bsub>A,R\<^esub>)
[PROOF STEP]
apply (simp add:surjec_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; f \<in> aHom A R \<and> surj_to f (carrier A) (carrier 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> surj_to (f\<degree>\<^bsub>A,R\<^esub>) (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))) (carrier R)
[PROOF STEP]
apply (simp add:rHom_aHom)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; surj_to f (carrier A) (carrier R); f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R\<rbrakk> \<Longrightarrow> surj_to (f\<degree>\<^bsub>A,R\<^esub>) (carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f))) (carrier R)
[PROOF STEP]
apply (rule surj_to_test)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; surj_to f (carrier A) (carrier 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> carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) \<rightarrow> carrier R
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; surj_to f (carrier A) (carrier R); f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R\<rbrakk> \<Longrightarrow> \<forall>b\<in>carrier R. \<exists>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) a = b
[PROOF STEP]
apply (simp add:rHom_def aHom_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; surj_to f (carrier A) (carrier R); f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R\<rbrakk> \<Longrightarrow> \<forall>b\<in>carrier R. \<exists>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) a = b
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; surj_to f (carrier A) (carrier R); f\<degree>\<^bsub>A,R\<^esub> \<in> rHom (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)) R; b \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) a = b
[PROOF STEP]
apply (simp add:surj_to_def, frule sym,
                        thin_tac "f ` carrier A = carrier R", simp,
                        thin_tac "carrier R = f ` carrier A")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<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; b \<in> f ` carrier A\<rbrakk> \<Longrightarrow> \<exists>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) a = b
[PROOF STEP]
apply (simp add:image_def, erule bexE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b 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; x \<in> carrier A; b = f x\<rbrakk> \<Longrightarrow> \<exists>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) a = b
[PROOF STEP]
apply (frule_tac a1 = x in rind_hom_well_def[THEN sym, of "A" "R" "f"],
                   assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b 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; x \<in> carrier A; b = f x; (f\<degree>\<^bsub>A,R\<^esub>) (x \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) = f x\<rbrakk> \<Longrightarrow> \<exists>a\<in>carrier (A /\<^sub>r (ker\<^bsub>A,R\<^esub> f)). (f\<degree>\<^bsub>A,R\<^esub>) a = b
[PROOF STEP]
apply (frule ker_ideal[of "A" "R" "f"], assumption+,
        simp add:Ring.carrier_qring1,
        frule_tac a = x in Ring.mem_set_ar_cos[of "A" "ker\<^bsub>A,R\<^esub> f"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b 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; x \<in> carrier A; b = f x; (f\<degree>\<^bsub>A,R\<^esub>) (x \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f) = f x; ideal A (ker\<^bsub>A,R\<^esub> f); x \<uplus>\<^bsub>A\<^esub> ker\<^bsub>A,R\<^esub> f \<in> set_ar_cos A (ker\<^bsub>A,R\<^esub> f)\<rbrakk> \<Longrightarrow> \<exists>a\<in>set_ar_cos A (ker\<^bsub>A,R\<^esub> f). (f\<degree>\<^bsub>A,R\<^esub>) a = f x
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ridmap_ind_bijec:"Ring A \<Longrightarrow>
     bijec\<^bsub>(qring A (ker\<^bsub>A,A\<^esub> (ridmap A))),A\<^esub> ((ridmap A)\<degree>\<^bsub>A,A\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ring A \<Longrightarrow> bijec\<^bsub>A /\<^sub>r (ker\<^bsub>A,A\<^esub> ridmap A),A\<^esub> (ridmap A\<degree>\<^bsub>A,A\<^esub>)
[PROOF STEP]
apply (frule ridmap_surjec[of "A"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; surjec\<^bsub>A,A\<^esub> ridmap A\<rbrakk> \<Longrightarrow> bijec\<^bsub>A /\<^sub>r (ker\<^bsub>A,A\<^esub> ridmap A),A\<^esub> (ridmap A\<degree>\<^bsub>A,A\<^esub>)
[PROOF STEP]
apply (rule surjec_ind_bijec [of "A" "A" "ridmap A"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; surjec\<^bsub>A,A\<^esub> ridmap A\<rbrakk> \<Longrightarrow> ridmap A \<in> rHom A A
 2. \<lbrakk>Ring A; surjec\<^bsub>A,A\<^esub> ridmap A\<rbrakk> \<Longrightarrow> surjec\<^bsub>A,A\<^esub> ridmap A
[PROOF STEP]
apply (simp add:rHom_def, simp add:surjec_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; ridmap A \<in> aHom A A \<and> surj_to (ridmap A) (carrier A) (carrier A)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier A. \<forall>y\<in>carrier A. ridmap A (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = ridmap A x \<cdot>\<^sub>r\<^bsub>A\<^esub> ridmap A y) \<and> ridmap A 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>A\<^esub>
 2. \<lbrakk>Ring A; surjec\<^bsub>A,A\<^esub> ridmap A\<rbrakk> \<Longrightarrow> surjec\<^bsub>A,A\<^esub> ridmap A
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring A; ridmap A \<in> aHom A A \<and> surj_to (ridmap A) (carrier A) (carrier A)\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. ridmap A (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = ridmap A x \<cdot>\<^sub>r\<^bsub>A\<^esub> ridmap A y
 2. \<lbrakk>Ring A; ridmap A \<in> aHom A A \<and> surj_to (ridmap A) (carrier A) (carrier A)\<rbrakk> \<Longrightarrow> ridmap A 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>A\<^esub>
 3. \<lbrakk>Ring A; surjec\<^bsub>A,A\<^esub> ridmap A\<rbrakk> \<Longrightarrow> surjec\<^bsub>A,A\<^esub> ridmap A
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>Ring A; ridmap A \<in> aHom A A \<and> surj_to (ridmap A) (carrier A) (carrier A); x \<in> carrier A; y \<in> carrier A\<rbrakk> \<Longrightarrow> ridmap A (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = ridmap A x \<cdot>\<^sub>r\<^bsub>A\<^esub> ridmap A y
 2. \<lbrakk>Ring A; ridmap A \<in> aHom A A \<and> surj_to (ridmap A) (carrier A) (carrier A)\<rbrakk> \<Longrightarrow> ridmap A 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>A\<^esub>
 3. \<lbrakk>Ring A; surjec\<^bsub>A,A\<^esub> ridmap A\<rbrakk> \<Longrightarrow> surjec\<^bsub>A,A\<^esub> ridmap A
[PROOF STEP]
apply (frule_tac x = x and y = y in Ring.ring_tOp_closed[of "A"],
          assumption+, simp add:ridmap_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; ridmap A \<in> aHom A A \<and> surj_to (ridmap A) (carrier A) (carrier A)\<rbrakk> \<Longrightarrow> ridmap A 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>A\<^esub>
 2. \<lbrakk>Ring A; surjec\<^bsub>A,A\<^esub> ridmap A\<rbrakk> \<Longrightarrow> surjec\<^bsub>A,A\<^esub> ridmap A
[PROOF STEP]
apply (simp add:ridmap_def Ring.ring_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; surjec\<^bsub>A,A\<^esub> ridmap A\<rbrakk> \<Longrightarrow> surjec\<^bsub>A,A\<^esub> ridmap A
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ker_of_idmap:"Ring A \<Longrightarrow> ker\<^bsub>A,A\<^esub> (ridmap A) = {\<zero>\<^bsub>A\<^esub>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ring A \<Longrightarrow> ker\<^bsub>A,A\<^esub> ridmap A = {\<zero>\<^bsub>A\<^esub>}
[PROOF STEP]
apply (simp add:ker_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ring A \<Longrightarrow> {a \<in> carrier A. ridmap A a = \<zero>\<^bsub>A\<^esub>} = {\<zero>\<^bsub>A\<^esub>}
[PROOF STEP]
apply (simp add:ridmap_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ring A \<Longrightarrow> {a. (a \<in> carrier A \<longrightarrow> a = \<zero>\<^bsub>A\<^esub>) \<and> a \<in> carrier A} = {\<zero>\<^bsub>A\<^esub>}
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Ring A \<Longrightarrow> {a. (a \<in> carrier A \<longrightarrow> a = \<zero>\<^bsub>A\<^esub>) \<and> a \<in> carrier A} \<subseteq> {\<zero>\<^bsub>A\<^esub>}
 2. Ring A \<Longrightarrow> {\<zero>\<^bsub>A\<^esub>} \<subseteq> {a. (a \<in> carrier A \<longrightarrow> a = \<zero>\<^bsub>A\<^esub>) \<and> a \<in> carrier A}
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>Ring A; x \<in> {a. (a \<in> carrier A \<longrightarrow> a = \<zero>\<^bsub>A\<^esub>) \<and> a \<in> carrier A}\<rbrakk> \<Longrightarrow> x \<in> {\<zero>\<^bsub>A\<^esub>}
 2. Ring A \<Longrightarrow> {\<zero>\<^bsub>A\<^esub>} \<subseteq> {a. (a \<in> carrier A \<longrightarrow> a = \<zero>\<^bsub>A\<^esub>) \<and> a \<in> carrier A}
[PROOF STEP]
apply (simp add:CollectI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ring A \<Longrightarrow> {\<zero>\<^bsub>A\<^esub>} \<subseteq> {a. (a \<in> carrier A \<longrightarrow> a = \<zero>\<^bsub>A\<^esub>) \<and> a \<in> carrier A}
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ring A; x \<in> {\<zero>\<^bsub>A\<^esub>}\<rbrakk> \<Longrightarrow> x \<in> {a. (a \<in> carrier A \<longrightarrow> a = \<zero>\<^bsub>A\<^esub>) \<and> a \<in> carrier A}
[PROOF STEP]
apply (simp add:CollectI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Ring A; x = \<zero>\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>A\<^esub> \<in> carrier A
[PROOF STEP]
apply (simp add:Ring.ring_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ring_natural_isom:"Ring A \<Longrightarrow>
         bijec\<^bsub>(qring A {\<zero>\<^bsub>A\<^esub>}),A\<^esub> ((ridmap A)\<degree>\<^bsub>A,A\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ring A \<Longrightarrow> bijec\<^bsub>A /\<^sub>r {\<zero>\<^bsub>A\<^esub>},A\<^esub> (ridmap A\<degree>\<^bsub>A,A\<^esub>)
[PROOF STEP]
apply (frule ridmap_ind_bijec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; bijec\<^bsub>A /\<^sub>r (ker\<^bsub>A,A\<^esub> ridmap A),A\<^esub> (ridmap A\<degree>\<^bsub>A,A\<^esub>)\<rbrakk> \<Longrightarrow> bijec\<^bsub>A /\<^sub>r {\<zero>\<^bsub>A\<^esub>},A\<^esub> (ridmap A\<degree>\<^bsub>A,A\<^esub>)
[PROOF STEP]
apply (simp add: ker_of_idmap)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pj_Hom:"\<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (pj R I) \<in> rHom R (qring R I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I \<in> rHom R (R /\<^sub>r I)
[PROOF STEP]
apply (simp add:rHom_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I \<in> aHom R (R /\<^sub>r I) \<and> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I \<in> aHom R (R /\<^sub>r I)
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (simp add:aHom_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I \<in> carrier R \<rightarrow> carrier (R /\<^sub>r I) \<and> pj R I \<in> extensional (carrier R) \<and> (\<forall>a\<in>carrier R. \<forall>b\<in>carrier R. pj R I (a \<plusminus>\<^bsub>R\<^esub> b) = pj R I a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> pj R I b)
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I \<in> carrier R \<rightarrow> carrier (R /\<^sub>r I)
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I \<in> extensional (carrier R) \<and> (\<forall>a\<in>carrier R. \<forall>b\<in>carrier R. pj R I (a \<plusminus>\<^bsub>R\<^esub> b) = pj R I a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> pj R I b)
 3. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (rule Pi_I)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>Ring R; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> pj R I x \<in> carrier (R /\<^sub>r I)
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I \<in> extensional (carrier R) \<and> (\<forall>a\<in>carrier R. \<forall>b\<in>carrier R. pj R I (a \<plusminus>\<^bsub>R\<^esub> b) = pj R I a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> pj R I b)
 3. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (simp add:qring_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>Ring R; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> pj R I x \<in> set_rcs (b_ag R) I
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I \<in> extensional (carrier R) \<and> (\<forall>a\<in>carrier R. \<forall>b\<in>carrier R. pj R I (a \<plusminus>\<^bsub>R\<^esub> b) = pj R I a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> pj R I b)
 3. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (frule Ring.ring_is_ag)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>Ring R; ideal R I; x \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> pj R I x \<in> set_rcs (b_ag R) I
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I \<in> extensional (carrier R) \<and> (\<forall>a\<in>carrier R. \<forall>b\<in>carrier R. pj R I (a \<plusminus>\<^bsub>R\<^esub> b) = pj R I a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> pj R I b)
 3. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (simp add:aGroup.ag_carrier_carrier [THEN sym])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>Ring R; ideal R I; x \<in> carrier (b_ag R); aGroup R\<rbrakk> \<Longrightarrow> pj R I x \<in> set_rcs (b_ag R) I
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I \<in> extensional (carrier R) \<and> (\<forall>a\<in>carrier R. \<forall>b\<in>carrier R. pj R I (a \<plusminus>\<^bsub>R\<^esub> b) = pj R I a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> pj R I b)
 3. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (simp add:pj_def Pj_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>Ring R; ideal R I; x \<in> carrier (b_ag R); aGroup R\<rbrakk> \<Longrightarrow> I \<bullet>\<^bsub>b_ag R\<^esub> x \<in> set_rcs (b_ag R) I
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I \<in> extensional (carrier R) \<and> (\<forall>a\<in>carrier R. \<forall>b\<in>carrier R. pj R I (a \<plusminus>\<^bsub>R\<^esub> b) = pj R I a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> pj R I b)
 3. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (simp add:set_rcs_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>Ring R; ideal R I; x \<in> carrier (b_ag R); aGroup R\<rbrakk> \<Longrightarrow> \<exists>a\<in>carrier (b_ag R). I \<bullet>\<^bsub>b_ag R\<^esub> x = I \<bullet>\<^bsub>b_ag R\<^esub> a
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I \<in> extensional (carrier R) \<and> (\<forall>a\<in>carrier R. \<forall>b\<in>carrier R. pj R I (a \<plusminus>\<^bsub>R\<^esub> b) = pj R I a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> pj R I b)
 3. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I \<in> extensional (carrier R) \<and> (\<forall>a\<in>carrier R. \<forall>b\<in>carrier R. pj R I (a \<plusminus>\<^bsub>R\<^esub> b) = pj R I a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> pj R I b)
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I \<in> extensional (carrier R)
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier R. \<forall>b\<in>carrier R. pj R I (a \<plusminus>\<^bsub>R\<^esub> b) = pj R I a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> pj R I b
 3. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (simp add:pj_def Pj_def extensional_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> \<forall>x. x \<in> carrier (b_ag R) \<longrightarrow> x \<notin> carrier R \<longrightarrow> I \<bullet>\<^bsub>b_ag R\<^esub> x = undefined
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier R. \<forall>b\<in>carrier R. pj R I (a \<plusminus>\<^bsub>R\<^esub> b) = pj R I a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> pj R I b
 3. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (frule Ring.ring_is_ag)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring R; ideal R I; aGroup R\<rbrakk> \<Longrightarrow> \<forall>x. x \<in> carrier (b_ag R) \<longrightarrow> x \<notin> carrier R \<longrightarrow> I \<bullet>\<^bsub>b_ag R\<^esub> x = undefined
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier R. \<forall>b\<in>carrier R. pj R I (a \<plusminus>\<^bsub>R\<^esub> b) = pj R I a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> pj R I b
 3. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (simp add:aGroup.ag_carrier_carrier)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier R. \<forall>b\<in>carrier R. pj R I (a \<plusminus>\<^bsub>R\<^esub> b) = pj R I a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> pj R I b
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>Ring R; ideal R I; a \<in> carrier R; b \<in> carrier R\<rbrakk> \<Longrightarrow> pj R I (a \<plusminus>\<^bsub>R\<^esub> b) = pj R I a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> pj R I b
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (frule Ring.ring_is_ag)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>Ring R; ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> pj R I (a \<plusminus>\<^bsub>R\<^esub> b) = pj R I a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> pj R I b
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (frule_tac x = a and y = b in aGroup.ag_pOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>Ring R; ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<plusminus>\<^bsub>R\<^esub> b \<in> carrier R\<rbrakk> \<Longrightarrow> pj R I (a \<plusminus>\<^bsub>R\<^esub> b) = pj R I a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> pj R I b
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (simp add:aGroup.ag_carrier_carrier [THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>Ring R; ideal R I; a \<in> carrier (b_ag R); b \<in> carrier (b_ag R); aGroup R; a \<plusminus>\<^bsub>R\<^esub> b \<in> carrier (b_ag R)\<rbrakk> \<Longrightarrow> pj R I (a \<plusminus>\<^bsub>R\<^esub> b) = pj R I a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> pj R I b
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (simp add:pj_def Pj_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>Ring R; ideal R I; a \<in> carrier (b_ag R); b \<in> carrier (b_ag R); aGroup R; a \<plusminus>\<^bsub>R\<^esub> b \<in> carrier (b_ag R)\<rbrakk> \<Longrightarrow> I \<bullet>\<^bsub>b_ag R\<^esub> (a \<plusminus>\<^bsub>R\<^esub> b) = I \<bullet>\<^bsub>b_ag R\<^esub> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> I \<bullet>\<^bsub>b_ag R\<^esub> b
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (simp add:qring_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>Ring R; ideal R I; a \<in> carrier (b_ag R); b \<in> carrier (b_ag R); aGroup R; a \<plusminus>\<^bsub>R\<^esub> b \<in> carrier (b_ag R)\<rbrakk> \<Longrightarrow> I \<bullet>\<^bsub>b_ag R\<^esub> (a \<plusminus>\<^bsub>R\<^esub> b) = c_top (b_ag R) I (I \<bullet>\<^bsub>b_ag R\<^esub> a) (I \<bullet>\<^bsub>b_ag R\<^esub> b)
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (frule aGroup.b_ag_group)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>Ring R; ideal R I; a \<in> carrier (b_ag R); b \<in> carrier (b_ag R); aGroup R; a \<plusminus>\<^bsub>R\<^esub> b \<in> carrier (b_ag R); Group (b_ag R)\<rbrakk> \<Longrightarrow> I \<bullet>\<^bsub>b_ag R\<^esub> (a \<plusminus>\<^bsub>R\<^esub> b) = c_top (b_ag R) I (I \<bullet>\<^bsub>b_ag R\<^esub> a) (I \<bullet>\<^bsub>b_ag R\<^esub> b)
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (simp add:aGroup.agop_gop [THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>Ring R; ideal R I; a \<in> carrier (b_ag R); b \<in> carrier (b_ag R); aGroup R; a \<cdot>\<^bsub>b_ag R\<^esub> b \<in> carrier (b_ag R); Group (b_ag R)\<rbrakk> \<Longrightarrow> I \<bullet>\<^bsub>b_ag R\<^esub> (a \<cdot>\<^bsub>b_ag R\<^esub> b) = c_top (b_ag R) I (I \<bullet>\<^bsub>b_ag R\<^esub> a) (I \<bullet>\<^bsub>b_ag R\<^esub> b)
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (subst Group.c_top_welldef[of "b_ag R" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>Ring R; ideal R I; a \<in> carrier (b_ag R); b \<in> carrier (b_ag R); aGroup R; a \<cdot>\<^bsub>b_ag R\<^esub> b \<in> carrier (b_ag R); Group (b_ag R)\<rbrakk> \<Longrightarrow> b_ag R \<triangleright> I
 2. \<And>a b. \<lbrakk>Ring R; ideal R I; a \<in> carrier (b_ag R); b \<in> carrier (b_ag R); aGroup R; a \<cdot>\<^bsub>b_ag R\<^esub> b \<in> carrier (b_ag R); Group (b_ag R)\<rbrakk> \<Longrightarrow> a \<in> carrier (b_ag R)
 3. \<And>a b. \<lbrakk>Ring R; ideal R I; a \<in> carrier (b_ag R); b \<in> carrier (b_ag R); aGroup R; a \<cdot>\<^bsub>b_ag R\<^esub> b \<in> carrier (b_ag R); Group (b_ag R)\<rbrakk> \<Longrightarrow> b \<in> carrier (b_ag R)
 4. \<And>a b. \<lbrakk>Ring R; ideal R I; a \<in> carrier (b_ag R); b \<in> carrier (b_ag R); aGroup R; a \<cdot>\<^bsub>b_ag R\<^esub> b \<in> carrier (b_ag R); Group (b_ag R)\<rbrakk> \<Longrightarrow> c_top (b_ag R) I (I \<bullet>\<^bsub>b_ag R\<^esub> a) (I \<bullet>\<^bsub>b_ag R\<^esub> b) = c_top (b_ag R) I (I \<bullet>\<^bsub>b_ag R\<^esub> a) (I \<bullet>\<^bsub>b_ag R\<^esub> b)
 5. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (frule Ring.ideal_asubg[of "R" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>Ring R; ideal R I; a \<in> carrier (b_ag R); b \<in> carrier (b_ag R); aGroup R; a \<cdot>\<^bsub>b_ag R\<^esub> b \<in> carrier (b_ag R); Group (b_ag R); R +> I\<rbrakk> \<Longrightarrow> b_ag R \<triangleright> I
 2. \<And>a b. \<lbrakk>Ring R; ideal R I; a \<in> carrier (b_ag R); b \<in> carrier (b_ag R); aGroup R; a \<cdot>\<^bsub>b_ag R\<^esub> b \<in> carrier (b_ag R); Group (b_ag R)\<rbrakk> \<Longrightarrow> a \<in> carrier (b_ag R)
 3. \<And>a b. \<lbrakk>Ring R; ideal R I; a \<in> carrier (b_ag R); b \<in> carrier (b_ag R); aGroup R; a \<cdot>\<^bsub>b_ag R\<^esub> b \<in> carrier (b_ag R); Group (b_ag R)\<rbrakk> \<Longrightarrow> b \<in> carrier (b_ag R)
 4. \<And>a b. \<lbrakk>Ring R; ideal R I; a \<in> carrier (b_ag R); b \<in> carrier (b_ag R); aGroup R; a \<cdot>\<^bsub>b_ag R\<^esub> b \<in> carrier (b_ag R); Group (b_ag R)\<rbrakk> \<Longrightarrow> c_top (b_ag R) I (I \<bullet>\<^bsub>b_ag R\<^esub> a) (I \<bullet>\<^bsub>b_ag R\<^esub> b) = c_top (b_ag R) I (I \<bullet>\<^bsub>b_ag R\<^esub> a) (I \<bullet>\<^bsub>b_ag R\<^esub> b)
 5. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (simp add:aGroup.asubg_nsubg)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>Ring R; ideal R I; a \<in> carrier (b_ag R); b \<in> carrier (b_ag R); aGroup R; a \<cdot>\<^bsub>b_ag R\<^esub> b \<in> carrier (b_ag R); Group (b_ag R)\<rbrakk> \<Longrightarrow> a \<in> carrier (b_ag R)
 2. \<And>a b. \<lbrakk>Ring R; ideal R I; a \<in> carrier (b_ag R); b \<in> carrier (b_ag R); aGroup R; a \<cdot>\<^bsub>b_ag R\<^esub> b \<in> carrier (b_ag R); Group (b_ag R)\<rbrakk> \<Longrightarrow> b \<in> carrier (b_ag R)
 3. \<And>a b. \<lbrakk>Ring R; ideal R I; a \<in> carrier (b_ag R); b \<in> carrier (b_ag R); aGroup R; a \<cdot>\<^bsub>b_ag R\<^esub> b \<in> carrier (b_ag R); Group (b_ag R)\<rbrakk> \<Longrightarrow> c_top (b_ag R) I (I \<bullet>\<^bsub>b_ag R\<^esub> a) (I \<bullet>\<^bsub>b_ag R\<^esub> b) = c_top (b_ag R) I (I \<bullet>\<^bsub>b_ag R\<^esub> a) (I \<bullet>\<^bsub>b_ag R\<^esub> b)
 4. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply assumption+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>Ring R; ideal R I; a \<in> carrier (b_ag R); b \<in> carrier (b_ag R); aGroup R; a \<cdot>\<^bsub>b_ag R\<^esub> b \<in> carrier (b_ag R); Group (b_ag R)\<rbrakk> \<Longrightarrow> c_top (b_ag R) I (I \<bullet>\<^bsub>b_ag R\<^esub> a) (I \<bullet>\<^bsub>b_ag R\<^esub> b) = c_top (b_ag R) I (I \<bullet>\<^bsub>b_ag R\<^esub> a) (I \<bullet>\<^bsub>b_ag R\<^esub> b)
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y) \<and> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = pj R I x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> pj R I y
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (simp add: qring_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = rcostOp R I (pj R I x) (pj R I y)
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (frule_tac x = x and y = y in Ring.ring_tOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r\<^bsub>R\<^esub> y \<in> carrier R\<rbrakk> \<Longrightarrow> pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = rcostOp R I (pj R I x) (pj R I y)
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (frule Ring.ring_is_ag)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r\<^bsub>R\<^esub> y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = rcostOp R I (pj R I x) (pj R I y)
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (simp add:aGroup.ag_carrier_carrier [THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; x \<in> carrier (b_ag R); y \<in> carrier (b_ag R); x \<cdot>\<^sub>r\<^bsub>R\<^esub> y \<in> carrier (b_ag R); aGroup R\<rbrakk> \<Longrightarrow> pj R I (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = rcostOp R I (pj R I x) (pj R I y)
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (simp add:pj_def Pj_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; x \<in> carrier (b_ag R); y \<in> carrier (b_ag R); x \<cdot>\<^sub>r\<^bsub>R\<^esub> y \<in> carrier (b_ag R); aGroup R\<rbrakk> \<Longrightarrow> I \<bullet>\<^bsub>b_ag R\<^esub> (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = rcostOp R I (I \<bullet>\<^bsub>b_ag R\<^esub> x) (I \<bullet>\<^bsub>b_ag R\<^esub> y)
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (simp add:aGroup.ag_carrier_carrier)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r\<^bsub>R\<^esub> y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> I \<bullet>\<^bsub>b_ag R\<^esub> (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = rcostOp R I (I \<bullet>\<^bsub>b_ag R\<^esub> x) (I \<bullet>\<^bsub>b_ag R\<^esub> y)
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (frule_tac a1 = x and b1 = y in Ring.rcostOp [THEN sym, of "R" "I"],
                                                             assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring R; ideal R I; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r\<^bsub>R\<^esub> y \<in> carrier R; aGroup R; x \<cdot>\<^sub>r\<^bsub>R\<^esub> y \<uplus>\<^bsub>R\<^esub> I = rcostOp R I (x \<uplus>\<^bsub>R\<^esub> I) (y \<uplus>\<^bsub>R\<^esub> I)\<rbrakk> \<Longrightarrow> I \<bullet>\<^bsub>b_ag R\<^esub> (x \<cdot>\<^sub>r\<^bsub>R\<^esub> y) = rcostOp R I (I \<bullet>\<^bsub>b_ag R\<^esub> x) (I \<bullet>\<^bsub>b_ag R\<^esub> y)
 2. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (simp add:ar_coset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (simp add:qring_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring R; ideal R I\<rbrakk> \<Longrightarrow> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R\<^esub> \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (frule Ring.ring_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring R; ideal R I; 1\<^sub>r\<^bsub>R\<^esub> \<in> carrier R\<rbrakk> \<Longrightarrow> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R\<^esub> \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (frule Ring.ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring R; ideal R I; 1\<^sub>r\<^bsub>R\<^esub> \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R\<^esub> \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (simp add:aGroup.ag_carrier_carrier [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring R; ideal R I; 1\<^sub>r\<^bsub>R\<^esub> \<in> carrier (b_ag R); aGroup R\<rbrakk> \<Longrightarrow> pj R I 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R\<^esub> \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (simp add:pj_def Pj_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring R; ideal R I; 1\<^sub>r\<^bsub>R\<^esub> \<in> carrier (b_ag R); aGroup R\<rbrakk> \<Longrightarrow> I \<bullet>\<^bsub>b_ag R\<^esub> 1\<^sub>r\<^bsub>R\<^esub> = 1\<^sub>r\<^bsub>R\<^esub> \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (simp add:ar_coset_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pj_mem:"\<lbrakk>Ring R; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> pj R I x = x \<uplus>\<^bsub>R\<^esub> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring R; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> pj R I x = x \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (frule Ring.ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring R; ideal R I; x \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> pj R I x = x \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (simp add:aGroup.ag_carrier_carrier [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring R; ideal R I; x \<in> carrier (b_ag R); aGroup R\<rbrakk> \<Longrightarrow> pj R I x = x \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (simp add:pj_def Pj_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring R; ideal R I; x \<in> carrier (b_ag R); aGroup R\<rbrakk> \<Longrightarrow> I \<bullet>\<^bsub>b_ag R\<^esub> x = x \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (simp add:ar_coset_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pj_zero:"\<lbrakk>Ring R; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow>
                         (pj R I x = \<zero>\<^bsub>(R /\<^sub>r I)\<^esub>) = (x \<in> I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring R; ideal R I; x \<in> carrier R\<rbrakk> \<Longrightarrow> (pj R I x = \<zero>\<^bsub>R /\<^sub>r I\<^esub>) = (x \<in> I)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring R; ideal R I; x \<in> carrier R; pj R I x = \<zero>\<^bsub>R /\<^sub>r I\<^esub>\<rbrakk> \<Longrightarrow> x \<in> I
 2. \<lbrakk>Ring R; ideal R I; x \<in> carrier R; x \<in> I\<rbrakk> \<Longrightarrow> pj R I x = \<zero>\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (simp add:pj_mem Ring.qring_zero,
       simp add:Ring.qring_zero_1[of "R" "x" "I"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring R; ideal R I; x \<in> carrier R; x \<in> I\<rbrakk> \<Longrightarrow> pj R I x = \<zero>\<^bsub>R /\<^sub>r I\<^esub>
[PROOF STEP]
apply (simp add:pj_mem Ring.qring_zero,
       rule Ring.Qring_fix1, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pj_surj_to:"\<lbrakk>Ring R; ideal R J; X \<in> carrier (R /\<^sub>r J)\<rbrakk> \<Longrightarrow>
                   \<exists>r\<in> carrier R. pj R J r = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring R; ideal R J; X \<in> carrier (R /\<^sub>r J)\<rbrakk> \<Longrightarrow> \<exists>r\<in>carrier R. pj R J r = X
[PROOF STEP]
apply (simp add:qring_def set_rcs_def,
       fold ar_coset_def, simp add:b_ag_def, erule bexE,
       frule_tac x = a in pj_mem[of R J], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>Ring R; ideal R J; a \<in> carrier R; X = a \<uplus>\<^bsub>R\<^esub> J; pj R J a = a \<uplus>\<^bsub>R\<^esub> J\<rbrakk> \<Longrightarrow> \<exists>r\<in>carrier R. pj R J r = a \<uplus>\<^bsub>R\<^esub> J
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done