[STATEMENT]
lemma (in aGroup) Ag_ind_aGroup:"\<lbrakk>f \<in> carrier A \<rightarrow> D;
      bij_to f (carrier A) (D::'d set)\<rbrakk> \<Longrightarrow> aGroup (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> aGroup (Ag_ind A f)
[PROOF STEP]
apply (simp add: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> aGroup (Ag_ind A f)
[PROOF STEP]
apply (simp add:aGroup_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> (\<plusminus>\<^bsub>Ag_ind A f\<^esub>) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>c. c \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b \<plusminus>\<^bsub>Ag_ind A f\<^esub> c = a \<plusminus>\<^bsub>Ag_ind A f\<^esub> (b \<plusminus>\<^bsub>Ag_ind A f\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b = b \<plusminus>\<^bsub>Ag_ind A f\<^esub> a)) \<and> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[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; surj_to f (carrier A) D; inj_on f (carrier A)\<rbrakk> \<Longrightarrow> (\<plusminus>\<^bsub>Ag_ind A f\<^esub>) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f)
 2. \<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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>c. c \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b \<plusminus>\<^bsub>Ag_ind A f\<^esub> c = a \<plusminus>\<^bsub>Ag_ind A f\<^esub> (b \<plusminus>\<^bsub>Ag_ind A f\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b = b \<plusminus>\<^bsub>Ag_ind A f\<^esub> a)) \<and> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (rule Pi_I)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); x \<in> carrier (Ag_ind A f); xa \<in> carrier (Ag_ind A f)\<rbrakk> \<Longrightarrow> x \<plusminus>\<^bsub>Ag_ind A f\<^esub> xa \<in> carrier (Ag_ind A f)
 2. \<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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>c. c \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b \<plusminus>\<^bsub>Ag_ind A f\<^esub> c = a \<plusminus>\<^bsub>Ag_ind A f\<^esub> (b \<plusminus>\<^bsub>Ag_ind A f\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b = b \<plusminus>\<^bsub>Ag_ind A f\<^esub> a)) \<and> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:Ag_ind_carrier surj_to_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); x \<in> D; xa \<in> D\<rbrakk> \<Longrightarrow> x \<plusminus>\<^bsub>Ag_ind A f\<^esub> xa \<in> D
 2. \<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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>c. c \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b \<plusminus>\<^bsub>Ag_ind A f\<^esub> c = a \<plusminus>\<^bsub>Ag_ind A f\<^esub> (b \<plusminus>\<^bsub>Ag_ind A f\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b = b \<plusminus>\<^bsub>Ag_ind A f\<^esub> a)) \<and> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (frule_tac b = x in invfun_mem1[of "f" "carrier A" "D"], assumption+,
        frule_tac b = xa in invfun_mem1[of "f" "carrier A" "D"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); x \<in> D; xa \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) x \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) xa \<in> carrier A\<rbrakk> \<Longrightarrow> x \<plusminus>\<^bsub>Ag_ind A f\<^esub> xa \<in> D
 2. \<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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>c. c \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b \<plusminus>\<^bsub>Ag_ind A f\<^esub> c = a \<plusminus>\<^bsub>Ag_ind A f\<^esub> (b \<plusminus>\<^bsub>Ag_ind A f\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b = b \<plusminus>\<^bsub>Ag_ind A f\<^esub> a)) \<and> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:Ag_ind_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); x \<in> D; xa \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) x \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) xa \<in> carrier A\<rbrakk> \<Longrightarrow> f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) x \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) xa) \<in> D
 2. \<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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>c. c \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b \<plusminus>\<^bsub>Ag_ind A f\<^esub> c = a \<plusminus>\<^bsub>Ag_ind A f\<^esub> (b \<plusminus>\<^bsub>Ag_ind A f\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b = b \<plusminus>\<^bsub>Ag_ind A f\<^esub> a)) \<and> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (rule funcset_mem[of "f" "carrier A" "D"], assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); x \<in> D; xa \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) x \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) xa \<in> carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>D,carrier A\<^esub>) x \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) xa \<in> carrier A
 2. \<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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>c. c \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b \<plusminus>\<^bsub>Ag_ind A f\<^esub> c = a \<plusminus>\<^bsub>Ag_ind A f\<^esub> (b \<plusminus>\<^bsub>Ag_ind A f\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b = b \<plusminus>\<^bsub>Ag_ind A f\<^esub> a)) \<and> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:ag_pOp_closed)
[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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>c. c \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b \<plusminus>\<^bsub>Ag_ind A f\<^esub> c = a \<plusminus>\<^bsub>Ag_ind A f\<^esub> (b \<plusminus>\<^bsub>Ag_ind A f\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b = b \<plusminus>\<^bsub>Ag_ind A f\<^esub> a)) \<and> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[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; surj_to f (carrier A) D; inj_on f (carrier A)\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>c. c \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b \<plusminus>\<^bsub>Ag_ind A f\<^esub> c = a \<plusminus>\<^bsub>Ag_ind A f\<^esub> (b \<plusminus>\<^bsub>Ag_ind A f\<^esub> c)))
 2. \<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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b = b \<plusminus>\<^bsub>Ag_ind A f\<^esub> a)) \<and> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (rule allI, rule impI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> carrier (Ag_ind A f); b \<in> carrier (Ag_ind A f); c \<in> carrier (Ag_ind A f)\<rbrakk> \<Longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b \<plusminus>\<^bsub>Ag_ind A f\<^esub> c = a \<plusminus>\<^bsub>Ag_ind A f\<^esub> (b \<plusminus>\<^bsub>Ag_ind A f\<^esub> c)
 2. \<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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b = b \<plusminus>\<^bsub>Ag_ind A f\<^esub> a)) \<and> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add: Ag_ind_carrier surj_to_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); a \<in> D; b \<in> D; c \<in> D\<rbrakk> \<Longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b \<plusminus>\<^bsub>Ag_ind A f\<^esub> c = a \<plusminus>\<^bsub>Ag_ind A f\<^esub> (b \<plusminus>\<^bsub>Ag_ind A f\<^esub> c)
 2. \<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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b = b \<plusminus>\<^bsub>Ag_ind A f\<^esub> a)) \<and> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (frule_tac b = a in invfun_mem1[of "f" "carrier A" "D"], assumption+,
        frule_tac b = b in invfun_mem1[of "f" "carrier A" "D"], assumption+,
        frule_tac b = c in invfun_mem1[of "f" "carrier A" "D"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); a \<in> D; b \<in> D; c \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) c \<in> carrier A\<rbrakk> \<Longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b \<plusminus>\<^bsub>Ag_ind A f\<^esub> c = a \<plusminus>\<^bsub>Ag_ind A f\<^esub> (b \<plusminus>\<^bsub>Ag_ind A f\<^esub> c)
 2. \<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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b = b \<plusminus>\<^bsub>Ag_ind A f\<^esub> a)) \<and> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:Ag_ind_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); a \<in> D; b \<in> D; c \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) c \<in> carrier A\<rbrakk> \<Longrightarrow> (f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b) \<in> D \<longrightarrow> (f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c) \<in> D \<longrightarrow> f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) (f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b)) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c) = f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) (f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c)))) \<and> (f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c) \<notin> D \<longrightarrow> f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) (f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b)) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c) = undefined)) \<and> (f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b) \<notin> D \<longrightarrow> (f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c) \<in> D \<longrightarrow> undefined c = f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) (f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c)))) \<and> (f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c) \<notin> D \<longrightarrow> undefined c = undefined))
 2. \<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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b = b \<plusminus>\<^bsub>Ag_ind A f\<^esub> a)) \<and> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (frule_tac x = "invfun (carrier A) D f a" and
                  y = "invfun (carrier A) D f b" in ag_pOp_closed, assumption+,
        frule_tac x = "invfun (carrier A) D f b" and
                  y = "invfun (carrier A) D f c" in ag_pOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); a \<in> D; b \<in> D; c \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) c \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c \<in> carrier A\<rbrakk> \<Longrightarrow> (f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b) \<in> D \<longrightarrow> (f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c) \<in> D \<longrightarrow> f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) (f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b)) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c) = f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) (f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c)))) \<and> (f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c) \<notin> D \<longrightarrow> f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) (f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b)) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c) = undefined)) \<and> (f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b) \<notin> D \<longrightarrow> (f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c) \<in> D \<longrightarrow> undefined c = f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) (f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c)))) \<and> (f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c) \<notin> D \<longrightarrow> undefined c = undefined))
 2. \<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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b = b \<plusminus>\<^bsub>Ag_ind A f\<^esub> a)) \<and> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:Pi_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<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); a \<in> D; b \<in> D; c \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) c \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c \<in> carrier A\<rbrakk> \<Longrightarrow> f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) (f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b)) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c) = f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) (f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c)))
 2. \<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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b = b \<plusminus>\<^bsub>Ag_ind A f\<^esub> a)) \<and> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (unfold bij_to_def, frule conjunct1, fold bij_to_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<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); a \<in> D; b \<in> D; c \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) c \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c \<in> carrier A; surj_to f (carrier A) D\<rbrakk> \<Longrightarrow> f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) (f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b)) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c) = f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) (f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c)))
 2. \<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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b = b \<plusminus>\<^bsub>Ag_ind A f\<^esub> a)) \<and> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:invfun_l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<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); a \<in> D; b \<in> D; c \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) c \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c \<in> carrier A; surj_to f (carrier A) D\<rbrakk> \<Longrightarrow> f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c) = f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> ((f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c))
 2. \<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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b = b \<plusminus>\<^bsub>Ag_ind A f\<^esub> a)) \<and> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (subst injective_iff[of "f" "carrier A", THEN sym], assumption)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b c. \<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); a \<in> D; b \<in> D; c \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) c \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c \<in> carrier A; surj_to f (carrier A) D\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c \<in> carrier A
 2. \<And>a b c. \<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); a \<in> D; b \<in> D; c \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) c \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c \<in> carrier A; surj_to f (carrier A) D\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> ((f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c) \<in> carrier A
 3. \<And>a b c. \<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); a \<in> D; b \<in> D; c \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) c \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c \<in> carrier A; surj_to f (carrier A) D\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c = (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> ((f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c)
 4. \<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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b = b \<plusminus>\<^bsub>Ag_ind A f\<^esub> a)) \<and> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:ag_pOp_closed)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<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); a \<in> D; b \<in> D; c \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) c \<in> carrier A; surj_to f (carrier A) D\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c = (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> ((f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) c)
 2. \<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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b = b \<plusminus>\<^bsub>Ag_ind A f\<^esub> a)) \<and> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:ag_pOp_assoc)
[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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b = b \<plusminus>\<^bsub>Ag_ind A f\<^esub> a)) \<and> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[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; surj_to f (carrier A) D; inj_on f (carrier A)\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> (\<forall>b. b \<in> carrier (Ag_ind A f) \<longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b = b \<plusminus>\<^bsub>Ag_ind A f\<^esub> a)
 2. \<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> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (rule allI, rule impI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> carrier (Ag_ind A f); b \<in> carrier (Ag_ind A f)\<rbrakk> \<Longrightarrow> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> b = b \<plusminus>\<^bsub>Ag_ind A f\<^esub> a
 2. \<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> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:Ag_ind_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A\<rbrakk> \<Longrightarrow> f ((f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b) = f ((f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a)
 2. \<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> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (subst injective_iff[of "f" "carrier A", THEN sym], assumption)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b \<in> carrier A
 2. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a \<in> carrier A
 3. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b = (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a
 4. \<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> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (frule_tac b = a in invfun_mem1[of "f" "carrier A" "D"], assumption+,
        frule_tac b = b in invfun_mem1[of "f" "carrier A" "D"], assumption+)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A\<rbrakk> \<Longrightarrow> b \<in> D
 2. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<in> carrier A\<rbrakk> \<Longrightarrow> a \<in> D
 3. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b \<in> carrier A
 4. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a \<in> carrier A
 5. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b = (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a
 6. \<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> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:surj_to_def)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<in> carrier A\<rbrakk> \<Longrightarrow> a \<in> D
 2. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b \<in> carrier A
 3. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a \<in> carrier A
 4. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b = (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a
 5. \<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> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:surj_to_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b \<in> carrier A
 2. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a \<in> carrier A
 3. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b = (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a
 4. \<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> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:surj_to_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); a \<in> D; b \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<in> carrier A
 2. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a \<in> carrier A
 3. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b = (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a
 4. \<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> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (frule_tac b = b in invfun_mem1[of "f" "carrier A" "D"], assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); a \<in> D; b \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<in> carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<in> carrier A
 2. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a \<in> carrier A
 3. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b = (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a
 4. \<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> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:ag_pOp_closed)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a \<in> carrier A
 2. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b = (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a
 3. \<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> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:surj_to_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); a \<in> D; b \<in> D\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A
 2. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b = (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a
 3. \<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> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (frule_tac b = a in invfun_mem1[of "f" "carrier A" "D"], assumption+,
        frule_tac b = b in invfun_mem1[of "f" "carrier A" "D"], assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); a \<in> D; b \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<in> carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A
 2. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b = (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a
 3. \<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> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:ag_pOp_closed)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> f ` carrier A; b \<in> f ` carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b = (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>f ` carrier A,carrier A\<^esub>) a
 2. \<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> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:surj_to_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); a \<in> D; b \<in> D\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b = (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a
 2. \<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> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (frule_tac b = a in invfun_mem1[of "f" "carrier A" "D"], assumption+,
        frule_tac b = b in invfun_mem1[of "f" "carrier A" "D"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); a \<in> D; b \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<in> carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) b = (f\<inverse>\<^bsub>D,carrier A\<^esub>) b \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a
 2. \<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> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:ag_pOp_commute)
[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> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[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; surj_to f (carrier A) D; inj_on f (carrier A)\<rbrakk> \<Longrightarrow> mop (Ag_ind A f) \<in> carrier (Ag_ind A f) \<rightarrow> carrier (Ag_ind A f)
 2. \<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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (rule Pi_I)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); x \<in> carrier (Ag_ind A f)\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> x \<in> carrier (Ag_ind A f)
 2. \<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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:Ag_ind_def surj_to_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); x \<in> D\<rbrakk> \<Longrightarrow> f (-\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) x) \<in> D
 2. \<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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (rule funcset_mem[of "f" "carrier A" "D"], assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); x \<in> D\<rbrakk> \<Longrightarrow> -\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) x \<in> carrier A
 2. \<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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (frule_tac b = x in invfun_mem1[of "f" "carrier A" "D"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); x \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) x \<in> carrier A\<rbrakk> \<Longrightarrow> -\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) x \<in> carrier A
 2. \<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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:ag_mOp_closed)
[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> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>) \<and> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[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; surj_to f (carrier A) D; inj_on f (carrier A)\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>
 2. \<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> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> carrier (Ag_ind A f)\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>Ag_ind A f\<^esub> a \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = \<zero>\<^bsub>Ag_ind A f\<^esub>
 2. \<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> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:Ag_ind_def surj_to_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); a \<in> D\<rbrakk> \<Longrightarrow> (f (-\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a) \<in> D \<longrightarrow> f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) (f (-\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a)) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a) = f \<zero>) \<and> (f (-\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a) \<notin> D \<longrightarrow> undefined a = f \<zero>)
 2. \<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> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (frule_tac b = a in invfun_mem1[of "f" "carrier A" "D"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); a \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A\<rbrakk> \<Longrightarrow> (f (-\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a) \<in> D \<longrightarrow> f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) (f (-\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a)) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a) = f \<zero>) \<and> (f (-\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a) \<notin> D \<longrightarrow> undefined a = f \<zero>)
 2. \<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> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (frule_tac x = "invfun (carrier A) D f a" in ag_mOp_closed)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); a \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; -\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A\<rbrakk> \<Longrightarrow> (f (-\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a) \<in> D \<longrightarrow> f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) (f (-\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a)) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a) = f \<zero>) \<and> (f (-\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a) \<notin> D \<longrightarrow> undefined a = f \<zero>)
 2. \<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> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:Pi_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<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); a \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; -\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A\<rbrakk> \<Longrightarrow> f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) (f (-\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a)) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a) = f \<zero>
 2. \<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> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (subst injective_iff[of "f" "carrier A", THEN sym], assumption)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a. \<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); a \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; -\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>D,carrier A\<^esub>) (f (-\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a)) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A
 2. \<And>a. \<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); a \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; -\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A\<rbrakk> \<Longrightarrow> \<zero> \<in> carrier A
 3. \<And>a. \<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); a \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; -\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>D,carrier A\<^esub>) (f (-\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a)) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a = \<zero>
 4. \<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> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (unfold bij_to_def, frule conjunct1, fold bij_to_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a. \<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); a \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; -\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; surj_to f (carrier A) D\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>D,carrier A\<^esub>) (f (-\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a)) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A
 2. \<And>a. \<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); a \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; -\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A\<rbrakk> \<Longrightarrow> \<zero> \<in> carrier A
 3. \<And>a. \<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); a \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; -\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>D,carrier A\<^esub>) (f (-\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a)) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a = \<zero>
 4. \<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> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:invfun_l)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a. \<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); a \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; -\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; surj_to f (carrier A) D\<rbrakk> \<Longrightarrow> -\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A
 2. \<And>a. \<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); a \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; -\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A\<rbrakk> \<Longrightarrow> \<zero> \<in> carrier A
 3. \<And>a. \<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); a \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; -\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>D,carrier A\<^esub>) (f (-\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a)) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a = \<zero>
 4. \<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> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:ag_pOp_closed)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a. \<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); a \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; -\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A\<rbrakk> \<Longrightarrow> \<zero> \<in> carrier A
 2. \<And>a. \<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); a \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; -\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>D,carrier A\<^esub>) (f (-\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a)) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a = \<zero>
 3. \<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> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:ag_inc_zero)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<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); a \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; -\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>D,carrier A\<^esub>) (f (-\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a)) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a = \<zero>
 2. \<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> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (unfold bij_to_def, frule conjunct1, fold bij_to_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<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); a \<in> D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; -\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A; surj_to f (carrier A) D\<rbrakk> \<Longrightarrow> (f\<inverse>\<^bsub>D,carrier A\<^esub>) (f (-\<^sub>a (f\<inverse>\<^bsub>D,carrier A\<^esub>) a)) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a = \<zero>
 2. \<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> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[PROOF STEP]
apply (simp add:invfun_l l_m)
[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> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f) \<and> (\<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a)
[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; surj_to f (carrier A) D; inj_on f (carrier A)\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<in> carrier (Ag_ind A f)
 2. \<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> \<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a
[PROOF STEP]
apply (simp add:Ag_ind_def surj_to_def)
[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> f \<zero> \<in> D
 2. \<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> \<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a
[PROOF STEP]
apply (rule funcset_mem[of "f" "carrier A" "D"], assumption)
[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> \<zero> \<in> carrier A
 2. \<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> \<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a
[PROOF STEP]
apply (simp add:ag_inc_zero)
[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> \<forall>a. a \<in> carrier (Ag_ind A f) \<longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; surj_to f (carrier A) D; inj_on f (carrier A); a \<in> carrier (Ag_ind A f)\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>Ag_ind A f\<^esub> \<plusminus>\<^bsub>Ag_ind A f\<^esub> a = a
[PROOF STEP]
apply (simp add:Ag_ind_def surj_to_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); a \<in> D\<rbrakk> \<Longrightarrow> (f \<zero> \<in> D \<longrightarrow> f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) (f \<zero>) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a) = a) \<and> (f \<zero> \<notin> D \<longrightarrow> undefined a = a)
[PROOF STEP]
apply (cut_tac ag_inc_zero, simp add:funcset_mem del:Pi_I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); a \<in> D; \<zero> \<in> carrier A\<rbrakk> \<Longrightarrow> f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) (f \<zero>) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a) = a
[PROOF STEP]
apply (unfold bij_to_def, frule conjunct1, fold bij_to_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); a \<in> D; \<zero> \<in> carrier A; surj_to f (carrier A) D\<rbrakk> \<Longrightarrow> f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) (f \<zero>) \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a) = a
[PROOF STEP]
apply (simp add:invfun_l)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); a \<in> D; \<zero> \<in> carrier A; surj_to f (carrier A) D\<rbrakk> \<Longrightarrow> f (\<zero> \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a) = a
[PROOF STEP]
apply (frule_tac b = a in invfun_mem1[of "f" "carrier A" "D"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); a \<in> D; \<zero> \<in> carrier A; surj_to f (carrier A) D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A\<rbrakk> \<Longrightarrow> f (\<zero> \<plusminus> (f\<inverse>\<^bsub>D,carrier A\<^esub>) a) = a
[PROOF STEP]
apply (simp add:l_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>f \<in> carrier A \<rightarrow> D; bij_to f (carrier A) D; f ` carrier A = D; inj_on f (carrier A); a \<in> D; \<zero> \<in> carrier A; surj_to f (carrier A) D; (f\<inverse>\<^bsub>D,carrier A\<^esub>) a \<in> carrier A\<rbrakk> \<Longrightarrow> f ((f\<inverse>\<^bsub>D,carrier A\<^esub>) a) = a
[PROOF STEP]
apply (simp add:invfun_r)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma aHom_mem:"\<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; a \<in> carrier F\<rbrakk> \<Longrightarrow>
                       f a \<in> carrier G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; a \<in> carrier F\<rbrakk> \<Longrightarrow> f a \<in> carrier G
[PROOF STEP]
apply (simp add:aHom_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> carrier F \<rightarrow> carrier G \<and> f \<in> extensional (carrier F) \<and> (\<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); a \<in> carrier F\<rbrakk> \<Longrightarrow> f a \<in> carrier G
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; a \<in> 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\<rbrakk> \<Longrightarrow> f a \<in> carrier G
[PROOF STEP]
apply (simp add:Pi_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma aHom_func:"f \<in> aHom F G \<Longrightarrow> f \<in> carrier F \<rightarrow> carrier G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> aHom F G \<Longrightarrow> f \<in> carrier F \<rightarrow> carrier G
[PROOF STEP]
by (simp add:aHom_def)


[STATEMENT]
lemma aHom_add:"\<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; a \<in> carrier F;
 b \<in> carrier F\<rbrakk> \<Longrightarrow> f (a \<plusminus>\<^bsub>F\<^esub> b) = (f a) \<plusminus>\<^bsub>G\<^esub> (f b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; a \<in> carrier F; b \<in> carrier F\<rbrakk> \<Longrightarrow> f (a \<plusminus>\<^bsub>F\<^esub> b) = f a \<plusminus>\<^bsub>G\<^esub> f b
[PROOF STEP]
apply (simp add:aHom_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma aHom_0_0:"\<lbrakk>aGroup F; aGroup G; f \<in> aHom F G\<rbrakk> \<Longrightarrow> f (\<zero>\<^bsub>F\<^esub>) = \<zero>\<^bsub>G\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G\<rbrakk> \<Longrightarrow> f \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>G\<^esub>
[PROOF STEP]
apply (frule aGroup.ag_inc_zero [of "F"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; \<zero>\<^bsub>F\<^esub> \<in> carrier F\<rbrakk> \<Longrightarrow> f \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>G\<^esub>
[PROOF STEP]
apply (subst aGroup.ag_l_zero [THEN sym, of "F" "\<zero>\<^bsub>F\<^esub>"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; \<zero>\<^bsub>F\<^esub> \<in> carrier F\<rbrakk> \<Longrightarrow> f (\<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>F\<^esub> \<zero>\<^bsub>F\<^esub>) = \<zero>\<^bsub>G\<^esub>
[PROOF STEP]
apply (simp add:aHom_add)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; \<zero>\<^bsub>F\<^esub> \<in> carrier F\<rbrakk> \<Longrightarrow> f \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>G\<^esub> f \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>G\<^esub>
[PROOF STEP]
apply (frule aGroup.ag_l_zero [THEN sym, of "F" "\<zero>\<^bsub>F\<^esub>"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; \<zero>\<^bsub>F\<^esub> \<in> carrier F; \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>F\<^esub> \<zero>\<^bsub>F\<^esub>\<rbrakk> \<Longrightarrow> f \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>G\<^esub> f \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>G\<^esub>
[PROOF STEP]
apply (subgoal_tac "f (\<zero>\<^bsub>F\<^esub>) = f (\<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>F\<^esub> \<zero>\<^bsub>F\<^esub>)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; \<zero>\<^bsub>F\<^esub> \<in> carrier F; \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>F\<^esub> \<zero>\<^bsub>F\<^esub>; f \<zero>\<^bsub>F\<^esub> = f (\<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>F\<^esub> \<zero>\<^bsub>F\<^esub>)\<rbrakk> \<Longrightarrow> f \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>G\<^esub> f \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>G\<^esub>
 2. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; \<zero>\<^bsub>F\<^esub> \<in> carrier F; \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>F\<^esub> \<zero>\<^bsub>F\<^esub>\<rbrakk> \<Longrightarrow> f \<zero>\<^bsub>F\<^esub> = f (\<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>F\<^esub> \<zero>\<^bsub>F\<^esub>)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; \<zero>\<^bsub>F\<^esub> \<in> carrier F; \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>F\<^esub> \<zero>\<^bsub>F\<^esub>\<rbrakk> \<Longrightarrow> f \<zero>\<^bsub>F\<^esub> = f (\<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>F\<^esub> \<zero>\<^bsub>F\<^esub>)
 2. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; \<zero>\<^bsub>F\<^esub> \<in> carrier F; \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>F\<^esub> \<zero>\<^bsub>F\<^esub>; f \<zero>\<^bsub>F\<^esub> = f (\<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>F\<^esub> \<zero>\<^bsub>F\<^esub>)\<rbrakk> \<Longrightarrow> f \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>G\<^esub> f \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>G\<^esub>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; \<zero>\<^bsub>F\<^esub> \<in> carrier F; \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>F\<^esub> \<zero>\<^bsub>F\<^esub>; f \<zero>\<^bsub>F\<^esub> = f (\<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>F\<^esub> \<zero>\<^bsub>F\<^esub>)\<rbrakk> \<Longrightarrow> f \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>G\<^esub> f \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>G\<^esub>
[PROOF STEP]
apply (thin_tac "\<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>F\<^esub> \<zero>\<^bsub>F\<^esub>")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; \<zero>\<^bsub>F\<^esub> \<in> carrier F; f \<zero>\<^bsub>F\<^esub> = f (\<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>F\<^esub> \<zero>\<^bsub>F\<^esub>)\<rbrakk> \<Longrightarrow> f \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>G\<^esub> f \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>G\<^esub>
[PROOF STEP]
apply (simp add:aHom_add)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; \<zero>\<^bsub>F\<^esub> \<in> carrier F; f \<zero>\<^bsub>F\<^esub> = f \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>G\<^esub> f \<zero>\<^bsub>F\<^esub>\<rbrakk> \<Longrightarrow> f \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>G\<^esub>
[PROOF STEP]
apply (frule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; \<zero>\<^bsub>F\<^esub> \<in> carrier F; f \<zero>\<^bsub>F\<^esub> = f \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>G\<^esub> f \<zero>\<^bsub>F\<^esub>; f \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>G\<^esub> f \<zero>\<^bsub>F\<^esub> = f \<zero>\<^bsub>F\<^esub>\<rbrakk> \<Longrightarrow> f \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>G\<^esub>
[PROOF STEP]
apply (thin_tac "f \<zero>\<^bsub>F\<^esub> = f \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>G\<^esub> f \<zero>\<^bsub>F\<^esub>")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; \<zero>\<^bsub>F\<^esub> \<in> carrier F; f \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>G\<^esub> f \<zero>\<^bsub>F\<^esub> = f \<zero>\<^bsub>F\<^esub>\<rbrakk> \<Longrightarrow> f \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>G\<^esub>
[PROOF STEP]
apply (frule aHom_mem[of "F" "G" "f" "\<zero>\<^bsub>F\<^esub>"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; \<zero>\<^bsub>F\<^esub> \<in> carrier F; f \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>G\<^esub> f \<zero>\<^bsub>F\<^esub> = f \<zero>\<^bsub>F\<^esub>; f \<zero>\<^bsub>F\<^esub> \<in> carrier G\<rbrakk> \<Longrightarrow> f \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>G\<^esub>
[PROOF STEP]
apply (frule aGroup.ag_mOp_closed[of "G" "f \<zero>\<^bsub>F\<^esub>"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; \<zero>\<^bsub>F\<^esub> \<in> carrier F; f \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>G\<^esub> f \<zero>\<^bsub>F\<^esub> = f \<zero>\<^bsub>F\<^esub>; f \<zero>\<^bsub>F\<^esub> \<in> carrier G; -\<^sub>a\<^bsub>G\<^esub> f \<zero>\<^bsub>F\<^esub> \<in> carrier G\<rbrakk> \<Longrightarrow> f \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>G\<^esub>
[PROOF STEP]
apply (frule aGroup.aassoc[of "G" "-\<^sub>a\<^bsub>G\<^esub> (f \<zero>\<^bsub>F\<^esub>)" "f \<zero>\<^bsub>F\<^esub>" "f \<zero>\<^bsub>F\<^esub>"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; \<zero>\<^bsub>F\<^esub> \<in> carrier F; f \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>G\<^esub> f \<zero>\<^bsub>F\<^esub> = f \<zero>\<^bsub>F\<^esub>; f \<zero>\<^bsub>F\<^esub> \<in> carrier G; -\<^sub>a\<^bsub>G\<^esub> f \<zero>\<^bsub>F\<^esub> \<in> carrier G; -\<^sub>a\<^bsub>G\<^esub> f \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>G\<^esub> f \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>G\<^esub> f \<zero>\<^bsub>F\<^esub> = -\<^sub>a\<^bsub>G\<^esub> f \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>G\<^esub> (f \<zero>\<^bsub>F\<^esub> \<plusminus>\<^bsub>G\<^esub> f \<zero>\<^bsub>F\<^esub>)\<rbrakk> \<Longrightarrow> f \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>G\<^esub>
[PROOF STEP]
apply (simp add:aGroup.l_m aGroup.l_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ker_inc_zero:"\<lbrakk>aGroup F; aGroup G; f \<in> aHom F G\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>F\<^esub> \<in> 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> \<zero>\<^bsub>F\<^esub> \<in> ker\<^bsub>F,G\<^esub> f
[PROOF STEP]
by (frule aHom_0_0[of "F" "G" "f"], assumption+,
       simp add:ker_def, simp add:aGroup.ag_inc_zero [of "F"])


[STATEMENT]
lemma aHom_inv_inv:"\<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; a \<in> carrier F\<rbrakk> \<Longrightarrow>
                         f (-\<^sub>a\<^bsub>F\<^esub> a) = -\<^sub>a\<^bsub>G\<^esub> (f a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; a \<in> carrier F\<rbrakk> \<Longrightarrow> f (-\<^sub>a\<^bsub>F\<^esub> a) = -\<^sub>a\<^bsub>G\<^esub> f a
[PROOF STEP]
apply (frule aGroup.ag_l_inv1 [of "F" "a"], assumption+,
       frule sym, thin_tac "-\<^sub>a\<^bsub>F\<^esub> a \<plusminus>\<^bsub>F\<^esub> a = \<zero>\<^bsub>F\<^esub>",
       frule aHom_0_0[of "F" "G" "f"], assumption+,
       frule aGroup.ag_mOp_closed[of "F" "a"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; a \<in> carrier F; \<zero>\<^bsub>F\<^esub> = -\<^sub>a\<^bsub>F\<^esub> a \<plusminus>\<^bsub>F\<^esub> a; f \<zero>\<^bsub>F\<^esub> = \<zero>\<^bsub>G\<^esub>; -\<^sub>a\<^bsub>F\<^esub> a \<in> carrier F\<rbrakk> \<Longrightarrow> f (-\<^sub>a\<^bsub>F\<^esub> a) = -\<^sub>a\<^bsub>G\<^esub> f a
[PROOF STEP]
apply (simp add:aHom_add, thin_tac "\<zero>\<^bsub>F\<^esub> = -\<^sub>a\<^bsub>F\<^esub> a \<plusminus>\<^bsub>F\<^esub> a")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; a \<in> carrier F; f (-\<^sub>a\<^bsub>F\<^esub> a) \<plusminus>\<^bsub>G\<^esub> f a = \<zero>\<^bsub>G\<^esub>; -\<^sub>a\<^bsub>F\<^esub> a \<in> carrier F\<rbrakk> \<Longrightarrow> f (-\<^sub>a\<^bsub>F\<^esub> a) = -\<^sub>a\<^bsub>G\<^esub> f a
[PROOF STEP]
apply (frule aHom_mem[of "F" "G" "f" "-\<^sub>a\<^bsub>F\<^esub> a"], assumption+,
        frule aHom_mem[of "F" "G" "f" "a"], assumption+,
        simp only:aGroup.ag_pOp_commute[of "G" "f (-\<^sub>a\<^bsub>F\<^esub> a)" "f a"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup F; aGroup G; f \<in> aHom F G; a \<in> carrier F; f a \<plusminus>\<^bsub>G\<^esub> f (-\<^sub>a\<^bsub>F\<^esub> a) = \<zero>\<^bsub>G\<^esub>; -\<^sub>a\<^bsub>F\<^esub> a \<in> carrier F; f (-\<^sub>a\<^bsub>F\<^esub> a) \<in> carrier G; f a \<in> carrier G\<rbrakk> \<Longrightarrow> f (-\<^sub>a\<^bsub>F\<^esub> a) = -\<^sub>a\<^bsub>G\<^esub> f a
[PROOF STEP]
apply (rule aGroup.ag_inv_unique[of "G"], assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done