[STATEMENT]
lemma dsumag_aGroup:"\<forall>k\<in>I. aGroup (A k) \<Longrightarrow> aGroup (dsumag I A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> aGroup (a\<Oplus>\<^bsub>I\<^esub> A)
[PROOF STEP]
apply (simp add:aGroup_def [of "dsumag I A"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> (\<plusminus>\<^bsub>a\<Oplus>\<^bsub>I\<^esub> A\<^esub>) \<in> carrier (a\<Oplus>\<^bsub>I\<^esub> A) \<rightarrow> carrier (a\<Oplus>\<^bsub>I\<^esub> A) \<rightarrow> carrier (a\<Oplus>\<^bsub>I\<^esub> A) \<and> (\<forall>a. a \<in> carrier (a\<Oplus>\<^bsub>I\<^esub> A) \<longrightarrow> (\<forall>b. b \<in> carrier (a\<Oplus>\<^bsub>I\<^esub> A) \<longrightarrow> (\<forall>c. c \<in> carrier (a\<Oplus>\<^bsub>I\<^esub> A) \<longrightarrow> a \<plusminus>\<^bsub>a\<Oplus>\<^bsub>I\<^esub> A\<^esub> b \<plusminus>\<^bsub>a\<Oplus>\<^bsub>I\<^esub> A\<^esub> c = a \<plusminus>\<^bsub>a\<Oplus>\<^bsub>I\<^esub> A\<^esub> (b \<plusminus>\<^bsub>a\<Oplus>\<^bsub>I\<^esub> A\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (a\<Oplus>\<^bsub>I\<^esub> A) \<longrightarrow> (\<forall>b. b \<in> carrier (a\<Oplus>\<^bsub>I\<^esub> A) \<longrightarrow> a \<plusminus>\<^bsub>a\<Oplus>\<^bsub>I\<^esub> A\<^esub> b = b \<plusminus>\<^bsub>a\<Oplus>\<^bsub>I\<^esub> A\<^esub> a)) \<and> mop (a\<Oplus>\<^bsub>I\<^esub> A) \<in> carrier (a\<Oplus>\<^bsub>I\<^esub> A) \<rightarrow> carrier (a\<Oplus>\<^bsub>I\<^esub> A) \<and> (\<forall>a. a \<in> carrier (a\<Oplus>\<^bsub>I\<^esub> A) \<longrightarrow> -\<^sub>a\<^bsub>a\<Oplus>\<^bsub>I\<^esub> A\<^esub> a \<plusminus>\<^bsub>a\<Oplus>\<^bsub>I\<^esub> A\<^esub> a = \<zero>\<^bsub>a\<Oplus>\<^bsub>I\<^esub> A\<^esub>) \<and> \<zero>\<^bsub>a\<Oplus>\<^bsub>I\<^esub> A\<^esub> \<in> carrier (a\<Oplus>\<^bsub>I\<^esub> A) \<and> (\<forall>a. a \<in> carrier (a\<Oplus>\<^bsub>I\<^esub> A) \<longrightarrow> \<zero>\<^bsub>a\<Oplus>\<^bsub>I\<^esub> A\<^esub> \<plusminus>\<^bsub>a\<Oplus>\<^bsub>I\<^esub> A\<^esub> a = a)
[PROOF STEP]
apply (simp add:dsumag_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> prod_pOp I A \<in> carr_dsumag I A \<rightarrow> carr_dsumag I A \<rightarrow> carr_dsumag I A \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> (\<forall>c. c \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_pOp I A a b) c = prod_pOp I A a (prod_pOp I A b c)))) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> prod_mOp I A \<in> carr_dsumag I A \<rightarrow> carr_dsumag I A \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> prod_zero I A \<in> carr_dsumag I A \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (simp add:dsum_pOp_func)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> (\<forall>c. c \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_pOp I A a b) c = prod_pOp I A a (prod_pOp I A b c)))) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> prod_mOp I A \<in> carr_dsumag I A \<rightarrow> carr_dsumag I A \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> prod_zero I A \<in> carr_dsumag I A \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (simp add:dsum_iOp_func)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> (\<forall>c. c \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_pOp I A a b) c = prod_pOp I A a (prod_pOp I A b c)))) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> prod_zero I A \<in> carr_dsumag I A \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (simp add:dsum_zero_func)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> (\<forall>c. c \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_pOp I A a b) c = prod_pOp I A a (prod_pOp I A b c)))) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (frule dsumag_sub_prodag[of "I" "A"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> (\<forall>c. c \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_pOp I A a b) c = prod_pOp I A a (prod_pOp I A b c)))) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> (\<forall>c. c \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_pOp I A a b) c = prod_pOp I A a (prod_pOp I A b c)))
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (rule allI, rule impI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> prod_pOp I A (prod_pOp I A a b) c = prod_pOp I A a (prod_pOp I A b c)
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (frule_tac X = a and Y = b in dsum_pOp_mem, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A; prod_pOp I A a b \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> prod_pOp I A (prod_pOp I A a b) c = prod_pOp I A a (prod_pOp I A b c)
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (frule_tac X = b and Y = c in dsum_pOp_mem, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A; prod_pOp I A a b \<in> carr_dsumag I A; prod_pOp I A b c \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> prod_pOp I A (prod_pOp I A a b) c = prod_pOp I A a (prod_pOp I A b c)
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (frule_tac X = "prod_pOp I A a b" and Y = c in dsum_pOp_mem,
                    assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A; prod_pOp I A a b \<in> carr_dsumag I A; prod_pOp I A b c \<in> carr_dsumag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> prod_pOp I A (prod_pOp I A a b) c = prod_pOp I A a (prod_pOp I A b c)
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (frule_tac Y = "prod_pOp I A b c" and X = a in dsum_pOp_mem,
                    assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A; prod_pOp I A a b \<in> carr_dsumag I A; prod_pOp I A b c \<in> carr_dsumag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_dsumag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> prod_pOp I A (prod_pOp I A a b) c = prod_pOp I A a (prod_pOp I A b c)
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (rule carr_prodag_mem_eq [of "I" "A"], assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b c. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A; prod_pOp I A a b \<in> carr_dsumag I A; prod_pOp I A b c \<in> carr_dsumag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_dsumag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> prod_pOp I A (prod_pOp I A a b) c \<in> carr_prodag I A
 2. \<And>a b c. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A; prod_pOp I A a b \<in> carr_dsumag I A; prod_pOp I A b c \<in> carr_dsumag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_dsumag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> prod_pOp I A a (prod_pOp I A b c) \<in> carr_prodag I A
 3. \<And>a b c. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A; prod_pOp I A a b \<in> carr_dsumag I A; prod_pOp I A b c \<in> carr_dsumag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_dsumag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> \<forall>l\<in>I. prod_pOp I A (prod_pOp I A a b) c l = prod_pOp I A a (prod_pOp I A b c) l
 4. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (simp add:subsetD)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b c. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A; prod_pOp I A a b \<in> carr_dsumag I A; prod_pOp I A b c \<in> carr_dsumag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_dsumag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> prod_pOp I A a (prod_pOp I A b c) \<in> carr_prodag I A
 2. \<And>a b c. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A; prod_pOp I A a b \<in> carr_dsumag I A; prod_pOp I A b c \<in> carr_dsumag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_dsumag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> \<forall>l\<in>I. prod_pOp I A (prod_pOp I A a b) c l = prod_pOp I A a (prod_pOp I A b c) l
 3. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (simp add:subsetD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A; prod_pOp I A a b \<in> carr_dsumag I A; prod_pOp I A b c \<in> carr_dsumag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_dsumag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> \<forall>l\<in>I. prod_pOp I A (prod_pOp I A a b) c l = prod_pOp I A a (prod_pOp I A b c) l
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A; prod_pOp I A a b \<in> carr_dsumag I A; prod_pOp I A b c \<in> carr_dsumag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_dsumag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_dsumag I A; l \<in> I\<rbrakk> \<Longrightarrow> prod_pOp I A (prod_pOp I A a b) c l = prod_pOp I A a (prod_pOp I A b c) l
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (subst prod_pOp_mem_i, assumption+, (simp add:subsetD)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A; prod_pOp I A a b \<in> carr_dsumag I A; prod_pOp I A b c \<in> carr_dsumag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_dsumag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_dsumag I A; l \<in> I\<rbrakk> \<Longrightarrow> prod_pOp I A a b l \<plusminus>\<^bsub>A l\<^esub> c l = prod_pOp I A a (prod_pOp I A b c) l
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (subst prod_pOp_mem_i, assumption+)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b c l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A; prod_pOp I A a b \<in> carr_dsumag I A; prod_pOp I A b c \<in> carr_dsumag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_dsumag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_dsumag I A; l \<in> I\<rbrakk> \<Longrightarrow> a \<in> carr_prodag I A
 2. \<And>a b c l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A; prod_pOp I A a b \<in> carr_dsumag I A; prod_pOp I A b c \<in> carr_dsumag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_dsumag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_dsumag I A; l \<in> I\<rbrakk> \<Longrightarrow> b \<in> carr_prodag I A
 3. \<And>a b c l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A; prod_pOp I A a b \<in> carr_dsumag I A; prod_pOp I A b c \<in> carr_dsumag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_dsumag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_dsumag I A; l \<in> I\<rbrakk> \<Longrightarrow> l \<in> I
 4. \<And>a b c l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A; prod_pOp I A a b \<in> carr_dsumag I A; prod_pOp I A b c \<in> carr_dsumag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_dsumag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_dsumag I A; l \<in> I\<rbrakk> \<Longrightarrow> a l \<plusminus>\<^bsub>A l\<^esub> b l \<plusminus>\<^bsub>A l\<^esub> c l = prod_pOp I A a (prod_pOp I A b c) l
 5. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (simp add:subsetD)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A; prod_pOp I A a b \<in> carr_dsumag I A; prod_pOp I A b c \<in> carr_dsumag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_dsumag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_dsumag I A; l \<in> I\<rbrakk> \<Longrightarrow> a l \<plusminus>\<^bsub>A l\<^esub> b l \<plusminus>\<^bsub>A l\<^esub> c l = prod_pOp I A a (prod_pOp I A b c) l
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (subst prod_pOp_mem_i, assumption+, (simp add:subsetD)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A; prod_pOp I A a b \<in> carr_dsumag I A; prod_pOp I A b c \<in> carr_dsumag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_dsumag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_dsumag I A; l \<in> I\<rbrakk> \<Longrightarrow> a l \<plusminus>\<^bsub>A l\<^esub> b l \<plusminus>\<^bsub>A l\<^esub> c l = a l \<plusminus>\<^bsub>A l\<^esub> prod_pOp I A b c l
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (subst prod_pOp_mem_i, assumption+)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b c l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A; prod_pOp I A a b \<in> carr_dsumag I A; prod_pOp I A b c \<in> carr_dsumag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_dsumag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_dsumag I A; l \<in> I\<rbrakk> \<Longrightarrow> b \<in> carr_prodag I A
 2. \<And>a b c l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A; prod_pOp I A a b \<in> carr_dsumag I A; prod_pOp I A b c \<in> carr_dsumag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_dsumag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_dsumag I A; l \<in> I\<rbrakk> \<Longrightarrow> c \<in> carr_prodag I A
 3. \<And>a b c l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A; prod_pOp I A a b \<in> carr_dsumag I A; prod_pOp I A b c \<in> carr_dsumag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_dsumag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_dsumag I A; l \<in> I\<rbrakk> \<Longrightarrow> l \<in> I
 4. \<And>a b c l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A; prod_pOp I A a b \<in> carr_dsumag I A; prod_pOp I A b c \<in> carr_dsumag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_dsumag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_dsumag I A; l \<in> I\<rbrakk> \<Longrightarrow> a l \<plusminus>\<^bsub>A l\<^esub> b l \<plusminus>\<^bsub>A l\<^esub> c l = a l \<plusminus>\<^bsub>A l\<^esub> (b l \<plusminus>\<^bsub>A l\<^esub> c l)
 5. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (simp add:subsetD)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A; prod_pOp I A a b \<in> carr_dsumag I A; prod_pOp I A b c \<in> carr_dsumag I A; prod_pOp I A (prod_pOp I A a b) c \<in> carr_dsumag I A; prod_pOp I A a (prod_pOp I A b c) \<in> carr_dsumag I A; l \<in> I\<rbrakk> \<Longrightarrow> a l \<plusminus>\<^bsub>A l\<^esub> b l \<plusminus>\<^bsub>A l\<^esub> c l = a l \<plusminus>\<^bsub>A l\<^esub> (b l \<plusminus>\<^bsub>A l\<^esub> c l)
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (thin_tac "prod_pOp I A a b \<in> carr_dsumag I A",
        thin_tac "prod_pOp I A b c \<in> carr_dsumag I A",
        thin_tac "prod_pOp I A (prod_pOp I A a b) c \<in> carr_dsumag I A",
        thin_tac "prod_pOp I A a (prod_pOp I A b c) \<in> carr_dsumag I A",
        thin_tac "carr_dsumag I A \<subseteq> carr_prodag I A")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; c \<in> carr_dsumag I A; l \<in> I\<rbrakk> \<Longrightarrow> a l \<plusminus>\<^bsub>A l\<^esub> b l \<plusminus>\<^bsub>A l\<^esub> c l = a l \<plusminus>\<^bsub>A l\<^esub> (b l \<plusminus>\<^bsub>A l\<^esub> c l)
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (frule_tac x = l in bspec, assumption,
        thin_tac "\<forall>k\<in>I. aGroup (A k)",
        simp add:carr_dsumag_def finiteHom_def, (erule conjE)+,
        simp add:carr_prodag_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c l. \<lbrakk>l \<in> I; aGroup (A l); \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. a j = \<zero>\<^bsub>A j\<^esub>); \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. b j = \<zero>\<^bsub>A j\<^esub>); \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. c j = \<zero>\<^bsub>A j\<^esub>); a \<in> extensional I; b \<in> extensional I; c \<in> extensional I; a \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. a i \<in> carrier (A i); b \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. b i \<in> carrier (A i); c \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. c i \<in> carrier (A i)\<rbrakk> \<Longrightarrow> a l \<plusminus>\<^bsub>A l\<^esub> b l \<plusminus>\<^bsub>A l\<^esub> c l = a l \<plusminus>\<^bsub>A l\<^esub> (b l \<plusminus>\<^bsub>A l\<^esub> c l)
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (frule_tac x = l in bspec, assumption,
        thin_tac "\<forall>i\<in>I. a i \<in> carrier (A i)",
        frule_tac x = l in bspec, assumption,
        thin_tac "\<forall>i\<in>I. b i \<in> carrier (A i)",
        frule_tac x = l in bspec, assumption,
        thin_tac "\<forall>i\<in>I. c i \<in> carrier (A i)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c l. \<lbrakk>l \<in> I; aGroup (A l); \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. a j = \<zero>\<^bsub>A j\<^esub>); \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. b j = \<zero>\<^bsub>A j\<^esub>); \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. c j = \<zero>\<^bsub>A j\<^esub>); a \<in> extensional I; b \<in> extensional I; c \<in> extensional I; a \<in> I \<rightarrow> Un_carrier I A; b \<in> I \<rightarrow> Un_carrier I A; c \<in> I \<rightarrow> Un_carrier I A; a l \<in> carrier (A l); b l \<in> carrier (A l); c l \<in> carrier (A l)\<rbrakk> \<Longrightarrow> a l \<plusminus>\<^bsub>A l\<^esub> b l \<plusminus>\<^bsub>A l\<^esub> c l = a l \<plusminus>\<^bsub>A l\<^esub> (b l \<plusminus>\<^bsub>A l\<^esub> c l)
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (simp add:aGroup.aassoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carr_dsumag I A \<longrightarrow> (\<forall>b. b \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (rule allI, rule impI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> prod_pOp I A a b = prod_pOp I A b a
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (rule carr_prodag_mem_eq [of "I" "A"], assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> prod_pOp I A a b \<in> carr_prodag I A
 2. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> prod_pOp I A b a \<in> carr_prodag I A
 3. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> \<forall>l\<in>I. prod_pOp I A a b l = prod_pOp I A b a l
 4. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (frule_tac X = a and Y = b in prod_pOp_mem[of "I" "A"],
         (simp add:subsetD)+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> prod_pOp I A b a \<in> carr_prodag I A
 2. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> \<forall>l\<in>I. prod_pOp I A a b l = prod_pOp I A b a l
 3. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (frule_tac X = b and Y = a in prod_pOp_mem[of "I" "A"],
         (simp add:subsetD)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> \<forall>l\<in>I. prod_pOp I A a b l = prod_pOp I A b a l
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (rule ballI,
         subst prod_pOp_mem_i, assumption+, (simp add:subsetD)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; l \<in> I\<rbrakk> \<Longrightarrow> a l \<plusminus>\<^bsub>A l\<^esub> b l = prod_pOp I A b a l
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (subst prod_pOp_mem_i, assumption+, (simp add:subsetD)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; l \<in> I\<rbrakk> \<Longrightarrow> a l \<plusminus>\<^bsub>A l\<^esub> b l = b l \<plusminus>\<^bsub>A l\<^esub> a l
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (frule_tac x = l in bspec, assumption,
         thin_tac "\<forall>k\<in>I. aGroup (A k)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b l. \<lbrakk>carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; b \<in> carr_dsumag I A; l \<in> I; aGroup (A l)\<rbrakk> \<Longrightarrow> a l \<plusminus>\<^bsub>A l\<^esub> b l = b l \<plusminus>\<^bsub>A l\<^esub> a l
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (frule_tac c = a in subsetD[of "carr_dsumag I A" "carr_prodag I A"],
          assumption+, thin_tac "a \<in> carr_dsumag I A",
         frule_tac c = b in subsetD[of "carr_dsumag I A" "carr_prodag I A"],
          assumption+, thin_tac "b \<in> carr_dsumag I A",
          thin_tac "carr_dsumag I A \<subseteq> carr_prodag I A")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b l. \<lbrakk>l \<in> I; aGroup (A l); a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> a l \<plusminus>\<^bsub>A l\<^esub> b l = b l \<plusminus>\<^bsub>A l\<^esub> a l
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (simp add:carr_prodag_def, (erule conjE)+,
         simp add:aGroup.ag_pOp_commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a
[PROOF STEP]
apply (frule_tac X = a in prod_mOp_mem[of "I" "A"],
        simp add:subsetD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; prod_mOp I A a \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a
[PROOF STEP]
apply (frule_tac X = "prod_mOp I A a" and Y = a in prod_pOp_mem[of "I" "A"],
        simp add:subsetD, simp add:subsetD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; prod_mOp I A a \<in> carr_prodag I A; prod_pOp I A (prod_mOp I A a) a \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a
[PROOF STEP]
apply (rule carr_prodag_mem_eq [of "I" "A"], assumption+,
        simp add:prod_zero_func)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; prod_mOp I A a \<in> carr_prodag I A; prod_pOp I A (prod_mOp I A a) a \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>l\<in>I. prod_pOp I A (prod_mOp I A a) a l = prod_zero I A l
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; prod_mOp I A a \<in> carr_prodag I A; prod_pOp I A (prod_mOp I A a) a \<in> carr_prodag I A; l \<in> I\<rbrakk> \<Longrightarrow> prod_pOp I A (prod_mOp I A a) a l = prod_zero I A l
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a
[PROOF STEP]
apply (subst prod_pOp_mem_i, assumption+,
        simp add:subsetD, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; prod_mOp I A a \<in> carr_prodag I A; prod_pOp I A (prod_mOp I A a) a \<in> carr_prodag I A; l \<in> I\<rbrakk> \<Longrightarrow> prod_mOp I A a l \<plusminus>\<^bsub>A l\<^esub> a l = prod_zero I A l
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a
[PROOF STEP]
apply (subst prod_mOp_mem_i, assumption+, simp add:subsetD, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; prod_mOp I A a \<in> carr_prodag I A; prod_pOp I A (prod_mOp I A a) a \<in> carr_prodag I A; l \<in> I\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>A l\<^esub> a l \<plusminus>\<^bsub>A l\<^esub> a l = prod_zero I A l
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a
[PROOF STEP]
apply (simp add:prod_zero_i)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; prod_mOp I A a \<in> carr_prodag I A; prod_pOp I A (prod_mOp I A a) a \<in> carr_prodag I A; l \<in> I\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>A l\<^esub> a l \<plusminus>\<^bsub>A l\<^esub> a l = \<zero>\<^bsub>A l\<^esub>
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a
[PROOF STEP]
apply (frule_tac x = l in bspec, assumption,
         thin_tac "\<forall>k\<in>I. aGroup (A k)",
         thin_tac "prod_mOp I A a \<in> carr_prodag I A",
         thin_tac "prod_pOp I A (prod_mOp I A a) a \<in> carr_prodag I A",
        frule_tac c = a in subsetD[of "carr_dsumag I A" "carr_prodag I A"],
         assumption,
        thin_tac "carr_dsumag I A \<subseteq> carr_prodag I A",
        simp add:carr_prodag_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a l. \<lbrakk>a \<in> carr_dsumag I A; l \<in> I; aGroup (A l); a \<in> extensional I; a \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. a i \<in> carrier (A i)\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>A l\<^esub> a l \<plusminus>\<^bsub>A l\<^esub> a l = \<zero>\<^bsub>A l\<^esub>
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a
[PROOF STEP]
apply (frule_tac x = l in bspec, assumption,
         thin_tac "\<forall>i\<in>I. a i \<in> carrier (A i)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a l. \<lbrakk>a \<in> carr_dsumag I A; l \<in> I; aGroup (A l); a \<in> extensional I; a \<in> I \<rightarrow> Un_carrier I A; a l \<in> carrier (A l)\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>A l\<^esub> a l \<plusminus>\<^bsub>A l\<^esub> a l = \<zero>\<^bsub>A l\<^esub>
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a
[PROOF STEP]
apply (rule aGroup.l_m, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carr_dsumag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> prod_pOp I A (prod_zero I A) a = a
[PROOF STEP]
apply (frule prod_zero_func[of "I" "A"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; prod_zero I A \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_pOp I A (prod_zero I A) a = a
[PROOF STEP]
apply (frule_tac X = "prod_zero I A" and Y = a in prod_pOp_mem[of "I" "A"],
            assumption+, simp add:subsetD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; prod_zero I A \<in> carr_prodag I A; prod_pOp I A (prod_zero I A) a \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_pOp I A (prod_zero I A) a = a
[PROOF STEP]
apply (rule carr_prodag_mem_eq [of "I" "A"], assumption+,
        simp add:subsetD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; prod_zero I A \<in> carr_prodag I A; prod_pOp I A (prod_zero I A) a \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>l\<in>I. prod_pOp I A (prod_zero I A) a l = a l
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; prod_zero I A \<in> carr_prodag I A; prod_pOp I A (prod_zero I A) a \<in> carr_prodag I A; l \<in> I\<rbrakk> \<Longrightarrow> prod_pOp I A (prod_zero I A) a l = a l
[PROOF STEP]
apply (subst prod_pOp_mem_i, assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; prod_zero I A \<in> carr_prodag I A; prod_pOp I A (prod_zero I A) a \<in> carr_prodag I A; l \<in> I\<rbrakk> \<Longrightarrow> a \<in> carr_prodag I A
 2. \<And>a l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; prod_zero I A \<in> carr_prodag I A; prod_pOp I A (prod_zero I A) a \<in> carr_prodag I A; l \<in> I\<rbrakk> \<Longrightarrow> l \<in> I
 3. \<And>a l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; prod_zero I A \<in> carr_prodag I A; prod_pOp I A (prod_zero I A) a \<in> carr_prodag I A; l \<in> I\<rbrakk> \<Longrightarrow> prod_zero I A l \<plusminus>\<^bsub>A l\<^esub> a l = a l
[PROOF STEP]
apply (simp add:subsetD, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); carr_dsumag I A \<subseteq> carr_prodag I A; a \<in> carr_dsumag I A; prod_zero I A \<in> carr_prodag I A; prod_pOp I A (prod_zero I A) a \<in> carr_prodag I A; l \<in> I\<rbrakk> \<Longrightarrow> prod_zero I A l \<plusminus>\<^bsub>A l\<^esub> a l = a l
[PROOF STEP]
apply (simp add:prod_zero_i,
        frule_tac x = l in bspec, assumption,
        thin_tac "\<forall>k\<in>I. aGroup (A k)",
        frule_tac c = a in subsetD[of "carr_dsumag I A" "carr_prodag I A"],
                  assumption+,
        thin_tac "carr_dsumag I A \<subseteq> carr_prodag I A",
        thin_tac "a \<in> carr_dsumag I A",
        thin_tac "prod_pOp I A (prod_zero I A) a \<in> carr_prodag I A")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>prod_zero I A \<in> carr_prodag I A; l \<in> I; aGroup (A l); a \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>A l\<^esub> \<plusminus>\<^bsub>A l\<^esub> a l = a l
[PROOF STEP]
apply (simp add:carr_prodag_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> I; aGroup (A l); prod_zero I A \<in> extensional I; a \<in> extensional I; prod_zero I A \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. prod_zero I A i \<in> carrier (A i); a \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. a i \<in> carrier (A i)\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>A l\<^esub> \<plusminus>\<^bsub>A l\<^esub> a l = a l
[PROOF STEP]
apply (rule aGroup.l_zero, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>l \<in> I; aGroup (A l); prod_zero I A \<in> extensional I; a \<in> extensional I; prod_zero I A \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. prod_zero I A i \<in> carrier (A i); a \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. a i \<in> carrier (A i)\<rbrakk> \<Longrightarrow> a l \<in> carrier (A l)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma dsumag_pOp:"\<forall>k\<in>I. aGroup (A k) \<Longrightarrow>
                  pop (dsumag I A) = prod_pOp I A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> (\<plusminus>\<^bsub>a\<Oplus>\<^bsub>I\<^esub> A\<^esub>) = prod_pOp I A
[PROOF STEP]
apply (simp add:dsumag_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma dsumag_mOp:"\<forall>k\<in>I. aGroup (A k) \<Longrightarrow>
                  mop (dsumag I A) = prod_mOp I A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> mop (a\<Oplus>\<^bsub>I\<^esub> A) = prod_mOp I A
[PROOF STEP]
apply (simp add:dsumag_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma dsumag_zero:"\<forall>k\<in>I. aGroup (A k) \<Longrightarrow>
                  zero (dsumag I A) = prod_zero I A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<zero>\<^bsub>a\<Oplus>\<^bsub>I\<^esub> A\<^esub> = prod_zero I A
[PROOF STEP]
apply (simp add:dsumag_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma direct_prod_mem_eq:"\<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A);
       g \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. (PRoject I A j) f = (PRoject I A j) g\<rbrakk> \<Longrightarrow>
       f = g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); g \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. (\<pi>\<^bsub>I,A,j\<^esub>) f = (\<pi>\<^bsub>I,A,j\<^esub>) g\<rbrakk> \<Longrightarrow> f = g
[PROOF STEP]
apply (rule funcset_eq[of "f" "I" "g"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); g \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. (\<pi>\<^bsub>I,A,j\<^esub>) f = (\<pi>\<^bsub>I,A,j\<^esub>) g\<rbrakk> \<Longrightarrow> f \<in> extensional I
 2. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); g \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. (\<pi>\<^bsub>I,A,j\<^esub>) f = (\<pi>\<^bsub>I,A,j\<^esub>) g\<rbrakk> \<Longrightarrow> g \<in> extensional I
 3. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); g \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. (\<pi>\<^bsub>I,A,j\<^esub>) f = (\<pi>\<^bsub>I,A,j\<^esub>) g\<rbrakk> \<Longrightarrow> \<forall>x\<in>I. f x = g x
[PROOF STEP]
apply (thin_tac "\<forall>j\<in>I. aGroup (A j)",
        thin_tac "g \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A)",
        thin_tac "\<forall>j\<in>I. (\<pi>\<^bsub>I,A,j\<^esub>) f = (\<pi>\<^bsub>I,A,j\<^esub>) g",
        simp add:prodag_def carr_prodag_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); g \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. (\<pi>\<^bsub>I,A,j\<^esub>) f = (\<pi>\<^bsub>I,A,j\<^esub>) g\<rbrakk> \<Longrightarrow> g \<in> extensional I
 2. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); g \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. (\<pi>\<^bsub>I,A,j\<^esub>) f = (\<pi>\<^bsub>I,A,j\<^esub>) g\<rbrakk> \<Longrightarrow> \<forall>x\<in>I. f x = g x
[PROOF STEP]
apply (thin_tac "\<forall>j\<in>I. aGroup (A j)",
        thin_tac "f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A)",
        thin_tac "\<forall>j\<in>I. (\<pi>\<^bsub>I,A,j\<^esub>) f = (\<pi>\<^bsub>I,A,j\<^esub>) g",
        simp add:prodag_def carr_prodag_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); g \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. (\<pi>\<^bsub>I,A,j\<^esub>) f = (\<pi>\<^bsub>I,A,j\<^esub>) g\<rbrakk> \<Longrightarrow> \<forall>x\<in>I. f x = g x
[PROOF STEP]
apply (simp add:PRoject_def prodag_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma map_family_fun:"\<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S;
      \<forall>j\<in>I. ((g j) \<in> aHom S (A j)); x \<in> carrier S\<rbrakk> \<Longrightarrow>
         (\<lambda>y \<in> carrier S. (\<lambda>j\<in>I. (g j) y)) x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); x \<in> carrier S\<rbrakk> \<Longrightarrow> (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A)
[PROOF STEP]
apply (simp add:prodag_def carr_prodag_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); x \<in> carrier S\<rbrakk> \<Longrightarrow> (\<lambda>j\<in>I. g j x) \<in> I \<rightarrow> Un_carrier I A \<and> (\<forall>i\<in>I. g i x \<in> carrier (A i))
[PROOF STEP]
apply (simp add:aHom_mem)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); x \<in> carrier S\<rbrakk> \<Longrightarrow> (\<lambda>j\<in>I. g j x) \<in> I \<rightarrow> Un_carrier I A
[PROOF STEP]
apply (rule Pi_I, simp add:Un_carrier_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); x \<in> carrier S; xa \<in> I\<rbrakk> \<Longrightarrow> \<exists>xb. (\<exists>i\<in>I. xb = carrier (A i)) \<and> g xa x \<in> xb
[PROOF STEP]
apply (frule_tac x = xa in bspec, assumption,
        thin_tac "\<forall>j\<in>I. aGroup (A j)",
        frule_tac x = xa in bspec, assumption,
        thin_tac "\<forall>j\<in>I. g j \<in> aHom S (A j)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>aGroup S; x \<in> carrier S; xa \<in> I; aGroup (A xa); g xa \<in> aHom S (A xa)\<rbrakk> \<Longrightarrow> \<exists>xb. (\<exists>i\<in>I. xb = carrier (A i)) \<and> g xa x \<in> xb
[PROOF STEP]
apply (frule_tac G = "A xa" and f = "g xa" and a = x in aHom_mem[of "S"],
        assumption+, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma map_family_aHom:"\<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S;
      \<forall>j\<in>I. ((g j) \<in> aHom S (A j))\<rbrakk> \<Longrightarrow>
         (\<lambda>y \<in> carrier S. (\<lambda>j\<in>I. (g j) y)) \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j)\<rbrakk> \<Longrightarrow> (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A)
[PROOF STEP]
apply (subst aHom_def, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j)\<rbrakk> \<Longrightarrow> (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) \<in> carrier S \<rightarrow> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>a\<in>carrier S. \<forall>b\<in>carrier S. (a \<plusminus>\<^bsub>S\<^esub> b \<in> carrier S \<longrightarrow> (\<lambda>j\<in>I. g j (a \<plusminus>\<^bsub>S\<^esub> b)) = (\<lambda>j\<in>I. g j a) \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> (\<lambda>j\<in>I. g j b)) \<and> (a \<plusminus>\<^bsub>S\<^esub> b \<notin> carrier S \<longrightarrow> undefined = (\<lambda>j\<in>I. g j a) \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> (\<lambda>j\<in>I. g j b)))
[PROOF STEP]
apply (simp add:aGroup.ag_pOp_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j)\<rbrakk> \<Longrightarrow> (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) \<in> carrier S \<rightarrow> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>a\<in>carrier S. \<forall>b\<in>carrier S. (\<lambda>j\<in>I. g j (a \<plusminus>\<^bsub>S\<^esub> b)) = (\<lambda>j\<in>I. g j a) \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> (\<lambda>j\<in>I. g j b))
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j)\<rbrakk> \<Longrightarrow> (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) \<in> carrier S \<rightarrow> carrier (a\<Pi>\<^bsub>I\<^esub> A)
 2. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j)\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier S. \<forall>b\<in>carrier S. (\<lambda>j\<in>I. g j (a \<plusminus>\<^bsub>S\<^esub> b)) = (\<lambda>j\<in>I. g j a) \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> (\<lambda>j\<in>I. g j b)
[PROOF STEP]
apply (rule Pi_I)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); x \<in> carrier S\<rbrakk> \<Longrightarrow> (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A)
 2. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j)\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier S. \<forall>b\<in>carrier S. (\<lambda>j\<in>I. g j (a \<plusminus>\<^bsub>S\<^esub> b)) = (\<lambda>j\<in>I. g j a) \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> (\<lambda>j\<in>I. g j b)
[PROOF STEP]
apply (rule map_family_fun[of "I" "A" "S" "g"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j)\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier S. \<forall>b\<in>carrier S. (\<lambda>j\<in>I. g j (a \<plusminus>\<^bsub>S\<^esub> b)) = (\<lambda>j\<in>I. g j a) \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> (\<lambda>j\<in>I. g j b)
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); a \<in> carrier S; b \<in> carrier S\<rbrakk> \<Longrightarrow> (\<lambda>j\<in>I. g j (a \<plusminus>\<^bsub>S\<^esub> b)) = (\<lambda>j\<in>I. g j a) \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> (\<lambda>j\<in>I. g j b)
[PROOF STEP]
apply (frule_tac x = a and y = b in aGroup.ag_pOp_closed[of "S"],
                   assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); a \<in> carrier S; b \<in> carrier S; a \<plusminus>\<^bsub>S\<^esub> b \<in> carrier S\<rbrakk> \<Longrightarrow> (\<lambda>j\<in>I. g j (a \<plusminus>\<^bsub>S\<^esub> b)) = (\<lambda>j\<in>I. g j a) \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> (\<lambda>j\<in>I. g j b)
[PROOF STEP]
apply (frule_tac x = "a \<plusminus>\<^bsub>S\<^esub> b" in map_family_fun[of "I" "A" "S" "g"],
          assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); a \<in> carrier S; b \<in> carrier S; a \<plusminus>\<^bsub>S\<^esub> b \<in> carrier S; (\<lambda>j\<in>I. g j (a \<plusminus>\<^bsub>S\<^esub> b)) \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> (\<lambda>j\<in>I. g j (a \<plusminus>\<^bsub>S\<^esub> b)) = (\<lambda>j\<in>I. g j a) \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> (\<lambda>j\<in>I. g j b)
[PROOF STEP]
apply (frule_tac x = a in map_family_fun[of "I" "A" "S" "g"],
          assumption+, simp,
         frule_tac x = b in map_family_fun[of "I" "A" "S" "g"],
          assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); a \<in> carrier S; b \<in> carrier S; a \<plusminus>\<^bsub>S\<^esub> b \<in> carrier S; (\<lambda>j\<in>I. g j (a \<plusminus>\<^bsub>S\<^esub> b)) \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); (\<lambda>j\<in>I. g j a) \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); (\<lambda>j\<in>I. g j b) \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> (\<lambda>j\<in>I. g j (a \<plusminus>\<^bsub>S\<^esub> b)) = (\<lambda>j\<in>I. g j a) \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> (\<lambda>j\<in>I. g j b)
[PROOF STEP]
apply (frule prodag_aGroup[of "I" "A"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); a \<in> carrier S; b \<in> carrier S; a \<plusminus>\<^bsub>S\<^esub> b \<in> carrier S; (\<lambda>j\<in>I. g j (a \<plusminus>\<^bsub>S\<^esub> b)) \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); (\<lambda>j\<in>I. g j a) \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); (\<lambda>j\<in>I. g j b) \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); aGroup (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> (\<lambda>j\<in>I. g j (a \<plusminus>\<^bsub>S\<^esub> b)) = (\<lambda>j\<in>I. g j a) \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> (\<lambda>j\<in>I. g j b)
[PROOF STEP]
apply (frule_tac x = "(\<lambda>j\<in>I. g j a)" and y = "(\<lambda>j\<in>I. g j b)" in
        aGroup.ag_pOp_closed[of "a\<Pi>\<^bsub>I\<^esub> A"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); a \<in> carrier S; b \<in> carrier S; a \<plusminus>\<^bsub>S\<^esub> b \<in> carrier S; (\<lambda>j\<in>I. g j (a \<plusminus>\<^bsub>S\<^esub> b)) \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); (\<lambda>j\<in>I. g j a) \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); (\<lambda>j\<in>I. g j b) \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); aGroup (a\<Pi>\<^bsub>I\<^esub> A); (\<lambda>j\<in>I. g j a) \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> (\<lambda>j\<in>I. g j b) \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> (\<lambda>j\<in>I. g j (a \<plusminus>\<^bsub>S\<^esub> b)) = (\<lambda>j\<in>I. g j a) \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> (\<lambda>j\<in>I. g j b)
[PROOF STEP]
apply (simp only:prodag_carrier)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); a \<in> carrier S; b \<in> carrier S; a \<plusminus>\<^bsub>S\<^esub> b \<in> carrier S; (\<lambda>j\<in>I. g j (a \<plusminus>\<^bsub>S\<^esub> b)) \<in> carr_prodag I A; (\<lambda>j\<in>I. g j a) \<in> carr_prodag I A; (\<lambda>j\<in>I. g j b) \<in> carr_prodag I A; aGroup (a\<Pi>\<^bsub>I\<^esub> A); (\<lambda>j\<in>I. g j a) \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> (\<lambda>j\<in>I. g j b) \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<lambda>j\<in>I. g j (a \<plusminus>\<^bsub>S\<^esub> b)) = (\<lambda>j\<in>I. g j a) \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> (\<lambda>j\<in>I. g j b)
[PROOF STEP]
apply (rule carr_prodag_mem_eq, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); a \<in> carrier S; b \<in> carrier S; a \<plusminus>\<^bsub>S\<^esub> b \<in> carrier S; (\<lambda>j\<in>I. g j (a \<plusminus>\<^bsub>S\<^esub> b)) \<in> carr_prodag I A; (\<lambda>j\<in>I. g j a) \<in> carr_prodag I A; (\<lambda>j\<in>I. g j b) \<in> carr_prodag I A; aGroup (a\<Pi>\<^bsub>I\<^esub> A); (\<lambda>j\<in>I. g j a) \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> (\<lambda>j\<in>I. g j b) \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> \<forall>l\<in>I. (\<lambda>j\<in>I. g j (a \<plusminus>\<^bsub>S\<^esub> b)) l = ((\<lambda>j\<in>I. g j a) \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> (\<lambda>j\<in>I. g j b)) l
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b l. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); a \<in> carrier S; b \<in> carrier S; a \<plusminus>\<^bsub>S\<^esub> b \<in> carrier S; (\<lambda>j\<in>I. g j (a \<plusminus>\<^bsub>S\<^esub> b)) \<in> carr_prodag I A; (\<lambda>j\<in>I. g j a) \<in> carr_prodag I A; (\<lambda>j\<in>I. g j b) \<in> carr_prodag I A; aGroup (a\<Pi>\<^bsub>I\<^esub> A); (\<lambda>j\<in>I. g j a) \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> (\<lambda>j\<in>I. g j b) \<in> carr_prodag I A; l \<in> I\<rbrakk> \<Longrightarrow> (\<lambda>j\<in>I. g j (a \<plusminus>\<^bsub>S\<^esub> b)) l = ((\<lambda>j\<in>I. g j a) \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> (\<lambda>j\<in>I. g j b)) l
[PROOF STEP]
apply (subst prodag_def, simp add:prod_pOp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b l. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); a \<in> carrier S; b \<in> carrier S; a \<plusminus>\<^bsub>S\<^esub> b \<in> carrier S; (\<lambda>j\<in>I. g j (a \<plusminus>\<^bsub>S\<^esub> b)) \<in> carr_prodag I A; (\<lambda>j\<in>I. g j a) \<in> carr_prodag I A; (\<lambda>j\<in>I. g j b) \<in> carr_prodag I A; aGroup (a\<Pi>\<^bsub>I\<^esub> A); (\<lambda>j\<in>I. g j a) \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> (\<lambda>j\<in>I. g j b) \<in> carr_prodag I A; l \<in> I\<rbrakk> \<Longrightarrow> g l (a \<plusminus>\<^bsub>S\<^esub> b) = g l a \<plusminus>\<^bsub>A l\<^esub> g l b
[PROOF STEP]
apply (simp add:aHom_add)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma map_family_triangle:"\<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S;
         \<forall>j\<in>I. ((g j) \<in> aHom S (A j))\<rbrakk> \<Longrightarrow> \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and>
                  (\<forall>j\<in>I. compos S (PRoject I A j) f =  (g j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j)\<rbrakk> \<Longrightarrow> \<exists>!f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j)
[PROOF STEP]
apply (rule ex_ex1I)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j)\<rbrakk> \<Longrightarrow> \<exists>f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j)
 2. \<And>f y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); y \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) y = g j)\<rbrakk> \<Longrightarrow> f = y
[PROOF STEP]
apply (frule map_family_aHom[of "I" "A" "S" "g"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> \<exists>f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j)
 2. \<And>f y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); y \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) y = g j)\<rbrakk> \<Longrightarrow> f = y
[PROOF STEP]
apply (subgoal_tac "\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) = g j")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) = g j\<rbrakk> \<Longrightarrow> \<exists>f. f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j)
 2. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) = g j
 3. \<And>f y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); y \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) y = g j)\<rbrakk> \<Longrightarrow> f = y
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) = g j
 2. \<And>f y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); y \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) y = g j)\<rbrakk> \<Longrightarrow> f = y
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); j \<in> I\<rbrakk> \<Longrightarrow> compos S (\<pi>\<^bsub>I,A,j\<^esub>) (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) = g j
 2. \<And>f y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); y \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) y = g j)\<rbrakk> \<Longrightarrow> f = y
[PROOF STEP]
apply (simp add:compos_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); j \<in> I\<rbrakk> \<Longrightarrow> compose (carrier S) (\<pi>\<^bsub>I,A,j\<^esub>) (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) = g j
 2. \<And>f y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); y \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) y = g j)\<rbrakk> \<Longrightarrow> f = y
[PROOF STEP]
apply (rule funcset_eq[of _ "carrier S"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); j \<in> I\<rbrakk> \<Longrightarrow> compose (carrier S) (\<pi>\<^bsub>I,A,j\<^esub>) (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) \<in> extensional (carrier S)
 2. \<And>j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); j \<in> I\<rbrakk> \<Longrightarrow> g j \<in> extensional (carrier S)
 3. \<And>j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); j \<in> I\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier S. compose (carrier S) (\<pi>\<^bsub>I,A,j\<^esub>) (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) x = g j x
 4. \<And>f y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); y \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) y = g j)\<rbrakk> \<Longrightarrow> f = y
[PROOF STEP]
apply (simp add:compose_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); j \<in> I\<rbrakk> \<Longrightarrow> g j \<in> extensional (carrier S)
 2. \<And>j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); j \<in> I\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier S. compose (carrier S) (\<pi>\<^bsub>I,A,j\<^esub>) (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) x = g j x
 3. \<And>f y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); y \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) y = g j)\<rbrakk> \<Longrightarrow> f = y
[PROOF STEP]
apply (simp add:aHom_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); j \<in> I\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier S. compose (carrier S) (\<pi>\<^bsub>I,A,j\<^esub>) (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) x = g j x
 2. \<And>f y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); y \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) y = g j)\<rbrakk> \<Longrightarrow> f = y
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j x. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); j \<in> I; x \<in> carrier S\<rbrakk> \<Longrightarrow> compose (carrier S) (\<pi>\<^bsub>I,A,j\<^esub>) (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) x = g j x
 2. \<And>f y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); y \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) y = g j)\<rbrakk> \<Longrightarrow> f = y
[PROOF STEP]
apply (frule prodag_aGroup[of "I" "A"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j x. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); j \<in> I; x \<in> carrier S; aGroup (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> compose (carrier S) (\<pi>\<^bsub>I,A,j\<^esub>) (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) x = g j x
 2. \<And>f y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); y \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) y = g j)\<rbrakk> \<Longrightarrow> f = y
[PROOF STEP]
apply (frule prodag_carrier[of "I" "A"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j x. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); j \<in> I; x \<in> carrier S; aGroup (a\<Pi>\<^bsub>I\<^esub> A); carrier (a\<Pi>\<^bsub>I\<^esub> A) = carr_prodag I A\<rbrakk> \<Longrightarrow> compose (carrier S) (\<pi>\<^bsub>I,A,j\<^esub>) (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) x = g j x
 2. \<And>f y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); y \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) y = g j)\<rbrakk> \<Longrightarrow> f = y
[PROOF STEP]
apply (frule_tac f = "\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y" and a = x in
        aHom_mem[of "S" "a\<Pi>\<^bsub>I\<^esub> A"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j x. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); j \<in> I; x \<in> carrier S; aGroup (a\<Pi>\<^bsub>I\<^esub> A); carrier (a\<Pi>\<^bsub>I\<^esub> A) = carr_prodag I A; (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> compose (carrier S) (\<pi>\<^bsub>I,A,j\<^esub>) (\<lambda>y\<in>carrier S. \<lambda>j\<in>I. g j y) x = g j x
 2. \<And>f y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); y \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) y = g j)\<rbrakk> \<Longrightarrow> f = y
[PROOF STEP]
apply (simp add:compose_def, simp add:PRoject_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f y. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); y \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) y = g j)\<rbrakk> \<Longrightarrow> f = y
[PROOF STEP]
apply (rename_tac f f1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f f1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j); f1 \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f1 = g j)\<rbrakk> \<Longrightarrow> f = f1
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f f1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j; f1 \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f1 = g j\<rbrakk> \<Longrightarrow> f = f1
[PROOF STEP]
apply (rule funcset_eq[of _ "carrier S"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>f f1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j; f1 \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f1 = g j\<rbrakk> \<Longrightarrow> f \<in> extensional (carrier S)
 2. \<And>f f1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j; f1 \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f1 = g j\<rbrakk> \<Longrightarrow> f1 \<in> extensional (carrier S)
 3. \<And>f f1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j; f1 \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f1 = g j\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier S. f x = f1 x
[PROOF STEP]
apply (simp add:aHom_def, simp add:aHom_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f f1. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j; f1 \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f1 = g j\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier S. f x = f1 x
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f f1 x. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j; f1 \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f1 = g j; x \<in> carrier S\<rbrakk> \<Longrightarrow> f x = f1 x
[PROOF STEP]
apply (frule prodag_aGroup[of "I" "A"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f f1 x. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j; f1 \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f1 = g j; x \<in> carrier S; aGroup (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> f x = f1 x
[PROOF STEP]
apply (frule_tac f = f and a = x in aHom_mem[of "S" "a\<Pi>\<^bsub>I\<^esub> A"], assumption+,
        frule_tac f = f1 and a = x in aHom_mem[of "S" "a\<Pi>\<^bsub>I\<^esub> A"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f f1 x. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j; f1 \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f1 = g j; x \<in> carrier S; aGroup (a\<Pi>\<^bsub>I\<^esub> A); f x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); f1 x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> f x = f1 x
[PROOF STEP]
apply (rule_tac f = "f x" and g = "f1 x" in direct_prod_mem_eq[of "I" "A"],
        assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f f1 x. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j; f1 \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f1 = g j; x \<in> carrier S; aGroup (a\<Pi>\<^bsub>I\<^esub> A); f x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); f1 x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> \<forall>j\<in>I. (\<pi>\<^bsub>I,A,j\<^esub>) (f x) = (\<pi>\<^bsub>I,A,j\<^esub>) (f1 x)
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f f1 x j. \<lbrakk>\<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j; f1 \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); \<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f1 = g j; x \<in> carrier S; aGroup (a\<Pi>\<^bsub>I\<^esub> A); f x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); f1 x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); j \<in> I\<rbrakk> \<Longrightarrow> (\<pi>\<^bsub>I,A,j\<^esub>) (f x) = (\<pi>\<^bsub>I,A,j\<^esub>) (f1 x)
[PROOF STEP]
apply (rotate_tac 4,
        frule_tac x = j in bspec, assumption,
        thin_tac "\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f = g j",
         frule_tac x = j in bspec, assumption,
        thin_tac "\<forall>j\<in>I. compos S (\<pi>\<^bsub>I,A,j\<^esub>) f1 = g j",
        simp add:compos_def compose_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f f1 x j. \<lbrakk>f1 \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); x \<in> carrier S; aGroup (a\<Pi>\<^bsub>I\<^esub> A); f x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); f1 x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); j \<in> I; \<forall>j\<in>I. aGroup (A j); aGroup S; \<forall>j\<in>I. g j \<in> aHom S (A j); f \<in> aHom S (a\<Pi>\<^bsub>I\<^esub> A); (\<lambda>x\<in>carrier S. (\<pi>\<^bsub>I,A,j\<^esub>) (f x)) = g j; (\<lambda>x\<in>carrier S. (\<pi>\<^bsub>I,A,j\<^esub>) (f1 x)) = g j\<rbrakk> \<Longrightarrow> (\<pi>\<^bsub>I,A,j\<^esub>) (f x) = (\<pi>\<^bsub>I,A,j\<^esub>) (f1 x)
[PROOF STEP]
apply (subgoal_tac "(\<lambda>x\<in>carrier S. (\<pi>\<^bsub>I,A,j\<^esub>) (f x)) x = g j x",
        subgoal_tac "(\<lambda>x\<in>carrier S. (\<pi>\<^bsub>I,A,j\<^esub>) (f1 x)) x = g j x",
        thin_tac "(\<lambda>x\<in>carrier S. (\<pi>\<^bsub>I,A,j\<^esub>) (f x)) = g j",
        thin_tac "(\<lambda>x\<in>carrier S. (\<pi>\<^bsub>I,A,j\<^esub>) (f1 x)) = g j",
simp+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done