[STATEMENT]
lemma Ag_ind_bijec:"\<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D;
      bij_to f (carrier A) (D::'d set)\<rbrakk> \<Longrightarrow> bijec\<^bsub>A, (Ag_ind A f)\<^esub> (Agii A f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D\<rbrakk> \<Longrightarrow> bijec\<^bsub>A,Ag_ind A f\<^esub> Agii A f
[PROOF STEP]
apply (frule aGroup.Ag_ind_aHom[of "A" "f" "D"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f)\<rbrakk> \<Longrightarrow> bijec\<^bsub>A,Ag_ind A f\<^esub> Agii A f
[PROOF STEP]
apply (frule aGroup.Ag_ind_aGroup[of "A" "f" "D"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> bijec\<^bsub>A,Ag_ind A f\<^esub> Agii A f
[PROOF STEP]
apply (simp add:bijec_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> injec\<^bsub>A,Ag_ind A f\<^esub> Agii A f \<and> surjec\<^bsub>A,Ag_ind A f\<^esub> Agii A f
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> injec\<^bsub>A,Ag_ind A f\<^esub> Agii A f
 2. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> surjec\<^bsub>A,Ag_ind A f\<^esub> Agii A f
[PROOF STEP]
apply (simp add:injec_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> ker\<^bsub>A,Ag_ind A f\<^esub> Agii A f = {\<zero>\<^bsub>A\<^esub>}
 2. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> surjec\<^bsub>A,Ag_ind A f\<^esub> Agii A f
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> ker\<^bsub>A,Ag_ind A f\<^esub> Agii A f \<subseteq> {\<zero>\<^bsub>A\<^esub>}
 2. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>A\<^esub>} \<subseteq> ker\<^bsub>A,Ag_ind A f\<^esub> Agii A f
 3. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> surjec\<^bsub>A,Ag_ind A f\<^esub> Agii A f
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f); x \<in> ker\<^bsub>A,Ag_ind A f\<^esub> Agii A f\<rbrakk> \<Longrightarrow> x \<in> {\<zero>\<^bsub>A\<^esub>}
 2. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>A\<^esub>} \<subseteq> ker\<^bsub>A,Ag_ind A f\<^esub> Agii A f
 3. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> surjec\<^bsub>A,Ag_ind A f\<^esub> Agii A f
[PROOF STEP]
apply (simp add:ker_def, erule conjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f); x \<in> carrier A; Agii A f x = \<zero>\<^bsub>Ag_ind A f\<^esub>\<rbrakk> \<Longrightarrow> x = \<zero>\<^bsub>A\<^esub>
 2. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>A\<^esub>} \<subseteq> ker\<^bsub>A,Ag_ind A f\<^esub> Agii A f
 3. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> surjec\<^bsub>A,Ag_ind A f\<^esub> Agii A f
[PROOF STEP]
apply (frule aHom_0_0[of "A" "Ag_ind A f" "Agii A f"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f); x \<in> carrier A; Agii A f x = \<zero>\<^bsub>Ag_ind A f\<^esub>; Agii A f \<zero>\<^bsub>A\<^esub> = \<zero>\<^bsub>Ag_ind A f\<^esub>\<rbrakk> \<Longrightarrow> x = \<zero>\<^bsub>A\<^esub>
 2. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>A\<^esub>} \<subseteq> ker\<^bsub>A,Ag_ind A f\<^esub> Agii A f
 3. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> surjec\<^bsub>A,Ag_ind A f\<^esub> Agii A f
[PROOF STEP]
apply (rotate_tac -2, frule sym, thin_tac "Agii A f x = \<zero>\<^bsub>Ag_ind A f\<^esub>", simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>Agii A f \<zero>\<^bsub>A\<^esub> = Agii A f x; aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f); x \<in> carrier A; \<zero>\<^bsub>Ag_ind A f\<^esub> = Agii A f x\<rbrakk> \<Longrightarrow> x = \<zero>\<^bsub>A\<^esub>
 2. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>A\<^esub>} \<subseteq> ker\<^bsub>A,Ag_ind A f\<^esub> Agii A f
 3. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> surjec\<^bsub>A,Ag_ind A f\<^esub> Agii A f
[PROOF STEP]
apply (frule aGroup.ag_inc_zero[of "A"], simp add:Agii_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>f \<zero>\<^bsub>A\<^esub> = f x; aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; restrict f (carrier A) \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f); x \<in> carrier A; \<zero>\<^bsub>Ag_ind A f\<^esub> = f x; \<zero>\<^bsub>A\<^esub> \<in> carrier A\<rbrakk> \<Longrightarrow> x = \<zero>\<^bsub>A\<^esub>
 2. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>A\<^esub>} \<subseteq> ker\<^bsub>A,Ag_ind A f\<^esub> Agii A f
 3. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> surjec\<^bsub>A,Ag_ind A f\<^esub> Agii A f
[PROOF STEP]
apply (unfold bij_to_def, frule conjunct2, fold bij_to_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>f \<zero>\<^bsub>A\<^esub> = f x; aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; restrict f (carrier A) \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f); x \<in> carrier A; \<zero>\<^bsub>Ag_ind A f\<^esub> = f x; \<zero>\<^bsub>A\<^esub> \<in> carrier A; inj_on f (carrier A)\<rbrakk> \<Longrightarrow> x = \<zero>\<^bsub>A\<^esub>
 2. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>A\<^esub>} \<subseteq> ker\<^bsub>A,Ag_ind A f\<^esub> Agii A f
 3. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> surjec\<^bsub>A,Ag_ind A f\<^esub> Agii A f
[PROOF STEP]
apply (frule aGroup.ag_inc_zero[of "A"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>f \<zero>\<^bsub>A\<^esub> = f x; aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; restrict f (carrier A) \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f); x \<in> carrier A; \<zero>\<^bsub>Ag_ind A f\<^esub> = f x; \<zero>\<^bsub>A\<^esub> \<in> carrier A; inj_on f (carrier A); \<zero>\<^bsub>A\<^esub> \<in> carrier A\<rbrakk> \<Longrightarrow> x = \<zero>\<^bsub>A\<^esub>
 2. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>A\<^esub>} \<subseteq> ker\<^bsub>A,Ag_ind A f\<^esub> Agii A f
 3. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> surjec\<^bsub>A,Ag_ind A f\<^esub> Agii A f
[PROOF STEP]
apply (simp add:injective_iff[THEN sym, of "f" "carrier A" "\<zero>\<^bsub>A\<^esub>"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>A\<^esub>} \<subseteq> ker\<^bsub>A,Ag_ind A f\<^esub> Agii A f
 2. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> surjec\<^bsub>A,Ag_ind A f\<^esub> Agii A f
[PROOF STEP]
apply (rule subsetI, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f); x = \<zero>\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>A\<^esub> \<in> ker\<^bsub>A,Ag_ind A f\<^esub> Agii A f
 2. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> surjec\<^bsub>A,Ag_ind A f\<^esub> Agii A f
[PROOF STEP]
apply (subst ker_def, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f); x = \<zero>\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>A\<^esub> \<in> carrier A \<and> Agii A f \<zero>\<^bsub>A\<^esub> = \<zero>\<^bsub>Ag_ind A f\<^esub>
 2. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> surjec\<^bsub>A,Ag_ind A f\<^esub> Agii A f
[PROOF STEP]
apply (simp add:aGroup.ag_inc_zero, simp add:aHom_0_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> surjec\<^bsub>A,Ag_ind A f\<^esub> Agii A f
[PROOF STEP]
apply (subst surjec_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f)\<rbrakk> \<Longrightarrow> Agii A f \<in> aHom A (Ag_ind A f) \<and> surj_to (Agii A f) (carrier A) (carrier (Ag_ind A f))
[PROOF STEP]
apply (unfold bij_to_def, frule conjunct1, fold bij_to_def, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; Agii A f \<in> aHom A (Ag_ind A f); aGroup (Ag_ind A f); surj_to f (carrier A) D\<rbrakk> \<Longrightarrow> surj_to (Agii A f) (carrier A) (carrier (Ag_ind A f))
[PROOF STEP]
apply (simp add:aGroup.Ag_ind_carrier surj_to_def Agii_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ker_subg:"\<lbrakk>aGroup F; aGroup G; f \<in> aHom F G \<rbrakk> \<Longrightarrow> F +> ker\<^bsub>F,G\<^esub> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G\<rbrakk> \<Longrightarrow> F +> ker\<^bsub>F,G\<^esub> f
[PROOF STEP]
apply (rule aGroup.asubg_test, assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G\<rbrakk> \<Longrightarrow> ker\<^bsub>F,G\<^esub> f \<subseteq> carrier F
 2. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G\<rbrakk> \<Longrightarrow> ker\<^bsub>F,G\<^esub> f \<noteq> {}
 3. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G\<rbrakk> \<Longrightarrow> \<forall>a\<in>ker\<^bsub>F,G\<^esub> f. \<forall>b\<in>ker\<^bsub>F,G\<^esub> f. a \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> b \<in> ker\<^bsub>F,G\<^esub> f
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; x \<in> ker\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> x \<in> carrier F
 2. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G\<rbrakk> \<Longrightarrow> ker\<^bsub>F,G\<^esub> f \<noteq> {}
 3. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G\<rbrakk> \<Longrightarrow> \<forall>a\<in>ker\<^bsub>F,G\<^esub> f. \<forall>b\<in>ker\<^bsub>F,G\<^esub> f. a \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> b \<in> ker\<^bsub>F,G\<^esub> f
[PROOF STEP]
apply (simp add:ker_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G\<rbrakk> \<Longrightarrow> ker\<^bsub>F,G\<^esub> f \<noteq> {}
 2. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G\<rbrakk> \<Longrightarrow> \<forall>a\<in>ker\<^bsub>F,G\<^esub> f. \<forall>b\<in>ker\<^bsub>F,G\<^esub> f. a \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> b \<in> ker\<^bsub>F,G\<^esub> f
[PROOF STEP]
apply (simp add:ker_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> carrier F \<and> f x = \<zero>\<^bsub>G\<^esub>
 2. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G\<rbrakk> \<Longrightarrow> \<forall>a\<in>ker\<^bsub>F,G\<^esub> f. \<forall>b\<in>ker\<^bsub>F,G\<^esub> f. a \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> b \<in> ker\<^bsub>F,G\<^esub> f
[PROOF STEP]
apply (frule aHom_0_0 [of "F" "G" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; f \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>G\<^esub>\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> carrier F \<and> f x = \<zero>\<^bsub>G\<^esub>
 2. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G\<rbrakk> \<Longrightarrow> \<forall>a\<in>ker\<^bsub>F,G\<^esub> f. \<forall>b\<in>ker\<^bsub>F,G\<^esub> f. a \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> b \<in> ker\<^bsub>F,G\<^esub> f
[PROOF STEP]
apply (frule aGroup.ex_zero [of "F"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; f \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>G\<^esub>; \<zero>\<^bsub>F\<^esub> \<in> carrier F\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> carrier F \<and> f x = \<zero>\<^bsub>G\<^esub>
 2. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G\<rbrakk> \<Longrightarrow> \<forall>a\<in>ker\<^bsub>F,G\<^esub> f. \<forall>b\<in>ker\<^bsub>F,G\<^esub> f. a \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> b \<in> ker\<^bsub>F,G\<^esub> f
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G\<rbrakk> \<Longrightarrow> \<forall>a\<in>ker\<^bsub>F,G\<^esub> f. \<forall>b\<in>ker\<^bsub>F,G\<^esub> f. a \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> b \<in> ker\<^bsub>F,G\<^esub> f
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; a \<in> ker\<^bsub>F,G\<^esub> f; b \<in> ker\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> a \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> b \<in> ker\<^bsub>F,G\<^esub> f
[PROOF STEP]
apply (simp add:ker_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; a \<in> carrier F \<and> f a = \<zero>\<^bsub>G\<^esub>; b \<in> carrier F \<and> f b = \<zero>\<^bsub>G\<^esub>\<rbrakk> \<Longrightarrow> a \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> b \<in> carrier F \<and> f (a \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> b) = \<zero>\<^bsub>G\<^esub>
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; a \<in> carrier F; f a = \<zero>\<^bsub>G\<^esub>; b \<in> carrier F; f b = \<zero>\<^bsub>G\<^esub>\<rbrakk> \<Longrightarrow> a \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> b \<in> carrier F \<and> f (a \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> b) = \<zero>\<^bsub>G\<^esub>
[PROOF STEP]
apply (frule_tac x = b in aGroup.ag_mOp_closed[of "F"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; a \<in> carrier F; f a = \<zero>\<^bsub>G\<^esub>; b \<in> carrier F; f b = \<zero>\<^bsub>G\<^esub>; -\<^sub>a\<^bsub>F\<^esub> b \<in> carrier F\<rbrakk> \<Longrightarrow> a \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> b \<in> carrier F \<and> f (a \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> b) = \<zero>\<^bsub>G\<^esub>
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; a \<in> carrier F; f a = \<zero>\<^bsub>G\<^esub>; b \<in> carrier F; f b = \<zero>\<^bsub>G\<^esub>; -\<^sub>a\<^bsub>F\<^esub> b \<in> carrier F\<rbrakk> \<Longrightarrow> a \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> b \<in> carrier F
 2. \<And>a b. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; a \<in> carrier F; f a = \<zero>\<^bsub>G\<^esub>; b \<in> carrier F; f b = \<zero>\<^bsub>G\<^esub>; -\<^sub>a\<^bsub>F\<^esub> b \<in> carrier F\<rbrakk> \<Longrightarrow> f (a \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> b) = \<zero>\<^bsub>G\<^esub>
[PROOF STEP]
apply (rule aGroup.ag_pOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; a \<in> carrier F; f a = \<zero>\<^bsub>G\<^esub>; b \<in> carrier F; f b = \<zero>\<^bsub>G\<^esub>; -\<^sub>a\<^bsub>F\<^esub> b \<in> carrier F\<rbrakk> \<Longrightarrow> f (a \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> b) = \<zero>\<^bsub>G\<^esub>
[PROOF STEP]
apply (simp add:aHom_add)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; a \<in> carrier F; f a = \<zero>\<^bsub>G\<^esub>; b \<in> carrier F; f b = \<zero>\<^bsub>G\<^esub>; -\<^sub>a\<^bsub>F\<^esub> b \<in> carrier F\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>G\<^esub> \<plusminus>\<^bsub>G\<^esub> f (-\<^sub>a\<^bsub>F\<^esub> b) = \<zero>\<^bsub>G\<^esub>
[PROOF STEP]
apply (simp add:aHom_inv_inv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; a \<in> carrier F; f a = \<zero>\<^bsub>G\<^esub>; b \<in> carrier F; f b = \<zero>\<^bsub>G\<^esub>; -\<^sub>a\<^bsub>F\<^esub> b \<in> carrier F\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>G\<^esub> \<plusminus>\<^bsub>G\<^esub> -\<^sub>a\<^bsub>G\<^esub> \<zero>\<^bsub>G\<^esub> = \<zero>\<^bsub>G\<^esub>
[PROOF STEP]
apply (simp add:aGroup.ag_inv_zero[of "G"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; a \<in> carrier F; f a = \<zero>\<^bsub>G\<^esub>; b \<in> carrier F; f b = \<zero>\<^bsub>G\<^esub>; -\<^sub>a\<^bsub>F\<^esub> b \<in> carrier F\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>G\<^esub> \<plusminus>\<^bsub>G\<^esub> \<zero>\<^bsub>G\<^esub> = \<zero>\<^bsub>G\<^esub>
[PROOF STEP]
apply (cut_tac aGroup.ex_zero[of "G"], simp add:aGroup.l_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; a \<in> carrier F; f a = \<zero>\<^bsub>G\<^esub>; b \<in> carrier F; f b = \<zero>\<^bsub>G\<^esub>; -\<^sub>a\<^bsub>F\<^esub> b \<in> carrier F\<rbrakk> \<Longrightarrow> aGroup G
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) ag_a_in_ar_cos:"\<lbrakk>A +> H; a \<in> carrier A\<rbrakk> \<Longrightarrow> a \<in> a \<uplus>\<^bsub>A\<^esub> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; a \<in> carrier A\<rbrakk> \<Longrightarrow> a \<in> a \<uplus>\<^bsub>A\<^esub> H
[PROOF STEP]
apply (simp add:ar_coset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; a \<in> carrier A\<rbrakk> \<Longrightarrow> a \<in> H \<bullet>\<^bsub>b_ag A\<^esub> a
[PROOF STEP]
apply (simp add:asubGroup_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ag A \<guillemotright> H ; a \<in> carrier A\<rbrakk> \<Longrightarrow> a \<in> H \<bullet>\<^bsub>b_ag A\<^esub> a
[PROOF STEP]
apply (cut_tac b_ag_group)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ag A \<guillemotright> H ; a \<in> carrier A; Group (b_ag A)\<rbrakk> \<Longrightarrow> a \<in> H \<bullet>\<^bsub>b_ag A\<^esub> a
[PROOF STEP]
apply (rule Group.a_in_rcs[of "b_ag A" "H" "a"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ag A \<guillemotright> H ; a \<in> carrier A; Group (b_ag A)\<rbrakk> \<Longrightarrow> a \<in> carrier (b_ag A)
[PROOF STEP]
apply (simp add:ag_carrier_carrier[THEN sym])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) r_cos_subset:"\<lbrakk>A +> H; X \<in> set_rcs (b_ag A) H\<rbrakk> \<Longrightarrow>
                   X \<subseteq> carrier A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; X \<in> set_rcs (b_ag A) H\<rbrakk> \<Longrightarrow> X \<subseteq> carrier A
[PROOF STEP]
apply (simp add:asubGroup_def set_rcs_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ag A \<guillemotright> H ; \<exists>a\<in>carrier (b_ag A). X = H \<bullet>\<^bsub>b_ag A\<^esub> a\<rbrakk> \<Longrightarrow> X \<subseteq> carrier A
[PROOF STEP]
apply (erule bexE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>b_ag A \<guillemotright> H ; a \<in> carrier (b_ag A); X = H \<bullet>\<^bsub>b_ag A\<^esub> a\<rbrakk> \<Longrightarrow> X \<subseteq> carrier A
[PROOF STEP]
apply (cut_tac  b_ag_group)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>b_ag A \<guillemotright> H ; a \<in> carrier (b_ag A); X = H \<bullet>\<^bsub>b_ag A\<^esub> a; Group (b_ag A)\<rbrakk> \<Longrightarrow> X \<subseteq> carrier A
[PROOF STEP]
apply (frule_tac a = a in Group.rcs_subset[of "b_ag A" "H"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>b_ag A \<guillemotright> H ; a \<in> carrier (b_ag A); X = H \<bullet>\<^bsub>b_ag A\<^esub> a; Group (b_ag A); H \<bullet>\<^bsub>b_ag A\<^esub> a \<subseteq> carrier (b_ag A)\<rbrakk> \<Longrightarrow> X \<subseteq> carrier A
[PROOF STEP]
apply (simp add:ag_carrier_carrier)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) asubg_costOp_commute:"\<lbrakk>A +> H; x \<in> set_rcs (b_ag A) H;
       y \<in> set_rcs (b_ag A) H\<rbrakk> \<Longrightarrow>
             c_top (b_ag A) H x y = c_top (b_ag A) H y x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; x \<in> set_rcs (b_ag A) H; y \<in> set_rcs (b_ag A) H\<rbrakk> \<Longrightarrow> c_top (b_ag A) H x y = c_top (b_ag A) H y x
[PROOF STEP]
apply (simp add:set_rcs_def, (erule bexE)+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa. \<lbrakk>A +> H; a \<in> carrier (b_ag A); x = H \<bullet>\<^bsub>b_ag A\<^esub> a; aa \<in> carrier (b_ag A); y = H \<bullet>\<^bsub>b_ag A\<^esub> aa\<rbrakk> \<Longrightarrow> c_top (b_ag A) H (H \<bullet>\<^bsub>b_ag A\<^esub> a) (H \<bullet>\<^bsub>b_ag A\<^esub> aa) = c_top (b_ag A) H (H \<bullet>\<^bsub>b_ag A\<^esub> aa) (H \<bullet>\<^bsub>b_ag A\<^esub> a)
[PROOF STEP]
apply (cut_tac b_ag_group)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa. \<lbrakk>A +> H; a \<in> carrier (b_ag A); x = H \<bullet>\<^bsub>b_ag A\<^esub> a; aa \<in> carrier (b_ag A); y = H \<bullet>\<^bsub>b_ag A\<^esub> aa; Group (b_ag A)\<rbrakk> \<Longrightarrow> c_top (b_ag A) H (H \<bullet>\<^bsub>b_ag A\<^esub> a) (H \<bullet>\<^bsub>b_ag A\<^esub> aa) = c_top (b_ag A) H (H \<bullet>\<^bsub>b_ag A\<^esub> aa) (H \<bullet>\<^bsub>b_ag A\<^esub> a)
[PROOF STEP]
apply (subst Group.c_top_welldef[THEN sym], assumption+,
       simp add:asubg_nsubg,
       (simp add:ag_carrier_carrier)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa. \<lbrakk>A +> H; a \<in> carrier A; x = H \<bullet>\<^bsub>b_ag A\<^esub> a; aa \<in> carrier A; y = H \<bullet>\<^bsub>b_ag A\<^esub> aa; Group (b_ag A)\<rbrakk> \<Longrightarrow> H \<bullet>\<^bsub>b_ag A\<^esub> (a \<cdot>\<^bsub>b_ag A\<^esub> aa) = c_top (b_ag A) H (H \<bullet>\<^bsub>b_ag A\<^esub> aa) (H \<bullet>\<^bsub>b_ag A\<^esub> a)
[PROOF STEP]
apply (subst Group.c_top_welldef[THEN sym], assumption+,
       simp add:asubg_nsubg,
       (simp add:ag_carrier_carrier)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa. \<lbrakk>A +> H; a \<in> carrier A; x = H \<bullet>\<^bsub>b_ag A\<^esub> a; aa \<in> carrier A; y = H \<bullet>\<^bsub>b_ag A\<^esub> aa; Group (b_ag A)\<rbrakk> \<Longrightarrow> H \<bullet>\<^bsub>b_ag A\<^esub> (a \<cdot>\<^bsub>b_ag A\<^esub> aa) = H \<bullet>\<^bsub>b_ag A\<^esub> (aa \<cdot>\<^bsub>b_ag A\<^esub> a)
[PROOF STEP]
apply (simp add:agop_gop)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa. \<lbrakk>A +> H; a \<in> carrier A; x = H \<bullet>\<^bsub>b_ag A\<^esub> a; aa \<in> carrier A; y = H \<bullet>\<^bsub>b_ag A\<^esub> aa; Group (b_ag A)\<rbrakk> \<Longrightarrow> H \<bullet>\<^bsub>b_ag A\<^esub> (a \<plusminus> aa) = H \<bullet>\<^bsub>b_ag A\<^esub> (aa \<plusminus> a)
[PROOF STEP]
apply (simp add:ag_pOp_commute)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) Subg_Qgroup:"A +> H \<Longrightarrow> aGroup (aqgrp A H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A +> H \<Longrightarrow> aGroup (aqgrp A H)
[PROOF STEP]
apply (frule asubg_nsubg[of "H"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; b_ag A \<triangleright> H\<rbrakk> \<Longrightarrow> aGroup (aqgrp A H)
[PROOF STEP]
apply (cut_tac b_ag_group)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; b_ag A \<triangleright> H; Group (b_ag A)\<rbrakk> \<Longrightarrow> aGroup (aqgrp A H)
[PROOF STEP]
apply (simp add:aGroup_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; b_ag A \<triangleright> H; Group (b_ag A)\<rbrakk> \<Longrightarrow> (\<plusminus>\<^bsub>aqgrp A H\<^esub>) \<in> carrier (aqgrp A H) \<rightarrow> carrier (aqgrp A H) \<rightarrow> carrier (aqgrp A H) \<and> (\<forall>a. a \<in> carrier (aqgrp A H) \<longrightarrow> (\<forall>b. b \<in> carrier (aqgrp A H) \<longrightarrow> (\<forall>c. c \<in> carrier (aqgrp A H) \<longrightarrow> a \<plusminus>\<^bsub>aqgrp A H\<^esub> b \<plusminus>\<^bsub>aqgrp A H\<^esub> c = a \<plusminus>\<^bsub>aqgrp A H\<^esub> (b \<plusminus>\<^bsub>aqgrp A H\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (aqgrp A H) \<longrightarrow> (\<forall>b. b \<in> carrier (aqgrp A H) \<longrightarrow> a \<plusminus>\<^bsub>aqgrp A H\<^esub> b = b \<plusminus>\<^bsub>aqgrp A H\<^esub> a)) \<and> mop (aqgrp A H) \<in> carrier (aqgrp A H) \<rightarrow> carrier (aqgrp A H) \<and> (\<forall>a. a \<in> carrier (aqgrp A H) \<longrightarrow> -\<^sub>a\<^bsub>aqgrp A H\<^esub> a \<plusminus>\<^bsub>aqgrp A H\<^esub> a = \<zero>\<^bsub>aqgrp A H\<^esub>) \<and> \<zero>\<^bsub>aqgrp A H\<^esub> \<in> carrier (aqgrp A H) \<and> (\<forall>a. a \<in> carrier (aqgrp A H) \<longrightarrow> \<zero>\<^bsub>aqgrp A H\<^esub> \<plusminus>\<^bsub>aqgrp A H\<^esub> a = a)
[PROOF STEP]
apply (simp add:aqgrp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; b_ag A \<triangleright> H; Group (b_ag A)\<rbrakk> \<Longrightarrow> c_top (b_ag A) H \<in> set_rcs (b_ag A) H \<rightarrow> set_rcs (b_ag A) H \<rightarrow> set_rcs (b_ag A) H \<and> (\<forall>a. a \<in> set_rcs (b_ag A) H \<longrightarrow> (\<forall>b. b \<in> set_rcs (b_ag A) H \<longrightarrow> (\<forall>c. c \<in> set_rcs (b_ag A) H \<longrightarrow> c_top (b_ag A) H (c_top (b_ag A) H a b) c = c_top (b_ag A) H a (c_top (b_ag A) H b c)))) \<and> (\<forall>a. a \<in> set_rcs (b_ag A) H \<longrightarrow> (\<forall>b. b \<in> set_rcs (b_ag A) H \<longrightarrow> c_top (b_ag A) H a b = c_top (b_ag A) H b a)) \<and> c_iop (b_ag A) H \<in> set_rcs (b_ag A) H \<rightarrow> set_rcs (b_ag A) H \<and> (\<forall>a. a \<in> set_rcs (b_ag A) H \<longrightarrow> c_top (b_ag A) H (c_iop (b_ag A) H a) a = H) \<and> H \<in> set_rcs (b_ag A) H \<and> (\<forall>a. a \<in> set_rcs (b_ag A) H \<longrightarrow> c_top (b_ag A) H H a = a)
[PROOF STEP]
apply (simp add:Group.Qg_top [of "b_ag A" "H"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; b_ag A \<triangleright> H; Group (b_ag A)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> set_rcs (b_ag A) H \<longrightarrow> (\<forall>b. b \<in> set_rcs (b_ag A) H \<longrightarrow> (\<forall>c. c \<in> set_rcs (b_ag A) H \<longrightarrow> c_top (b_ag A) H (c_top (b_ag A) H a b) c = c_top (b_ag A) H a (c_top (b_ag A) H b c)))) \<and> (\<forall>a. a \<in> set_rcs (b_ag A) H \<longrightarrow> (\<forall>b. b \<in> set_rcs (b_ag A) H \<longrightarrow> c_top (b_ag A) H a b = c_top (b_ag A) H b a)) \<and> c_iop (b_ag A) H \<in> set_rcs (b_ag A) H \<rightarrow> set_rcs (b_ag A) H \<and> (\<forall>a. a \<in> set_rcs (b_ag A) H \<longrightarrow> c_top (b_ag A) H (c_iop (b_ag A) H a) a = H) \<and> H \<in> set_rcs (b_ag A) H \<and> (\<forall>a. a \<in> set_rcs (b_ag A) H \<longrightarrow> c_top (b_ag A) H H a = a)
[PROOF STEP]
apply (simp add:Group.Qg_iop [of "b_ag A" "H"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; b_ag A \<triangleright> H; Group (b_ag A)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> set_rcs (b_ag A) H \<longrightarrow> (\<forall>b. b \<in> set_rcs (b_ag A) H \<longrightarrow> (\<forall>c. c \<in> set_rcs (b_ag A) H \<longrightarrow> c_top (b_ag A) H (c_top (b_ag A) H a b) c = c_top (b_ag A) H a (c_top (b_ag A) H b c)))) \<and> (\<forall>a. a \<in> set_rcs (b_ag A) H \<longrightarrow> (\<forall>b. b \<in> set_rcs (b_ag A) H \<longrightarrow> c_top (b_ag A) H a b = c_top (b_ag A) H b a)) \<and> (\<forall>a. a \<in> set_rcs (b_ag A) H \<longrightarrow> c_top (b_ag A) H (c_iop (b_ag A) H a) a = H) \<and> H \<in> set_rcs (b_ag A) H \<and> (\<forall>a. a \<in> set_rcs (b_ag A) H \<longrightarrow> c_top (b_ag A) H H a = a)
[PROOF STEP]
apply (frule Group.nsg_sg[of "b_ag A" "H"], assumption+,
        simp add:Group.unit_rcs_in_set_rcs[of "b_ag A" "H"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; b_ag A \<triangleright> H; Group (b_ag A); b_ag A \<guillemotright> H \<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> set_rcs (b_ag A) H \<longrightarrow> (\<forall>b. b \<in> set_rcs (b_ag A) H \<longrightarrow> (\<forall>c. c \<in> set_rcs (b_ag A) H \<longrightarrow> c_top (b_ag A) H (c_top (b_ag A) H a b) c = c_top (b_ag A) H a (c_top (b_ag A) H b c)))) \<and> (\<forall>a. a \<in> set_rcs (b_ag A) H \<longrightarrow> (\<forall>b. b \<in> set_rcs (b_ag A) H \<longrightarrow> c_top (b_ag A) H a b = c_top (b_ag A) H b a)) \<and> (\<forall>a. a \<in> set_rcs (b_ag A) H \<longrightarrow> c_top (b_ag A) H (c_iop (b_ag A) H a) a = H) \<and> (\<forall>a. a \<in> set_rcs (b_ag A) H \<longrightarrow> c_top (b_ag A) H H a = a)
[PROOF STEP]
apply (simp add:Group.Qg_tassoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; b_ag A \<triangleright> H; Group (b_ag A); b_ag A \<guillemotright> H \<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> set_rcs (b_ag A) H \<longrightarrow> (\<forall>b. b \<in> set_rcs (b_ag A) H \<longrightarrow> c_top (b_ag A) H a b = c_top (b_ag A) H b a)) \<and> (\<forall>a. a \<in> set_rcs (b_ag A) H \<longrightarrow> c_top (b_ag A) H (c_iop (b_ag A) H a) a = H) \<and> (\<forall>a. a \<in> set_rcs (b_ag A) H \<longrightarrow> c_top (b_ag A) H H a = a)
[PROOF STEP]
apply (simp add:asubg_costOp_commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; b_ag A \<triangleright> H; Group (b_ag A); b_ag A \<guillemotright> H \<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> set_rcs (b_ag A) H \<longrightarrow> c_top (b_ag A) H (c_iop (b_ag A) H a) a = H) \<and> (\<forall>a. a \<in> set_rcs (b_ag A) H \<longrightarrow> c_top (b_ag A) H H a = a)
[PROOF STEP]
apply (simp add:Group.Qg_i[of "b_ag A" "H"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; b_ag A \<triangleright> H; Group (b_ag A); b_ag A \<guillemotright> H \<rbrakk> \<Longrightarrow> \<forall>a. a \<in> set_rcs (b_ag A) H \<longrightarrow> c_top (b_ag A) H H a = a
[PROOF STEP]
apply (simp add:Group.Qg_unit[of "b_ag A" "H"])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) plus_subgs:"\<lbrakk>A +> H1; A +> H2\<rbrakk> \<Longrightarrow> A +> H1 \<minusplus> H2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H1; A +> H2\<rbrakk> \<Longrightarrow> A +> H1 \<minusplus> H2
[PROOF STEP]
apply (simp add:aset_sum_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H1; A +> H2\<rbrakk> \<Longrightarrow> A +> H1 \<diamondop>\<^bsub>b_ag A\<^esub> H2
[PROOF STEP]
apply (frule asubg_nsubg[of "H2"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H1; A +> H2; b_ag A \<triangleright> H2\<rbrakk> \<Longrightarrow> A +> H1 \<diamondop>\<^bsub>b_ag A\<^esub> H2
[PROOF STEP]
apply (simp add:asubGroup_def[of _ "H1"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ag A \<guillemotright> H1 ; A +> H2; b_ag A \<triangleright> H2\<rbrakk> \<Longrightarrow> A +> H1 \<diamondop>\<^bsub>b_ag A\<^esub> H2
[PROOF STEP]
apply (cut_tac "b_ag_group")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ag A \<guillemotright> H1 ; A +> H2; b_ag A \<triangleright> H2; Group (b_ag A)\<rbrakk> \<Longrightarrow> A +> H1 \<diamondop>\<^bsub>b_ag A\<^esub> H2
[PROOF STEP]
apply (frule Group.smult_sg_nsg[of "b_ag A" "H1" "H2"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ag A \<guillemotright> H1 ; A +> H2; b_ag A \<triangleright> H2; Group (b_ag A); b_ag A \<guillemotright> H1 \<diamondop>\<^bsub>b_ag A\<^esub> H2 \<rbrakk> \<Longrightarrow> A +> H1 \<diamondop>\<^bsub>b_ag A\<^esub> H2
[PROOF STEP]
apply (simp add:asubGroup_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) set_sum:"\<lbrakk>H \<subseteq> carrier A; K \<subseteq> carrier A\<rbrakk> \<Longrightarrow>
                    H \<minusplus> K = {x. \<exists>h\<in>H. \<exists>k\<in>K. x = h \<plusminus> k}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<subseteq> carrier A; K \<subseteq> carrier A\<rbrakk> \<Longrightarrow> H \<minusplus> K = {x. \<exists>h\<in>H. \<exists>k\<in>K. x = h \<plusminus> k}
[PROOF STEP]
apply (cut_tac b_ag_group)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<subseteq> carrier A; K \<subseteq> carrier A; Group (b_ag A)\<rbrakk> \<Longrightarrow> H \<minusplus> K = {x. \<exists>h\<in>H. \<exists>k\<in>K. x = h \<plusminus> k}
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>H \<subseteq> carrier A; K \<subseteq> carrier A; Group (b_ag A)\<rbrakk> \<Longrightarrow> H \<minusplus> K \<subseteq> {x. \<exists>h\<in>H. \<exists>k\<in>K. x = h \<plusminus> k}
 2. \<lbrakk>H \<subseteq> carrier A; K \<subseteq> carrier A; Group (b_ag A)\<rbrakk> \<Longrightarrow> {x. \<exists>h\<in>H. \<exists>k\<in>K. x = h \<plusminus> k} \<subseteq> H \<minusplus> K
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>H \<subseteq> carrier A; K \<subseteq> carrier A; Group (b_ag A); x \<in> H \<minusplus> K\<rbrakk> \<Longrightarrow> x \<in> {x. \<exists>h\<in>H. \<exists>k\<in>K. x = h \<plusminus> k}
 2. \<lbrakk>H \<subseteq> carrier A; K \<subseteq> carrier A; Group (b_ag A)\<rbrakk> \<Longrightarrow> {x. \<exists>h\<in>H. \<exists>k\<in>K. x = h \<plusminus> k} \<subseteq> H \<minusplus> K
[PROOF STEP]
apply (simp add:aset_sum_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>H \<subseteq> carrier A; K \<subseteq> carrier A; Group (b_ag A); x \<in> H \<diamondop>\<^bsub>b_ag A\<^esub> K\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. \<exists>k\<in>K. x = h \<plusminus> k
 2. \<lbrakk>H \<subseteq> carrier A; K \<subseteq> carrier A; Group (b_ag A)\<rbrakk> \<Longrightarrow> {x. \<exists>h\<in>H. \<exists>k\<in>K. x = h \<plusminus> k} \<subseteq> H \<minusplus> K
[PROOF STEP]
apply (simp add:agop_gop[THEN sym] s_top_def, (erule bexE)+,
        frule sym, thin_tac "xa \<cdot>\<^bsub>b_ag A\<^esub> y = x", simp, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<subseteq> carrier A; K \<subseteq> carrier A; Group (b_ag A)\<rbrakk> \<Longrightarrow> {x. \<exists>h\<in>H. \<exists>k\<in>K. x = h \<plusminus> k} \<subseteq> H \<minusplus> K
[PROOF STEP]
apply (rule subsetI, simp add:aset_sum_def, (erule bexE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x h k. \<lbrakk>H \<subseteq> carrier A; K \<subseteq> carrier A; Group (b_ag A); h \<in> H; k \<in> K; x = h \<plusminus> k\<rbrakk> \<Longrightarrow> x \<in> H \<diamondop>\<^bsub>b_ag A\<^esub> K
[PROOF STEP]
apply (frule_tac c = h in subsetD[of H "carrier A"], assumption+,
        frule_tac c = k in subsetD[of K "carrier A"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x h k. \<lbrakk>H \<subseteq> carrier A; K \<subseteq> carrier A; Group (b_ag A); h \<in> H; k \<in> K; x = h \<plusminus> k; h \<in> carrier A; k \<in> carrier A\<rbrakk> \<Longrightarrow> x \<in> H \<diamondop>\<^bsub>b_ag A\<^esub> K
[PROOF STEP]
apply (simp add:agop_gop[THEN sym], simp add:s_top_def, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) mem_set_sum:"\<lbrakk>H \<subseteq> carrier A; K \<subseteq> carrier A;
                  x \<in> H \<minusplus> K \<rbrakk> \<Longrightarrow> \<exists>h\<in>H. \<exists>k\<in>K. x = h \<plusminus> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<subseteq> carrier A; K \<subseteq> carrier A; x \<in> H \<minusplus> K\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. \<exists>k\<in>K. x = h \<plusminus> k
[PROOF STEP]
by (simp add:set_sum)


[STATEMENT]
lemma (in aGroup) mem_sum_subgs:"\<lbrakk>A +> H; A +> K; h \<in> H; k \<in> K\<rbrakk> \<Longrightarrow>
                    h \<plusminus> k \<in> H \<minusplus> K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; A +> K; h \<in> H; k \<in> K\<rbrakk> \<Longrightarrow> h \<plusminus> k \<in> H \<minusplus> K
[PROOF STEP]
apply (frule asubg_subset[of H],
       frule asubg_subset[of K],
       simp add:set_sum, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) aqgrp_carrier:"A +> H \<Longrightarrow>
                   set_rcs (b_ag A ) H = set_ar_cos A H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A +> H \<Longrightarrow> set_rcs (b_ag A) H = set_ar_cos A H
[PROOF STEP]
apply (simp add:set_ar_cos_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A +> H \<Longrightarrow> set_rcs (b_ag A) H = {X. \<exists>a\<in>carrier A. X = a \<uplus>\<^bsub>A\<^esub> H}
[PROOF STEP]
apply (simp add:ag_carrier_carrier [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A +> H \<Longrightarrow> set_rcs (b_ag A) H = {X. \<exists>a\<in>carrier (b_ag A). X = a \<uplus>\<^bsub>A\<^esub> H}
[PROOF STEP]
apply (simp add:ar_coset_def set_rcs_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) unit_in_set_ar_cos:"A +> H \<Longrightarrow> H \<in> set_ar_cos A H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A +> H \<Longrightarrow> H \<in> set_ar_cos A H
[PROOF STEP]
apply (simp add:aqgrp_carrier[THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A +> H \<Longrightarrow> H \<in> set_rcs (b_ag A) H
[PROOF STEP]
apply (cut_tac b_ag_group)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; Group (b_ag A)\<rbrakk> \<Longrightarrow> H \<in> set_rcs (b_ag A) H
[PROOF STEP]
apply (simp add:asubGroup_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ag A \<guillemotright> H ; Group (b_ag A)\<rbrakk> \<Longrightarrow> H \<in> set_rcs (b_ag A) H
[PROOF STEP]
apply (simp add:Group.unit_rcs_in_set_rcs[of "b_ag A" "H"])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) aqgrp_pOp_maps:"\<lbrakk>A +> H; a \<in> carrier A; b \<in> carrier A\<rbrakk> \<Longrightarrow>
      pop (aqgrp A H) (a \<uplus>\<^bsub>A\<^esub> H) (b \<uplus>\<^bsub>A\<^esub> H) = (a \<plusminus> b) \<uplus>\<^bsub>A\<^esub> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; a \<in> carrier A; b \<in> carrier A\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>A\<^esub> H \<plusminus>\<^bsub>aqgrp A H\<^esub> b \<uplus>\<^bsub>A\<^esub> H = (a \<plusminus> b) \<uplus>\<^bsub>A\<^esub> H
[PROOF STEP]
apply (simp add:aqgrp_def ar_coset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; a \<in> carrier A; b \<in> carrier A\<rbrakk> \<Longrightarrow> c_top (b_ag A) H (H \<bullet>\<^bsub>b_ag A\<^esub> a) (H \<bullet>\<^bsub>b_ag A\<^esub> b) = H \<bullet>\<^bsub>b_ag A\<^esub> (a \<plusminus> b)
[PROOF STEP]
apply (cut_tac b_ag_group)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; a \<in> carrier A; b \<in> carrier A; Group (b_ag A)\<rbrakk> \<Longrightarrow> c_top (b_ag A) H (H \<bullet>\<^bsub>b_ag A\<^esub> a) (H \<bullet>\<^bsub>b_ag A\<^esub> b) = H \<bullet>\<^bsub>b_ag A\<^esub> (a \<plusminus> b)
[PROOF STEP]
apply (frule asubg_nsubg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; a \<in> carrier A; b \<in> carrier A; Group (b_ag A); b_ag A \<triangleright> H\<rbrakk> \<Longrightarrow> c_top (b_ag A) H (H \<bullet>\<^bsub>b_ag A\<^esub> a) (H \<bullet>\<^bsub>b_ag A\<^esub> b) = H \<bullet>\<^bsub>b_ag A\<^esub> (a \<plusminus> b)
[PROOF STEP]
apply (simp add:ag_carrier_carrier [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; a \<in> carrier (b_ag A); b \<in> carrier (b_ag A); Group (b_ag A); b_ag A \<triangleright> H\<rbrakk> \<Longrightarrow> c_top (b_ag A) H (H \<bullet>\<^bsub>b_ag A\<^esub> a) (H \<bullet>\<^bsub>b_ag A\<^esub> b) = H \<bullet>\<^bsub>b_ag A\<^esub> (a \<plusminus> b)
[PROOF STEP]
apply (subst Group.c_top_welldef [THEN sym], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; a \<in> carrier (b_ag A); b \<in> carrier (b_ag A); Group (b_ag A); b_ag A \<triangleright> H\<rbrakk> \<Longrightarrow> H \<bullet>\<^bsub>b_ag A\<^esub> (a \<cdot>\<^bsub>b_ag A\<^esub> b) = H \<bullet>\<^bsub>b_ag A\<^esub> (a \<plusminus> b)
[PROOF STEP]
apply (simp add:agop_gop)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) aqgrp_mOp_maps:"\<lbrakk>A +> H; a \<in> carrier A\<rbrakk> \<Longrightarrow>
                   mop (aqgrp A H) (a \<uplus>\<^bsub>A\<^esub> H) = (-\<^sub>a a) \<uplus>\<^bsub>A\<^esub> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; a \<in> carrier A\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>aqgrp A H\<^esub> a \<uplus>\<^bsub>A\<^esub> H = (-\<^sub>a a) \<uplus>\<^bsub>A\<^esub> H
[PROOF STEP]
apply (simp add:aqgrp_def ar_coset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; a \<in> carrier A\<rbrakk> \<Longrightarrow> c_iop (b_ag A) H (H \<bullet>\<^bsub>b_ag A\<^esub> a) = H \<bullet>\<^bsub>b_ag A\<^esub> (-\<^sub>a a)
[PROOF STEP]
apply (cut_tac b_ag_group)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; a \<in> carrier A; Group (b_ag A)\<rbrakk> \<Longrightarrow> c_iop (b_ag A) H (H \<bullet>\<^bsub>b_ag A\<^esub> a) = H \<bullet>\<^bsub>b_ag A\<^esub> (-\<^sub>a a)
[PROOF STEP]
apply (frule asubg_nsubg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; a \<in> carrier A; Group (b_ag A); b_ag A \<triangleright> H\<rbrakk> \<Longrightarrow> c_iop (b_ag A) H (H \<bullet>\<^bsub>b_ag A\<^esub> a) = H \<bullet>\<^bsub>b_ag A\<^esub> (-\<^sub>a a)
[PROOF STEP]
apply (simp add:ag_carrier_carrier [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; a \<in> carrier (b_ag A); Group (b_ag A); b_ag A \<triangleright> H\<rbrakk> \<Longrightarrow> c_iop (b_ag A) H (H \<bullet>\<^bsub>b_ag A\<^esub> a) = H \<bullet>\<^bsub>b_ag A\<^esub> (-\<^sub>a a)
[PROOF STEP]
apply (subst Group.c_iop_welldef, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; a \<in> carrier (b_ag A); Group (b_ag A); b_ag A \<triangleright> H\<rbrakk> \<Longrightarrow> H \<bullet>\<^bsub>b_ag A\<^esub> \<rho>\<^bsub>b_ag A\<^esub> a = H \<bullet>\<^bsub>b_ag A\<^esub> (-\<^sub>a a)
[PROOF STEP]
apply (simp add:agiop_giop)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) aqgrp_zero:"A +> H \<Longrightarrow> zero (aqgrp A H) = H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A +> H \<Longrightarrow> \<zero>\<^bsub>aqgrp A H\<^esub> = H
[PROOF STEP]
apply (simp add:aqgrp_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) arcos_fixed:"\<lbrakk>A +> H; a \<in> carrier A; h \<in> H \<rbrakk> \<Longrightarrow>
                              a \<uplus>\<^bsub>A\<^esub> H = (h \<plusminus> a) \<uplus>\<^bsub>A\<^esub> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; a \<in> carrier A; h \<in> H\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>A\<^esub> H = (h \<plusminus> a) \<uplus>\<^bsub>A\<^esub> H
[PROOF STEP]
apply (cut_tac b_ag_group)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; a \<in> carrier A; h \<in> H; Group (b_ag A)\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>A\<^esub> H = (h \<plusminus> a) \<uplus>\<^bsub>A\<^esub> H
[PROOF STEP]
apply (simp add:agop_gop[THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; a \<in> carrier A; h \<in> H; Group (b_ag A)\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>A\<^esub> H = h \<cdot>\<^bsub>b_ag A\<^esub> a \<uplus>\<^bsub>A\<^esub> H
[PROOF STEP]
apply (simp add:ag_carrier_carrier[THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; a \<in> carrier (b_ag A); h \<in> H; Group (b_ag A)\<rbrakk> \<Longrightarrow> a \<uplus>\<^bsub>A\<^esub> H = h \<cdot>\<^bsub>b_ag A\<^esub> a \<uplus>\<^bsub>A\<^esub> H
[PROOF STEP]
apply (simp add:ar_coset_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A +> H; a \<in> carrier (b_ag A); h \<in> H; Group (b_ag A)\<rbrakk> \<Longrightarrow> H \<bullet>\<^bsub>b_ag A\<^esub> a = H \<bullet>\<^bsub>b_ag A\<^esub> (h \<cdot>\<^bsub>b_ag A\<^esub> a)
[PROOF STEP]
apply (simp add:asubGroup_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b_ag A \<guillemotright> H ; a \<in> carrier (b_ag A); h \<in> H; Group (b_ag A)\<rbrakk> \<Longrightarrow> H \<bullet>\<^bsub>b_ag A\<^esub> a = H \<bullet>\<^bsub>b_ag A\<^esub> (h \<cdot>\<^bsub>b_ag A\<^esub> a)
[PROOF STEP]
apply (simp add:Group.rcs_fixed1[of "b_ag A" "H"])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prodag_comp_i:"\<lbrakk>a \<in> carr_prodag I A; i \<in> I\<rbrakk> \<Longrightarrow> (a i) \<in> carrier (A i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carr_prodag I A; i \<in> I\<rbrakk> \<Longrightarrow> a i \<in> carrier (A i)
[PROOF STEP]
by (simp add:carr_prodag_def)


[STATEMENT]
lemma prod_pOp_func:"\<forall>k\<in>I. aGroup (A k) \<Longrightarrow>
    prod_pOp I A \<in> carr_prodag I A \<rightarrow> carr_prodag I A \<rightarrow> carr_prodag I A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> prod_pOp I A \<in> carr_prodag I A \<rightarrow> carr_prodag I A \<rightarrow> carr_prodag I A
[PROOF STEP]
apply (rule Pi_I)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_prodag I A; xa \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_pOp I A x xa \<in> carr_prodag I A
[PROOF STEP]
apply(rename_tac a b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_pOp I A a b \<in> carr_prodag I A
[PROOF STEP]
apply (subst carr_prodag_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_pOp I A a b \<in> {f \<in> extensional I. f \<in> I \<rightarrow> Un_carrier I A \<and> (\<forall>i\<in>I. f i \<in> carrier (A i))}
[PROOF STEP]
apply (simp add:CollectI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_pOp I A a b \<in> extensional I \<and> prod_pOp I A a b \<in> I \<rightarrow> Un_carrier I A \<and> (\<forall>i\<in>I. prod_pOp I A a b i \<in> carrier (A i))
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_pOp I A a b \<in> extensional I
 2. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_pOp I A a b \<in> I \<rightarrow> Un_carrier I A \<and> (\<forall>i\<in>I. prod_pOp I A a b i \<in> carrier (A i))
[PROOF STEP]
apply (simp add:prod_pOp_def restrict_def extensional_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_pOp I A a b \<in> I \<rightarrow> Un_carrier I A \<and> (\<forall>i\<in>I. prod_pOp I A a b i \<in> carrier (A i))
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_pOp I A a b \<in> I \<rightarrow> Un_carrier I A
 2. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. prod_pOp I A a b i \<in> carrier (A i)
[PROOF STEP]
apply (rule Pi_I)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A; x \<in> I\<rbrakk> \<Longrightarrow> prod_pOp I A a b x \<in> Un_carrier I A
 2. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. prod_pOp I A a b i \<in> carrier (A i)
[PROOF STEP]
apply (simp add:prod_pOp_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A; x \<in> I\<rbrakk> \<Longrightarrow> a x \<plusminus>\<^bsub>A x\<^esub> b x \<in> Un_carrier I A
 2. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. prod_pOp I A a b i \<in> carrier (A i)
[PROOF STEP]
apply (subst Un_carrier_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A; x \<in> I\<rbrakk> \<Longrightarrow> a x \<plusminus>\<^bsub>A x\<^esub> b x \<in> \<Union> {X. \<exists>i\<in>I. X = carrier (A i)}
 2. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. prod_pOp I A a b i \<in> carrier (A i)
[PROOF STEP]
apply (simp add:CollectI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A; x \<in> I\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>i\<in>I. xa = carrier (A i)) \<and> a x \<plusminus>\<^bsub>A x\<^esub> b x \<in> xa
 2. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. prod_pOp I A a b i \<in> carrier (A i)
[PROOF STEP]
apply (frule_tac x = x in bspec, assumption,
        thin_tac "\<forall>k\<in>I. aGroup (A k)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b x. \<lbrakk>a \<in> carr_prodag I A; b \<in> carr_prodag I A; x \<in> I; aGroup (A x)\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>i\<in>I. xa = carrier (A i)) \<and> a x \<plusminus>\<^bsub>A x\<^esub> b x \<in> xa
 2. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. prod_pOp I A a b i \<in> carrier (A i)
[PROOF STEP]
apply (simp add:carr_prodag_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b x. \<lbrakk>a \<in> extensional I \<and> a \<in> I \<rightarrow> Un_carrier I A \<and> (\<forall>i\<in>I. a i \<in> carrier (A i)); b \<in> extensional I \<and> b \<in> I \<rightarrow> Un_carrier I A \<and> (\<forall>i\<in>I. b i \<in> carrier (A i)); x \<in> I; aGroup (A x)\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>i\<in>I. xa = carrier (A i)) \<and> a x \<plusminus>\<^bsub>A x\<^esub> b x \<in> xa
 2. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. prod_pOp I A a b i \<in> carrier (A i)
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b x. \<lbrakk>x \<in> I; aGroup (A x); a \<in> extensional I; b \<in> extensional I; a \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. a i \<in> carrier (A i); b \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. b i \<in> carrier (A i)\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>i\<in>I. xa = carrier (A i)) \<and> a x \<plusminus>\<^bsub>A x\<^esub> b x \<in> xa
 2. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. prod_pOp I A a b i \<in> carrier (A i)
[PROOF STEP]
apply (thin_tac "a \<in> I \<rightarrow> Un_carrier I A")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b x. \<lbrakk>x \<in> I; aGroup (A x); a \<in> extensional I; b \<in> extensional I; \<forall>i\<in>I. a i \<in> carrier (A i); b \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. b i \<in> carrier (A i)\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>i\<in>I. xa = carrier (A i)) \<and> a x \<plusminus>\<^bsub>A x\<^esub> b x \<in> xa
 2. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. prod_pOp I A a b i \<in> carrier (A i)
[PROOF STEP]
apply (thin_tac "b \<in> I \<rightarrow> Un_carrier I A")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b x. \<lbrakk>x \<in> I; aGroup (A x); a \<in> extensional I; b \<in> extensional I; \<forall>i\<in>I. a i \<in> carrier (A i); \<forall>i\<in>I. b i \<in> carrier (A i)\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>i\<in>I. xa = carrier (A i)) \<and> a x \<plusminus>\<^bsub>A x\<^esub> b x \<in> xa
 2. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. prod_pOp I A a b i \<in> carrier (A i)
[PROOF STEP]
apply (frule_tac x = x in bspec, assumption,
        thin_tac "\<forall>i\<in>I. a i \<in> carrier (A i)",
        frule_tac x = x in bspec, assumption,
        thin_tac "\<forall>i\<in>I. b i \<in> carrier (A i)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b x. \<lbrakk>x \<in> I; aGroup (A x); a \<in> extensional I; b \<in> extensional I; a x \<in> carrier (A x); b x \<in> carrier (A x)\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>i\<in>I. xa = carrier (A i)) \<and> a x \<plusminus>\<^bsub>A x\<^esub> b x \<in> xa
 2. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. prod_pOp I A a b i \<in> carrier (A i)
[PROOF STEP]
apply (frule_tac x = "a x" and y = "b x" in aGroup.ag_pOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b x. \<lbrakk>x \<in> I; aGroup (A x); a \<in> extensional I; b \<in> extensional I; a x \<in> carrier (A x); b x \<in> carrier (A x); a x \<plusminus>\<^bsub>A x\<^esub> b x \<in> carrier (A x)\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>i\<in>I. xa = carrier (A i)) \<and> a x \<plusminus>\<^bsub>A x\<^esub> b x \<in> xa
 2. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. prod_pOp I A a b i \<in> carrier (A i)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. prod_pOp I A a b i \<in> carrier (A i)
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b i. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A; i \<in> I\<rbrakk> \<Longrightarrow> prod_pOp I A a b i \<in> carrier (A i)
[PROOF STEP]
apply (simp add:prod_pOp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b i. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A; i \<in> I\<rbrakk> \<Longrightarrow> a i \<plusminus>\<^bsub>A i\<^esub> b i \<in> carrier (A i)
[PROOF STEP]
apply (rule_tac A = "A i" and x = "a i" and y = "b i" in aGroup.ag_pOp_closed)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b i. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A; i \<in> I\<rbrakk> \<Longrightarrow> aGroup (A i)
 2. \<And>a b i. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A; i \<in> I\<rbrakk> \<Longrightarrow> a i \<in> carrier (A i)
 3. \<And>a b i. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A; i \<in> I\<rbrakk> \<Longrightarrow> b i \<in> carrier (A i)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b i. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A; i \<in> I\<rbrakk> \<Longrightarrow> a i \<in> carrier (A i)
 2. \<And>a b i. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A; i \<in> I\<rbrakk> \<Longrightarrow> b i \<in> carrier (A i)
[PROOF STEP]
apply (simp add:carr_prodag_def)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prod_pOp_mem:"\<lbrakk>\<forall>k\<in>I. aGroup (A k); X \<in> carr_prodag I A;
 Y \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_pOp I A X Y \<in> carr_prodag I A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); X \<in> carr_prodag I A; Y \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_pOp I A X Y \<in> carr_prodag I A
[PROOF STEP]
apply (frule prod_pOp_func)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); X \<in> carr_prodag I A; Y \<in> carr_prodag I A; prod_pOp I A \<in> carr_prodag I A \<rightarrow> carr_prodag I A \<rightarrow> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_pOp I A X Y \<in> carr_prodag I A
[PROOF STEP]
apply (frule funcset_mem[of "prod_pOp I A"
                        "carr_prodag I A" "carr_prodag I A \<rightarrow> carr_prodag I A"
                         "X"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); X \<in> carr_prodag I A; Y \<in> carr_prodag I A; prod_pOp I A \<in> carr_prodag I A \<rightarrow> carr_prodag I A \<rightarrow> carr_prodag I A; prod_pOp I A X \<in> carr_prodag I A \<rightarrow> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_pOp I A X Y \<in> carr_prodag I A
[PROOF STEP]
apply (rule funcset_mem[of "prod_pOp I A X" "carr_prodag I A"
                           "carr_prodag I A" "Y"], assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prod_pOp_mem_i:"\<lbrakk>\<forall>k\<in>I. aGroup (A k); X \<in> carr_prodag I A;
 Y \<in> carr_prodag I A; i \<in> I\<rbrakk> \<Longrightarrow> prod_pOp I A X Y i = (X i) \<plusminus>\<^bsub>(A i)\<^esub> (Y i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); X \<in> carr_prodag I A; Y \<in> carr_prodag I A; i \<in> I\<rbrakk> \<Longrightarrow> prod_pOp I A X Y i = X i \<plusminus>\<^bsub>A i\<^esub> Y i
[PROOF STEP]
apply (simp add:prod_pOp_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prod_mOp_func:"\<forall>k\<in>I. aGroup (A k) \<Longrightarrow>
                  prod_mOp I A \<in> carr_prodag I A \<rightarrow> carr_prodag I A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> prod_mOp I A \<in> carr_prodag I A \<rightarrow> carr_prodag I A
[PROOF STEP]
apply (rule Pi_I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_mOp I A x \<in> carr_prodag I A
[PROOF STEP]
apply (simp add:prod_mOp_def carr_prodag_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> extensional I \<and> x \<in> I \<rightarrow> Un_carrier I A \<and> (\<forall>i\<in>I. x i \<in> carrier (A i))\<rbrakk> \<Longrightarrow> (\<lambda>xa\<in>I. -\<^sub>a\<^bsub>A xa\<^esub> x xa) \<in> I \<rightarrow> Un_carrier I A \<and> (\<forall>i\<in>I. -\<^sub>a\<^bsub>A i\<^esub> x i \<in> carrier (A i))
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> extensional I; x \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. x i \<in> carrier (A i)\<rbrakk> \<Longrightarrow> (\<lambda>xa\<in>I. -\<^sub>a\<^bsub>A xa\<^esub> x xa) \<in> I \<rightarrow> Un_carrier I A \<and> (\<forall>i\<in>I. -\<^sub>a\<^bsub>A i\<^esub> x i \<in> carrier (A i))
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> extensional I; x \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. x i \<in> carrier (A i)\<rbrakk> \<Longrightarrow> (\<lambda>xa\<in>I. -\<^sub>a\<^bsub>A xa\<^esub> x xa) \<in> I \<rightarrow> Un_carrier I A
 2. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> extensional I; x \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. x i \<in> carrier (A i)\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. -\<^sub>a\<^bsub>A i\<^esub> x i \<in> carrier (A i)
[PROOF STEP]
apply (rule Pi_I)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> extensional I; x \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. x i \<in> carrier (A i); xa \<in> I\<rbrakk> \<Longrightarrow> (\<lambda>xa\<in>I. -\<^sub>a\<^bsub>A xa\<^esub> x xa) xa \<in> Un_carrier I A
 2. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> extensional I; x \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. x i \<in> carrier (A i)\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. -\<^sub>a\<^bsub>A i\<^esub> x i \<in> carrier (A i)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> extensional I; x \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. x i \<in> carrier (A i); xa \<in> I\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>A xa\<^esub> x xa \<in> Un_carrier I A
 2. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> extensional I; x \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. x i \<in> carrier (A i)\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. -\<^sub>a\<^bsub>A i\<^esub> x i \<in> carrier (A i)
[PROOF STEP]
apply (rename_tac f j)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f j. \<lbrakk>\<forall>k\<in>I. aGroup (A k); f \<in> extensional I; f \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. f i \<in> carrier (A i); j \<in> I\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>A j\<^esub> f j \<in> Un_carrier I A
 2. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> extensional I; x \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. x i \<in> carrier (A i)\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. -\<^sub>a\<^bsub>A i\<^esub> x i \<in> carrier (A i)
[PROOF STEP]
apply (frule_tac f = f and x = j in funcset_mem [of _ "I" "Un_carrier I A"],
                             assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f j. \<lbrakk>\<forall>k\<in>I. aGroup (A k); f \<in> extensional I; f \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. f i \<in> carrier (A i); j \<in> I; f j \<in> Un_carrier I A\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>A j\<^esub> f j \<in> Un_carrier I A
 2. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> extensional I; x \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. x i \<in> carrier (A i)\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. -\<^sub>a\<^bsub>A i\<^esub> x i \<in> carrier (A i)
[PROOF STEP]
apply (thin_tac "f \<in> I \<rightarrow> Un_carrier I A")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f j. \<lbrakk>\<forall>k\<in>I. aGroup (A k); f \<in> extensional I; \<forall>i\<in>I. f i \<in> carrier (A i); j \<in> I; f j \<in> Un_carrier I A\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>A j\<^esub> f j \<in> Un_carrier I A
 2. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> extensional I; x \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. x i \<in> carrier (A i)\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. -\<^sub>a\<^bsub>A i\<^esub> x i \<in> carrier (A i)
[PROOF STEP]
apply (frule_tac x = j in bspec, assumption,
        thin_tac "\<forall>k\<in>I. aGroup (A k)",
        frule_tac x = j in bspec, assumption,
        thin_tac "\<forall>i\<in>I. f i \<in> carrier (A i)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f j. \<lbrakk>f \<in> extensional I; j \<in> I; f j \<in> Un_carrier I A; aGroup (A j); f j \<in> carrier (A j)\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>A j\<^esub> f j \<in> Un_carrier I A
 2. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> extensional I; x \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. x i \<in> carrier (A i)\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. -\<^sub>a\<^bsub>A i\<^esub> x i \<in> carrier (A i)
[PROOF STEP]
apply (thin_tac "f j \<in> Un_carrier I A")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f j. \<lbrakk>f \<in> extensional I; j \<in> I; aGroup (A j); f j \<in> carrier (A j)\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>A j\<^esub> f j \<in> Un_carrier I A
 2. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> extensional I; x \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. x i \<in> carrier (A i)\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. -\<^sub>a\<^bsub>A i\<^esub> x i \<in> carrier (A i)
[PROOF STEP]
apply (simp add:Un_carrier_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f j. \<lbrakk>f \<in> extensional I; j \<in> I; aGroup (A j); f j \<in> carrier (A j)\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>i\<in>I. x = carrier (A i)) \<and> -\<^sub>a\<^bsub>A j\<^esub> f j \<in> x
 2. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> extensional I; x \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. x i \<in> carrier (A i)\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. -\<^sub>a\<^bsub>A i\<^esub> x i \<in> carrier (A i)
[PROOF STEP]
apply (frule aGroup.ag_mOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f j. \<lbrakk>f \<in> extensional I; j \<in> I; aGroup (A j); f j \<in> carrier (A j); -\<^sub>a\<^bsub>A j\<^esub> f j \<in> carrier (A j)\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>i\<in>I. x = carrier (A i)) \<and> -\<^sub>a\<^bsub>A j\<^esub> f j \<in> x
 2. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> extensional I; x \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. x i \<in> carrier (A i)\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. -\<^sub>a\<^bsub>A i\<^esub> x i \<in> carrier (A i)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> extensional I; x \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. x i \<in> carrier (A i)\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. -\<^sub>a\<^bsub>A i\<^esub> x i \<in> carrier (A i)
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> extensional I; x \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. x i \<in> carrier (A i); i \<in> I\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>A i\<^esub> x i \<in> carrier (A i)
[PROOF STEP]
apply (rule_tac A = "A i" and x = "x i" in aGroup.ag_mOp_closed)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x i. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> extensional I; x \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. x i \<in> carrier (A i); i \<in> I\<rbrakk> \<Longrightarrow> aGroup (A i)
 2. \<And>x i. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> extensional I; x \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. x i \<in> carrier (A i); i \<in> I\<rbrakk> \<Longrightarrow> x i \<in> carrier (A i)
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prod_mOp_mem:"\<lbrakk>\<forall>j\<in>I. aGroup (A j); X \<in> carr_prodag I A\<rbrakk> \<Longrightarrow>
                         prod_mOp I A X \<in> carr_prodag I A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); X \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_mOp I A X \<in> carr_prodag I A
[PROOF STEP]
apply (frule prod_mOp_func)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); X \<in> carr_prodag I A; prod_mOp I A \<in> carr_prodag I A \<rightarrow> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_mOp I A X \<in> carr_prodag I A
[PROOF STEP]
apply (simp add:Pi_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prod_mOp_mem_i:"\<lbrakk>\<forall>j\<in>I. aGroup (A j); X \<in> carr_prodag I A; i \<in> I\<rbrakk> \<Longrightarrow>
                         prod_mOp I A X i = -\<^sub>a\<^bsub>(A i)\<^esub> (X i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); X \<in> carr_prodag I A; i \<in> I\<rbrakk> \<Longrightarrow> prod_mOp I A X i = -\<^sub>a\<^bsub>A i\<^esub> X i
[PROOF STEP]
apply (simp add:prod_mOp_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prod_zero_func:"\<forall>k\<in>I. aGroup (A k) \<Longrightarrow>
                           prod_zero I A \<in> carr_prodag I A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> prod_zero I A \<in> carr_prodag I A
[PROOF STEP]
apply (simp add:prod_zero_def prodag_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> (\<lambda>x\<in>I. \<zero>\<^bsub>A x\<^esub>) \<in> carr_prodag I A
[PROOF STEP]
apply (simp add:carr_prodag_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> (\<lambda>x\<in>I. \<zero>\<^bsub>A x\<^esub>) \<in> I \<rightarrow> Un_carrier I A \<and> (\<forall>i\<in>I. \<zero>\<^bsub>A i\<^esub> \<in> carrier (A i))
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> (\<lambda>x\<in>I. \<zero>\<^bsub>A x\<^esub>) \<in> I \<rightarrow> Un_carrier I A
 2. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<forall>i\<in>I. \<zero>\<^bsub>A i\<^esub> \<in> carrier (A i)
[PROOF STEP]
apply (rule Pi_I)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> I\<rbrakk> \<Longrightarrow> (\<lambda>x\<in>I. \<zero>\<^bsub>A x\<^esub>) x \<in> Un_carrier I A
 2. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<forall>i\<in>I. \<zero>\<^bsub>A i\<^esub> \<in> carrier (A i)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> I\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>A x\<^esub> \<in> Un_carrier I A
 2. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<forall>i\<in>I. \<zero>\<^bsub>A i\<^esub> \<in> carrier (A i)
[PROOF STEP]
apply (subgoal_tac "aGroup (A x)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> I; aGroup (A x)\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>A x\<^esub> \<in> Un_carrier I A
 2. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> I\<rbrakk> \<Longrightarrow> aGroup (A x)
 3. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<forall>i\<in>I. \<zero>\<^bsub>A i\<^esub> \<in> carrier (A i)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> I\<rbrakk> \<Longrightarrow> aGroup (A x)
 2. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> I; aGroup (A x)\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>A x\<^esub> \<in> Un_carrier I A
 3. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<forall>i\<in>I. \<zero>\<^bsub>A i\<^esub> \<in> carrier (A i)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> I; aGroup (A x)\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>A x\<^esub> \<in> Un_carrier I A
 2. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<forall>i\<in>I. \<zero>\<^bsub>A i\<^esub> \<in> carrier (A i)
[PROOF STEP]
apply (thin_tac "\<forall>k\<in>I. aGroup (A k)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> I; aGroup (A x)\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>A x\<^esub> \<in> Un_carrier I A
 2. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<forall>i\<in>I. \<zero>\<^bsub>A i\<^esub> \<in> carrier (A i)
[PROOF STEP]
apply (simp add:Un_carrier_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> I; aGroup (A x)\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>i\<in>I. xa = carrier (A i)) \<and> \<zero>\<^bsub>A x\<^esub> \<in> xa
 2. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<forall>i\<in>I. \<zero>\<^bsub>A i\<^esub> \<in> carrier (A i)
[PROOF STEP]
apply (frule aGroup.ex_zero)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> I; aGroup (A x); \<zero>\<^bsub>A x\<^esub> \<in> carrier (A x)\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>i\<in>I. xa = carrier (A i)) \<and> \<zero>\<^bsub>A x\<^esub> \<in> xa
 2. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<forall>i\<in>I. \<zero>\<^bsub>A i\<^esub> \<in> carrier (A i)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<forall>k\<in>I. aGroup (A k); i \<in> I\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>A i\<^esub> \<in> carrier (A i)
[PROOF STEP]
apply (frule_tac x = i in bspec, assumption,
       thin_tac "\<forall>k\<in>I. aGroup (A k)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>i \<in> I; aGroup (A i)\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>A i\<^esub> \<in> carrier (A i)
[PROOF STEP]
apply (simp add:aGroup.ex_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prod_zero_i:"\<lbrakk>\<forall>k\<in>I. aGroup (A k); i \<in> I\<rbrakk> \<Longrightarrow>
                           prod_zero I A i = \<zero>\<^bsub>(A i)\<^esub> "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); i \<in> I\<rbrakk> \<Longrightarrow> prod_zero I A i = \<zero>\<^bsub>A i\<^esub>
[PROOF STEP]
by (simp add:prod_zero_def)


[STATEMENT]
lemma carr_prodag_mem_eq:"\<lbrakk>\<forall>k\<in>I. aGroup (A k); X \<in> carr_prodag I A;
Y \<in> carr_prodag I A; \<forall>l\<in>I. (X l) = (Y l) \<rbrakk> \<Longrightarrow> X = Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); X \<in> carr_prodag I A; Y \<in> carr_prodag I A; \<forall>l\<in>I. X l = Y l\<rbrakk> \<Longrightarrow> X = Y
[PROOF STEP]
apply (simp add:carr_prodag_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); X \<in> extensional I \<and> X \<in> I \<rightarrow> Un_carrier I A \<and> (\<forall>i\<in>I. Y i \<in> carrier (A i)); Y \<in> extensional I \<and> Y \<in> I \<rightarrow> Un_carrier I A; \<forall>l\<in>I. X l = Y l\<rbrakk> \<Longrightarrow> X = Y
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>l\<in>I. X l = Y l; X \<in> extensional I; Y \<in> extensional I; Y \<in> I \<rightarrow> Un_carrier I A; X \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. Y i \<in> carrier (A i)\<rbrakk> \<Longrightarrow> X = Y
[PROOF STEP]
apply (simp add:funcset_eq)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prod_pOp_assoc:"\<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A;
      b \<in> carr_prodag I A; c \<in> carr_prodag I A\<rbrakk> \<Longrightarrow>
      prod_pOp I A (prod_pOp I A a b) c =
                               prod_pOp I A a (prod_pOp I A b c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A; c \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_pOp I A (prod_pOp I A a b) c = prod_pOp I A a (prod_pOp I A b c)
[PROOF STEP]
apply (frule_tac X = a and Y = b in prod_pOp_mem[of "I" "A"], assumption+,
        frule_tac X = b and Y = c in prod_pOp_mem[of "I" "A"], assumption+,
        frule_tac X = "prod_pOp I A a b" and Y = c in prod_pOp_mem[of "I"
            "A"], assumption+,
        frule_tac X = a and Y = "prod_pOp I A b c" in prod_pOp_mem[of "I"
            "A"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A; c \<in> carr_prodag I A; prod_pOp I A a b \<in> carr_prodag I A; prod_pOp I A b c \<in> carr_prodag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_prodag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_pOp I A (prod_pOp I A a b) c = prod_pOp I A a (prod_pOp I A b c)
[PROOF STEP]
apply (rule carr_prodag_mem_eq[of "I" "A"], assumption+,
       rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A; c \<in> carr_prodag I A; prod_pOp I A a b \<in> carr_prodag I A; prod_pOp I A b c \<in> carr_prodag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_prodag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_prodag I A; l \<in> I\<rbrakk> \<Longrightarrow> prod_pOp I A (prod_pOp I A a b) c l = prod_pOp I A a (prod_pOp I A b c) l
[PROOF STEP]
apply (simp add:prod_pOp_mem_i)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A; c \<in> carr_prodag I A; prod_pOp I A a b \<in> carr_prodag I A; prod_pOp I A b c \<in> carr_prodag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_prodag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_prodag I A; l \<in> I\<rbrakk> \<Longrightarrow> a l \<plusminus>\<^bsub>A l\<^esub> b l \<plusminus>\<^bsub>A l\<^esub> c l = a l \<plusminus>\<^bsub>A l\<^esub> (b l \<plusminus>\<^bsub>A l\<^esub> c l)
[PROOF STEP]
apply (frule_tac x = l in bspec, assumption,
        thin_tac "\<forall>k\<in>I. aGroup (A k)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>a \<in> carr_prodag I A; b \<in> carr_prodag I A; c \<in> carr_prodag I A; prod_pOp I A a b \<in> carr_prodag I A; prod_pOp I A b c \<in> carr_prodag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_prodag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_prodag I A; l \<in> I; aGroup (A l)\<rbrakk> \<Longrightarrow> a l \<plusminus>\<^bsub>A l\<^esub> b l \<plusminus>\<^bsub>A l\<^esub> c l = a l \<plusminus>\<^bsub>A l\<^esub> (b l \<plusminus>\<^bsub>A l\<^esub> c l)
[PROOF STEP]
apply (rule aGroup.ag_pOp_assoc, assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>l. \<lbrakk>a \<in> carr_prodag I A; b \<in> carr_prodag I A; c \<in> carr_prodag I A; prod_pOp I A a b \<in> carr_prodag I A; prod_pOp I A b c \<in> carr_prodag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_prodag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_prodag I A; l \<in> I; aGroup (A l)\<rbrakk> \<Longrightarrow> a l \<in> carrier (A l)
 2. \<And>l. \<lbrakk>a \<in> carr_prodag I A; b \<in> carr_prodag I A; c \<in> carr_prodag I A; prod_pOp I A a b \<in> carr_prodag I A; prod_pOp I A b c \<in> carr_prodag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_prodag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_prodag I A; l \<in> I; aGroup (A l)\<rbrakk> \<Longrightarrow> b l \<in> carrier (A l)
 3. \<And>l. \<lbrakk>a \<in> carr_prodag I A; b \<in> carr_prodag I A; c \<in> carr_prodag I A; prod_pOp I A a b \<in> carr_prodag I A; prod_pOp I A b c \<in> carr_prodag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_prodag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_prodag I A; l \<in> I; aGroup (A l)\<rbrakk> \<Longrightarrow> c l \<in> carrier (A l)
[PROOF STEP]
apply (simp add:prodag_comp_i)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prod_pOp_commute:"\<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A;
                           b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow>
                           prod_pOp I A a b = prod_pOp I A b a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_pOp I A a b = prod_pOp I A b a
[PROOF STEP]
apply (frule_tac X = a and Y = b in prod_pOp_mem[of "I" "A"], assumption+,
         frule_tac X = b and Y = a in prod_pOp_mem[of "I" "A"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A; prod_pOp I A a b \<in> carr_prodag I A; prod_pOp I A b a \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_pOp I A a b = prod_pOp I A b a
[PROOF STEP]
apply (rule carr_prodag_mem_eq[of "I" "A"], assumption+,
        rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A; prod_pOp I A a b \<in> carr_prodag I A; prod_pOp I A b a \<in> carr_prodag I A; l \<in> I\<rbrakk> \<Longrightarrow> prod_pOp I A a b l = prod_pOp I A b a l
[PROOF STEP]
apply (simp add:prod_pOp_mem_i)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag I A; b \<in> carr_prodag I A; prod_pOp I A a b \<in> carr_prodag I A; prod_pOp I A b a \<in> carr_prodag I A; l \<in> I\<rbrakk> \<Longrightarrow> a l \<plusminus>\<^bsub>A l\<^esub> b l = b l \<plusminus>\<^bsub>A l\<^esub> a l
[PROOF STEP]
apply (frule_tac x = l in bspec, assumption,
        thin_tac "\<forall>k\<in>I. aGroup (A k)",
        rule aGroup.ag_pOp_commute, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l. \<lbrakk>a \<in> carr_prodag I A; b \<in> carr_prodag I A; prod_pOp I A a b \<in> carr_prodag I A; prod_pOp I A b a \<in> carr_prodag I A; l \<in> I; aGroup (A l)\<rbrakk> \<Longrightarrow> a l \<in> carrier (A l)
 2. \<And>l. \<lbrakk>a \<in> carr_prodag I A; b \<in> carr_prodag I A; prod_pOp I A a b \<in> carr_prodag I A; prod_pOp I A b a \<in> carr_prodag I A; l \<in> I; aGroup (A l)\<rbrakk> \<Longrightarrow> b l \<in> carrier (A l)
[PROOF STEP]
apply (simp add:prodag_comp_i)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done