[STATEMENT]
lemma (in Ring) ar_cos_mem:"\<lbrakk>ideal R I; a \<in> carrier R\<rbrakk> \<Longrightarrow>
                                 a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag 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> set_rcs (b_ag R) I
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I
[PROOF STEP]
apply (simp add:set_rcs_def ar_coset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> \<exists>aa\<in>carrier (b_ag R). I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> aa
[PROOF STEP]
apply (frule aGroup.ag_carrier_carrier[THEN sym, of "R"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; aGroup R; carrier R = carrier (b_ag R)\<rbrakk> \<Longrightarrow> \<exists>aa\<in>carrier (b_ag R). I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> aa
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier (b_ag R); aGroup R; carrier R = carrier (b_ag R)\<rbrakk> \<Longrightarrow> \<exists>aa\<in>carrier (b_ag R). I \<bullet>\<^bsub>b_ag R\<^esub> a = I \<bullet>\<^bsub>b_ag R\<^esub> aa
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) mem_ar_coset1:"\<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow>
                                 \<exists>h\<in>I. h \<plusminus> a = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> \<exists>h\<in>I. h \<plusminus> a = x
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I; aGroup R\<rbrakk> \<Longrightarrow> \<exists>h\<in>I. h \<plusminus> a = x
[PROOF STEP]
apply (frule aGroup.ag_carrier_carrier[THEN sym, of "R"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I; aGroup R; carrier R = carrier (b_ag R)\<rbrakk> \<Longrightarrow> \<exists>h\<in>I. h \<plusminus> a = x
[PROOF STEP]
apply (frule aGroup.agop_gop [THEN sym, of "R"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I; aGroup R; carrier R = carrier (b_ag R); (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>h\<in>I. h \<plusminus> a = x
[PROOF STEP]
apply (frule aGroup.agiop_giop [THEN sym, of "R"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I; aGroup R; carrier R = carrier (b_ag R); (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>); mop R = iop (b_ag R)\<rbrakk> \<Longrightarrow> \<exists>h\<in>I. h \<plusminus> a = x
[PROOF STEP]
apply (simp add:ar_coset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier (b_ag R); x \<in> I \<bullet>\<^bsub>b_ag R\<^esub> a; aGroup R; carrier R = carrier (b_ag R); (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>); mop R = iop (b_ag R)\<rbrakk> \<Longrightarrow> \<exists>h\<in>I. h \<cdot>\<^bsub>b_ag R\<^esub> a = x
[PROOF STEP]
apply (simp add:ideal_def asubGroup_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ag R \<guillemotright> I  \<and> (\<forall>r\<in>carrier (b_ag R). \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I); a \<in> carrier (b_ag R); x \<in> I \<bullet>\<^bsub>b_ag R\<^esub> a; aGroup R; carrier R = carrier (b_ag R); (\<plusminus>) = (\<cdot>\<^bsub>b_ag R\<^esub>); mop R = iop (b_ag R)\<rbrakk> \<Longrightarrow> \<exists>h\<in>I. h \<cdot>\<^bsub>b_ag R\<^esub> a = x
[PROOF STEP]
apply (simp add:rcs_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ar_coset_mem2:"\<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow>
                           \<exists>h\<in>I. x = a \<plusminus> h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> \<exists>h\<in>I. x = a \<plusminus> h
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I; aGroup R\<rbrakk> \<Longrightarrow> \<exists>h\<in>I. x = a \<plusminus> h
[PROOF STEP]
apply (frule mem_ar_coset1 [of "I" "a" "x"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I; aGroup R; \<exists>h\<in>I. h \<plusminus> a = x\<rbrakk> \<Longrightarrow> \<exists>h\<in>I. x = a \<plusminus> h
[PROOF STEP]
apply (erule bexE,
       frule_tac h = h in ideal_subset[of "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. \<lbrakk>ideal R I; a \<in> carrier R; x \<in> a \<uplus>\<^bsub>R\<^esub> I; aGroup R; h \<in> I; h \<plusminus> a = x; h \<in> carrier R\<rbrakk> \<Longrightarrow> \<exists>h\<in>I. x = a \<plusminus> h
[PROOF STEP]
apply (simp add:aGroup.ag_pOp_commute[of "R" _ "a"],
       frule sym, thin_tac "a \<plusminus> h = x", blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


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


[STATEMENT]
lemma (in Ring) ar_c_top: "\<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R\<rbrakk>
       \<Longrightarrow> (c_top (b_ag 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> c_top (b_ag R) I (a \<uplus>\<^bsub>R\<^esub> I) (b \<uplus>\<^bsub>R\<^esub> I) = (a \<plusminus> b) \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (cut_tac ring_is_ag, frule ideal_asubg,
       frule aGroup.asubg_nsubg[of "R" "I"], assumption,
       frule aGroup.b_ag_group[of "R"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> c_top (b_ag R) I (a \<uplus>\<^bsub>R\<^esub> I) (b \<uplus>\<^bsub>R\<^esub> I) = (a \<plusminus> b) \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (simp add:ar_coset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; R +> I; b_ag R \<triangleright> I; 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) = I \<bullet>\<^bsub>b_ag R\<^esub> (a \<plusminus> b)
[PROOF STEP]
apply (subst Group.c_top_welldef[THEN sym], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> a \<in> carrier (b_ag R)
 2. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> b \<in> carrier (b_ag R)
 3. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> I \<bullet>\<^bsub>b_ag R\<^esub> (a \<cdot>\<^bsub>b_ag R\<^esub> b) = I \<bullet>\<^bsub>b_ag R\<^esub> (a \<plusminus> b)
[PROOF STEP]
apply (simp add:aGroup.ag_carrier_carrier)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> I \<bullet>\<^bsub>b_ag R\<^esub> (a \<cdot>\<^bsub>b_ag R\<^esub> b) = I \<bullet>\<^bsub>b_ag R\<^esub> (a \<plusminus> b)
[PROOF STEP]
apply (simp add:aGroup.agop_gop)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) quotient_ring_tr1:"\<lbrakk>ideal R I; a1 \<in> carrier R; a2 \<in> carrier R;
                b1 \<in> carrier R; b2 \<in> carrier R;
                a1 \<uplus>\<^bsub>R\<^esub> I = a2 \<uplus>\<^bsub>R\<^esub> I; b1 \<uplus>\<^bsub>R\<^esub> I = b2 \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow>
                             (a1 \<cdot>\<^sub>r b1) \<uplus>\<^bsub>R\<^esub> I = (a2 \<cdot>\<^sub>r b2) \<uplus>\<^bsub>R\<^esub> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a1 \<in> carrier R; a2 \<in> carrier R; b1 \<in> carrier R; b2 \<in> carrier R; a1 \<uplus>\<^bsub>R\<^esub> I = a2 \<uplus>\<^bsub>R\<^esub> I; b1 \<uplus>\<^bsub>R\<^esub> I = b2 \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> a1 \<cdot>\<^sub>r b1 \<uplus>\<^bsub>R\<^esub> I = a2 \<cdot>\<^sub>r b2 \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (rule ar_coset_same1, assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ideal R I; a1 \<in> carrier R; a2 \<in> carrier R; b1 \<in> carrier R; b2 \<in> carrier R; a1 \<uplus>\<^bsub>R\<^esub> I = a2 \<uplus>\<^bsub>R\<^esub> I; b1 \<uplus>\<^bsub>R\<^esub> I = b2 \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> a1 \<cdot>\<^sub>r b1 \<in> carrier R
 2. \<lbrakk>ideal R I; a1 \<in> carrier R; a2 \<in> carrier R; b1 \<in> carrier R; b2 \<in> carrier R; a1 \<uplus>\<^bsub>R\<^esub> I = a2 \<uplus>\<^bsub>R\<^esub> I; b1 \<uplus>\<^bsub>R\<^esub> I = b2 \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> a2 \<cdot>\<^sub>r b2 \<in> carrier R
 3. \<lbrakk>ideal R I; a1 \<in> carrier R; a2 \<in> carrier R; b1 \<in> carrier R; b2 \<in> carrier R; a1 \<uplus>\<^bsub>R\<^esub> I = a2 \<uplus>\<^bsub>R\<^esub> I; b1 \<uplus>\<^bsub>R\<^esub> I = b2 \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> a2 \<cdot>\<^sub>r b2 \<plusminus> -\<^sub>a a1 \<cdot>\<^sub>r b1 \<in> I
[PROOF STEP]
apply (simp add: ring_tOp_closed)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a1 \<in> carrier R; a2 \<in> carrier R; b1 \<in> carrier R; b2 \<in> carrier R; a1 \<uplus>\<^bsub>R\<^esub> I = a2 \<uplus>\<^bsub>R\<^esub> I; b1 \<uplus>\<^bsub>R\<^esub> I = b2 \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> a2 \<cdot>\<^sub>r b2 \<plusminus> -\<^sub>a a1 \<cdot>\<^sub>r b1 \<in> I
[PROOF STEP]
apply (frule ar_coset_same2 [of "I" "a1" "a2"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a1 \<in> carrier R; a2 \<in> carrier R; b1 \<in> carrier R; b2 \<in> carrier R; a1 \<uplus>\<^bsub>R\<^esub> I = a2 \<uplus>\<^bsub>R\<^esub> I; b1 \<uplus>\<^bsub>R\<^esub> I = b2 \<uplus>\<^bsub>R\<^esub> I; a2 \<plusminus> -\<^sub>a a1 \<in> I\<rbrakk> \<Longrightarrow> a2 \<cdot>\<^sub>r b2 \<plusminus> -\<^sub>a a1 \<cdot>\<^sub>r b1 \<in> I
[PROOF STEP]
apply (frule ar_coset_same2 [of "I" "b1" "b2"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a1 \<in> carrier R; a2 \<in> carrier R; b1 \<in> carrier R; b2 \<in> carrier R; a1 \<uplus>\<^bsub>R\<^esub> I = a2 \<uplus>\<^bsub>R\<^esub> I; b1 \<uplus>\<^bsub>R\<^esub> I = b2 \<uplus>\<^bsub>R\<^esub> I; a2 \<plusminus> -\<^sub>a a1 \<in> I; b2 \<plusminus> -\<^sub>a b1 \<in> I\<rbrakk> \<Longrightarrow> a2 \<cdot>\<^sub>r b2 \<plusminus> -\<^sub>a a1 \<cdot>\<^sub>r b1 \<in> I
[PROOF STEP]
apply (frule ring_distrib4[of "a2" "b2" "a1" "b1"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a1 \<in> carrier R; a2 \<in> carrier R; b1 \<in> carrier R; b2 \<in> carrier R; a1 \<uplus>\<^bsub>R\<^esub> I = a2 \<uplus>\<^bsub>R\<^esub> I; b1 \<uplus>\<^bsub>R\<^esub> I = b2 \<uplus>\<^bsub>R\<^esub> I; a2 \<plusminus> -\<^sub>a a1 \<in> I; b2 \<plusminus> -\<^sub>a b1 \<in> I; a2 \<cdot>\<^sub>r b2 \<plusminus> -\<^sub>a a1 \<cdot>\<^sub>r b1 = a2 \<cdot>\<^sub>r (b2 \<plusminus> -\<^sub>a b1) \<plusminus> (a2 \<plusminus> -\<^sub>a a1) \<cdot>\<^sub>r b1\<rbrakk> \<Longrightarrow> a2 \<cdot>\<^sub>r b2 \<plusminus> -\<^sub>a a1 \<cdot>\<^sub>r b1 \<in> I
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a1 \<in> carrier R; a2 \<in> carrier R; b1 \<in> carrier R; b2 \<in> carrier R; a1 \<uplus>\<^bsub>R\<^esub> I = a2 \<uplus>\<^bsub>R\<^esub> I; b1 \<uplus>\<^bsub>R\<^esub> I = b2 \<uplus>\<^bsub>R\<^esub> I; a2 \<plusminus> -\<^sub>a a1 \<in> I; b2 \<plusminus> -\<^sub>a b1 \<in> I; a2 \<cdot>\<^sub>r b2 \<plusminus> -\<^sub>a a1 \<cdot>\<^sub>r b1 = a2 \<cdot>\<^sub>r (b2 \<plusminus> -\<^sub>a b1) \<plusminus> (a2 \<plusminus> -\<^sub>a a1) \<cdot>\<^sub>r b1\<rbrakk> \<Longrightarrow> a2 \<cdot>\<^sub>r (b2 \<plusminus> -\<^sub>a b1) \<plusminus> (a2 \<plusminus> -\<^sub>a a1) \<cdot>\<^sub>r b1 \<in> I
[PROOF STEP]
apply (rule ideal_pOp_closed[of "I"], assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; a1 \<in> carrier R; a2 \<in> carrier R; b1 \<in> carrier R; b2 \<in> carrier R; a1 \<uplus>\<^bsub>R\<^esub> I = a2 \<uplus>\<^bsub>R\<^esub> I; b1 \<uplus>\<^bsub>R\<^esub> I = b2 \<uplus>\<^bsub>R\<^esub> I; a2 \<plusminus> -\<^sub>a a1 \<in> I; b2 \<plusminus> -\<^sub>a b1 \<in> I; a2 \<cdot>\<^sub>r b2 \<plusminus> -\<^sub>a a1 \<cdot>\<^sub>r b1 = a2 \<cdot>\<^sub>r (b2 \<plusminus> -\<^sub>a b1) \<plusminus> (a2 \<plusminus> -\<^sub>a a1) \<cdot>\<^sub>r b1\<rbrakk> \<Longrightarrow> a2 \<cdot>\<^sub>r (b2 \<plusminus> -\<^sub>a b1) \<in> I
 2. \<lbrakk>ideal R I; a1 \<in> carrier R; a2 \<in> carrier R; b1 \<in> carrier R; b2 \<in> carrier R; a1 \<uplus>\<^bsub>R\<^esub> I = a2 \<uplus>\<^bsub>R\<^esub> I; b1 \<uplus>\<^bsub>R\<^esub> I = b2 \<uplus>\<^bsub>R\<^esub> I; a2 \<plusminus> -\<^sub>a a1 \<in> I; b2 \<plusminus> -\<^sub>a b1 \<in> I; a2 \<cdot>\<^sub>r b2 \<plusminus> -\<^sub>a a1 \<cdot>\<^sub>r b1 = a2 \<cdot>\<^sub>r (b2 \<plusminus> -\<^sub>a b1) \<plusminus> (a2 \<plusminus> -\<^sub>a a1) \<cdot>\<^sub>r b1\<rbrakk> \<Longrightarrow> (a2 \<plusminus> -\<^sub>a a1) \<cdot>\<^sub>r b1 \<in> I
[PROOF STEP]
apply (simp add:ideal_ring_multiple, simp add:ideal_ring_multiple1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) rcostOp:"\<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R\<rbrakk> \<Longrightarrow>
                    rcostOp 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> rcostOp 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 STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> rcostOp 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 STEP]
apply (frule ar_cos_mem[of "I" "a"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> rcostOp 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 STEP]
apply (frule ar_cos_mem[of "I" "b"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> rcostOp 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 STEP]
apply (simp add:rcostOp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> {z. \<exists>x\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>h\<in>I. x \<cdot>\<^sub>r y \<plusminus> h = z} = a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> {z. \<exists>x\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>h\<in>I. x \<cdot>\<^sub>r y \<plusminus> h = z} \<subseteq> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I
 2. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I \<subseteq> {z. \<exists>x\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>h\<in>I. x \<cdot>\<^sub>r y \<plusminus> h = z}
[PROOF STEP]
apply (rule subsetI, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; \<exists>xa\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>h\<in>I. xa \<cdot>\<^sub>r y \<plusminus> h = x\<rbrakk> \<Longrightarrow> x \<in> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I
 2. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I \<subseteq> {z. \<exists>x\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>h\<in>I. x \<cdot>\<^sub>r y \<plusminus> h = z}
[PROOF STEP]
apply (erule bexE)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa y h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; xa \<in> a \<uplus>\<^bsub>R\<^esub> I; y \<in> b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; xa \<cdot>\<^sub>r y \<plusminus> h = x\<rbrakk> \<Longrightarrow> x \<in> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I
 2. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I \<subseteq> {z. \<exists>x\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>h\<in>I. x \<cdot>\<^sub>r y \<plusminus> h = z}
[PROOF STEP]
apply (rule belong_ar_coset1, assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x xa y h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; xa \<in> a \<uplus>\<^bsub>R\<^esub> I; y \<in> b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; xa \<cdot>\<^sub>r y \<plusminus> h = x\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<in> carrier R
 2. \<And>x xa y h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; xa \<in> a \<uplus>\<^bsub>R\<^esub> I; y \<in> b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; xa \<cdot>\<^sub>r y \<plusminus> h = x\<rbrakk> \<Longrightarrow> x \<in> carrier R
 3. \<And>x xa y h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; xa \<in> a \<uplus>\<^bsub>R\<^esub> I; y \<in> b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; xa \<cdot>\<^sub>r y \<plusminus> h = x\<rbrakk> \<Longrightarrow> x \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b \<in> I
 4. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I \<subseteq> {z. \<exists>x\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>h\<in>I. x \<cdot>\<^sub>r y \<plusminus> h = z}
[PROOF STEP]
apply (simp add:ring_tOp_closed)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa y h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; xa \<in> a \<uplus>\<^bsub>R\<^esub> I; y \<in> b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; xa \<cdot>\<^sub>r y \<plusminus> h = x\<rbrakk> \<Longrightarrow> x \<in> carrier R
 2. \<And>x xa y h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; xa \<in> a \<uplus>\<^bsub>R\<^esub> I; y \<in> b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; xa \<cdot>\<^sub>r y \<plusminus> h = x\<rbrakk> \<Longrightarrow> x \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b \<in> I
 3. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I \<subseteq> {z. \<exists>x\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>h\<in>I. x \<cdot>\<^sub>r y \<plusminus> h = z}
[PROOF STEP]
apply (frule sym, thin_tac "xa \<cdot>\<^sub>r y \<plusminus> h = x", simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa y h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; xa \<in> a \<uplus>\<^bsub>R\<^esub> I; y \<in> b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; x = xa \<cdot>\<^sub>r y \<plusminus> h\<rbrakk> \<Longrightarrow> xa \<cdot>\<^sub>r y \<plusminus> h \<in> carrier R
 2. \<And>x xa y h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; xa \<in> a \<uplus>\<^bsub>R\<^esub> I; y \<in> b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; xa \<cdot>\<^sub>r y \<plusminus> h = x\<rbrakk> \<Longrightarrow> x \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b \<in> I
 3. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I \<subseteq> {z. \<exists>x\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>h\<in>I. x \<cdot>\<^sub>r y \<plusminus> h = z}
[PROOF STEP]
apply (rule aGroup.ag_pOp_closed, assumption)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x xa y h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; xa \<in> a \<uplus>\<^bsub>R\<^esub> I; y \<in> b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; x = xa \<cdot>\<^sub>r y \<plusminus> h\<rbrakk> \<Longrightarrow> xa \<cdot>\<^sub>r y \<in> carrier R
 2. \<And>x xa y h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; xa \<in> a \<uplus>\<^bsub>R\<^esub> I; y \<in> b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; x = xa \<cdot>\<^sub>r y \<plusminus> h\<rbrakk> \<Longrightarrow> h \<in> carrier R
 3. \<And>x xa y h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; xa \<in> a \<uplus>\<^bsub>R\<^esub> I; y \<in> b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; xa \<cdot>\<^sub>r y \<plusminus> h = x\<rbrakk> \<Longrightarrow> x \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b \<in> I
 4. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I \<subseteq> {z. \<exists>x\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>h\<in>I. x \<cdot>\<^sub>r y \<plusminus> h = z}
[PROOF STEP]
apply (frule_tac x = xa in ar_coset_mem2[of "I" "a"], assumption+,
        frule_tac x = y in ar_coset_mem2[of "I" "b"], assumption+,
        (erule bexE)+, simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x xa y h ha hb. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; a \<plusminus> ha \<in> a \<uplus>\<^bsub>R\<^esub> I; b \<plusminus> hb \<in> b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; x = (a \<plusminus> ha) \<cdot>\<^sub>r (b \<plusminus> hb) \<plusminus> h; ha \<in> I; xa = a \<plusminus> ha; hb \<in> I; y = b \<plusminus> hb\<rbrakk> \<Longrightarrow> (a \<plusminus> ha) \<cdot>\<^sub>r (b \<plusminus> hb) \<in> carrier R
 2. \<And>x xa y h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; xa \<in> a \<uplus>\<^bsub>R\<^esub> I; y \<in> b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; x = xa \<cdot>\<^sub>r y \<plusminus> h\<rbrakk> \<Longrightarrow> h \<in> carrier R
 3. \<And>x xa y h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; xa \<in> a \<uplus>\<^bsub>R\<^esub> I; y \<in> b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; xa \<cdot>\<^sub>r y \<plusminus> h = x\<rbrakk> \<Longrightarrow> x \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b \<in> I
 4. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I \<subseteq> {z. \<exists>x\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>h\<in>I. x \<cdot>\<^sub>r y \<plusminus> h = z}
[PROOF STEP]
apply (rule ring_tOp_closed, rule aGroup.ag_pOp_closed, assumption+,
        simp add:ideal_subset)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x xa y h ha hb. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; a \<plusminus> ha \<in> a \<uplus>\<^bsub>R\<^esub> I; b \<plusminus> hb \<in> b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; x = (a \<plusminus> ha) \<cdot>\<^sub>r (b \<plusminus> hb) \<plusminus> h; ha \<in> I; xa = a \<plusminus> ha; hb \<in> I; y = b \<plusminus> hb\<rbrakk> \<Longrightarrow> b \<plusminus> hb \<in> carrier R
 2. \<And>x xa y h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; xa \<in> a \<uplus>\<^bsub>R\<^esub> I; y \<in> b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; x = xa \<cdot>\<^sub>r y \<plusminus> h\<rbrakk> \<Longrightarrow> h \<in> carrier R
 3. \<And>x xa y h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; xa \<in> a \<uplus>\<^bsub>R\<^esub> I; y \<in> b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; xa \<cdot>\<^sub>r y \<plusminus> h = x\<rbrakk> \<Longrightarrow> x \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b \<in> I
 4. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I \<subseteq> {z. \<exists>x\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>h\<in>I. x \<cdot>\<^sub>r y \<plusminus> h = z}
[PROOF STEP]
apply (rule aGroup.ag_pOp_closed, assumption+, simp add:ideal_subset,
        simp add:ideal_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa y h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; xa \<in> a \<uplus>\<^bsub>R\<^esub> I; y \<in> b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; xa \<cdot>\<^sub>r y \<plusminus> h = x\<rbrakk> \<Longrightarrow> x \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b \<in> I
 2. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I \<subseteq> {z. \<exists>x\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>h\<in>I. x \<cdot>\<^sub>r y \<plusminus> h = z}
[PROOF STEP]
apply (frule sym, thin_tac "xa \<cdot>\<^sub>r y \<plusminus> h = x", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa y h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; xa \<in> a \<uplus>\<^bsub>R\<^esub> I; y \<in> b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; x = xa \<cdot>\<^sub>r y \<plusminus> h\<rbrakk> \<Longrightarrow> xa \<cdot>\<^sub>r y \<plusminus> h \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b \<in> I
 2. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I \<subseteq> {z. \<exists>x\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>h\<in>I. x \<cdot>\<^sub>r y \<plusminus> h = z}
[PROOF STEP]
apply (frule_tac x = xa in belong_ar_coset2[of "I" "a"], assumption+,
        frule_tac x = y in belong_ar_coset2[of "I" "b"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa y h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; xa \<in> a \<uplus>\<^bsub>R\<^esub> I; y \<in> b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; x = xa \<cdot>\<^sub>r y \<plusminus> h; xa \<plusminus> -\<^sub>a a \<in> I; y \<plusminus> -\<^sub>a b \<in> I\<rbrakk> \<Longrightarrow> xa \<cdot>\<^sub>r y \<plusminus> h \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b \<in> I
 2. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I \<subseteq> {z. \<exists>x\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>h\<in>I. x \<cdot>\<^sub>r y \<plusminus> h = z}
[PROOF STEP]
apply (frule_tac x = xa in ar_coset_subsetD[of "I" "a"], assumption+,
        frule_tac x = y in ar_coset_subsetD[of "I" "b"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa y h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; xa \<in> a \<uplus>\<^bsub>R\<^esub> I; y \<in> b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; x = xa \<cdot>\<^sub>r y \<plusminus> h; xa \<plusminus> -\<^sub>a a \<in> I; y \<plusminus> -\<^sub>a b \<in> I; xa \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> xa \<cdot>\<^sub>r y \<plusminus> h \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b \<in> I
 2. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I \<subseteq> {z. \<exists>x\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>h\<in>I. x \<cdot>\<^sub>r y \<plusminus> h = z}
[PROOF STEP]
apply (subst aGroup.ag_pOp_commute, assumption,
        simp add:ring_tOp_closed, simp add:ideal_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa y h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; xa \<in> a \<uplus>\<^bsub>R\<^esub> I; y \<in> b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; x = xa \<cdot>\<^sub>r y \<plusminus> h; xa \<plusminus> -\<^sub>a a \<in> I; y \<plusminus> -\<^sub>a b \<in> I; xa \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> h \<plusminus> xa \<cdot>\<^sub>r y \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b \<in> I
 2. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I \<subseteq> {z. \<exists>x\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>h\<in>I. x \<cdot>\<^sub>r y \<plusminus> h = z}
[PROOF STEP]
apply (subst aGroup.ag_pOp_assoc, assumption,
        simp add:ideal_subset, simp add:ring_tOp_closed,
        rule aGroup.ag_mOp_closed, simp add:ring_tOp_closed,
        simp add:ring_tOp_closed)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa y h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; xa \<in> a \<uplus>\<^bsub>R\<^esub> I; y \<in> b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; x = xa \<cdot>\<^sub>r y \<plusminus> h; xa \<plusminus> -\<^sub>a a \<in> I; y \<plusminus> -\<^sub>a b \<in> I; xa \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> h \<plusminus> (xa \<cdot>\<^sub>r y \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b) \<in> I
 2. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I \<subseteq> {z. \<exists>x\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>h\<in>I. x \<cdot>\<^sub>r y \<plusminus> h = z}
[PROOF STEP]
apply (rule ideal_pOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa y h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; xa \<in> a \<uplus>\<^bsub>R\<^esub> I; y \<in> b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; x = xa \<cdot>\<^sub>r y \<plusminus> h; xa \<plusminus> -\<^sub>a a \<in> I; y \<plusminus> -\<^sub>a b \<in> I; xa \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> xa \<cdot>\<^sub>r y \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b \<in> I
 2. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I \<subseteq> {z. \<exists>x\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>h\<in>I. x \<cdot>\<^sub>r y \<plusminus> h = z}
[PROOF STEP]
apply (rule_tac a = xa and a' = y and b = a and b' = b in times_modTr,
        assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I \<subseteq> {z. \<exists>x\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>h\<in>I. x \<cdot>\<^sub>r y \<plusminus> h = z}
[PROOF STEP]
apply (rule subsetI, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; x \<in> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> \<exists>xa\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>h\<in>I. xa \<cdot>\<^sub>r y \<plusminus> h = x
[PROOF STEP]
apply (frule_tac x = x in ar_coset_mem2[of "I" "a \<cdot>\<^sub>r b"],
        simp add:ring_tOp_closed, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; x \<in> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I; \<exists>h\<in>I. x = a \<cdot>\<^sub>r b \<plusminus> h\<rbrakk> \<Longrightarrow> \<exists>xa\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>h\<in>I. xa \<cdot>\<^sub>r y \<plusminus> h = x
[PROOF STEP]
apply (erule bexE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; x \<in> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; x = a \<cdot>\<^sub>r b \<plusminus> h\<rbrakk> \<Longrightarrow> \<exists>xa\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>h\<in>I. xa \<cdot>\<^sub>r y \<plusminus> h = x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; a \<cdot>\<^sub>r b \<plusminus> h \<in> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; x = a \<cdot>\<^sub>r b \<plusminus> h\<rbrakk> \<Longrightarrow> \<exists>x\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>ha\<in>I. x \<cdot>\<^sub>r y \<plusminus> ha = a \<cdot>\<^sub>r b \<plusminus> h
[PROOF STEP]
apply (frule a_in_ar_coset[of "I" "a"], assumption+,
        frule a_in_ar_coset[of "I" "b"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x h. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; aGroup R; a \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; b \<uplus>\<^bsub>R\<^esub> I \<in> set_rcs (b_ag R) I; a \<cdot>\<^sub>r b \<plusminus> h \<in> a \<cdot>\<^sub>r b \<uplus>\<^bsub>R\<^esub> I; h \<in> I; x = a \<cdot>\<^sub>r b \<plusminus> h; a \<in> a \<uplus>\<^bsub>R\<^esub> I; b \<in> b \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> \<exists>x\<in>a \<uplus>\<^bsub>R\<^esub> I. \<exists>y\<in>b \<uplus>\<^bsub>R\<^esub> I. \<exists>ha\<in>I. x \<cdot>\<^sub>r y \<plusminus> ha = a \<cdot>\<^sub>r b \<plusminus> h
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) carrier_qring:"ideal R I \<Longrightarrow>
                               carrier (qring R I) = set_rcs (b_ag R) I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> carrier (R /\<^sub>r I) = set_rcs (b_ag R) I
[PROOF STEP]
by (simp add:qring_def)


[STATEMENT]
lemma (in Ring) carrier_qring1:"ideal R I \<Longrightarrow>
                                carrier (qring R I) = set_ar_cos R I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> carrier (R /\<^sub>r I) = set_ar_cos R I
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; aGroup R\<rbrakk> \<Longrightarrow> carrier (R /\<^sub>r I) = set_ar_cos R I
[PROOF STEP]
apply (simp add:carrier_qring set_rcs_def set_ar_cos_def)
[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 = a \<uplus>\<^bsub>R\<^esub> I}
[PROOF STEP]
apply (simp add:ar_coset_def aGroup.ag_carrier_carrier)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done