[STATEMENT]
lemma aHom_compos:"\<lbrakk>aGroup L; aGroup M; aGroup N; f \<in> aHom L M; g \<in> aHom M N \<rbrakk>
  \<Longrightarrow> compos L g f \<in> aHom L N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup L; aGroup M; aGroup N; f \<in> aHom L M; g \<in> aHom M N\<rbrakk> \<Longrightarrow> compos L g f \<in> aHom L N
[PROOF STEP]
apply (simp add:aHom_def [of "L" "N"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup L; aGroup M; aGroup N; f \<in> aHom L M; g \<in> aHom M N\<rbrakk> \<Longrightarrow> compos L g f \<in> carrier L \<rightarrow> carrier N \<and> compos L g f \<in> extensional (carrier L) \<and> (\<forall>a\<in>carrier L. \<forall>b\<in>carrier L. compos L g f (a \<plusminus>\<^bsub>L\<^esub> b) = compos L g f a \<plusminus>\<^bsub>N\<^esub> compos L g f b)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup L; aGroup M; aGroup N; f \<in> aHom L M; g \<in> aHom M N\<rbrakk> \<Longrightarrow> compos L g f \<in> carrier L \<rightarrow> carrier N
 2. \<lbrakk>aGroup L; aGroup M; aGroup N; f \<in> aHom L M; g \<in> aHom M N\<rbrakk> \<Longrightarrow> compos L g f \<in> extensional (carrier L) \<and> (\<forall>a\<in>carrier L. \<forall>b\<in>carrier L. compos L g f (a \<plusminus>\<^bsub>L\<^esub> b) = compos L g f a \<plusminus>\<^bsub>N\<^esub> compos L g f b)
[PROOF STEP]
apply (rule Pi_I)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>aGroup L; aGroup M; aGroup N; f \<in> aHom L M; g \<in> aHom M N; x \<in> carrier L\<rbrakk> \<Longrightarrow> compos L g f x \<in> carrier N
 2. \<lbrakk>aGroup L; aGroup M; aGroup N; f \<in> aHom L M; g \<in> aHom M N\<rbrakk> \<Longrightarrow> compos L g f \<in> extensional (carrier L) \<and> (\<forall>a\<in>carrier L. \<forall>b\<in>carrier L. compos L g f (a \<plusminus>\<^bsub>L\<^esub> b) = compos L g f a \<plusminus>\<^bsub>N\<^esub> compos L g f b)
[PROOF STEP]
apply (simp add:compos_def compose_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>aGroup L; aGroup M; aGroup N; f \<in> aHom L M; g \<in> aHom M N; x \<in> carrier L\<rbrakk> \<Longrightarrow> g (f x) \<in> carrier N
 2. \<lbrakk>aGroup L; aGroup M; aGroup N; f \<in> aHom L M; g \<in> aHom M N\<rbrakk> \<Longrightarrow> compos L g f \<in> extensional (carrier L) \<and> (\<forall>a\<in>carrier L. \<forall>b\<in>carrier L. compos L g f (a \<plusminus>\<^bsub>L\<^esub> b) = compos L g f a \<plusminus>\<^bsub>N\<^esub> compos L g f b)
[PROOF STEP]
apply (rule aHom_mem [of "M" "N" "g"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>aGroup L; aGroup M; aGroup N; f \<in> aHom L M; g \<in> aHom M N; x \<in> carrier L\<rbrakk> \<Longrightarrow> f x \<in> carrier M
 2. \<lbrakk>aGroup L; aGroup M; aGroup N; f \<in> aHom L M; g \<in> aHom M N\<rbrakk> \<Longrightarrow> compos L g f \<in> extensional (carrier L) \<and> (\<forall>a\<in>carrier L. \<forall>b\<in>carrier L. compos L g f (a \<plusminus>\<^bsub>L\<^esub> b) = compos L g f a \<plusminus>\<^bsub>N\<^esub> compos L g f b)
[PROOF STEP]
apply (simp add:aHom_mem [of "L" "M" "f"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup L; aGroup M; aGroup N; f \<in> aHom L M; g \<in> aHom M N\<rbrakk> \<Longrightarrow> compos L g f \<in> extensional (carrier L) \<and> (\<forall>a\<in>carrier L. \<forall>b\<in>carrier L. compos L g f (a \<plusminus>\<^bsub>L\<^esub> b) = compos L g f a \<plusminus>\<^bsub>N\<^esub> compos L g f b)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup L; aGroup M; aGroup N; f \<in> aHom L M; g \<in> aHom M N\<rbrakk> \<Longrightarrow> compos L g f \<in> extensional (carrier L)
 2. \<lbrakk>aGroup L; aGroup M; aGroup N; f \<in> aHom L M; g \<in> aHom M N\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier L. \<forall>b\<in>carrier L. compos L g f (a \<plusminus>\<^bsub>L\<^esub> b) = compos L g f a \<plusminus>\<^bsub>N\<^esub> compos L g f b
[PROOF STEP]
apply (simp add:compos_def compose_def extensional_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup L; aGroup M; aGroup N; f \<in> aHom L M; g \<in> aHom M N\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier L. \<forall>b\<in>carrier L. compos L g f (a \<plusminus>\<^bsub>L\<^esub> b) = compos L g f a \<plusminus>\<^bsub>N\<^esub> compos L g f b
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup L; aGroup M; aGroup N; f \<in> aHom L M; g \<in> aHom M N; a \<in> carrier L; b \<in> carrier L\<rbrakk> \<Longrightarrow> compos L g f (a \<plusminus>\<^bsub>L\<^esub> b) = compos L g f a \<plusminus>\<^bsub>N\<^esub> compos L g f b
[PROOF STEP]
apply (simp add:compos_def compose_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup L; aGroup M; aGroup N; f \<in> aHom L M; g \<in> aHom M N; a \<in> carrier L; b \<in> carrier L\<rbrakk> \<Longrightarrow> (a \<plusminus>\<^bsub>L\<^esub> b \<in> carrier L \<longrightarrow> g (f (a \<plusminus>\<^bsub>L\<^esub> b)) = g (f a) \<plusminus>\<^bsub>N\<^esub> g (f b)) \<and> (a \<plusminus>\<^bsub>L\<^esub> b \<notin> carrier L \<longrightarrow> undefined = g (f a) \<plusminus>\<^bsub>N\<^esub> g (f b))
[PROOF STEP]
apply (simp add:aGroup.ag_pOp_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup L; aGroup M; aGroup N; f \<in> aHom L M; g \<in> aHom M N; a \<in> carrier L; b \<in> carrier L\<rbrakk> \<Longrightarrow> g (f (a \<plusminus>\<^bsub>L\<^esub> b)) = g (f a) \<plusminus>\<^bsub>N\<^esub> g (f b)
[PROOF STEP]
apply (simp add:aHom_add)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup L; aGroup M; aGroup N; f \<in> aHom L M; g \<in> aHom M N; a \<in> carrier L; b \<in> carrier L\<rbrakk> \<Longrightarrow> g (f a \<plusminus>\<^bsub>M\<^esub> f b) = g (f a) \<plusminus>\<^bsub>N\<^esub> g (f b)
[PROOF STEP]
apply (rule aHom_add, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>aGroup L; aGroup M; aGroup N; f \<in> aHom L M; g \<in> aHom M N; a \<in> carrier L; b \<in> carrier L\<rbrakk> \<Longrightarrow> f a \<in> carrier M
 2. \<And>a b. \<lbrakk>aGroup L; aGroup M; aGroup N; f \<in> aHom L M; g \<in> aHom M N; a \<in> carrier L; b \<in> carrier L\<rbrakk> \<Longrightarrow> f b \<in> carrier M
[PROOF STEP]
apply (simp add:aHom_mem)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma aHom_compos_assoc:"\<lbrakk>aGroup K; aGroup L; aGroup M; aGroup N; f \<in> aHom K L;
      g \<in> aHom L M; h \<in> aHom M N \<rbrakk>  \<Longrightarrow>
      compos K h (compos K g f) = compos K (compos L h g) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup K; aGroup L; aGroup M; aGroup N; f \<in> aHom K L; g \<in> aHom L M; h \<in> aHom M N\<rbrakk> \<Longrightarrow> compos K h (compos K g f) = compos K (compos L h g) f
[PROOF STEP]
apply (simp add:compos_def compose_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup K; aGroup L; aGroup M; aGroup N; f \<in> aHom K L; g \<in> aHom L M; h \<in> aHom M N\<rbrakk> \<Longrightarrow> (\<lambda>x\<in>carrier K. h (if x \<in> carrier K then g (f x) else undefined)) = (\<lambda>x\<in>carrier K. if f x \<in> carrier L then h (g (f x)) else undefined)
[PROOF STEP]
apply (rule funcset_eq[of _ "carrier K"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>aGroup K; aGroup L; aGroup M; aGroup N; f \<in> aHom K L; g \<in> aHom L M; h \<in> aHom M N\<rbrakk> \<Longrightarrow> (\<lambda>x\<in>carrier K. h (if x \<in> carrier K then g (f x) else undefined)) \<in> extensional (carrier K)
 2. \<lbrakk>aGroup K; aGroup L; aGroup M; aGroup N; f \<in> aHom K L; g \<in> aHom L M; h \<in> aHom M N\<rbrakk> \<Longrightarrow> (\<lambda>x\<in>carrier K. if f x \<in> carrier L then h (g (f x)) else undefined) \<in> extensional (carrier K)
 3. \<lbrakk>aGroup K; aGroup L; aGroup M; aGroup N; f \<in> aHom K L; g \<in> aHom L M; h \<in> aHom M N\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier K. (\<lambda>x\<in>carrier K. h (if x \<in> carrier K then g (f x) else undefined)) x = (\<lambda>x\<in>carrier K. if f x \<in> carrier L then h (g (f x)) else undefined) x
[PROOF STEP]
apply (simp add:restrict_def extensional_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup K; aGroup L; aGroup M; aGroup N; f \<in> aHom K L; g \<in> aHom L M; h \<in> aHom M N\<rbrakk> \<Longrightarrow> (\<lambda>x\<in>carrier K. if f x \<in> carrier L then h (g (f x)) else undefined) \<in> extensional (carrier K)
 2. \<lbrakk>aGroup K; aGroup L; aGroup M; aGroup N; f \<in> aHom K L; g \<in> aHom L M; h \<in> aHom M N\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier K. (\<lambda>x\<in>carrier K. h (if x \<in> carrier K then g (f x) else undefined)) x = (\<lambda>x\<in>carrier K. if f x \<in> carrier L then h (g (f x)) else undefined) x
[PROOF STEP]
apply (simp add:restrict_def extensional_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup K; aGroup L; aGroup M; aGroup N; f \<in> aHom K L; g \<in> aHom L M; h \<in> aHom M N\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier K. (\<lambda>x\<in>carrier K. h (if x \<in> carrier K then g (f x) else undefined)) x = (\<lambda>x\<in>carrier K. if f x \<in> carrier L then h (g (f x)) else undefined) x
[PROOF STEP]
apply (rule ballI, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>aGroup K; aGroup L; aGroup M; aGroup N; f \<in> aHom K L; g \<in> aHom L M; h \<in> aHom M N; x \<in> carrier K\<rbrakk> \<Longrightarrow> f x \<notin> carrier L \<longrightarrow> h (g (f x)) = undefined
[PROOF STEP]
apply (simp add:aHom_mem)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma injec_inj_on:"\<lbrakk>aGroup F; aGroup G; injec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> inj_on f (carrier F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; injec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> inj_on f (carrier F)
[PROOF STEP]
apply (simp add:inj_on_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; injec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier F. \<forall>y\<in>carrier F. f x = f y \<longrightarrow> x = y
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>aGroup F; aGroup G; injec\<^bsub>F,G\<^esub> f; x \<in> carrier F; y \<in> carrier F\<rbrakk> \<Longrightarrow> f x = f y \<longrightarrow> x = y
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>aGroup F; aGroup G; injec\<^bsub>F,G\<^esub> f; x \<in> carrier F; y \<in> carrier F; f x = f y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (simp add:injec_def, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>aGroup F; aGroup G; x \<in> carrier F; y \<in> carrier F; f x = f y; f \<in> aHom F G; ker\<^bsub>F,G\<^esub> f = {\<zero>\<^bsub>F\<^esub>}\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (frule_tac a = x in aHom_mem[of "F" "G" "f"], assumption+,
        frule_tac a = x in aHom_mem[of "F" "G" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>aGroup F; aGroup G; x \<in> carrier F; y \<in> carrier F; f x = f y; f \<in> aHom F G; ker\<^bsub>F,G\<^esub> f = {\<zero>\<^bsub>F\<^esub>}; f x \<in> carrier G; f x \<in> carrier G\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (frule_tac x = "f x" in aGroup.ag_r_inv1[of "G"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>aGroup F; aGroup G; x \<in> carrier F; y \<in> carrier F; f x = f y; f \<in> aHom F G; ker\<^bsub>F,G\<^esub> f = {\<zero>\<^bsub>F\<^esub>}; f x \<in> carrier G; f x \<in> carrier G; f x \<plusminus>\<^bsub>G\<^esub> -\<^sub>a\<^bsub>G\<^esub> f x = \<zero>\<^bsub>G\<^esub>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (simp only:aHom_inv_inv[THEN sym, of "F" "G" "f"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>aGroup F; aGroup G; x \<in> carrier F; y \<in> carrier F; f x = f y; f \<in> aHom F G; ker\<^bsub>F,G\<^esub> f = {\<zero>\<^bsub>F\<^esub>}; f y \<in> carrier G; True; f y \<plusminus>\<^bsub>G\<^esub> f (-\<^sub>a\<^bsub>F\<^esub> y) = \<zero>\<^bsub>G\<^esub>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (frule sym, thin_tac "f x = f y", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>aGroup F; aGroup G; x \<in> carrier F; y \<in> carrier F; f \<in> aHom F G; ker\<^bsub>F,G\<^esub> f = {\<zero>\<^bsub>F\<^esub>}; f x \<in> carrier G; f x \<plusminus>\<^bsub>G\<^esub> f (-\<^sub>a\<^bsub>F\<^esub> y) = \<zero>\<^bsub>G\<^esub>; f y = f x\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (frule_tac x = y in aGroup.ag_mOp_closed[of "F"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>aGroup F; aGroup G; x \<in> carrier F; y \<in> carrier F; f \<in> aHom F G; ker\<^bsub>F,G\<^esub> f = {\<zero>\<^bsub>F\<^esub>}; f x \<in> carrier G; f x \<plusminus>\<^bsub>G\<^esub> f (-\<^sub>a\<^bsub>F\<^esub> y) = \<zero>\<^bsub>G\<^esub>; f y = f x; -\<^sub>a\<^bsub>F\<^esub> y \<in> carrier F\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (simp add:aHom_add[THEN sym], simp add:ker_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>aGroup F; aGroup G; x \<in> carrier F; y \<in> carrier F; f \<in> aHom F G; {a \<in> carrier F. f a = \<zero>\<^bsub>G\<^esub>} = {\<zero>\<^bsub>F\<^esub>}; f x \<in> carrier G; f (x \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> y) = \<zero>\<^bsub>G\<^esub>; f y = f x; -\<^sub>a\<^bsub>F\<^esub> y \<in> carrier F\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
apply (subgoal_tac "x \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> y \<in> {a \<in> carrier F. f a = \<zero>\<^bsub>G\<^esub>}",
        simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>aGroup F; aGroup G; x \<in> carrier F; y \<in> carrier F; f \<in> aHom F G; {a \<in> carrier F. f a = \<zero>\<^bsub>G\<^esub>} = {\<zero>\<^bsub>F\<^esub>}; f x \<in> carrier G; f \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>G\<^esub>; f y = f x; -\<^sub>a\<^bsub>F\<^esub> y \<in> carrier F; x \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> y = \<zero>\<^bsub>F\<^esub>\<rbrakk> \<Longrightarrow> x = y
 2. \<And>x y. \<lbrakk>aGroup F; aGroup G; x \<in> carrier F; y \<in> carrier F; f \<in> aHom F G; {a \<in> carrier F. f a = \<zero>\<^bsub>G\<^esub>} = {\<zero>\<^bsub>F\<^esub>}; f x \<in> carrier G; f (x \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> y) = \<zero>\<^bsub>G\<^esub>; f y = f x; -\<^sub>a\<^bsub>F\<^esub> y \<in> carrier F\<rbrakk> \<Longrightarrow> x \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> y \<in> {a \<in> carrier F. f a = \<zero>\<^bsub>G\<^esub>}
[PROOF STEP]
apply (subst aGroup.ag_eq_diffzero[of "F"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>aGroup F; aGroup G; x \<in> carrier F; y \<in> carrier F; f \<in> aHom F G; {a \<in> carrier F. f a = \<zero>\<^bsub>G\<^esub>} = {\<zero>\<^bsub>F\<^esub>}; f x \<in> carrier G; f (x \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> y) = \<zero>\<^bsub>G\<^esub>; f y = f x; -\<^sub>a\<^bsub>F\<^esub> y \<in> carrier F\<rbrakk> \<Longrightarrow> x \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> y \<in> {a \<in> carrier F. f a = \<zero>\<^bsub>G\<^esub>}
[PROOF STEP]
apply (frule_tac x = x and y = "-\<^sub>a\<^bsub>F\<^esub> y" in aGroup.ag_pOp_closed[of "F"],
           assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>aGroup F; aGroup G; x \<in> carrier F; y \<in> carrier F; f \<in> aHom F G; {a \<in> carrier F. f a = \<zero>\<^bsub>G\<^esub>} = {\<zero>\<^bsub>F\<^esub>}; f x \<in> carrier G; f (x \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> y) = \<zero>\<^bsub>G\<^esub>; f y = f x; -\<^sub>a\<^bsub>F\<^esub> y \<in> carrier F; x \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> y \<in> carrier F\<rbrakk> \<Longrightarrow> x \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> y \<in> {a \<in> carrier F. f a = \<zero>\<^bsub>G\<^esub>}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>aGroup F; aGroup G; x \<in> carrier F; y \<in> carrier F; f \<in> aHom F G; {a \<in> carrier F. f a = \<zero>\<^bsub>G\<^esub>} = {\<zero>\<^bsub>F\<^esub>}; f x \<in> carrier G; f (x \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> y) = \<zero>\<^bsub>G\<^esub>; f y = f x; -\<^sub>a\<^bsub>F\<^esub> y \<in> carrier F; x \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> y \<in> carrier F\<rbrakk> \<Longrightarrow> x \<plusminus>\<^bsub>F\<^esub> -\<^sub>a\<^bsub>F\<^esub> y = \<zero>\<^bsub>F\<^esub>
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma surjec_surj_to:"surjec\<^bsub>R,S\<^esub> f \<Longrightarrow> surj_to f (carrier R) (carrier S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surjec\<^bsub>R,S\<^esub> f \<Longrightarrow> surj_to f (carrier R) (carrier S)
[PROOF STEP]
by (simp add:surjec_def)


[STATEMENT]
lemma compos_bijec:"\<lbrakk>aGroup E; aGroup F; aGroup G; bijec\<^bsub>E,F\<^esub> f; bijec\<^bsub>F,G\<^esub> g\<rbrakk> \<Longrightarrow>
                     bijec\<^bsub>E,G\<^esub> (compos E g f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup E; aGroup F; aGroup G; bijec\<^bsub>E,F\<^esub> f; bijec\<^bsub>F,G\<^esub> g\<rbrakk> \<Longrightarrow> bijec\<^bsub>E,G\<^esub> compos E g f
[PROOF STEP]
apply (simp add:bijec_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup E; aGroup F; aGroup G; injec\<^bsub>E,F\<^esub> f; surjec\<^bsub>E,F\<^esub> f; injec\<^bsub>F,G\<^esub> g; surjec\<^bsub>F,G\<^esub> g\<rbrakk> \<Longrightarrow> injec\<^bsub>E,G\<^esub> compos E g f \<and> surjec\<^bsub>E,G\<^esub> compos E g f
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup E; aGroup F; aGroup G; injec\<^bsub>E,F\<^esub> f; surjec\<^bsub>E,F\<^esub> f; injec\<^bsub>F,G\<^esub> g; surjec\<^bsub>F,G\<^esub> g\<rbrakk> \<Longrightarrow> injec\<^bsub>E,G\<^esub> compos E g f
 2. \<lbrakk>aGroup E; aGroup F; aGroup G; injec\<^bsub>E,F\<^esub> f; surjec\<^bsub>E,F\<^esub> f; injec\<^bsub>F,G\<^esub> g; surjec\<^bsub>F,G\<^esub> g\<rbrakk> \<Longrightarrow> surjec\<^bsub>E,G\<^esub> compos E g f
[PROOF STEP]
apply (simp add:injec_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup E; aGroup F; aGroup G; surjec\<^bsub>E,F\<^esub> f; surjec\<^bsub>F,G\<^esub> g; f \<in> aHom E F; ker\<^bsub>E,F\<^esub> f = {\<zero>\<^bsub>E\<^esub>}; g \<in> aHom F G; ker\<^bsub>F,G\<^esub> g = {\<zero>\<^bsub>F\<^esub>}\<rbrakk> \<Longrightarrow> compos E g f \<in> aHom E G \<and> ker\<^bsub>E,G\<^esub> compos E g f = {\<zero>\<^bsub>E\<^esub>}
 2. \<lbrakk>aGroup E; aGroup F; aGroup G; injec\<^bsub>E,F\<^esub> f; surjec\<^bsub>E,F\<^esub> f; injec\<^bsub>F,G\<^esub> g; surjec\<^bsub>F,G\<^esub> g\<rbrakk> \<Longrightarrow> surjec\<^bsub>E,G\<^esub> compos E g f
[PROOF STEP]
apply (simp add:aHom_compos[of "E" "F" "G" "f" "g"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup E; aGroup F; aGroup G; surjec\<^bsub>E,F\<^esub> f; surjec\<^bsub>F,G\<^esub> g; f \<in> aHom E F; ker\<^bsub>E,F\<^esub> f = {\<zero>\<^bsub>E\<^esub>}; g \<in> aHom F G; ker\<^bsub>F,G\<^esub> g = {\<zero>\<^bsub>F\<^esub>}\<rbrakk> \<Longrightarrow> ker\<^bsub>E,G\<^esub> compos E g f = {\<zero>\<^bsub>E\<^esub>}
 2. \<lbrakk>aGroup E; aGroup F; aGroup G; injec\<^bsub>E,F\<^esub> f; surjec\<^bsub>E,F\<^esub> f; injec\<^bsub>F,G\<^esub> g; surjec\<^bsub>F,G\<^esub> g\<rbrakk> \<Longrightarrow> surjec\<^bsub>E,G\<^esub> compos E g f
[PROOF STEP]
apply (rule equalityI, rule subsetI, simp add:ker_def, erule conjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>aGroup E; aGroup F; aGroup G; surjec\<^bsub>E,F\<^esub> f; surjec\<^bsub>F,G\<^esub> g; f \<in> aHom E F; {a \<in> carrier E. f a = \<zero>\<^bsub>F\<^esub>} = {\<zero>\<^bsub>E\<^esub>}; g \<in> aHom F G; {a \<in> carrier F. g a = \<zero>\<^bsub>G\<^esub>} = {\<zero>\<^bsub>F\<^esub>}; x \<in> carrier E; compos E g f x = \<zero>\<^bsub>G\<^esub>\<rbrakk> \<Longrightarrow> x = \<zero>\<^bsub>E\<^esub>
 2. \<lbrakk>aGroup E; aGroup F; aGroup G; surjec\<^bsub>E,F\<^esub> f; surjec\<^bsub>F,G\<^esub> g; f \<in> aHom E F; ker\<^bsub>E,F\<^esub> f = {\<zero>\<^bsub>E\<^esub>}; g \<in> aHom F G; ker\<^bsub>F,G\<^esub> g = {\<zero>\<^bsub>F\<^esub>}\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>E\<^esub>} \<subseteq> ker\<^bsub>E,G\<^esub> compos E g f
 3. \<lbrakk>aGroup E; aGroup F; aGroup G; injec\<^bsub>E,F\<^esub> f; surjec\<^bsub>E,F\<^esub> f; injec\<^bsub>F,G\<^esub> g; surjec\<^bsub>F,G\<^esub> g\<rbrakk> \<Longrightarrow> surjec\<^bsub>E,G\<^esub> compos E g f
[PROOF STEP]
apply (simp add:compos_def compose_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>aGroup E; aGroup F; aGroup G; surjec\<^bsub>E,F\<^esub> f; surjec\<^bsub>F,G\<^esub> g; f \<in> aHom E F; {a \<in> carrier E. f a = \<zero>\<^bsub>F\<^esub>} = {\<zero>\<^bsub>E\<^esub>}; g \<in> aHom F G; {a \<in> carrier F. g a = \<zero>\<^bsub>G\<^esub>} = {\<zero>\<^bsub>F\<^esub>}; x \<in> carrier E; g (f x) = \<zero>\<^bsub>G\<^esub>\<rbrakk> \<Longrightarrow> x = \<zero>\<^bsub>E\<^esub>
 2. \<lbrakk>aGroup E; aGroup F; aGroup G; surjec\<^bsub>E,F\<^esub> f; surjec\<^bsub>F,G\<^esub> g; f \<in> aHom E F; ker\<^bsub>E,F\<^esub> f = {\<zero>\<^bsub>E\<^esub>}; g \<in> aHom F G; ker\<^bsub>F,G\<^esub> g = {\<zero>\<^bsub>F\<^esub>}\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>E\<^esub>} \<subseteq> ker\<^bsub>E,G\<^esub> compos E g f
 3. \<lbrakk>aGroup E; aGroup F; aGroup G; injec\<^bsub>E,F\<^esub> f; surjec\<^bsub>E,F\<^esub> f; injec\<^bsub>F,G\<^esub> g; surjec\<^bsub>F,G\<^esub> g\<rbrakk> \<Longrightarrow> surjec\<^bsub>E,G\<^esub> compos E g f
[PROOF STEP]
apply (frule_tac a = x in aHom_mem[of "E" "F" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>aGroup E; aGroup F; aGroup G; surjec\<^bsub>E,F\<^esub> f; surjec\<^bsub>F,G\<^esub> g; f \<in> aHom E F; {a \<in> carrier E. f a = \<zero>\<^bsub>F\<^esub>} = {\<zero>\<^bsub>E\<^esub>}; g \<in> aHom F G; {a \<in> carrier F. g a = \<zero>\<^bsub>G\<^esub>} = {\<zero>\<^bsub>F\<^esub>}; x \<in> carrier E; g (f x) = \<zero>\<^bsub>G\<^esub>; f x \<in> carrier F\<rbrakk> \<Longrightarrow> x = \<zero>\<^bsub>E\<^esub>
 2. \<lbrakk>aGroup E; aGroup F; aGroup G; surjec\<^bsub>E,F\<^esub> f; surjec\<^bsub>F,G\<^esub> g; f \<in> aHom E F; ker\<^bsub>E,F\<^esub> f = {\<zero>\<^bsub>E\<^esub>}; g \<in> aHom F G; ker\<^bsub>F,G\<^esub> g = {\<zero>\<^bsub>F\<^esub>}\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>E\<^esub>} \<subseteq> ker\<^bsub>E,G\<^esub> compos E g f
 3. \<lbrakk>aGroup E; aGroup F; aGroup G; injec\<^bsub>E,F\<^esub> f; surjec\<^bsub>E,F\<^esub> f; injec\<^bsub>F,G\<^esub> g; surjec\<^bsub>F,G\<^esub> g\<rbrakk> \<Longrightarrow> surjec\<^bsub>E,G\<^esub> compos E g f
[PROOF STEP]
apply (subgoal_tac "(f x) \<in> {a \<in> carrier F. g a = \<zero>\<^bsub>G\<^esub>}", simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>aGroup E; aGroup F; aGroup G; surjec\<^bsub>E,F\<^esub> f; surjec\<^bsub>F,G\<^esub> g; f \<in> aHom E F; {a \<in> carrier E. f a = \<zero>\<^bsub>F\<^esub>} = {\<zero>\<^bsub>E\<^esub>}; g \<in> aHom F G; {a \<in> carrier F. g a = \<zero>\<^bsub>G\<^esub>} = {\<zero>\<^bsub>F\<^esub>}; x \<in> carrier E; g \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>G\<^esub>; \<zero>\<^bsub>F\<^esub> \<in> carrier F; f x = \<zero>\<^bsub>F\<^esub>\<rbrakk> \<Longrightarrow> x = \<zero>\<^bsub>E\<^esub>
 2. \<And>x. \<lbrakk>aGroup E; aGroup F; aGroup G; surjec\<^bsub>E,F\<^esub> f; surjec\<^bsub>F,G\<^esub> g; f \<in> aHom E F; {a \<in> carrier E. f a = \<zero>\<^bsub>F\<^esub>} = {\<zero>\<^bsub>E\<^esub>}; g \<in> aHom F G; {a \<in> carrier F. g a = \<zero>\<^bsub>G\<^esub>} = {\<zero>\<^bsub>F\<^esub>}; x \<in> carrier E; g (f x) = \<zero>\<^bsub>G\<^esub>; f x \<in> carrier F\<rbrakk> \<Longrightarrow> f x \<in> {a \<in> carrier F. g a = \<zero>\<^bsub>G\<^esub>}
 3. \<lbrakk>aGroup E; aGroup F; aGroup G; surjec\<^bsub>E,F\<^esub> f; surjec\<^bsub>F,G\<^esub> g; f \<in> aHom E F; ker\<^bsub>E,F\<^esub> f = {\<zero>\<^bsub>E\<^esub>}; g \<in> aHom F G; ker\<^bsub>F,G\<^esub> g = {\<zero>\<^bsub>F\<^esub>}\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>E\<^esub>} \<subseteq> ker\<^bsub>E,G\<^esub> compos E g f
 4. \<lbrakk>aGroup E; aGroup F; aGroup G; injec\<^bsub>E,F\<^esub> f; surjec\<^bsub>E,F\<^esub> f; injec\<^bsub>F,G\<^esub> g; surjec\<^bsub>F,G\<^esub> g\<rbrakk> \<Longrightarrow> surjec\<^bsub>E,G\<^esub> compos E g f
[PROOF STEP]
apply (subgoal_tac "x \<in> {a \<in> carrier E. f a = \<zero>\<^bsub>F\<^esub>}", simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>aGroup E; aGroup F; aGroup G; surjec\<^bsub>E,F\<^esub> f; surjec\<^bsub>F,G\<^esub> g; f \<in> aHom E F; {a \<in> carrier E. f a = \<zero>\<^bsub>F\<^esub>} = {\<zero>\<^bsub>E\<^esub>}; g \<in> aHom F G; {a \<in> carrier F. g a = \<zero>\<^bsub>G\<^esub>} = {\<zero>\<^bsub>F\<^esub>}; x \<in> carrier E; g \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>G\<^esub>; \<zero>\<^bsub>F\<^esub> \<in> carrier F; f x = \<zero>\<^bsub>F\<^esub>\<rbrakk> \<Longrightarrow> x \<in> {a \<in> carrier E. f a = \<zero>\<^bsub>F\<^esub>}
 2. \<And>x. \<lbrakk>aGroup E; aGroup F; aGroup G; surjec\<^bsub>E,F\<^esub> f; surjec\<^bsub>F,G\<^esub> g; f \<in> aHom E F; {a \<in> carrier E. f a = \<zero>\<^bsub>F\<^esub>} = {\<zero>\<^bsub>E\<^esub>}; g \<in> aHom F G; {a \<in> carrier F. g a = \<zero>\<^bsub>G\<^esub>} = {\<zero>\<^bsub>F\<^esub>}; x \<in> carrier E; g (f x) = \<zero>\<^bsub>G\<^esub>; f x \<in> carrier F\<rbrakk> \<Longrightarrow> f x \<in> {a \<in> carrier F. g a = \<zero>\<^bsub>G\<^esub>}
 3. \<lbrakk>aGroup E; aGroup F; aGroup G; surjec\<^bsub>E,F\<^esub> f; surjec\<^bsub>F,G\<^esub> g; f \<in> aHom E F; ker\<^bsub>E,F\<^esub> f = {\<zero>\<^bsub>E\<^esub>}; g \<in> aHom F G; ker\<^bsub>F,G\<^esub> g = {\<zero>\<^bsub>F\<^esub>}\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>E\<^esub>} \<subseteq> ker\<^bsub>E,G\<^esub> compos E g f
 4. \<lbrakk>aGroup E; aGroup F; aGroup G; injec\<^bsub>E,F\<^esub> f; surjec\<^bsub>E,F\<^esub> f; injec\<^bsub>F,G\<^esub> g; surjec\<^bsub>F,G\<^esub> g\<rbrakk> \<Longrightarrow> surjec\<^bsub>E,G\<^esub> compos E g f
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>aGroup E; aGroup F; aGroup G; surjec\<^bsub>E,F\<^esub> f; surjec\<^bsub>F,G\<^esub> g; f \<in> aHom E F; {a \<in> carrier E. f a = \<zero>\<^bsub>F\<^esub>} = {\<zero>\<^bsub>E\<^esub>}; g \<in> aHom F G; {a \<in> carrier F. g a = \<zero>\<^bsub>G\<^esub>} = {\<zero>\<^bsub>F\<^esub>}; x \<in> carrier E; g (f x) = \<zero>\<^bsub>G\<^esub>; f x \<in> carrier F\<rbrakk> \<Longrightarrow> f x \<in> {a \<in> carrier F. g a = \<zero>\<^bsub>G\<^esub>}
 2. \<lbrakk>aGroup E; aGroup F; aGroup G; surjec\<^bsub>E,F\<^esub> f; surjec\<^bsub>F,G\<^esub> g; f \<in> aHom E F; ker\<^bsub>E,F\<^esub> f = {\<zero>\<^bsub>E\<^esub>}; g \<in> aHom F G; ker\<^bsub>F,G\<^esub> g = {\<zero>\<^bsub>F\<^esub>}\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>E\<^esub>} \<subseteq> ker\<^bsub>E,G\<^esub> compos E g f
 3. \<lbrakk>aGroup E; aGroup F; aGroup G; injec\<^bsub>E,F\<^esub> f; surjec\<^bsub>E,F\<^esub> f; injec\<^bsub>F,G\<^esub> g; surjec\<^bsub>F,G\<^esub> g\<rbrakk> \<Longrightarrow> surjec\<^bsub>E,G\<^esub> compos E g f
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup E; aGroup F; aGroup G; surjec\<^bsub>E,F\<^esub> f; surjec\<^bsub>F,G\<^esub> g; f \<in> aHom E F; ker\<^bsub>E,F\<^esub> f = {\<zero>\<^bsub>E\<^esub>}; g \<in> aHom F G; ker\<^bsub>F,G\<^esub> g = {\<zero>\<^bsub>F\<^esub>}\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>E\<^esub>} \<subseteq> ker\<^bsub>E,G\<^esub> compos E g f
 2. \<lbrakk>aGroup E; aGroup F; aGroup G; injec\<^bsub>E,F\<^esub> f; surjec\<^bsub>E,F\<^esub> f; injec\<^bsub>F,G\<^esub> g; surjec\<^bsub>F,G\<^esub> g\<rbrakk> \<Longrightarrow> surjec\<^bsub>E,G\<^esub> compos E g f
[PROOF STEP]
apply (rule subsetI, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>aGroup E; aGroup F; aGroup G; surjec\<^bsub>E,F\<^esub> f; surjec\<^bsub>F,G\<^esub> g; f \<in> aHom E F; ker\<^bsub>E,F\<^esub> f = {\<zero>\<^bsub>E\<^esub>}; g \<in> aHom F G; ker\<^bsub>F,G\<^esub> g = {\<zero>\<^bsub>F\<^esub>}; x = \<zero>\<^bsub>E\<^esub>\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>E\<^esub> \<in> ker\<^bsub>E,G\<^esub> compos E g f
 2. \<lbrakk>aGroup E; aGroup F; aGroup G; injec\<^bsub>E,F\<^esub> f; surjec\<^bsub>E,F\<^esub> f; injec\<^bsub>F,G\<^esub> g; surjec\<^bsub>F,G\<^esub> g\<rbrakk> \<Longrightarrow> surjec\<^bsub>E,G\<^esub> compos E g f
[PROOF STEP]
apply (simp add:ker_def compos_def compose_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>aGroup E; aGroup F; aGroup G; surjec\<^bsub>E,F\<^esub> f; surjec\<^bsub>F,G\<^esub> g; f \<in> aHom E F; {a \<in> carrier E. f a = \<zero>\<^bsub>F\<^esub>} = {\<zero>\<^bsub>E\<^esub>}; g \<in> aHom F G; {a \<in> carrier F. g a = \<zero>\<^bsub>G\<^esub>} = {\<zero>\<^bsub>F\<^esub>}; x = \<zero>\<^bsub>E\<^esub>\<rbrakk> \<Longrightarrow> (\<zero>\<^bsub>E\<^esub> \<in> carrier E \<longrightarrow> g (f \<zero>\<^bsub>E\<^esub>) = \<zero>\<^bsub>G\<^esub>) \<and> \<zero>\<^bsub>E\<^esub> \<in> carrier E
 2. \<lbrakk>aGroup E; aGroup F; aGroup G; injec\<^bsub>E,F\<^esub> f; surjec\<^bsub>E,F\<^esub> f; injec\<^bsub>F,G\<^esub> g; surjec\<^bsub>F,G\<^esub> g\<rbrakk> \<Longrightarrow> surjec\<^bsub>E,G\<^esub> compos E g f
[PROOF STEP]
apply (simp add:aGroup.ag_inc_zero)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>aGroup E; aGroup F; aGroup G; surjec\<^bsub>E,F\<^esub> f; surjec\<^bsub>F,G\<^esub> g; f \<in> aHom E F; {a \<in> carrier E. f a = \<zero>\<^bsub>F\<^esub>} = {\<zero>\<^bsub>E\<^esub>}; g \<in> aHom F G; {a \<in> carrier F. g a = \<zero>\<^bsub>G\<^esub>} = {\<zero>\<^bsub>F\<^esub>}; x = \<zero>\<^bsub>E\<^esub>\<rbrakk> \<Longrightarrow> g (f \<zero>\<^bsub>E\<^esub>) = \<zero>\<^bsub>G\<^esub>
 2. \<lbrakk>aGroup E; aGroup F; aGroup G; injec\<^bsub>E,F\<^esub> f; surjec\<^bsub>E,F\<^esub> f; injec\<^bsub>F,G\<^esub> g; surjec\<^bsub>F,G\<^esub> g\<rbrakk> \<Longrightarrow> surjec\<^bsub>E,G\<^esub> compos E g f
[PROOF STEP]
apply (simp add:aHom_0_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup E; aGroup F; aGroup G; injec\<^bsub>E,F\<^esub> f; surjec\<^bsub>E,F\<^esub> f; injec\<^bsub>F,G\<^esub> g; surjec\<^bsub>F,G\<^esub> g\<rbrakk> \<Longrightarrow> surjec\<^bsub>E,G\<^esub> compos E g f
[PROOF STEP]
apply (simp add:surjec_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup E; aGroup F; aGroup G; injec\<^bsub>E,F\<^esub> f; injec\<^bsub>F,G\<^esub> g; f \<in> aHom E F; surj_to f (carrier E) (carrier F); g \<in> aHom F G; surj_to g (carrier F) (carrier G)\<rbrakk> \<Longrightarrow> compos E g f \<in> aHom E G \<and> surj_to (compos E g f) (carrier E) (carrier G)
[PROOF STEP]
apply (simp add:aHom_compos)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup E; aGroup F; aGroup G; injec\<^bsub>E,F\<^esub> f; injec\<^bsub>F,G\<^esub> g; f \<in> aHom E F; surj_to f (carrier E) (carrier F); g \<in> aHom F G; surj_to g (carrier F) (carrier G)\<rbrakk> \<Longrightarrow> surj_to (compos E g f) (carrier E) (carrier G)
[PROOF STEP]
apply (simp add:aHom_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup E; aGroup F; aGroup G; injec\<^bsub>E,F\<^esub> f; injec\<^bsub>F,G\<^esub> g; surj_to f (carrier E) (carrier F); surj_to g (carrier F) (carrier G); f \<in> carrier E \<rightarrow> carrier F; g \<in> carrier F \<rightarrow> carrier G; f \<in> extensional (carrier E); \<forall>a\<in>carrier E. \<forall>b\<in>carrier E. f (a \<plusminus>\<^bsub>E\<^esub> b) = f a \<plusminus>\<^bsub>F\<^esub> f b; g \<in> extensional (carrier F); \<forall>a\<in>carrier F. \<forall>b\<in>carrier F. g (a \<plusminus>\<^bsub>F\<^esub> b) = g a \<plusminus>\<^bsub>G\<^esub> g b\<rbrakk> \<Longrightarrow> surj_to (compos E g f) (carrier E) (carrier G)
[PROOF STEP]
apply (simp add:compos_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup E; aGroup F; aGroup G; injec\<^bsub>E,F\<^esub> f; injec\<^bsub>F,G\<^esub> g; surj_to f (carrier E) (carrier F); surj_to g (carrier F) (carrier G); f \<in> carrier E \<rightarrow> carrier F; g \<in> carrier F \<rightarrow> carrier G; f \<in> extensional (carrier E); \<forall>a\<in>carrier E. \<forall>b\<in>carrier E. f (a \<plusminus>\<^bsub>E\<^esub> b) = f a \<plusminus>\<^bsub>F\<^esub> f b; g \<in> extensional (carrier F); \<forall>a\<in>carrier F. \<forall>b\<in>carrier F. g (a \<plusminus>\<^bsub>F\<^esub> b) = g a \<plusminus>\<^bsub>G\<^esub> g b\<rbrakk> \<Longrightarrow> surj_to (compose (carrier E) g f) (carrier E) (carrier G)
[PROOF STEP]
apply (rule compose_surj[of "f" "carrier E" "carrier F" "g" "carrier G"],
            assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ainvf_aHom:"\<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow>
                      ainvf\<^bsub>F,G\<^esub> f \<in> aHom G F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> ainvf\<^bsub>F,G\<^esub> f \<in> aHom G F
[PROOF STEP]
apply (subst aHom_def, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> ainvf\<^bsub>F,G\<^esub> f \<in> carrier G \<rightarrow> carrier F \<and> ainvf\<^bsub>F,G\<^esub> f \<in> extensional (carrier G) \<and> (\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. (ainvf\<^bsub>F,G\<^esub> f) (a \<plusminus>\<^bsub>G\<^esub> b) = (ainvf\<^bsub>F,G\<^esub> f) a \<plusminus>\<^bsub>F\<^esub> (ainvf\<^bsub>F,G\<^esub> f) b)
[PROOF STEP]
apply (simp add:ainvf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> carrier G \<rightarrow> carrier F \<and> f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> extensional (carrier G) \<and> (\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) = (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b)
[PROOF STEP]
apply (simp add:bijec_def, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; injec\<^bsub>F,G\<^esub> f; surjec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> carrier G \<rightarrow> carrier F \<and> f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> extensional (carrier G) \<and> (\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) = (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b)
[PROOF STEP]
apply (frule injec_inj_on[of "F" "G" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; injec\<^bsub>F,G\<^esub> f; surjec\<^bsub>F,G\<^esub> f; inj_on f (carrier F)\<rbrakk> \<Longrightarrow> f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> carrier G \<rightarrow> carrier F \<and> f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> extensional (carrier G) \<and> (\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) = (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b)
[PROOF STEP]
apply (simp add:surjec_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; injec\<^bsub>F,G\<^esub> f; inj_on f (carrier F); f \<in> aHom F G; surj_to f (carrier F) (carrier G)\<rbrakk> \<Longrightarrow> f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> carrier G \<rightarrow> carrier F \<and> f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> extensional (carrier G) \<and> (\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) = (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b)
[PROOF STEP]
apply (simp add:aHom_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; injec\<^bsub>F,G\<^esub> f; inj_on f (carrier F); surj_to f (carrier F) (carrier G); f \<in> carrier F \<rightarrow> carrier G; f \<in> extensional (carrier F); \<forall>a\<in>carrier F. \<forall>b\<in>carrier F. f (a \<plusminus>\<^bsub>F\<^esub> b) = f a \<plusminus>\<^bsub>G\<^esub> f b\<rbrakk> \<Longrightarrow> f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> carrier G \<rightarrow> carrier F \<and> f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> extensional (carrier G) \<and> (\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) = (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b)
[PROOF STEP]
apply (frule inv_func[of "f" "carrier F" "carrier G"], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; injec\<^bsub>F,G\<^esub> f; inj_on f (carrier F); surj_to f (carrier F) (carrier G); f \<in> carrier F \<rightarrow> carrier G; f \<in> extensional (carrier F); \<forall>a\<in>carrier F. \<forall>b\<in>carrier F. f (a \<plusminus>\<^bsub>F\<^esub> b) = f a \<plusminus>\<^bsub>G\<^esub> f b; f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> carrier G \<rightarrow> carrier F\<rbrakk> \<Longrightarrow> f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> extensional (carrier G) \<and> (\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) = (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup F; aGroup G; injec\<^bsub>F,G\<^esub> f; inj_on f (carrier F); surj_to f (carrier F) (carrier G); f \<in> carrier F \<rightarrow> carrier G; f \<in> extensional (carrier F); \<forall>a\<in>carrier F. \<forall>b\<in>carrier F. f (a \<plusminus>\<^bsub>F\<^esub> b) = f a \<plusminus>\<^bsub>G\<^esub> f b; f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> carrier G \<rightarrow> carrier F\<rbrakk> \<Longrightarrow> f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> extensional (carrier G)
 2. \<lbrakk>aGroup F; aGroup G; injec\<^bsub>F,G\<^esub> f; inj_on f (carrier F); surj_to f (carrier F) (carrier G); f \<in> carrier F \<rightarrow> carrier G; f \<in> extensional (carrier F); \<forall>a\<in>carrier F. \<forall>b\<in>carrier F. f (a \<plusminus>\<^bsub>F\<^esub> b) = f a \<plusminus>\<^bsub>G\<^esub> f b; f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> carrier G \<rightarrow> carrier F\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier G. \<forall>b\<in>carrier G. (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) = (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b
[PROOF STEP]
apply (simp add:invfun_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; injec\<^bsub>F,G\<^esub> f; inj_on f (carrier F); surj_to f (carrier F) (carrier G); f \<in> carrier F \<rightarrow> carrier G; f \<in> extensional (carrier F); \<forall>a\<in>carrier F. \<forall>b\<in>carrier F. f (a \<plusminus>\<^bsub>F\<^esub> b) = f a \<plusminus>\<^bsub>G\<^esub> f b; f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> carrier G \<rightarrow> carrier F\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier G. \<forall>b\<in>carrier G. (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) = (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup F; aGroup G; injec\<^bsub>F,G\<^esub> f; inj_on f (carrier F); surj_to f (carrier F) (carrier G); f \<in> carrier F \<rightarrow> carrier G; f \<in> extensional (carrier F); \<forall>a\<in>carrier F. \<forall>b\<in>carrier F. f (a \<plusminus>\<^bsub>F\<^esub> b) = f a \<plusminus>\<^bsub>G\<^esub> f b; f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> carrier G \<rightarrow> carrier F; a \<in> carrier G; b \<in> carrier G\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) = (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b
[PROOF STEP]
apply (frule_tac x = a in funcset_mem[of "Ifn F G f" "carrier G" "carrier F"],
      assumption+,
      frule_tac x = b in funcset_mem[of "Ifn F G f" "carrier G" "carrier F"],
      assumption+,
      frule_tac x = a and y = b in aGroup.ag_pOp_closed[of "G"], assumption+,
      frule_tac x = "a \<plusminus>\<^bsub>G\<^esub> b" in funcset_mem[of "Ifn F G f" "carrier G"
       "carrier F"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup F; aGroup G; injec\<^bsub>F,G\<^esub> f; inj_on f (carrier F); surj_to f (carrier F) (carrier G); f \<in> carrier F \<rightarrow> carrier G; f \<in> extensional (carrier F); \<forall>a\<in>carrier F. \<forall>b\<in>carrier F. f (a \<plusminus>\<^bsub>F\<^esub> b) = f a \<plusminus>\<^bsub>G\<^esub> f b; f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> carrier G \<rightarrow> carrier F; a \<in> carrier G; b \<in> carrier G; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<in> carrier F; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b \<in> carrier F; a \<plusminus>\<^bsub>G\<^esub> b \<in> carrier G; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) \<in> carrier F\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) = (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b
[PROOF STEP]
apply (frule_tac a = "(Ifn F G f) a" and b = "(Ifn F G f) b" in
           aHom_add[of "F" "G" "f"], assumption+, simp add:injec_def,
           assumption+,
           thin_tac "\<forall>a\<in>carrier F. \<forall>b\<in>carrier F. f (a \<plusminus>\<^bsub>F\<^esub> b) = f a \<plusminus>\<^bsub>G\<^esub> f b")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup F; aGroup G; injec\<^bsub>F,G\<^esub> f; inj_on f (carrier F); surj_to f (carrier F) (carrier G); f \<in> carrier F \<rightarrow> carrier G; f \<in> extensional (carrier F); f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> carrier G \<rightarrow> carrier F; a \<in> carrier G; b \<in> carrier G; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<in> carrier F; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b \<in> carrier F; a \<plusminus>\<^bsub>G\<^esub> b \<in> carrier G; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) \<in> carrier F; f ((f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b) = f ((f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a) \<plusminus>\<^bsub>G\<^esub> f ((f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b)\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) = (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b
[PROOF STEP]
apply (simp add:invfun_r[of "f" "carrier F" "carrier G"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup F; aGroup G; injec\<^bsub>F,G\<^esub> f; inj_on f (carrier F); surj_to f (carrier F) (carrier G); f \<in> carrier F \<rightarrow> carrier G; f \<in> extensional (carrier F); f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> carrier G \<rightarrow> carrier F; a \<in> carrier G; b \<in> carrier G; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<in> carrier F; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b \<in> carrier F; a \<plusminus>\<^bsub>G\<^esub> b \<in> carrier G; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) \<in> carrier F; f ((f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b) = a \<plusminus>\<^bsub>G\<^esub> b\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) = (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b
[PROOF STEP]
apply (frule_tac x = a and y = b in aGroup.ag_pOp_closed[of "G"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup F; aGroup G; injec\<^bsub>F,G\<^esub> f; inj_on f (carrier F); surj_to f (carrier F) (carrier G); f \<in> carrier F \<rightarrow> carrier G; f \<in> extensional (carrier F); f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> carrier G \<rightarrow> carrier F; a \<in> carrier G; b \<in> carrier G; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<in> carrier F; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b \<in> carrier F; a \<plusminus>\<^bsub>G\<^esub> b \<in> carrier G; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) \<in> carrier F; f ((f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b) = a \<plusminus>\<^bsub>G\<^esub> b; a \<plusminus>\<^bsub>G\<^esub> b \<in> carrier G\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) = (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b
[PROOF STEP]
apply (frule_tac b = "a \<plusminus>\<^bsub>G\<^esub> b" in invfun_r[of "f" "carrier F" "carrier G"],
           assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup F; aGroup G; injec\<^bsub>F,G\<^esub> f; inj_on f (carrier F); surj_to f (carrier F) (carrier G); f \<in> carrier F \<rightarrow> carrier G; f \<in> extensional (carrier F); f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> carrier G \<rightarrow> carrier F; a \<in> carrier G; b \<in> carrier G; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<in> carrier F; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b \<in> carrier F; a \<plusminus>\<^bsub>G\<^esub> b \<in> carrier G; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) \<in> carrier F; f ((f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b) = a \<plusminus>\<^bsub>G\<^esub> b; a \<plusminus>\<^bsub>G\<^esub> b \<in> carrier G; f ((f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b)) = a \<plusminus>\<^bsub>G\<^esub> b\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) = (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b
[PROOF STEP]
apply (simp add:inj_on_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup F; aGroup G; injec\<^bsub>F,G\<^esub> f; \<forall>x\<in>carrier F. \<forall>y\<in>carrier F. f x = f y \<longrightarrow> x = y; surj_to f (carrier F) (carrier G); f \<in> carrier F \<rightarrow> carrier G; f \<in> extensional (carrier F); f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> carrier G \<rightarrow> carrier F; a \<in> carrier G; b \<in> carrier G; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<in> carrier F; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b \<in> carrier F; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) \<in> carrier F; f ((f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b) = a \<plusminus>\<^bsub>G\<^esub> b; a \<plusminus>\<^bsub>G\<^esub> b \<in> carrier G; f ((f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b)) = a \<plusminus>\<^bsub>G\<^esub> b\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) = (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b
[PROOF STEP]
apply (frule_tac x = "(Ifn F G f) a" and y = "(Ifn F G f) b" in
          aGroup.ag_pOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup F; aGroup G; injec\<^bsub>F,G\<^esub> f; \<forall>x\<in>carrier F. \<forall>y\<in>carrier F. f x = f y \<longrightarrow> x = y; surj_to f (carrier F) (carrier G); f \<in> carrier F \<rightarrow> carrier G; f \<in> extensional (carrier F); f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> carrier G \<rightarrow> carrier F; a \<in> carrier G; b \<in> carrier G; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<in> carrier F; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b \<in> carrier F; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) \<in> carrier F; f ((f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b) = a \<plusminus>\<^bsub>G\<^esub> b; a \<plusminus>\<^bsub>G\<^esub> b \<in> carrier G; f ((f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b)) = a \<plusminus>\<^bsub>G\<^esub> b; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b \<in> carrier F\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) = (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b
[PROOF STEP]
apply (frule_tac x = "(Ifn F G f) (a \<plusminus>\<^bsub>G\<^esub> b)" in bspec, assumption,
        thin_tac "\<forall>x\<in>carrier F. \<forall>y\<in>carrier F. f x = f y \<longrightarrow> x = y")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup F; aGroup G; injec\<^bsub>F,G\<^esub> f; surj_to f (carrier F) (carrier G); f \<in> carrier F \<rightarrow> carrier G; f \<in> extensional (carrier F); f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> carrier G \<rightarrow> carrier F; a \<in> carrier G; b \<in> carrier G; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<in> carrier F; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b \<in> carrier F; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) \<in> carrier F; f ((f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b) = a \<plusminus>\<^bsub>G\<^esub> b; a \<plusminus>\<^bsub>G\<^esub> b \<in> carrier G; f ((f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b)) = a \<plusminus>\<^bsub>G\<^esub> b; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b \<in> carrier F; \<forall>y\<in>carrier F. f ((f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b)) = f y \<longrightarrow> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) = y\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) = (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b
[PROOF STEP]
apply (frule_tac x = "(Ifn F G f) a \<plusminus>\<^bsub>F\<^esub> (Ifn F G f) b" in bspec,
            assumption,
        thin_tac "\<forall>y\<in>carrier F.
              f ((Ifn F G f) (a \<plusminus>\<^bsub>G\<^esub> b)) = f y \<longrightarrow> (Ifn F G f) (a \<plusminus>\<^bsub>G\<^esub> b) = y")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup F; aGroup G; injec\<^bsub>F,G\<^esub> f; surj_to f (carrier F) (carrier G); f \<in> carrier F \<rightarrow> carrier G; f \<in> extensional (carrier F); f\<inverse>\<^bsub>carrier G,carrier F\<^esub> \<in> carrier G \<rightarrow> carrier F; a \<in> carrier G; b \<in> carrier G; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<in> carrier F; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b \<in> carrier F; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) \<in> carrier F; f ((f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b) = a \<plusminus>\<^bsub>G\<^esub> b; a \<plusminus>\<^bsub>G\<^esub> b \<in> carrier G; f ((f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b)) = a \<plusminus>\<^bsub>G\<^esub> b; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b \<in> carrier F; f ((f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b)) = f ((f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b) \<longrightarrow> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) = (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) (a \<plusminus>\<^bsub>G\<^esub> b) = (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a \<plusminus>\<^bsub>F\<^esub> (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ainvf_bijec:"\<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> bijec\<^bsub>G,F\<^esub> (ainvf\<^bsub>F,G\<^esub> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> bijec\<^bsub>G,F\<^esub> (ainvf\<^bsub>F,G\<^esub> f)
[PROOF STEP]
apply (subst bijec_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> injec\<^bsub>G,F\<^esub> (ainvf\<^bsub>F,G\<^esub> f) \<and> surjec\<^bsub>G,F\<^esub> (ainvf\<^bsub>F,G\<^esub> f)
[PROOF STEP]
apply (simp add:injec_def surjec_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> ainvf\<^bsub>F,G\<^esub> f \<in> aHom G F \<and> ker\<^bsub>G,F\<^esub> (ainvf\<^bsub>F,G\<^esub> f) = {\<zero>\<^bsub>G\<^esub>} \<and> ainvf\<^bsub>F,G\<^esub> f \<in> aHom G F \<and> surj_to (ainvf\<^bsub>F,G\<^esub> f) (carrier G) (carrier F)
[PROOF STEP]
apply (simp add:ainvf_aHom)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> ker\<^bsub>G,F\<^esub> (ainvf\<^bsub>F,G\<^esub> f) = {\<zero>\<^bsub>G\<^esub>} \<and> surj_to (ainvf\<^bsub>F,G\<^esub> f) (carrier G) (carrier F)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> ker\<^bsub>G,F\<^esub> (ainvf\<^bsub>F,G\<^esub> f) = {\<zero>\<^bsub>G\<^esub>}
 2. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> surj_to (ainvf\<^bsub>F,G\<^esub> f) (carrier G) (carrier F)
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> ker\<^bsub>G,F\<^esub> (ainvf\<^bsub>F,G\<^esub> f) \<subseteq> {\<zero>\<^bsub>G\<^esub>}
 2. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>G\<^esub>} \<subseteq> ker\<^bsub>G,F\<^esub> (ainvf\<^bsub>F,G\<^esub> f)
 3. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> surj_to (ainvf\<^bsub>F,G\<^esub> f) (carrier G) (carrier F)
[PROOF STEP]
apply (rule subsetI, simp add:ker_def, erule conjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f; x \<in> carrier G; (ainvf\<^bsub>F,G\<^esub> f) x = \<zero>\<^bsub>F\<^esub>\<rbrakk> \<Longrightarrow> x = \<zero>\<^bsub>G\<^esub>
 2. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>G\<^esub>} \<subseteq> ker\<^bsub>G,F\<^esub> (ainvf\<^bsub>F,G\<^esub> f)
 3. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> surj_to (ainvf\<^bsub>F,G\<^esub> f) (carrier G) (carrier F)
[PROOF STEP]
apply (simp add:ainvf_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f; x \<in> carrier G; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) x = \<zero>\<^bsub>F\<^esub>\<rbrakk> \<Longrightarrow> x = \<zero>\<^bsub>G\<^esub>
 2. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>G\<^esub>} \<subseteq> ker\<^bsub>G,F\<^esub> (ainvf\<^bsub>F,G\<^esub> f)
 3. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> surj_to (ainvf\<^bsub>F,G\<^esub> f) (carrier G) (carrier F)
[PROOF STEP]
apply (simp add:bijec_def,(erule conjE)+, simp add:surjec_def,
         (erule conjE)+, simp add:aHom_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>aGroup F; aGroup G; x \<in> carrier G; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) x = \<zero>\<^bsub>F\<^esub>; injec\<^bsub>F,G\<^esub> f; surj_to f (carrier F) (carrier G); f \<in> carrier F \<rightarrow> carrier G; f \<in> extensional (carrier F); \<forall>a\<in>carrier F. \<forall>b\<in>carrier F. f (a \<plusminus>\<^bsub>F\<^esub> b) = f a \<plusminus>\<^bsub>G\<^esub> f b\<rbrakk> \<Longrightarrow> x = \<zero>\<^bsub>G\<^esub>
 2. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>G\<^esub>} \<subseteq> ker\<^bsub>G,F\<^esub> (ainvf\<^bsub>F,G\<^esub> f)
 3. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> surj_to (ainvf\<^bsub>F,G\<^esub> f) (carrier G) (carrier F)
[PROOF STEP]
apply (frule injec_inj_on[of "F" "G" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>aGroup F; aGroup G; x \<in> carrier G; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) x = \<zero>\<^bsub>F\<^esub>; injec\<^bsub>F,G\<^esub> f; surj_to f (carrier F) (carrier G); f \<in> carrier F \<rightarrow> carrier G; f \<in> extensional (carrier F); \<forall>a\<in>carrier F. \<forall>b\<in>carrier F. f (a \<plusminus>\<^bsub>F\<^esub> b) = f a \<plusminus>\<^bsub>G\<^esub> f b; inj_on f (carrier F)\<rbrakk> \<Longrightarrow> x = \<zero>\<^bsub>G\<^esub>
 2. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>G\<^esub>} \<subseteq> ker\<^bsub>G,F\<^esub> (ainvf\<^bsub>F,G\<^esub> f)
 3. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> surj_to (ainvf\<^bsub>F,G\<^esub> f) (carrier G) (carrier F)
[PROOF STEP]
apply (subst invfun_r[THEN sym, of "f" "carrier F" "carrier G"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>aGroup F; aGroup G; x \<in> carrier G; (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) x = \<zero>\<^bsub>F\<^esub>; injec\<^bsub>F,G\<^esub> f; surj_to f (carrier F) (carrier G); f \<in> carrier F \<rightarrow> carrier G; f \<in> extensional (carrier F); \<forall>a\<in>carrier F. \<forall>b\<in>carrier F. f (a \<plusminus>\<^bsub>F\<^esub> b) = f a \<plusminus>\<^bsub>G\<^esub> f b; inj_on f (carrier F)\<rbrakk> \<Longrightarrow> f ((f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) x) = \<zero>\<^bsub>G\<^esub>
 2. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>G\<^esub>} \<subseteq> ker\<^bsub>G,F\<^esub> (ainvf\<^bsub>F,G\<^esub> f)
 3. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> surj_to (ainvf\<^bsub>F,G\<^esub> f) (carrier G) (carrier F)
[PROOF STEP]
apply (simp add:injec_def, (erule conjE)+, simp add:aHom_0_0)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>G\<^esub>} \<subseteq> ker\<^bsub>G,F\<^esub> (ainvf\<^bsub>F,G\<^esub> f)
 2. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> surj_to (ainvf\<^bsub>F,G\<^esub> f) (carrier G) (carrier F)
[PROOF STEP]
apply (rule subsetI, simp add:ker_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f; x = \<zero>\<^bsub>G\<^esub>\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>G\<^esub> \<in> carrier G \<and> (ainvf\<^bsub>F,G\<^esub> f) \<zero>\<^bsub>G\<^esub> = \<zero>\<^bsub>F\<^esub>
 2. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> surj_to (ainvf\<^bsub>F,G\<^esub> f) (carrier G) (carrier F)
[PROOF STEP]
apply (simp add:aGroup.ex_zero)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f; x = \<zero>\<^bsub>G\<^esub>\<rbrakk> \<Longrightarrow> (ainvf\<^bsub>F,G\<^esub> f) \<zero>\<^bsub>G\<^esub> = \<zero>\<^bsub>F\<^esub>
 2. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> surj_to (ainvf\<^bsub>F,G\<^esub> f) (carrier G) (carrier F)
[PROOF STEP]
apply (frule ainvf_aHom[of "F" "G" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f; x = \<zero>\<^bsub>G\<^esub>; ainvf\<^bsub>F,G\<^esub> f \<in> aHom G F\<rbrakk> \<Longrightarrow> (ainvf\<^bsub>F,G\<^esub> f) \<zero>\<^bsub>G\<^esub> = \<zero>\<^bsub>F\<^esub>
 2. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> surj_to (ainvf\<^bsub>F,G\<^esub> f) (carrier G) (carrier F)
[PROOF STEP]
apply (simp add:aHom_0_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> surj_to (ainvf\<^bsub>F,G\<^esub> f) (carrier G) (carrier F)
[PROOF STEP]
apply (frule ainvf_aHom[of "F" "G" "f"], assumption+,
        simp add:aHom_def, (erule conjE)+,
       rule surj_to_test[of "ainvf\<^bsub>F,G\<^esub> f" "carrier G" "carrier F"],
        assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f; ainvf\<^bsub>F,G\<^esub> f \<in> carrier G \<rightarrow> carrier F; ainvf\<^bsub>F,G\<^esub> f \<in> extensional (carrier G); \<forall>a\<in>carrier G. \<forall>b\<in>carrier G. (ainvf\<^bsub>F,G\<^esub> f) (a \<plusminus>\<^bsub>G\<^esub> b) = (ainvf\<^bsub>F,G\<^esub> f) a \<plusminus>\<^bsub>F\<^esub> (ainvf\<^bsub>F,G\<^esub> f) b\<rbrakk> \<Longrightarrow> \<forall>b\<in>carrier F. \<exists>a\<in>carrier G. (ainvf\<^bsub>F,G\<^esub> f) a = b
[PROOF STEP]
apply (rule ballI,
        thin_tac "\<forall>a\<in>carrier G. \<forall>b\<in>carrier G.
               (ainvf\<^bsub>F,G\<^esub> f) (a \<plusminus>\<^bsub>G\<^esub> b) = (ainvf\<^bsub>F,G\<^esub> f) a \<plusminus>\<^bsub>F\<^esub> (ainvf\<^bsub>F,G\<^esub> f) b")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>aGroup F; aGroup G; bijec\<^bsub>F,G\<^esub> f; ainvf\<^bsub>F,G\<^esub> f \<in> carrier G \<rightarrow> carrier F; ainvf\<^bsub>F,G\<^esub> f \<in> extensional (carrier G); b \<in> carrier F\<rbrakk> \<Longrightarrow> \<exists>a\<in>carrier G. (ainvf\<^bsub>F,G\<^esub> f) a = b
[PROOF STEP]
apply (simp add:bijec_def, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>aGroup F; aGroup G; ainvf\<^bsub>F,G\<^esub> f \<in> carrier G \<rightarrow> carrier F; ainvf\<^bsub>F,G\<^esub> f \<in> extensional (carrier G); b \<in> carrier F; injec\<^bsub>F,G\<^esub> f; surjec\<^bsub>F,G\<^esub> f\<rbrakk> \<Longrightarrow> \<exists>a\<in>carrier G. (ainvf\<^bsub>F,G\<^esub> f) a = b
[PROOF STEP]
apply (frule injec_inj_on[of "F" "G" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>aGroup F; aGroup G; ainvf\<^bsub>F,G\<^esub> f \<in> carrier G \<rightarrow> carrier F; ainvf\<^bsub>F,G\<^esub> f \<in> extensional (carrier G); b \<in> carrier F; injec\<^bsub>F,G\<^esub> f; surjec\<^bsub>F,G\<^esub> f; inj_on f (carrier F)\<rbrakk> \<Longrightarrow> \<exists>a\<in>carrier G. (ainvf\<^bsub>F,G\<^esub> f) a = b
[PROOF STEP]
apply (simp add:surjec_def aHom_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>aGroup F; aGroup G; ainvf\<^bsub>F,G\<^esub> f \<in> carrier G \<rightarrow> carrier F; ainvf\<^bsub>F,G\<^esub> f \<in> extensional (carrier G); b \<in> carrier F; injec\<^bsub>F,G\<^esub> f; inj_on f (carrier F); f \<in> carrier F \<rightarrow> carrier G; f \<in> extensional (carrier F); \<forall>a\<in>carrier F. \<forall>b\<in>carrier F. f (a \<plusminus>\<^bsub>F\<^esub> b) = f a \<plusminus>\<^bsub>G\<^esub> f b; surj_to f (carrier F) (carrier G)\<rbrakk> \<Longrightarrow> \<exists>a\<in>carrier G. (ainvf\<^bsub>F,G\<^esub> f) a = b
[PROOF STEP]
apply (subst ainvf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>aGroup F; aGroup G; ainvf\<^bsub>F,G\<^esub> f \<in> carrier G \<rightarrow> carrier F; ainvf\<^bsub>F,G\<^esub> f \<in> extensional (carrier G); b \<in> carrier F; injec\<^bsub>F,G\<^esub> f; inj_on f (carrier F); f \<in> carrier F \<rightarrow> carrier G; f \<in> extensional (carrier F); \<forall>a\<in>carrier F. \<forall>b\<in>carrier F. f (a \<plusminus>\<^bsub>F\<^esub> b) = f a \<plusminus>\<^bsub>G\<^esub> f b; surj_to f (carrier F) (carrier G)\<rbrakk> \<Longrightarrow> \<exists>a\<in>carrier G. (f\<inverse>\<^bsub>carrier G,carrier F\<^esub>) a = b
[PROOF STEP]
apply (frule_tac a = b in invfun_l[of "f" "carrier F" "carrier G"],
                  assumption+,
        frule_tac x = b in funcset_mem[of "f" "carrier F" "carrier G"],
                  assumption+, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ainvf_l:"\<lbrakk>aGroup E; aGroup F; bijec\<^bsub>E,F\<^esub> f; x \<in> carrier E\<rbrakk> \<Longrightarrow>
                      (ainvf\<^bsub>E,F\<^esub> f) (f x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup E; aGroup F; bijec\<^bsub>E,F\<^esub> f; x \<in> carrier E\<rbrakk> \<Longrightarrow> (ainvf\<^bsub>E,F\<^esub> f) (f x) = x
[PROOF STEP]
apply (simp add:bijec_def, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup E; aGroup F; x \<in> carrier E; injec\<^bsub>E,F\<^esub> f; surjec\<^bsub>E,F\<^esub> f\<rbrakk> \<Longrightarrow> (ainvf\<^bsub>E,F\<^esub> f) (f x) = x
[PROOF STEP]
apply (frule injec_inj_on[of "E" "F" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup E; aGroup F; x \<in> carrier E; injec\<^bsub>E,F\<^esub> f; surjec\<^bsub>E,F\<^esub> f; inj_on f (carrier E)\<rbrakk> \<Longrightarrow> (ainvf\<^bsub>E,F\<^esub> f) (f x) = x
[PROOF STEP]
apply (simp add:surjec_def aHom_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup E; aGroup F; x \<in> carrier E; injec\<^bsub>E,F\<^esub> f; inj_on f (carrier E); f \<in> carrier E \<rightarrow> carrier F; f \<in> extensional (carrier E); \<forall>a\<in>carrier E. \<forall>b\<in>carrier E. f (a \<plusminus>\<^bsub>E\<^esub> b) = f a \<plusminus>\<^bsub>F\<^esub> f b; surj_to f (carrier E) (carrier F)\<rbrakk> \<Longrightarrow> (ainvf\<^bsub>E,F\<^esub> f) (f x) = x
[PROOF STEP]
apply (frule invfun_l[of "f" "carrier E" "carrier F" "x"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup E; aGroup F; x \<in> carrier E; injec\<^bsub>E,F\<^esub> f; inj_on f (carrier E); f \<in> carrier E \<rightarrow> carrier F; f \<in> extensional (carrier E); \<forall>a\<in>carrier E. \<forall>b\<in>carrier E. f (a \<plusminus>\<^bsub>E\<^esub> b) = f a \<plusminus>\<^bsub>F\<^esub> f b; surj_to f (carrier E) (carrier F); (f\<inverse>\<^bsub>carrier F,carrier E\<^esub>) (f x) = x\<rbrakk> \<Longrightarrow> (ainvf\<^bsub>E,F\<^esub> f) (f x) = x
[PROOF STEP]
apply (simp add:ainvf_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) aI_aHom:"aI\<^bsub>A\<^esub> \<in> aHom A A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aI\<^bsub>A\<^esub> \<in> aHom A A
[PROOF STEP]
by (simp add:aHom_def ag_idmap_def ag_idmap_def ag_pOp_closed)


[STATEMENT]
lemma compos_aI_l:"\<lbrakk>aGroup A; aGroup B; f \<in> aHom A B\<rbrakk> \<Longrightarrow> compos A aI\<^bsub>B\<^esub> f = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B\<rbrakk> \<Longrightarrow> compos A aI\<^bsub>B\<^esub> f = f
[PROOF STEP]
apply (simp add:compos_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B\<rbrakk> \<Longrightarrow> compose (carrier A) aI\<^bsub>B\<^esub> f = f
[PROOF STEP]
apply (rule funcset_eq[of _ "carrier A"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B\<rbrakk> \<Longrightarrow> compose (carrier A) aI\<^bsub>B\<^esub> f \<in> extensional (carrier A)
 2. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B\<rbrakk> \<Longrightarrow> f \<in> extensional (carrier A)
 3. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier A. compose (carrier A) aI\<^bsub>B\<^esub> f x = f x
[PROOF STEP]
apply (simp add:compose_def extensional_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B\<rbrakk> \<Longrightarrow> f \<in> extensional (carrier A)
 2. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier A. compose (carrier A) aI\<^bsub>B\<^esub> f x = f x
[PROOF STEP]
apply (simp add:aHom_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier A. compose (carrier A) aI\<^bsub>B\<^esub> f x = f x
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; x \<in> carrier A\<rbrakk> \<Longrightarrow> compose (carrier A) aI\<^bsub>B\<^esub> f x = f x
[PROOF STEP]
apply (frule_tac a = x in aHom_mem[of "A" "B" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; x \<in> carrier A; f x \<in> carrier B\<rbrakk> \<Longrightarrow> compose (carrier A) aI\<^bsub>B\<^esub> f x = f x
[PROOF STEP]
apply (simp add:compose_def ag_idmap_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma compos_aI_r:"\<lbrakk>aGroup A; aGroup B; f \<in> aHom A B\<rbrakk> \<Longrightarrow> compos A f aI\<^bsub>A\<^esub> = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B\<rbrakk> \<Longrightarrow> compos A f aI\<^bsub>A\<^esub> = f
[PROOF STEP]
apply (simp add:compos_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B\<rbrakk> \<Longrightarrow> compose (carrier A) f aI\<^bsub>A\<^esub> = f
[PROOF STEP]
apply (rule funcset_eq[of _ "carrier A"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B\<rbrakk> \<Longrightarrow> compose (carrier A) f aI\<^bsub>A\<^esub> \<in> extensional (carrier A)
 2. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B\<rbrakk> \<Longrightarrow> f \<in> extensional (carrier A)
 3. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier A. compose (carrier A) f aI\<^bsub>A\<^esub> x = f x
[PROOF STEP]
apply (simp add:compose_def extensional_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B\<rbrakk> \<Longrightarrow> f \<in> extensional (carrier A)
 2. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier A. compose (carrier A) f aI\<^bsub>A\<^esub> x = f x
[PROOF STEP]
apply (simp add:aHom_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier A. compose (carrier A) f aI\<^bsub>A\<^esub> x = f x
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; x \<in> carrier A\<rbrakk> \<Longrightarrow> compose (carrier A) f aI\<^bsub>A\<^esub> x = f x
[PROOF STEP]
apply (simp add:compose_def ag_idmap_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma compos_aI_surj:"\<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A;
                      compos A g f = aI\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> surjec\<^bsub>B,A\<^esub> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; compos A g f = aI\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> surjec\<^bsub>B,A\<^esub> g
[PROOF STEP]
apply (simp add:surjec_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; compos A g f = aI\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> surj_to g (carrier B) (carrier A)
[PROOF STEP]
apply (rule surj_to_test[of "g" "carrier B" "carrier A"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; compos A g f = aI\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> g \<in> carrier B \<rightarrow> carrier A
 2. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; compos A g f = aI\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> \<forall>b\<in>carrier A. \<exists>a\<in>carrier B. g a = b
[PROOF STEP]
apply (simp add:aHom_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; compos A g f = aI\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> \<forall>b\<in>carrier A. \<exists>a\<in>carrier B. g a = b
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; compos A g f = aI\<^bsub>A\<^esub>; b \<in> carrier A\<rbrakk> \<Longrightarrow> \<exists>a\<in>carrier B. g a = b
[PROOF STEP]
apply (subgoal_tac "compos A g f b = aI\<^bsub>A\<^esub> b",
        thin_tac "compos A g f = aI\<^bsub>A\<^esub>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; b \<in> carrier A; compos A g f b = aI\<^bsub>A\<^esub> b\<rbrakk> \<Longrightarrow> \<exists>a\<in>carrier B. g a = b
 2. \<And>b. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; compos A g f = aI\<^bsub>A\<^esub>; b \<in> carrier A\<rbrakk> \<Longrightarrow> compos A g f b = aI\<^bsub>A\<^esub> b
[PROOF STEP]
apply (simp add:compos_def compose_def ag_idmap_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; b \<in> carrier A; g (f b) = b\<rbrakk> \<Longrightarrow> \<exists>a\<in>carrier B. g a = b
 2. \<And>b. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; compos A g f = aI\<^bsub>A\<^esub>; b \<in> carrier A\<rbrakk> \<Longrightarrow> compos A g f b = aI\<^bsub>A\<^esub> b
[PROOF STEP]
apply (frule_tac a = b in aHom_mem[of "A" "B" "f"], assumption+, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; compos A g f = aI\<^bsub>A\<^esub>; b \<in> carrier A\<rbrakk> \<Longrightarrow> compos A g f b = aI\<^bsub>A\<^esub> b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma compos_aI_inj:"\<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A;
                      compos A g f = aI\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> injec\<^bsub>A,B\<^esub> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; compos A g f = aI\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> injec\<^bsub>A,B\<^esub> f
[PROOF STEP]
apply (simp add:injec_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; compos A g f = aI\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> ker\<^bsub>A,B\<^esub> f = {\<zero>\<^bsub>A\<^esub>}
[PROOF STEP]
apply (simp add:ker_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; compos A g f = aI\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> {a \<in> carrier A. f a = \<zero>\<^bsub>B\<^esub>} = {\<zero>\<^bsub>A\<^esub>}
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; compos A g f = aI\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> {a \<in> carrier A. f a = \<zero>\<^bsub>B\<^esub>} \<subseteq> {\<zero>\<^bsub>A\<^esub>}
 2. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; compos A g f = aI\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>A\<^esub>} \<subseteq> {a \<in> carrier A. f a = \<zero>\<^bsub>B\<^esub>}
[PROOF STEP]
apply (rule subsetI, simp, erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; compos A g f = aI\<^bsub>A\<^esub>; x \<in> carrier A; f x = \<zero>\<^bsub>B\<^esub>\<rbrakk> \<Longrightarrow> x = \<zero>\<^bsub>A\<^esub>
 2. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; compos A g f = aI\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>A\<^esub>} \<subseteq> {a \<in> carrier A. f a = \<zero>\<^bsub>B\<^esub>}
[PROOF STEP]
apply (subgoal_tac "compos A g f x = aI\<^bsub>A\<^esub> x",
        thin_tac "compos A g f = aI\<^bsub>A\<^esub>")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; x \<in> carrier A; f x = \<zero>\<^bsub>B\<^esub>; compos A g f x = aI\<^bsub>A\<^esub> x\<rbrakk> \<Longrightarrow> x = \<zero>\<^bsub>A\<^esub>
 2. \<And>x. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; compos A g f = aI\<^bsub>A\<^esub>; x \<in> carrier A; f x = \<zero>\<^bsub>B\<^esub>\<rbrakk> \<Longrightarrow> compos A g f x = aI\<^bsub>A\<^esub> x
 3. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; compos A g f = aI\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>A\<^esub>} \<subseteq> {a \<in> carrier A. f a = \<zero>\<^bsub>B\<^esub>}
[PROOF STEP]
apply (simp add:compos_def compose_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; x \<in> carrier A; f x = \<zero>\<^bsub>B\<^esub>; g \<zero>\<^bsub>B\<^esub> = aI\<^bsub>A\<^esub> x\<rbrakk> \<Longrightarrow> x = \<zero>\<^bsub>A\<^esub>
 2. \<And>x. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; compos A g f = aI\<^bsub>A\<^esub>; x \<in> carrier A; f x = \<zero>\<^bsub>B\<^esub>\<rbrakk> \<Longrightarrow> compos A g f x = aI\<^bsub>A\<^esub> x
 3. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; compos A g f = aI\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>A\<^esub>} \<subseteq> {a \<in> carrier A. f a = \<zero>\<^bsub>B\<^esub>}
[PROOF STEP]
apply (simp add:aHom_0_0 ag_idmap_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; compos A g f = aI\<^bsub>A\<^esub>; x \<in> carrier A; f x = \<zero>\<^bsub>B\<^esub>\<rbrakk> \<Longrightarrow> compos A g f x = aI\<^bsub>A\<^esub> x
 2. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; compos A g f = aI\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>A\<^esub>} \<subseteq> {a \<in> carrier A. f a = \<zero>\<^bsub>B\<^esub>}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; compos A g f = aI\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> {\<zero>\<^bsub>A\<^esub>} \<subseteq> {a \<in> carrier A. f a = \<zero>\<^bsub>B\<^esub>}
[PROOF STEP]
apply (rule subsetI, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>aGroup A; aGroup B; f \<in> aHom A B; g \<in> aHom B A; compos A g f = aI\<^bsub>A\<^esub>; x = \<zero>\<^bsub>A\<^esub>\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>A\<^esub> \<in> carrier A \<and> f \<zero>\<^bsub>A\<^esub> = \<zero>\<^bsub>B\<^esub>
[PROOF STEP]
apply (simp add:aGroup.ag_inc_zero aHom_0_0)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) Ag_ind_aHom:"\<lbrakk>f \<in> carrier A \<rightarrow> D;
      bij_to f (carrier A) (D::'d set)\<rbrakk> \<Longrightarrow> Agii A f \<in> aHom A (Ag_ind A f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D\<rbrakk> \<Longrightarrow> Agii A f \<in> aHom A (Ag_ind A f)
[PROOF STEP]
apply (simp add:aHom_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D\<rbrakk> \<Longrightarrow> Agii A f \<in> carrier A \<rightarrow> carrier (Ag_ind A f) \<and> Agii A f \<in> extensional (carrier A) \<and> (\<forall>a\<in>carrier A. \<forall>b\<in>carrier A. Agii A f (a \<plusminus> b) = Agii A f a \<plusminus>\<^bsub>Ag_ind A f\<^esub> Agii A f b)
[PROOF STEP]
apply (unfold bij_to_def, frule conjunct1, frule conjunct2, fold bij_to_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A)\<rbrakk> \<Longrightarrow> Agii A f \<in> carrier A \<rightarrow> carrier (Ag_ind A f) \<and> Agii A f \<in> extensional (carrier A) \<and> (\<forall>a\<in>carrier A. \<forall>b\<in>carrier A. Agii A f (a \<plusminus> b) = Agii A f a \<plusminus>\<^bsub>Ag_ind A f\<^esub> Agii A f b)
[PROOF STEP]
apply (simp add:Ag_ind_carrier surj_to_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A)\<rbrakk> \<Longrightarrow> Agii A f \<in> carrier A \<rightarrow> D \<and> Agii A f \<in> extensional (carrier A) \<and> (\<forall>a\<in>carrier A. \<forall>b\<in>carrier A. Agii A f (a \<plusminus> b) = Agii A f a \<plusminus>\<^bsub>Ag_ind A f\<^esub> Agii A f b)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A)\<rbrakk> \<Longrightarrow> Agii A f \<in> carrier A \<rightarrow> D
 2. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A)\<rbrakk> \<Longrightarrow> Agii A f \<in> extensional (carrier A) \<and> (\<forall>a\<in>carrier A. \<forall>b\<in>carrier A. Agii A f (a \<plusminus> b) = Agii A f a \<plusminus>\<^bsub>Ag_ind A f\<^esub> Agii A f b)
[PROOF STEP]
apply (simp add:Agii_def Pi_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A)\<rbrakk> \<Longrightarrow> Agii A f \<in> extensional (carrier A) \<and> (\<forall>a\<in>carrier A. \<forall>b\<in>carrier A. Agii A f (a \<plusminus> b) = Agii A f a \<plusminus>\<^bsub>Ag_ind A f\<^esub> Agii A f b)
[PROOF STEP]
apply (simp add:Agii_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A)\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier A. \<forall>b\<in>carrier A. (a \<plusminus> b \<in> carrier A \<longrightarrow> f (a \<plusminus> b) = f a \<plusminus>\<^bsub>Ag_ind A f\<^esub> f b) \<and> (a \<plusminus> b \<notin> carrier A \<longrightarrow> undefined = f a \<plusminus>\<^bsub>Ag_ind A f\<^esub> f b)
[PROOF STEP]
apply (simp add:Ag_ind_def Pi_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. x \<in> carrier A \<longrightarrow> f x \<in> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A)\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier A. \<forall>b\<in>carrier A. (a \<plusminus> b \<in> carrier A \<longrightarrow> f (a \<plusminus> b) = f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) (f a) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) (f b))) \<and> (a \<plusminus> b \<notin> carrier A \<longrightarrow> undefined = f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) (f a) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) (f b)))
[PROOF STEP]
apply (unfold bij_to_def, frule conjunct1, fold bij_to_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. x \<in> carrier A \<longrightarrow> f x \<in> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); surj_to f (carrier A) D\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier A. \<forall>b\<in>carrier A. (a \<plusminus> b \<in> carrier A \<longrightarrow> f (a \<plusminus> b) = f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) (f a) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) (f b))) \<and> (a \<plusminus> b \<notin> carrier A \<longrightarrow> undefined = f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) (f a) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) (f b)))
[PROOF STEP]
apply (simp add:invfun_l)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. x \<in> carrier A \<longrightarrow> f x \<in> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); surj_to f (carrier A) D\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier A. \<forall>b\<in>carrier A. a \<plusminus> b \<notin> carrier A \<longrightarrow> undefined = f (a \<plusminus> b)
[PROOF STEP]
apply (simp add:ag_pOp_closed)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) Agii_mem:"\<lbrakk>f \<in> carrier A \<rightarrow> D; x \<in> carrier A;
      bij_to f (carrier A) (D::'d set)\<rbrakk> \<Longrightarrow> Agii A f x \<in> carrier (Ag_ind A f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> carrier A \<rightarrow> D; x \<in> carrier A; bij_to f (carrier A) D\<rbrakk> \<Longrightarrow> Agii A f x \<in> carrier (Ag_ind A f)
[PROOF STEP]
apply (simp add:Agii_def Ag_ind_carrier)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done