[STATEMENT]
lemma (in Ring) qring_ring:"ideal R I \<Longrightarrow> Ring (qring R I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> Ring (R /\<^sub>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> Ring (R /\<^sub>r I)
[PROOF STEP]
apply (frule ideal_asubg[of "I"],
        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; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> Ring (R /\<^sub>r I)
[PROOF STEP]
apply (subst Ring_def, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<plusminus>\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c = a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> b = b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> mop (R /\<^sub>r I) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = \<zero>\<^bsub>R /\<^sub>r I\<^esub>) \<and> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<plusminus>\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I)
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c = a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> b = b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> mop (R /\<^sub>r I) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = \<zero>\<^bsub>R /\<^sub>r I\<^esub>) \<and> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (rule Pi_I)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); x \<in> carrier (R /\<^sub>r I); xa \<in> carrier (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> x \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> xa \<in> carrier (R /\<^sub>r I)
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c = a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> b = b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> mop (R /\<^sub>r I) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = \<zero>\<^bsub>R /\<^sub>r I\<^esub>) \<and> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (simp add:carrier_qring, simp add:set_rcs_def, (erule bexE)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa a aa. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); a \<in> carrier (b_ag R); x = I \<bullet>\<^bsub>b_ag R\<^esub> a; aa \<in> carrier (b_ag R); xa = I \<bullet>\<^bsub>b_ag R\<^esub> aa\<rbrakk> \<Longrightarrow> \<exists>a\<in>carrier (b_ag R). x \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> xa = I \<bullet>\<^bsub>b_ag R\<^esub> a
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c = a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> b = b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> mop (R /\<^sub>r I) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = \<zero>\<^bsub>R /\<^sub>r I\<^esub>) \<and> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (subst qring_def, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa a aa. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); a \<in> carrier (b_ag R); x = I \<bullet>\<^bsub>b_ag R\<^esub> a; aa \<in> carrier (b_ag R); xa = I \<bullet>\<^bsub>b_ag R\<^esub> aa\<rbrakk> \<Longrightarrow> \<exists>ab\<in>carrier (b_ag R). c_top (b_ag R) I (I \<bullet>\<^bsub>b_ag R\<^esub> a) (I \<bullet>\<^bsub>b_ag R\<^esub> aa) = I \<bullet>\<^bsub>b_ag R\<^esub> ab
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c = a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> b = b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> mop (R /\<^sub>r I) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = \<zero>\<^bsub>R /\<^sub>r I\<^esub>) \<and> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (subst Group.c_top_welldef[THEN sym, of "b_ag R" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa a aa. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); a \<in> carrier (b_ag R); x = I \<bullet>\<^bsub>b_ag R\<^esub> a; aa \<in> carrier (b_ag R); xa = I \<bullet>\<^bsub>b_ag R\<^esub> aa\<rbrakk> \<Longrightarrow> \<exists>ab\<in>carrier (b_ag R). I \<bullet>\<^bsub>b_ag R\<^esub> (a \<cdot>\<^bsub>b_ag R\<^esub> aa) = I \<bullet>\<^bsub>b_ag R\<^esub> ab
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c = a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> b = b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> mop (R /\<^sub>r I) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = \<zero>\<^bsub>R /\<^sub>r I\<^esub>) \<and> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (blast dest: Group.mult_closed[of "b_ag R"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c = a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> b = b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> mop (R /\<^sub>r I) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = \<zero>\<^bsub>R /\<^sub>r I\<^esub>) \<and> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c = a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c)))
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> b = b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> mop (R /\<^sub>r I) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = \<zero>\<^bsub>R /\<^sub>r I\<^esub>) \<and> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (rule allI, rule impI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); a \<in> carrier (R /\<^sub>r I); b \<in> carrier (R /\<^sub>r I); c \<in> carrier (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c = a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c)
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> b = b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> mop (R /\<^sub>r I) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = \<zero>\<^bsub>R /\<^sub>r I\<^esub>) \<and> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (simp add:qring_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); a \<in> set_rcs (b_ag R) I; b \<in> set_rcs (b_ag R) I; c \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> c_top (b_ag R) I (c_top (b_ag R) I a b) c = c_top (b_ag R) I a (c_top (b_ag R) I b c)
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> b = b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> mop (R /\<^sub>r I) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = \<zero>\<^bsub>R /\<^sub>r I\<^esub>) \<and> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (simp add:Group.Qg_tassoc[of "b_ag R" "I"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> b = b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> mop (R /\<^sub>r I) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = \<zero>\<^bsub>R /\<^sub>r I\<^esub>) \<and> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> b = b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a)
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> mop (R /\<^sub>r I) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = \<zero>\<^bsub>R /\<^sub>r I\<^esub>) \<and> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (rule allI, rule impI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); a \<in> carrier (R /\<^sub>r I); b \<in> carrier (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> b = b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> mop (R /\<^sub>r I) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = \<zero>\<^bsub>R /\<^sub>r I\<^esub>) \<and> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (simp add:qring_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); a \<in> set_rcs (b_ag R) I; b \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> c_top (b_ag R) I a b = c_top (b_ag R) I b a
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> mop (R /\<^sub>r I) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = \<zero>\<^bsub>R /\<^sub>r I\<^esub>) \<and> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (simp add:set_rcs_def, (erule bexE)+, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ab. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); aa \<in> carrier (b_ag R); a = I \<bullet>\<^bsub>b_ag R\<^esub> aa; ab \<in> carrier (b_ag R); b = I \<bullet>\<^bsub>b_ag R\<^esub> ab\<rbrakk> \<Longrightarrow> c_top (b_ag R) I (I \<bullet>\<^bsub>b_ag R\<^esub> aa) (I \<bullet>\<^bsub>b_ag R\<^esub> ab) = c_top (b_ag R) I (I \<bullet>\<^bsub>b_ag R\<^esub> ab) (I \<bullet>\<^bsub>b_ag R\<^esub> aa)
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> mop (R /\<^sub>r I) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = \<zero>\<^bsub>R /\<^sub>r I\<^esub>) \<and> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (subst Group.c_top_welldef[THEN sym, of "b_ag R" "I"], assumption+)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ab. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); aa \<in> carrier (b_ag R); a = I \<bullet>\<^bsub>b_ag R\<^esub> aa; ab \<in> carrier (b_ag R); b = I \<bullet>\<^bsub>b_ag R\<^esub> ab\<rbrakk> \<Longrightarrow> I \<bullet>\<^bsub>b_ag R\<^esub> (aa \<cdot>\<^bsub>b_ag R\<^esub> ab) = I \<bullet>\<^bsub>b_ag R\<^esub> (ab \<cdot>\<^bsub>b_ag R\<^esub> aa)
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> mop (R /\<^sub>r I) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = \<zero>\<^bsub>R /\<^sub>r I\<^esub>) \<and> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (simp add:aGroup.agop_gop)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ab. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); aa \<in> carrier (b_ag R); a = I \<bullet>\<^bsub>b_ag R\<^esub> aa; ab \<in> carrier (b_ag R); b = I \<bullet>\<^bsub>b_ag R\<^esub> ab\<rbrakk> \<Longrightarrow> I \<bullet>\<^bsub>b_ag R\<^esub> (aa \<plusminus> ab) = I \<bullet>\<^bsub>b_ag R\<^esub> (ab \<plusminus> aa)
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> mop (R /\<^sub>r I) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = \<zero>\<^bsub>R /\<^sub>r I\<^esub>) \<and> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (simp add:aGroup.ag_carrier_carrier)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ab. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); aa \<in> carrier R; a = I \<bullet>\<^bsub>b_ag R\<^esub> aa; ab \<in> carrier R; b = I \<bullet>\<^bsub>b_ag R\<^esub> ab\<rbrakk> \<Longrightarrow> I \<bullet>\<^bsub>b_ag R\<^esub> (aa \<plusminus> ab) = I \<bullet>\<^bsub>b_ag R\<^esub> (ab \<plusminus> aa)
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> mop (R /\<^sub>r I) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = \<zero>\<^bsub>R /\<^sub>r I\<^esub>) \<and> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (simp add:aGroup.ag_pOp_commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> mop (R /\<^sub>r I) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = \<zero>\<^bsub>R /\<^sub>r I\<^esub>) \<and> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> mop (R /\<^sub>r I) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I)
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = \<zero>\<^bsub>R /\<^sub>r I\<^esub>) \<and> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (simp add:qring_def Group.Qg_iop_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = \<zero>\<^bsub>R /\<^sub>r I\<^esub>) \<and> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = \<zero>\<^bsub>R /\<^sub>r I\<^esub>
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); a \<in> carrier (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>R /\<^sub>r I\<^esub> a \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = \<zero>\<^bsub>R /\<^sub>r I\<^esub>
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (simp add:qring_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); a \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> c_top (b_ag R) I (c_iop (b_ag R) I a) a = I
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (simp add:Group.Qg_i[of "b_ag R" "I"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I)
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (simp add:qring_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> I \<in> set_rcs (b_ag R) I
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (frule Group.nsg_sg[of "b_ag R" "I"], assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); b_ag R \<guillemotright> I \<rbrakk> \<Longrightarrow> I \<in> set_rcs (b_ag R) I
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (simp add:Group.unit_rcs_in_set_rcs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); a \<in> carrier (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>R /\<^sub>r I\<^esub> \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a = a
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (simp add:qring_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); a \<in> set_rcs (b_ag R) I\<rbrakk> \<Longrightarrow> c_top (b_ag R) I I a = a
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (simp add:Group.Qg_unit[of "b_ag R" "I"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub>) \<in> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I) \<rightarrow> carrier (R /\<^sub>r I)
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply(rule Pi_I)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); x \<in> carrier (R /\<^sub>r I); xa \<in> carrier (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> xa \<in> carrier (R /\<^sub>r I)
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (simp add:qring_def aGroup.aqgrp_carrier)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); x \<in> set_ar_cos R I; xa \<in> set_ar_cos R I\<rbrakk> \<Longrightarrow> rcostOp R I x xa \<in> set_ar_cos R I
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (simp add:set_ar_cos_def, (erule bexE)+, simp add:rcostOp,
        blast dest: ring_tOp_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)))
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (rule allI, rule impI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); a \<in> carrier (R /\<^sub>r I); b \<in> carrier (R /\<^sub>r I); c \<in> carrier (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c)
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (simp add:qring_def aGroup.aqgrp_carrier)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); a \<in> set_ar_cos R I; b \<in> set_ar_cos R I; c \<in> set_ar_cos R I\<rbrakk> \<Longrightarrow> rcostOp R I (rcostOp R I a b) c = rcostOp R I a (rcostOp R I b c)
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (simp add:set_ar_cos_def, (erule bexE)+, simp add:rcostOp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c aa ab ac. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); aa \<in> carrier R; a = aa \<uplus>\<^bsub>R\<^esub> I; ab \<in> carrier R; b = ab \<uplus>\<^bsub>R\<^esub> I; ac \<in> carrier R; c = ac \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> rcostOp R I (aa \<cdot>\<^sub>r ab \<uplus>\<^bsub>R\<^esub> I) (ac \<uplus>\<^bsub>R\<^esub> I) = rcostOp R I (aa \<uplus>\<^bsub>R\<^esub> I) (ab \<cdot>\<^sub>r ac \<uplus>\<^bsub>R\<^esub> I)
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (frule_tac x = aa and y = ab in ring_tOp_closed, assumption+,
        frule_tac x = ab and y = ac in ring_tOp_closed, assumption+,
        simp add:rcostOp, simp add:ring_tOp_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)) \<and> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a)
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (rule allI, rule impI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); a \<in> carrier (R /\<^sub>r I); b \<in> carrier (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b = b \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (simp add:qring_def aGroup.aqgrp_carrier)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); a \<in> set_ar_cos R I; b \<in> set_ar_cos R I\<rbrakk> \<Longrightarrow> rcostOp R I a b = rcostOp R I b a
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (simp add:set_ar_cos_def, (erule bexE)+, simp add:rcostOp,
        simp add:ring_tOp_commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<in> carrier (R /\<^sub>r I)
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (simp add:qring_def aGroup.aqgrp_carrier)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> 1\<^sub>r \<uplus>\<^bsub>R\<^esub> I \<in> set_ar_cos R I
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (cut_tac ring_one, simp add:set_ar_cos_def, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>b. b \<in> carrier (R /\<^sub>r I) \<longrightarrow> (\<forall>c. c \<in> carrier (R /\<^sub>r I) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c))
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a
[PROOF STEP]
apply (rule allI, rule impI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); a \<in> carrier (R /\<^sub>r I); b \<in> carrier (R /\<^sub>r I); c \<in> carrier (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> (b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> b \<plusminus>\<^bsub>R /\<^sub>r I\<^esub> a \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> c
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a
[PROOF STEP]
apply (simp add:qring_def aGroup.aqgrp_carrier)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); a \<in> set_ar_cos R I; b \<in> set_ar_cos R I; c \<in> set_ar_cos R I\<rbrakk> \<Longrightarrow> rcostOp R I a (c_top (b_ag R) I b c) = c_top (b_ag R) I (rcostOp R I a b) (rcostOp R I a c)
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a
[PROOF STEP]
apply (simp add:set_ar_cos_def, (erule bexE)+, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c aa ab ac. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); aa \<in> carrier R; a = aa \<uplus>\<^bsub>R\<^esub> I; ab \<in> carrier R; b = ab \<uplus>\<^bsub>R\<^esub> I; ac \<in> carrier R; c = ac \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> rcostOp R I (aa \<uplus>\<^bsub>R\<^esub> I) (c_top (b_ag R) I (ab \<uplus>\<^bsub>R\<^esub> I) (ac \<uplus>\<^bsub>R\<^esub> I)) = c_top (b_ag R) I (rcostOp R I (aa \<uplus>\<^bsub>R\<^esub> I) (ab \<uplus>\<^bsub>R\<^esub> I)) (rcostOp R I (aa \<uplus>\<^bsub>R\<^esub> I) (ac \<uplus>\<^bsub>R\<^esub> I))
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a
[PROOF STEP]
apply (simp add:ar_c_top rcostOp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c aa ab ac. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); aa \<in> carrier R; a = aa \<uplus>\<^bsub>R\<^esub> I; ab \<in> carrier R; b = ab \<uplus>\<^bsub>R\<^esub> I; ac \<in> carrier R; c = ac \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> rcostOp R I (aa \<uplus>\<^bsub>R\<^esub> I) ((ab \<plusminus> ac) \<uplus>\<^bsub>R\<^esub> I) = c_top (b_ag R) I (aa \<cdot>\<^sub>r ab \<uplus>\<^bsub>R\<^esub> I) (aa \<cdot>\<^sub>r ac \<uplus>\<^bsub>R\<^esub> I)
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a
[PROOF STEP]
apply (frule_tac x = ab and y = ac in aGroup.ag_pOp_closed,
                  assumption+,
        frule_tac x = aa and y = ab in ring_tOp_closed, assumption+ ,
        frule_tac x = aa and y = ac in ring_tOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c aa ab ac. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); aa \<in> carrier R; a = aa \<uplus>\<^bsub>R\<^esub> I; ab \<in> carrier R; b = ab \<uplus>\<^bsub>R\<^esub> I; ac \<in> carrier R; c = ac \<uplus>\<^bsub>R\<^esub> I; ab \<plusminus> ac \<in> carrier R; aa \<cdot>\<^sub>r ab \<in> carrier R; aa \<cdot>\<^sub>r ac \<in> carrier R\<rbrakk> \<Longrightarrow> rcostOp R I (aa \<uplus>\<^bsub>R\<^esub> I) ((ab \<plusminus> ac) \<uplus>\<^bsub>R\<^esub> I) = c_top (b_ag R) I (aa \<cdot>\<^sub>r ab \<uplus>\<^bsub>R\<^esub> I) (aa \<cdot>\<^sub>r ac \<uplus>\<^bsub>R\<^esub> I)
 2. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a
[PROOF STEP]
apply (simp add:ar_c_top rcostOp, simp add:ring_distrib1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R)\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (R /\<^sub>r I) \<longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); a \<in> carrier (R /\<^sub>r I)\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> \<cdot>\<^sub>r\<^bsub>R /\<^sub>r I\<^esub> a = a
[PROOF STEP]
apply (simp add:qring_def aGroup.aqgrp_carrier)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); a \<in> set_ar_cos R I\<rbrakk> \<Longrightarrow> rcostOp R I (1\<^sub>r \<uplus>\<^bsub>R\<^esub> I) a = a
[PROOF STEP]
apply (simp add:set_ar_cos_def, erule bexE, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); aa \<in> carrier R; a = aa \<uplus>\<^bsub>R\<^esub> I\<rbrakk> \<Longrightarrow> rcostOp R I (1\<^sub>r \<uplus>\<^bsub>R\<^esub> I) (aa \<uplus>\<^bsub>R\<^esub> I) = aa \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (cut_tac ring_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa. \<lbrakk>ideal R I; aGroup R; R +> I; b_ag R \<triangleright> I; Group (b_ag R); aa \<in> carrier R; a = aa \<uplus>\<^bsub>R\<^esub> I; 1\<^sub>r \<in> carrier R\<rbrakk> \<Longrightarrow> rcostOp R I (1\<^sub>r \<uplus>\<^bsub>R\<^esub> I) (aa \<uplus>\<^bsub>R\<^esub> I) = aa \<uplus>\<^bsub>R\<^esub> I
[PROOF STEP]
apply (simp add:rcostOp, simp add:ring_l_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done