[STATEMENT]
lemma prodag_aGroup:"\<forall>k\<in>I. aGroup (A k) \<Longrightarrow> aGroup (prodag I A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> aGroup (a\<Pi>\<^bsub>I\<^esub> A)
[PROOF STEP]
apply (simp add:aGroup_def [of "(prodag I A)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> (\<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub>) \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>a. a \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<longrightarrow> (\<forall>b. b \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<longrightarrow> (\<forall>c. c \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<longrightarrow> a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> b \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> c = a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> (b \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<longrightarrow> (\<forall>b. b \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<longrightarrow> a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> b = b \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> a)) \<and> mop (a\<Pi>\<^bsub>I\<^esub> A) \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>a. a \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<longrightarrow> -\<^sub>a\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> a = \<zero>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub>) \<and> \<zero>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<and> (\<forall>a. a \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<longrightarrow> \<zero>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> a = a)
[PROOF STEP]
apply (simp add:prodag_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> prod_pOp I A \<in> carr_prodag I A \<rightarrow> carr_prodag I A \<rightarrow> carr_prodag I A \<and> (\<forall>a. a \<in> carr_prodag I A \<longrightarrow> (\<forall>b. b \<in> carr_prodag I A \<longrightarrow> (\<forall>c. c \<in> carr_prodag 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_prodag I A \<longrightarrow> (\<forall>b. b \<in> carr_prodag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> prod_mOp I A \<in> carr_prodag I A \<rightarrow> carr_prodag I A \<and> (\<forall>a. a \<in> carr_prodag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> prod_zero I A \<in> carr_prodag I A \<and> (\<forall>a. a \<in> carr_prodag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (simp add:prod_pOp_func)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> (\<forall>a. a \<in> carr_prodag I A \<longrightarrow> (\<forall>b. b \<in> carr_prodag I A \<longrightarrow> (\<forall>c. c \<in> carr_prodag 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_prodag I A \<longrightarrow> (\<forall>b. b \<in> carr_prodag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> prod_mOp I A \<in> carr_prodag I A \<rightarrow> carr_prodag I A \<and> (\<forall>a. a \<in> carr_prodag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> prod_zero I A \<in> carr_prodag I A \<and> (\<forall>a. a \<in> carr_prodag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (simp add:prod_mOp_func)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> (\<forall>a. a \<in> carr_prodag I A \<longrightarrow> (\<forall>b. b \<in> carr_prodag I A \<longrightarrow> (\<forall>c. c \<in> carr_prodag 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_prodag I A \<longrightarrow> (\<forall>b. b \<in> carr_prodag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_prodag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> prod_zero I A \<in> carr_prodag I A \<and> (\<forall>a. a \<in> carr_prodag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (simp add:prod_zero_func)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> (\<forall>a. a \<in> carr_prodag I A \<longrightarrow> (\<forall>b. b \<in> carr_prodag I A \<longrightarrow> (\<forall>c. c \<in> carr_prodag 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_prodag I A \<longrightarrow> (\<forall>b. b \<in> carr_prodag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_prodag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_prodag 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. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<forall>a. a \<in> carr_prodag I A \<longrightarrow> (\<forall>b. b \<in> carr_prodag I A \<longrightarrow> (\<forall>c. c \<in> carr_prodag 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. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> (\<forall>a. a \<in> carr_prodag I A \<longrightarrow> (\<forall>b. b \<in> carr_prodag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_prodag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_prodag 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); a \<in> carr_prodag I A; b \<in> carr_prodag I A; c \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_pOp I A (prod_pOp I A a b) c = prod_pOp I A a (prod_pOp I A b c)
 2. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> (\<forall>a. a \<in> carr_prodag I A \<longrightarrow> (\<forall>b. b \<in> carr_prodag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_prodag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_prodag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (simp add:prod_pOp_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> (\<forall>a. a \<in> carr_prodag I A \<longrightarrow> (\<forall>b. b \<in> carr_prodag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)) \<and> (\<forall>a. a \<in> carr_prodag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_prodag 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. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<forall>a. a \<in> carr_prodag I A \<longrightarrow> (\<forall>b. b \<in> carr_prodag I A \<longrightarrow> prod_pOp I A a b = prod_pOp I A b a)
 2. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> (\<forall>a. a \<in> carr_prodag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_prodag 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); a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_pOp I A a b = prod_pOp I A b a
 2. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> (\<forall>a. a \<in> carr_prodag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_prodag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a)
[PROOF STEP]
apply (simp add:prod_pOp_commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> (\<forall>a. a \<in> carr_prodag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A) \<and> (\<forall>a. a \<in> carr_prodag 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. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<forall>a. a \<in> carr_prodag I A \<longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A
 2. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<forall>a. a \<in> carr_prodag 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); a \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_pOp I A (prod_mOp I A a) a = prod_zero I A
 2. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<forall>a. a \<in> carr_prodag 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"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag 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. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<forall>a. a \<in> carr_prodag 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"],
        assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag 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. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<forall>a. a \<in> carr_prodag 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 (3 subgoals):
 1. \<And>a. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag 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_zero I A \<in> carr_prodag I A
 2. \<And>a. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag 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
 3. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<forall>a. a \<in> carr_prodag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a
[PROOF STEP]
apply (simp add:prod_zero_func)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag 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. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<forall>a. a \<in> carr_prodag 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); a \<in> carr_prodag 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. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<forall>a. a \<in> carr_prodag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a
[PROOF STEP]
apply (simp add:prod_pOp_mem_i,
         simp add:prod_zero_i)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag 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 = \<zero>\<^bsub>A l\<^esub>
 2. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<forall>a. a \<in> carr_prodag I A \<longrightarrow> prod_pOp I A (prod_zero I A) a = a
[PROOF STEP]
apply (
         simp add:prod_mOp_mem_i)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag 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. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<forall>a. a \<in> carr_prodag 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)",
         rule aGroup.l_m, assumption+, simp add:prodag_comp_i)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<forall>a. a \<in> carr_prodag 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); a \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> prod_pOp I A (prod_zero I A) a = a
[PROOF STEP]
apply (frule_tac prod_zero_func[of "I" "A"],
         frule_tac Y = a in prod_pOp_mem[of "I" "A" "prod_zero I A"],
          assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag 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+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag 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); a \<in> carr_prodag 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[of "I" "A"], assumption+,
         subst prod_zero_i[of "I" "A"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<forall>k\<in>I. aGroup (A k); a \<in> carr_prodag 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> \<zero>\<^bsub>A l\<^esub> \<plusminus>\<^bsub>A l\<^esub> a l = a l
[PROOF STEP]
apply (frule_tac x = l in bspec, assumption,
         rule aGroup.l_zero, assumption+,
         simp add:prodag_comp_i)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prodag_carrier:"\<forall>k\<in>I. aGroup (A k) \<Longrightarrow>
            carrier (prodag I A) = carr_prodag I A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> carrier (a\<Pi>\<^bsub>I\<^esub> A) = carr_prodag I A
[PROOF STEP]
by (simp add:prodag_def)


[STATEMENT]
lemma prodag_elemfun:"\<lbrakk>\<forall>k\<in>I. aGroup (A k); f \<in> carrier (prodag I A)\<rbrakk> \<Longrightarrow>
         f \<in> extensional I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> f \<in> extensional I
[PROOF STEP]
apply (simp add:prodag_carrier)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); f \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> f \<in> extensional I
[PROOF STEP]
apply (simp add:carr_prodag_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prodag_component:"\<lbrakk>f \<in> carrier (prodag I A); i \<in> I \<rbrakk> \<Longrightarrow>
                              f i \<in> carrier (A i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); i \<in> I\<rbrakk> \<Longrightarrow> f i \<in> carrier (A i)
[PROOF STEP]
by (simp add:prodag_def carr_prodag_def)


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


[STATEMENT]
lemma prodag_zero:"\<forall>k\<in>I. aGroup (A k) \<Longrightarrow>
                  zero (prodag 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\<Pi>\<^bsub>I\<^esub> A\<^esub> = prod_zero I A
[PROOF STEP]
apply (simp add:prodag_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prodag_sameTr0:"\<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k\<rbrakk>
                               \<Longrightarrow> Un_carrier I A = Un_carrier I B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k\<rbrakk> \<Longrightarrow> Un_carrier I A = Un_carrier I B
[PROOF STEP]
apply (simp add:Un_carrier_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prodag_sameTr1:"\<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k\<rbrakk>
                               \<Longrightarrow> carr_prodag I A = carr_prodag I B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k\<rbrakk> \<Longrightarrow> carr_prodag I A = carr_prodag I B
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k\<rbrakk> \<Longrightarrow> carr_prodag I A \<subseteq> carr_prodag I B
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k\<rbrakk> \<Longrightarrow> carr_prodag I B \<subseteq> carr_prodag I A
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k; x \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> x \<in> carr_prodag I B
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k\<rbrakk> \<Longrightarrow> carr_prodag I B \<subseteq> carr_prodag I A
[PROOF STEP]
apply (simp add:carr_prodag_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k; x \<in> extensional I; x \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. x i \<in> carrier (B i)\<rbrakk> \<Longrightarrow> x \<in> I \<rightarrow> Un_carrier I B
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k\<rbrakk> \<Longrightarrow> carr_prodag I B \<subseteq> carr_prodag I A
[PROOF STEP]
apply (rule Pi_I)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k; x \<in> extensional I; x \<in> I \<rightarrow> Un_carrier I A; \<forall>i\<in>I. x i \<in> carrier (B i); xa \<in> I\<rbrakk> \<Longrightarrow> x xa \<in> Un_carrier I B
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k\<rbrakk> \<Longrightarrow> carr_prodag I B \<subseteq> carr_prodag I A
[PROOF STEP]
apply (subst Un_carrier_def, simp, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k\<rbrakk> \<Longrightarrow> carr_prodag I B \<subseteq> carr_prodag I A
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k; x \<in> carr_prodag I B\<rbrakk> \<Longrightarrow> x \<in> carr_prodag I A
[PROOF STEP]
apply (simp add:carr_prodag_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k; x \<in> extensional I; x \<in> I \<rightarrow> Un_carrier I B; \<forall>i\<in>I. x i \<in> carrier (B i)\<rbrakk> \<Longrightarrow> x \<in> I \<rightarrow> Un_carrier I A
[PROOF STEP]
apply (rule Pi_I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k; x \<in> extensional I; x \<in> I \<rightarrow> Un_carrier I B; \<forall>i\<in>I. x i \<in> carrier (B i); xa \<in> I\<rbrakk> \<Longrightarrow> x xa \<in> Un_carrier I A
[PROOF STEP]
apply (subst Un_carrier_def, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k; x \<in> extensional I; x \<in> I \<rightarrow> Un_carrier I B; \<forall>i\<in>I. x i \<in> carrier (B i); xa \<in> I\<rbrakk> \<Longrightarrow> \<exists>xb. (\<exists>i\<in>I. xb = carrier (B i)) \<and> x xa \<in> xb
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prodag_sameTr2:"\<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k\<rbrakk>
                               \<Longrightarrow> prod_pOp I A = prod_pOp I B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k\<rbrakk> \<Longrightarrow> prod_pOp I A = prod_pOp I B
[PROOF STEP]
apply (frule prodag_sameTr1 [of "I" "A" "B"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B\<rbrakk> \<Longrightarrow> prod_pOp I A = prod_pOp I B
[PROOF STEP]
apply (simp add:prod_pOp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B\<rbrakk> \<Longrightarrow> (\<lambda>f\<in>carr_prodag I B. \<lambda>g\<in>carr_prodag I B. \<lambda>x\<in>I. f x \<plusminus>\<^bsub>A x\<^esub> g x) = (\<lambda>f\<in>carr_prodag I B. \<lambda>g\<in>carr_prodag I B. \<lambda>x\<in>I. f x \<plusminus>\<^bsub>B x\<^esub> g x)
[PROOF STEP]
apply (rule bivar_func_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B\<rbrakk> \<Longrightarrow> \<forall>a\<in>carr_prodag I B. \<forall>b\<in>carr_prodag I B. (\<lambda>x\<in>I. a x \<plusminus>\<^bsub>A x\<^esub> b x) = (\<lambda>x\<in>I. a x \<plusminus>\<^bsub>B x\<^esub> b x)
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B; a \<in> carr_prodag I B; b \<in> carr_prodag I B\<rbrakk> \<Longrightarrow> (\<lambda>x\<in>I. a x \<plusminus>\<^bsub>A x\<^esub> b x) = (\<lambda>x\<in>I. a x \<plusminus>\<^bsub>B x\<^esub> b x)
[PROOF STEP]
apply (rule funcset_eq [of _ "I"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B; a \<in> carr_prodag I B; b \<in> carr_prodag I B\<rbrakk> \<Longrightarrow> (\<lambda>x\<in>I. a x \<plusminus>\<^bsub>A x\<^esub> b x) \<in> extensional I
 2. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B; a \<in> carr_prodag I B; b \<in> carr_prodag I B\<rbrakk> \<Longrightarrow> (\<lambda>x\<in>I. a x \<plusminus>\<^bsub>B x\<^esub> b x) \<in> extensional I
 3. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B; a \<in> carr_prodag I B; b \<in> carr_prodag I B\<rbrakk> \<Longrightarrow> \<forall>x\<in>I. (\<lambda>x\<in>I. a x \<plusminus>\<^bsub>A x\<^esub> b x) x = (\<lambda>x\<in>I. a x \<plusminus>\<^bsub>B x\<^esub> b x) x
[PROOF STEP]
apply (simp add:restrict_def extensional_def)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prodag_sameTr3:"\<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k\<rbrakk>
                               \<Longrightarrow> prod_mOp I A = prod_mOp I B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k\<rbrakk> \<Longrightarrow> prod_mOp I A = prod_mOp I B
[PROOF STEP]
apply (frule prodag_sameTr1 [of "I" "A" "B"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B\<rbrakk> \<Longrightarrow> prod_mOp I A = prod_mOp I B
[PROOF STEP]
apply (simp add:prod_mOp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B\<rbrakk> \<Longrightarrow> (\<lambda>f\<in>carr_prodag I B. \<lambda>x\<in>I. -\<^sub>a\<^bsub>A x\<^esub> f x) = (\<lambda>f\<in>carr_prodag I B. \<lambda>x\<in>I. -\<^sub>a\<^bsub>B x\<^esub> f x)
[PROOF STEP]
apply (rule funcset_eq [of _ "carr_prodag I B"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B\<rbrakk> \<Longrightarrow> (\<lambda>f\<in>carr_prodag I B. \<lambda>x\<in>I. -\<^sub>a\<^bsub>A x\<^esub> f x) \<in> extensional (carr_prodag I B)
 2. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B\<rbrakk> \<Longrightarrow> (\<lambda>f\<in>carr_prodag I B. \<lambda>x\<in>I. -\<^sub>a\<^bsub>B x\<^esub> f x) \<in> extensional (carr_prodag I B)
 3. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B\<rbrakk> \<Longrightarrow> \<forall>x\<in>carr_prodag I B. (\<lambda>f\<in>carr_prodag I B. \<lambda>x\<in>I. -\<^sub>a\<^bsub>A x\<^esub> f x) x = (\<lambda>f\<in>carr_prodag I B. \<lambda>x\<in>I. -\<^sub>a\<^bsub>B x\<^esub> f x) x
[PROOF STEP]
apply (simp add:restrict_def extensional_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B\<rbrakk> \<Longrightarrow> (\<lambda>f\<in>carr_prodag I B. \<lambda>x\<in>I. -\<^sub>a\<^bsub>B x\<^esub> f x) \<in> extensional (carr_prodag I B)
 2. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B\<rbrakk> \<Longrightarrow> \<forall>x\<in>carr_prodag I B. (\<lambda>f\<in>carr_prodag I B. \<lambda>x\<in>I. -\<^sub>a\<^bsub>A x\<^esub> f x) x = (\<lambda>f\<in>carr_prodag I B. \<lambda>x\<in>I. -\<^sub>a\<^bsub>B x\<^esub> f x) x
[PROOF STEP]
apply (simp add:restrict_def extensional_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B\<rbrakk> \<Longrightarrow> \<forall>x\<in>carr_prodag I B. (\<lambda>f\<in>carr_prodag I B. \<lambda>x\<in>I. -\<^sub>a\<^bsub>A x\<^esub> f x) x = (\<lambda>f\<in>carr_prodag I B. \<lambda>x\<in>I. -\<^sub>a\<^bsub>B x\<^esub> f x) x
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B; x \<in> carr_prodag I B\<rbrakk> \<Longrightarrow> (\<lambda>f\<in>carr_prodag I B. \<lambda>x\<in>I. -\<^sub>a\<^bsub>A x\<^esub> f x) x = (\<lambda>f\<in>carr_prodag I B. \<lambda>x\<in>I. -\<^sub>a\<^bsub>B x\<^esub> f x) x
[PROOF STEP]
apply (rename_tac g)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>g. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B; g \<in> carr_prodag I B\<rbrakk> \<Longrightarrow> (\<lambda>f\<in>carr_prodag I B. \<lambda>x\<in>I. -\<^sub>a\<^bsub>A x\<^esub> f x) g = (\<lambda>f\<in>carr_prodag I B. \<lambda>x\<in>I. -\<^sub>a\<^bsub>B x\<^esub> f x) g
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>g. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B; g \<in> carr_prodag I B\<rbrakk> \<Longrightarrow> (\<lambda>x\<in>I. -\<^sub>a\<^bsub>A x\<^esub> g x) = (\<lambda>x\<in>I. -\<^sub>a\<^bsub>B x\<^esub> g x)
[PROOF STEP]
apply (rule funcset_eq [of _ "I"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>g. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B; g \<in> carr_prodag I B\<rbrakk> \<Longrightarrow> (\<lambda>x\<in>I. -\<^sub>a\<^bsub>A x\<^esub> g x) \<in> extensional I
 2. \<And>g. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B; g \<in> carr_prodag I B\<rbrakk> \<Longrightarrow> (\<lambda>x\<in>I. -\<^sub>a\<^bsub>B x\<^esub> g x) \<in> extensional I
 3. \<And>g. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B; g \<in> carr_prodag I B\<rbrakk> \<Longrightarrow> \<forall>x\<in>I. (\<lambda>x\<in>I. -\<^sub>a\<^bsub>A x\<^esub> g x) x = (\<lambda>x\<in>I. -\<^sub>a\<^bsub>B x\<^esub> g x) x
[PROOF STEP]
apply (simp add:restrict_def extensional_def)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prodag_sameTr4:"\<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k\<rbrakk>
                               \<Longrightarrow> prod_zero I A = prod_zero I B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k\<rbrakk> \<Longrightarrow> prod_zero I A = prod_zero I B
[PROOF STEP]
apply (simp add:prod_zero_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k\<rbrakk> \<Longrightarrow> (\<lambda>x\<in>I. \<zero>\<^bsub>A x\<^esub>) = (\<lambda>x\<in>I. \<zero>\<^bsub>B x\<^esub>)
[PROOF STEP]
apply (rule funcset_eq [of _ "I"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k\<rbrakk> \<Longrightarrow> (\<lambda>x\<in>I. \<zero>\<^bsub>A x\<^esub>) \<in> extensional I
 2. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k\<rbrakk> \<Longrightarrow> (\<lambda>x\<in>I. \<zero>\<^bsub>B x\<^esub>) \<in> extensional I
 3. \<lbrakk>\<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. A k = B k\<rbrakk> \<Longrightarrow> \<forall>x\<in>I. (\<lambda>x\<in>I. \<zero>\<^bsub>A x\<^esub>) x = (\<lambda>x\<in>I. \<zero>\<^bsub>B x\<^esub>) x
[PROOF STEP]
apply (simp add:restrict_def extensional_def)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma prodag_same:"\<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k\<rbrakk>
                               \<Longrightarrow> prodag I A = prodag I B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k\<rbrakk> \<Longrightarrow> a\<Pi>\<^bsub>I\<^esub> A = a\<Pi>\<^bsub>I\<^esub> B
[PROOF STEP]
apply (frule prodag_sameTr1, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B\<rbrakk> \<Longrightarrow> a\<Pi>\<^bsub>I\<^esub> A = a\<Pi>\<^bsub>I\<^esub> B
[PROOF STEP]
apply (frule prodag_sameTr2, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B; prod_pOp I A = prod_pOp I B\<rbrakk> \<Longrightarrow> a\<Pi>\<^bsub>I\<^esub> A = a\<Pi>\<^bsub>I\<^esub> B
[PROOF STEP]
apply (frule prodag_sameTr3, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B; prod_pOp I A = prod_pOp I B; prod_mOp I A = prod_mOp I B\<rbrakk> \<Longrightarrow> a\<Pi>\<^bsub>I\<^esub> A = a\<Pi>\<^bsub>I\<^esub> B
[PROOF STEP]
apply (frule prodag_sameTr4, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); \<forall>k\<in>I. A k = B k; carr_prodag I A = carr_prodag I B; prod_pOp I A = prod_pOp I B; prod_mOp I A = prod_mOp I B; prod_zero I A = prod_zero I B\<rbrakk> \<Longrightarrow> a\<Pi>\<^bsub>I\<^esub> A = a\<Pi>\<^bsub>I\<^esub> B
[PROOF STEP]
apply (simp add:prodag_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma project_mem:"\<lbrakk>\<forall>k\<in>I. aGroup (A k); j \<in> I; x \<in> carrier (prodag I A)\<rbrakk> \<Longrightarrow>
                         (PRoject I A j) x  \<in> carrier (A j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); j \<in> I; x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> (\<pi>\<^bsub>I,A,j\<^esub>) x \<in> carrier (A j)
[PROOF STEP]
apply (simp add:PRoject_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); j \<in> I; x \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> (x \<in> carr_prodag I A \<longrightarrow> x j \<in> carrier (A j)) \<and> (x \<notin> carr_prodag I A \<longrightarrow> undefined \<in> carrier (A j))
[PROOF STEP]
apply (simp add:prodag_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); j \<in> I; x \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> x j \<in> carrier (A j)
[PROOF STEP]
apply (simp add:carr_prodag_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma project_aHom:"\<lbrakk>\<forall>k\<in>I. aGroup (A k); j \<in> I\<rbrakk> \<Longrightarrow>
                         PRoject I A j \<in> aHom (prodag I A) (A j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); j \<in> I\<rbrakk> \<Longrightarrow> \<pi>\<^bsub>I,A,j\<^esub> \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (A j)
[PROOF STEP]
apply (simp add:aHom_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); j \<in> I\<rbrakk> \<Longrightarrow> \<pi>\<^bsub>I,A,j\<^esub> \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> carrier (A j) \<and> \<pi>\<^bsub>I,A,j\<^esub> \<in> extensional (carrier (a\<Pi>\<^bsub>I\<^esub> A)) \<and> (\<forall>a\<in>carrier (a\<Pi>\<^bsub>I\<^esub> A). \<forall>b\<in>carrier (a\<Pi>\<^bsub>I\<^esub> A). (\<pi>\<^bsub>I,A,j\<^esub>) (a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> b) = (\<pi>\<^bsub>I,A,j\<^esub>) a \<plusminus>\<^bsub>A j\<^esub> (\<pi>\<^bsub>I,A,j\<^esub>) b)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); j \<in> I\<rbrakk> \<Longrightarrow> \<pi>\<^bsub>I,A,j\<^esub> \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<rightarrow> carrier (A j)
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); j \<in> I\<rbrakk> \<Longrightarrow> \<pi>\<^bsub>I,A,j\<^esub> \<in> extensional (carrier (a\<Pi>\<^bsub>I\<^esub> A)) \<and> (\<forall>a\<in>carrier (a\<Pi>\<^bsub>I\<^esub> A). \<forall>b\<in>carrier (a\<Pi>\<^bsub>I\<^esub> A). (\<pi>\<^bsub>I,A,j\<^esub>) (a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> b) = (\<pi>\<^bsub>I,A,j\<^esub>) a \<plusminus>\<^bsub>A j\<^esub> (\<pi>\<^bsub>I,A,j\<^esub>) b)
[PROOF STEP]
apply (simp add:project_mem)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); j \<in> I\<rbrakk> \<Longrightarrow> \<pi>\<^bsub>I,A,j\<^esub> \<in> extensional (carrier (a\<Pi>\<^bsub>I\<^esub> A)) \<and> (\<forall>a\<in>carrier (a\<Pi>\<^bsub>I\<^esub> A). \<forall>b\<in>carrier (a\<Pi>\<^bsub>I\<^esub> A). (\<pi>\<^bsub>I,A,j\<^esub>) (a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> b) = (\<pi>\<^bsub>I,A,j\<^esub>) a \<plusminus>\<^bsub>A j\<^esub> (\<pi>\<^bsub>I,A,j\<^esub>) b)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); j \<in> I\<rbrakk> \<Longrightarrow> \<pi>\<^bsub>I,A,j\<^esub> \<in> extensional (carrier (a\<Pi>\<^bsub>I\<^esub> A))
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); j \<in> I\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier (a\<Pi>\<^bsub>I\<^esub> A). \<forall>b\<in>carrier (a\<Pi>\<^bsub>I\<^esub> A). (\<pi>\<^bsub>I,A,j\<^esub>) (a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> b) = (\<pi>\<^bsub>I,A,j\<^esub>) a \<plusminus>\<^bsub>A j\<^esub> (\<pi>\<^bsub>I,A,j\<^esub>) b
[PROOF STEP]
apply (simp add:PRoject_def restrict_def extensional_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); j \<in> I\<rbrakk> \<Longrightarrow> \<forall>x. x \<in> carr_prodag I A \<longrightarrow> x \<notin> carrier (a\<Pi>\<^bsub>I\<^esub> A) \<longrightarrow> x j = undefined
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); j \<in> I\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier (a\<Pi>\<^bsub>I\<^esub> A). \<forall>b\<in>carrier (a\<Pi>\<^bsub>I\<^esub> A). (\<pi>\<^bsub>I,A,j\<^esub>) (a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> b) = (\<pi>\<^bsub>I,A,j\<^esub>) a \<plusminus>\<^bsub>A j\<^esub> (\<pi>\<^bsub>I,A,j\<^esub>) b
[PROOF STEP]
apply (rule allI, rule impI, simp add:prodag_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); j \<in> I\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier (a\<Pi>\<^bsub>I\<^esub> A). \<forall>b\<in>carrier (a\<Pi>\<^bsub>I\<^esub> A). (\<pi>\<^bsub>I,A,j\<^esub>) (a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> b) = (\<pi>\<^bsub>I,A,j\<^esub>) a \<plusminus>\<^bsub>A j\<^esub> (\<pi>\<^bsub>I,A,j\<^esub>) b
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); j \<in> I; a \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A); b \<in> carrier (a\<Pi>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> (\<pi>\<^bsub>I,A,j\<^esub>) (a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub> b) = (\<pi>\<^bsub>I,A,j\<^esub>) a \<plusminus>\<^bsub>A j\<^esub> (\<pi>\<^bsub>I,A,j\<^esub>) b
[PROOF STEP]
apply (simp add:prodag_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); j \<in> I; a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<pi>\<^bsub>I,A,j\<^esub>) (prod_pOp I A a b) = (\<pi>\<^bsub>I,A,j\<^esub>) a \<plusminus>\<^bsub>A j\<^esub> (\<pi>\<^bsub>I,A,j\<^esub>) b
[PROOF STEP]
apply (simp add:prod_pOp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); j \<in> I; a \<in> carr_prodag I A; b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<pi>\<^bsub>I,A,j\<^esub>) (\<lambda>x\<in>I. a x \<plusminus>\<^bsub>A x\<^esub> b x) = (\<pi>\<^bsub>I,A,j\<^esub>) a \<plusminus>\<^bsub>A j\<^esub> (\<pi>\<^bsub>I,A,j\<^esub>) b
[PROOF STEP]
apply (frule_tac X = a and Y = b in prod_pOp_mem[of I A], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); j \<in> I; a \<in> carr_prodag I A; b \<in> carr_prodag I A; prod_pOp I A a b \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<pi>\<^bsub>I,A,j\<^esub>) (\<lambda>x\<in>I. a x \<plusminus>\<^bsub>A x\<^esub> b x) = (\<pi>\<^bsub>I,A,j\<^esub>) a \<plusminus>\<^bsub>A j\<^esub> (\<pi>\<^bsub>I,A,j\<^esub>) b
[PROOF STEP]
apply (simp add:prod_pOp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>k\<in>I. aGroup (A k); j \<in> I; a \<in> carr_prodag I A; b \<in> carr_prodag I A; (\<lambda>x\<in>I. a x \<plusminus>\<^bsub>A x\<^esub> b x) \<in> carr_prodag I A\<rbrakk> \<Longrightarrow> (\<pi>\<^bsub>I,A,j\<^esub>) (\<lambda>x\<in>I. a x \<plusminus>\<^bsub>A x\<^esub> b x) = (\<pi>\<^bsub>I,A,j\<^esub>) a \<plusminus>\<^bsub>A j\<^esub> (\<pi>\<^bsub>I,A,j\<^esub>) b
[PROOF STEP]
apply (simp add:PRoject_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma project_aHom1:"\<forall>k\<in>I. aGroup (A k) \<Longrightarrow>
                      \<forall>j \<in> I. PRoject I A j \<in> aHom (prodag I A) (A j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<forall>j\<in>I. \<pi>\<^bsub>I,A,j\<^esub> \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (A j)
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<forall>k\<in>I. aGroup (A k); j \<in> I\<rbrakk> \<Longrightarrow> \<pi>\<^bsub>I,A,j\<^esub> \<in> aHom (a\<Pi>\<^bsub>I\<^esub> A) (A j)
[PROOF STEP]
apply (rule project_aHom, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma A_to_prodag_mem:"\<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k);  \<forall>k\<in>I. (S k) \<in>
 aHom A (B k); x \<in> carrier A \<rbrakk> \<Longrightarrow> A_to_prodag A I S B x \<in> carr_prodag I B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); x \<in> carrier A\<rbrakk> \<Longrightarrow> A_to_prodag A I S B x \<in> carr_prodag I B
[PROOF STEP]
apply (simp add:carr_prodag_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); x \<in> carrier A\<rbrakk> \<Longrightarrow> A_to_prodag A I S B x \<in> extensional I \<and> A_to_prodag A I S B x \<in> I \<rightarrow> Un_carrier I B \<and> (\<forall>i\<in>I. A_to_prodag A I S B x i \<in> carrier (B i))
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); x \<in> carrier A\<rbrakk> \<Longrightarrow> A_to_prodag A I S B x \<in> extensional I
 2. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); x \<in> carrier A\<rbrakk> \<Longrightarrow> A_to_prodag A I S B x \<in> I \<rightarrow> Un_carrier I B \<and> (\<forall>i\<in>I. A_to_prodag A I S B x i \<in> carrier (B i))
[PROOF STEP]
apply (simp add:A_to_prodag_def extensional_def restrict_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); x \<in> carrier A\<rbrakk> \<Longrightarrow> A_to_prodag A I S B x \<in> I \<rightarrow> Un_carrier I B \<and> (\<forall>i\<in>I. A_to_prodag A I S B x i \<in> carrier (B i))
[PROOF STEP]
apply (simp add:Pi_def restrict_def A_to_prodag_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); x \<in> carrier A\<rbrakk> \<Longrightarrow> (\<forall>xa. xa \<in> I \<longrightarrow> S xa x \<in> Un_carrier I B) \<and> (\<forall>i\<in>I. S i x \<in> carrier (B i))
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); x \<in> carrier A\<rbrakk> \<Longrightarrow> \<forall>xa. xa \<in> I \<longrightarrow> S xa x \<in> Un_carrier I B
 2. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); x \<in> carrier A\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. S i x \<in> carrier (B i)
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); x \<in> carrier A\<rbrakk> \<Longrightarrow> xa \<in> I \<longrightarrow> S xa x \<in> Un_carrier I B
 2. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); x \<in> carrier A\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. S i x \<in> carrier (B i)
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); x \<in> carrier A; xa \<in> I\<rbrakk> \<Longrightarrow> S xa x \<in> Un_carrier I B
 2. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); x \<in> carrier A\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. S i x \<in> carrier (B i)
[PROOF STEP]
apply (simp add:Un_carrier_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); x \<in> carrier A; xa \<in> I\<rbrakk> \<Longrightarrow> \<exists>xb. (\<exists>i\<in>I. xb = carrier (B i)) \<and> S xa x \<in> xb
 2. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); x \<in> carrier A\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. S i x \<in> carrier (B i)
[PROOF STEP]
apply (rotate_tac 2,
        frule_tac x = xa in bspec, assumption,
        thin_tac "\<forall>k\<in>I. S k \<in> aHom A (B k)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> carrier A; xa \<in> I; aGroup A; \<forall>k\<in>I. aGroup (B k); S xa \<in> aHom A (B xa)\<rbrakk> \<Longrightarrow> \<exists>xb. (\<exists>i\<in>I. xb = carrier (B i)) \<and> S xa x \<in> xb
 2. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); x \<in> carrier A\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. S i x \<in> carrier (B i)
[PROOF STEP]
apply (simp add:aHom_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> carrier A; xa \<in> I; aGroup A; \<forall>k\<in>I. aGroup (B k); S xa \<in> carrier A \<rightarrow> carrier (B xa) \<and> S xa \<in> extensional (carrier A) \<and> (\<forall>a\<in>carrier A. \<forall>b\<in>carrier A. S xa (a \<plusminus>\<^bsub>A\<^esub> b) = S xa a \<plusminus>\<^bsub>B xa\<^esub> S xa b)\<rbrakk> \<Longrightarrow> \<exists>xb. (\<exists>i\<in>I. xb = carrier (B i)) \<and> S xa x \<in> xb
 2. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); x \<in> carrier A\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. S i x \<in> carrier (B i)
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> carrier A; xa \<in> I; aGroup A; \<forall>k\<in>I. aGroup (B k); S xa \<in> carrier A \<rightarrow> carrier (B xa); S xa \<in> extensional (carrier A); \<forall>a\<in>carrier A. \<forall>b\<in>carrier A. S xa (a \<plusminus>\<^bsub>A\<^esub> b) = S xa a \<plusminus>\<^bsub>B xa\<^esub> S xa b\<rbrakk> \<Longrightarrow> \<exists>xb. (\<exists>i\<in>I. xb = carrier (B i)) \<and> S xa x \<in> xb
 2. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); x \<in> carrier A\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. S i x \<in> carrier (B i)
[PROOF STEP]
apply (frule_tac f = "S xa" and A = "carrier A" and B = "carrier (B xa)"
           and x = x in funcset_mem, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> carrier A; xa \<in> I; aGroup A; \<forall>k\<in>I. aGroup (B k); S xa \<in> carrier A \<rightarrow> carrier (B xa); S xa \<in> extensional (carrier A); \<forall>a\<in>carrier A. \<forall>b\<in>carrier A. S xa (a \<plusminus>\<^bsub>A\<^esub> b) = S xa a \<plusminus>\<^bsub>B xa\<^esub> S xa b; S xa x \<in> carrier (B xa)\<rbrakk> \<Longrightarrow> \<exists>xb. (\<exists>i\<in>I. xb = carrier (B i)) \<and> S xa x \<in> xb
 2. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); x \<in> carrier A\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. S i x \<in> carrier (B i)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); x \<in> carrier A\<rbrakk> \<Longrightarrow> \<forall>i\<in>I. S i x \<in> carrier (B i)
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); x \<in> carrier A; i \<in> I\<rbrakk> \<Longrightarrow> S i x \<in> carrier (B i)
[PROOF STEP]
apply (rotate_tac 2,
        frule_tac x = i in bspec, assumption,
        thin_tac "\<forall>k\<in>I. S k \<in> aHom A (B k)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>x \<in> carrier A; i \<in> I; aGroup A; \<forall>k\<in>I. aGroup (B k); S i \<in> aHom A (B i)\<rbrakk> \<Longrightarrow> S i x \<in> carrier (B i)
[PROOF STEP]
apply (simp add:aHom_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>x \<in> carrier A; i \<in> I; aGroup A; \<forall>k\<in>I. aGroup (B k); S i \<in> carrier A \<rightarrow> carrier (B i) \<and> S i \<in> extensional (carrier A) \<and> (\<forall>a\<in>carrier A. \<forall>b\<in>carrier A. S i (a \<plusminus>\<^bsub>A\<^esub> b) = S i a \<plusminus>\<^bsub>B i\<^esub> S i b)\<rbrakk> \<Longrightarrow> S i x \<in> carrier (B i)
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>x \<in> carrier A; i \<in> I; aGroup A; \<forall>k\<in>I. aGroup (B k); S i \<in> carrier A \<rightarrow> carrier (B i); S i \<in> extensional (carrier A); \<forall>a\<in>carrier A. \<forall>b\<in>carrier A. S i (a \<plusminus>\<^bsub>A\<^esub> b) = S i a \<plusminus>\<^bsub>B i\<^esub> S i b\<rbrakk> \<Longrightarrow> S i x \<in> carrier (B i)
[PROOF STEP]
apply (simp add:Pi_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma A_to_prodag_aHom:"\<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. (S k) \<in>
 aHom A (B k) \<rbrakk>  \<Longrightarrow> A_to_prodag A I S B \<in> aHom A (a\<Pi>\<^bsub>I\<^esub> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k)\<rbrakk> \<Longrightarrow> A_to_prodag A I S B \<in> aHom A (a\<Pi>\<^bsub>I\<^esub> B)
[PROOF STEP]
apply (simp add:aHom_def [of "A" "a\<Pi>\<^bsub>I\<^esub> B"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k)\<rbrakk> \<Longrightarrow> A_to_prodag A I S B \<in> carrier A \<rightarrow> carrier (a\<Pi>\<^bsub>I\<^esub> B) \<and> A_to_prodag A I S B \<in> extensional (carrier A) \<and> (\<forall>a\<in>carrier A. \<forall>b\<in>carrier A. A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) = A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k)\<rbrakk> \<Longrightarrow> A_to_prodag A I S B \<in> carrier A \<rightarrow> carrier (a\<Pi>\<^bsub>I\<^esub> B)
 2. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k)\<rbrakk> \<Longrightarrow> A_to_prodag A I S B \<in> extensional (carrier A) \<and> (\<forall>a\<in>carrier A. \<forall>b\<in>carrier A. A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) = A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b)
[PROOF STEP]
apply (simp add:prodag_def A_to_prodag_mem)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k)\<rbrakk> \<Longrightarrow> A_to_prodag A I S B \<in> extensional (carrier A) \<and> (\<forall>a\<in>carrier A. \<forall>b\<in>carrier A. A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) = A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k)\<rbrakk> \<Longrightarrow> A_to_prodag A I S B \<in> extensional (carrier A)
 2. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k)\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier A. \<forall>b\<in>carrier A. A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) = A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b
[PROOF STEP]
apply (simp add:A_to_prodag_def restrict_def extensional_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k)\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier A. \<forall>b\<in>carrier A. A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) = A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); a \<in> carrier A; b \<in> carrier A\<rbrakk> \<Longrightarrow> A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) = A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b
[PROOF STEP]
apply (frule_tac x = a and y = b in aGroup.ag_pOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); a \<in> carrier A; b \<in> carrier A; a \<plusminus>\<^bsub>A\<^esub> b \<in> carrier A\<rbrakk> \<Longrightarrow> A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) = A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b
[PROOF STEP]
apply (frule_tac x = "a \<plusminus>\<^bsub>A\<^esub> b" in A_to_prodag_mem [of "A" "I" "B" "S"],
                                                       assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); a \<in> carrier A; b \<in> carrier A; a \<plusminus>\<^bsub>A\<^esub> b \<in> carrier A; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B\<rbrakk> \<Longrightarrow> A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) = A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b
[PROOF STEP]
apply (frule_tac x = a in A_to_prodag_mem [of "A" "I" "B" "S"],
                                                       assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); a \<in> carrier A; b \<in> carrier A; a \<plusminus>\<^bsub>A\<^esub> b \<in> carrier A; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B; A_to_prodag A I S B a \<in> carr_prodag I B\<rbrakk> \<Longrightarrow> A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) = A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b
[PROOF STEP]
apply (frule_tac x = b in A_to_prodag_mem [of "A" "I" "B" "S"],
                                                       assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); a \<in> carrier A; b \<in> carrier A; a \<plusminus>\<^bsub>A\<^esub> b \<in> carrier A; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B; A_to_prodag A I S B a \<in> carr_prodag I B; A_to_prodag A I S B b \<in> carr_prodag I B\<rbrakk> \<Longrightarrow> A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) = A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b
[PROOF STEP]
apply (frule prodag_aGroup [of "I" "B"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); a \<in> carrier A; b \<in> carrier A; a \<plusminus>\<^bsub>A\<^esub> b \<in> carrier A; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B; A_to_prodag A I S B a \<in> carr_prodag I B; A_to_prodag A I S B b \<in> carr_prodag I B; aGroup (a\<Pi>\<^bsub>I\<^esub> B)\<rbrakk> \<Longrightarrow> A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) = A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b
[PROOF STEP]
apply (frule_tac x = a in A_to_prodag_mem[of "A" "I" "B" "S"], assumption+,
        frule_tac x = b in A_to_prodag_mem[of "A" "I" "B" "S"], assumption+,
        frule_tac x = "a \<plusminus>\<^bsub>A\<^esub> b" in A_to_prodag_mem[of "A" "I" "B" "S"],
                                                 assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); a \<in> carrier A; b \<in> carrier A; a \<plusminus>\<^bsub>A\<^esub> b \<in> carrier A; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B; A_to_prodag A I S B a \<in> carr_prodag I B; A_to_prodag A I S B b \<in> carr_prodag I B; aGroup (a\<Pi>\<^bsub>I\<^esub> B); A_to_prodag A I S B a \<in> carr_prodag I B; A_to_prodag A I S B b \<in> carr_prodag I B; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B\<rbrakk> \<Longrightarrow> A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) = A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b
[PROOF STEP]
apply (frule prodag_aGroup[of "I" "B"],
        frule_tac x = "A_to_prodag A I S B a" and
 y = "A_to_prodag A I S B b" in aGroup.ag_pOp_closed [of "a\<Pi>\<^bsub>I\<^esub> B"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); a \<in> carrier A; b \<in> carrier A; a \<plusminus>\<^bsub>A\<^esub> b \<in> carrier A; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B; A_to_prodag A I S B a \<in> carr_prodag I B; A_to_prodag A I S B b \<in> carr_prodag I B; aGroup (a\<Pi>\<^bsub>I\<^esub> B); A_to_prodag A I S B a \<in> carr_prodag I B; A_to_prodag A I S B b \<in> carr_prodag I B; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B; aGroup (a\<Pi>\<^bsub>I\<^esub> B)\<rbrakk> \<Longrightarrow> A_to_prodag A I S B a \<in> carrier (a\<Pi>\<^bsub>I\<^esub> B)
 2. \<And>a b. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); a \<in> carrier A; b \<in> carrier A; a \<plusminus>\<^bsub>A\<^esub> b \<in> carrier A; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B; A_to_prodag A I S B a \<in> carr_prodag I B; A_to_prodag A I S B b \<in> carr_prodag I B; aGroup (a\<Pi>\<^bsub>I\<^esub> B); A_to_prodag A I S B a \<in> carr_prodag I B; A_to_prodag A I S B b \<in> carr_prodag I B; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B; aGroup (a\<Pi>\<^bsub>I\<^esub> B)\<rbrakk> \<Longrightarrow> A_to_prodag A I S B b \<in> carrier (a\<Pi>\<^bsub>I\<^esub> B)
 3. \<And>a b. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); a \<in> carrier A; b \<in> carrier A; a \<plusminus>\<^bsub>A\<^esub> b \<in> carrier A; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B; A_to_prodag A I S B a \<in> carr_prodag I B; A_to_prodag A I S B b \<in> carr_prodag I B; aGroup (a\<Pi>\<^bsub>I\<^esub> B); A_to_prodag A I S B a \<in> carr_prodag I B; A_to_prodag A I S B b \<in> carr_prodag I B; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B; aGroup (a\<Pi>\<^bsub>I\<^esub> B); A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b \<in> carrier (a\<Pi>\<^bsub>I\<^esub> B)\<rbrakk> \<Longrightarrow> A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) = A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b
[PROOF STEP]
apply (simp add:prodag_carrier)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); a \<in> carrier A; b \<in> carrier A; a \<plusminus>\<^bsub>A\<^esub> b \<in> carrier A; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B; A_to_prodag A I S B a \<in> carr_prodag I B; A_to_prodag A I S B b \<in> carr_prodag I B; aGroup (a\<Pi>\<^bsub>I\<^esub> B); A_to_prodag A I S B a \<in> carr_prodag I B; A_to_prodag A I S B b \<in> carr_prodag I B; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B; aGroup (a\<Pi>\<^bsub>I\<^esub> B)\<rbrakk> \<Longrightarrow> A_to_prodag A I S B b \<in> carrier (a\<Pi>\<^bsub>I\<^esub> B)
 2. \<And>a b. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); a \<in> carrier A; b \<in> carrier A; a \<plusminus>\<^bsub>A\<^esub> b \<in> carrier A; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B; A_to_prodag A I S B a \<in> carr_prodag I B; A_to_prodag A I S B b \<in> carr_prodag I B; aGroup (a\<Pi>\<^bsub>I\<^esub> B); A_to_prodag A I S B a \<in> carr_prodag I B; A_to_prodag A I S B b \<in> carr_prodag I B; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B; aGroup (a\<Pi>\<^bsub>I\<^esub> B); A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b \<in> carrier (a\<Pi>\<^bsub>I\<^esub> B)\<rbrakk> \<Longrightarrow> A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) = A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b
[PROOF STEP]
apply (simp add:prodag_carrier)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); a \<in> carrier A; b \<in> carrier A; a \<plusminus>\<^bsub>A\<^esub> b \<in> carrier A; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B; A_to_prodag A I S B a \<in> carr_prodag I B; A_to_prodag A I S B b \<in> carr_prodag I B; aGroup (a\<Pi>\<^bsub>I\<^esub> B); A_to_prodag A I S B a \<in> carr_prodag I B; A_to_prodag A I S B b \<in> carr_prodag I B; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B; aGroup (a\<Pi>\<^bsub>I\<^esub> B); A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b \<in> carrier (a\<Pi>\<^bsub>I\<^esub> B)\<rbrakk> \<Longrightarrow> A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) = A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b
[PROOF STEP]
apply (rule carr_prodag_mem_eq, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); a \<in> carrier A; b \<in> carrier A; a \<plusminus>\<^bsub>A\<^esub> b \<in> carrier A; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B; A_to_prodag A I S B a \<in> carr_prodag I B; A_to_prodag A I S B b \<in> carr_prodag I B; aGroup (a\<Pi>\<^bsub>I\<^esub> B); A_to_prodag A I S B a \<in> carr_prodag I B; A_to_prodag A I S B b \<in> carr_prodag I B; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B; aGroup (a\<Pi>\<^bsub>I\<^esub> B); A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b \<in> carrier (a\<Pi>\<^bsub>I\<^esub> B)\<rbrakk> \<Longrightarrow> A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b \<in> carr_prodag I B
 2. \<And>a b. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); a \<in> carrier A; b \<in> carrier A; a \<plusminus>\<^bsub>A\<^esub> b \<in> carrier A; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B; A_to_prodag A I S B a \<in> carr_prodag I B; A_to_prodag A I S B b \<in> carr_prodag I B; aGroup (a\<Pi>\<^bsub>I\<^esub> B); A_to_prodag A I S B a \<in> carr_prodag I B; A_to_prodag A I S B b \<in> carr_prodag I B; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B; aGroup (a\<Pi>\<^bsub>I\<^esub> B); A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b \<in> carrier (a\<Pi>\<^bsub>I\<^esub> B)\<rbrakk> \<Longrightarrow> \<forall>l\<in>I. A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) l = (A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b) l
[PROOF STEP]
apply (simp add:prodag_carrier)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); a \<in> carrier A; b \<in> carrier A; a \<plusminus>\<^bsub>A\<^esub> b \<in> carrier A; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B; A_to_prodag A I S B a \<in> carr_prodag I B; A_to_prodag A I S B b \<in> carr_prodag I B; aGroup (a\<Pi>\<^bsub>I\<^esub> B); A_to_prodag A I S B a \<in> carr_prodag I B; A_to_prodag A I S B b \<in> carr_prodag I B; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B; aGroup (a\<Pi>\<^bsub>I\<^esub> B); A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b \<in> carrier (a\<Pi>\<^bsub>I\<^esub> B)\<rbrakk> \<Longrightarrow> \<forall>l\<in>I. A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) l = (A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b) l
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b l. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); a \<in> carrier A; b \<in> carrier A; a \<plusminus>\<^bsub>A\<^esub> b \<in> carrier A; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B; A_to_prodag A I S B a \<in> carr_prodag I B; A_to_prodag A I S B b \<in> carr_prodag I B; aGroup (a\<Pi>\<^bsub>I\<^esub> B); A_to_prodag A I S B a \<in> carr_prodag I B; A_to_prodag A I S B b \<in> carr_prodag I B; A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) \<in> carr_prodag I B; aGroup (a\<Pi>\<^bsub>I\<^esub> B); A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b \<in> carrier (a\<Pi>\<^bsub>I\<^esub> B); l \<in> I\<rbrakk> \<Longrightarrow> A_to_prodag A I S B (a \<plusminus>\<^bsub>A\<^esub> b) l = (A_to_prodag A I S B a \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> A_to_prodag A I S B b) l
[PROOF STEP]
apply (simp add:A_to_prodag_def prod_pOp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b l. \<lbrakk>aGroup A; \<forall>k\<in>I. aGroup (B k); \<forall>k\<in>I. S k \<in> aHom A (B k); a \<in> carrier A; b \<in> carrier A; a \<plusminus>\<^bsub>A\<^esub> b \<in> carrier A; (\<lambda>k\<in>I. S k (a \<plusminus>\<^bsub>A\<^esub> b)) \<in> carr_prodag I B; (\<lambda>k\<in>I. S k a) \<in> carr_prodag I B; (\<lambda>k\<in>I. S k b) \<in> carr_prodag I B; aGroup (a\<Pi>\<^bsub>I\<^esub> B); (\<lambda>k\<in>I. S k a) \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> (\<lambda>k\<in>I. S k b) \<in> carrier (a\<Pi>\<^bsub>I\<^esub> B); l \<in> I\<rbrakk> \<Longrightarrow> S l (a \<plusminus>\<^bsub>A\<^esub> b) = ((\<lambda>k\<in>I. S k a) \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> (\<lambda>k\<in>I. S k b)) l
[PROOF STEP]
apply (rotate_tac 2,
        frule_tac x = l in bspec, assumption,
        thin_tac "\<forall>k\<in>I. S k \<in> aHom A (B k)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b l. \<lbrakk>a \<in> carrier A; b \<in> carrier A; a \<plusminus>\<^bsub>A\<^esub> b \<in> carrier A; (\<lambda>k\<in>I. S k (a \<plusminus>\<^bsub>A\<^esub> b)) \<in> carr_prodag I B; (\<lambda>k\<in>I. S k a) \<in> carr_prodag I B; (\<lambda>k\<in>I. S k b) \<in> carr_prodag I B; aGroup (a\<Pi>\<^bsub>I\<^esub> B); (\<lambda>k\<in>I. S k a) \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> (\<lambda>k\<in>I. S k b) \<in> carrier (a\<Pi>\<^bsub>I\<^esub> B); l \<in> I; aGroup A; \<forall>k\<in>I. aGroup (B k); S l \<in> aHom A (B l)\<rbrakk> \<Longrightarrow> S l (a \<plusminus>\<^bsub>A\<^esub> b) = ((\<lambda>k\<in>I. S k a) \<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> B\<^esub> (\<lambda>k\<in>I. S k b)) l
[PROOF STEP]
apply (simp add:prodag_def prod_pOp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b l. \<lbrakk>a \<in> carrier A; b \<in> carrier A; a \<plusminus>\<^bsub>A\<^esub> b \<in> carrier A; (\<lambda>k\<in>I. S k (a \<plusminus>\<^bsub>A\<^esub> b)) \<in> carr_prodag I B; (\<lambda>k\<in>I. S k a) \<in> carr_prodag I B; (\<lambda>k\<in>I. S k b) \<in> carr_prodag I B; aGroup \<lparr>carrier = carr_prodag I B, pop = \<lambda>f\<in>carr_prodag I B. \<lambda>g\<in>carr_prodag I B. \<lambda>x\<in>I. f x \<plusminus>\<^bsub>B x\<^esub> g x, mop = prod_mOp I B, zero = prod_zero I B\<rparr>; (\<lambda>x\<in>I. (if x \<in> I then S x a else undefined) \<plusminus>\<^bsub>B x\<^esub> (if x \<in> I then S x b else undefined)) \<in> carr_prodag I B; l \<in> I; aGroup A; \<forall>k\<in>I. aGroup (B k); S l \<in> aHom A (B l)\<rbrakk> \<Longrightarrow> S l (a \<plusminus>\<^bsub>A\<^esub> b) = S l a \<plusminus>\<^bsub>B l\<^esub> S l b
[PROOF STEP]
apply (frule_tac x = l in bspec, assumption,
        thin_tac "\<forall>k\<in>I. aGroup (B k)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b l. \<lbrakk>a \<in> carrier A; b \<in> carrier A; a \<plusminus>\<^bsub>A\<^esub> b \<in> carrier A; (\<lambda>k\<in>I. S k (a \<plusminus>\<^bsub>A\<^esub> b)) \<in> carr_prodag I B; (\<lambda>k\<in>I. S k a) \<in> carr_prodag I B; (\<lambda>k\<in>I. S k b) \<in> carr_prodag I B; aGroup \<lparr>carrier = carr_prodag I B, pop = \<lambda>f\<in>carr_prodag I B. \<lambda>g\<in>carr_prodag I B. \<lambda>x\<in>I. f x \<plusminus>\<^bsub>B x\<^esub> g x, mop = prod_mOp I B, zero = prod_zero I B\<rparr>; (\<lambda>x\<in>I. (if x \<in> I then S x a else undefined) \<plusminus>\<^bsub>B x\<^esub> (if x \<in> I then S x b else undefined)) \<in> carr_prodag I B; l \<in> I; aGroup A; S l \<in> aHom A (B l); aGroup (B l)\<rbrakk> \<Longrightarrow> S l (a \<plusminus>\<^bsub>A\<^esub> b) = S l a \<plusminus>\<^bsub>B l\<^esub> S l b
[PROOF STEP]
apply (simp add: aHom_add)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma dsum_pOp_func:"\<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"
[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
[PROOF STEP]
apply (rule Pi_I)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_dsumag I A; xa \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> prod_pOp I A x xa \<in> carr_dsumag I A
[PROOF STEP]
apply (subst carr_dsumag_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_dsumag I A; xa \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> prod_pOp I A x xa \<in> Collect (finiteHom I A)
[PROOF STEP]
apply (simp add:CollectI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_dsumag I A; xa \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> finiteHom I A (prod_pOp I A x xa)
[PROOF STEP]
apply (simp add:finiteHom_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_dsumag I A; xa \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> prod_pOp I A x xa \<in> carr_prodag I A \<and> (\<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_pOp I A x xa j = \<zero>\<^bsub>A j\<^esub>))
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_dsumag I A; xa \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> prod_pOp I A x xa \<in> carr_prodag I A
 2. \<And>x xa. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_dsumag I A; xa \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_pOp I A x xa j = \<zero>\<^bsub>A j\<^esub>)
[PROOF STEP]
apply (simp add:carr_dsumag_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>\<forall>k\<in>I. aGroup (A k); finiteHom I A x; finiteHom I A xa\<rbrakk> \<Longrightarrow> prod_pOp I A x xa \<in> carr_prodag I A
 2. \<And>x xa. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_dsumag I A; xa \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_pOp I A x xa j = \<zero>\<^bsub>A j\<^esub>)
[PROOF STEP]
apply (simp add:finiteHom_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_prodag I A \<and> (\<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. x j = \<zero>\<^bsub>A j\<^esub>)); xa \<in> carr_prodag I A \<and> (\<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. xa j = \<zero>\<^bsub>A j\<^esub>))\<rbrakk> \<Longrightarrow> prod_pOp I A x xa \<in> carr_prodag I A
 2. \<And>x xa. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_dsumag I A; xa \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_pOp I A x xa j = \<zero>\<^bsub>A j\<^esub>)
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_prodag I A; \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. x j = \<zero>\<^bsub>A j\<^esub>); xa \<in> carr_prodag I A; \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. xa j = \<zero>\<^bsub>A j\<^esub>)\<rbrakk> \<Longrightarrow> prod_pOp I A x xa \<in> carr_prodag I A
 2. \<And>x xa. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_dsumag I A; xa \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_pOp I A x xa j = \<zero>\<^bsub>A j\<^esub>)
[PROOF STEP]
apply (simp add:prod_pOp_mem)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_dsumag I A; xa \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_pOp I A x xa j = \<zero>\<^bsub>A j\<^esub>)
[PROOF STEP]
apply (simp add:carr_dsumag_def finiteHom_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_prodag I A \<and> (\<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. x j = \<zero>\<^bsub>A j\<^esub>)); xa \<in> carr_prodag I A \<and> (\<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. xa j = \<zero>\<^bsub>A j\<^esub>))\<rbrakk> \<Longrightarrow> \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_pOp I A x xa j = \<zero>\<^bsub>A j\<^esub>)
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_prodag I A; \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. x j = \<zero>\<^bsub>A j\<^esub>); xa \<in> carr_prodag I A; \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. xa j = \<zero>\<^bsub>A j\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_pOp I A x xa j = \<zero>\<^bsub>A j\<^esub>)
[PROOF STEP]
apply ((erule exE)+, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa H Ha. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_prodag I A; xa \<in> carr_prodag I A; H \<subseteq> I; Ha \<subseteq> I; finite H; \<forall>j\<in>I - H. x j = \<zero>\<^bsub>A j\<^esub>; finite Ha; \<forall>j\<in>I - Ha. xa j = \<zero>\<^bsub>A j\<^esub>\<rbrakk> \<Longrightarrow> \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_pOp I A x xa j = \<zero>\<^bsub>A j\<^esub>)
[PROOF STEP]
apply (frule_tac F = H and G = Ha in finite_UnI, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa H Ha. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_prodag I A; xa \<in> carr_prodag I A; H \<subseteq> I; Ha \<subseteq> I; finite H; \<forall>j\<in>I - H. x j = \<zero>\<^bsub>A j\<^esub>; finite Ha; \<forall>j\<in>I - Ha. xa j = \<zero>\<^bsub>A j\<^esub>; finite (H \<union> Ha)\<rbrakk> \<Longrightarrow> \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_pOp I A x xa j = \<zero>\<^bsub>A j\<^esub>)
[PROOF STEP]
apply (subgoal_tac "\<forall>j\<in>I - (H \<union> Ha). prod_pOp I A x xa j = \<zero>\<^bsub>A j\<^esub>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa H Ha. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_prodag I A; xa \<in> carr_prodag I A; H \<subseteq> I; Ha \<subseteq> I; finite H; \<forall>j\<in>I - H. x j = \<zero>\<^bsub>A j\<^esub>; finite Ha; \<forall>j\<in>I - Ha. xa j = \<zero>\<^bsub>A j\<^esub>; finite (H \<union> Ha); \<forall>j\<in>I - (H \<union> Ha). prod_pOp I A x xa j = \<zero>\<^bsub>A j\<^esub>\<rbrakk> \<Longrightarrow> \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_pOp I A x xa j = \<zero>\<^bsub>A j\<^esub>)
 2. \<And>x xa H Ha. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_prodag I A; xa \<in> carr_prodag I A; H \<subseteq> I; Ha \<subseteq> I; finite H; \<forall>j\<in>I - H. x j = \<zero>\<^bsub>A j\<^esub>; finite Ha; \<forall>j\<in>I - Ha. xa j = \<zero>\<^bsub>A j\<^esub>; finite (H \<union> Ha)\<rbrakk> \<Longrightarrow> \<forall>j\<in>I - (H \<union> Ha). prod_pOp I A x xa j = \<zero>\<^bsub>A j\<^esub>
[PROOF STEP]
apply (frule_tac A = H and B = Ha in Un_least[of _ "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa H Ha. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_prodag I A; xa \<in> carr_prodag I A; H \<subseteq> I; Ha \<subseteq> I; finite H; \<forall>j\<in>I - H. x j = \<zero>\<^bsub>A j\<^esub>; finite Ha; \<forall>j\<in>I - Ha. xa j = \<zero>\<^bsub>A j\<^esub>; finite (H \<union> Ha); \<forall>j\<in>I - (H \<union> Ha). prod_pOp I A x xa j = \<zero>\<^bsub>A j\<^esub>; H \<union> Ha \<subseteq> I\<rbrakk> \<Longrightarrow> \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_pOp I A x xa j = \<zero>\<^bsub>A j\<^esub>)
 2. \<And>x xa H Ha. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_prodag I A; xa \<in> carr_prodag I A; H \<subseteq> I; Ha \<subseteq> I; finite H; \<forall>j\<in>I - H. x j = \<zero>\<^bsub>A j\<^esub>; finite Ha; \<forall>j\<in>I - Ha. xa j = \<zero>\<^bsub>A j\<^esub>; finite (H \<union> Ha)\<rbrakk> \<Longrightarrow> \<forall>j\<in>I - (H \<union> Ha). prod_pOp I A x xa j = \<zero>\<^bsub>A j\<^esub>
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa H Ha. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_prodag I A; xa \<in> carr_prodag I A; H \<subseteq> I; Ha \<subseteq> I; finite H; \<forall>j\<in>I - H. x j = \<zero>\<^bsub>A j\<^esub>; finite Ha; \<forall>j\<in>I - Ha. xa j = \<zero>\<^bsub>A j\<^esub>; finite (H \<union> Ha)\<rbrakk> \<Longrightarrow> \<forall>j\<in>I - (H \<union> Ha). prod_pOp I A x xa j = \<zero>\<^bsub>A j\<^esub>
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa H Ha j. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_prodag I A; xa \<in> carr_prodag I A; H \<subseteq> I; Ha \<subseteq> I; finite H; \<forall>j\<in>I - H. x j = \<zero>\<^bsub>A j\<^esub>; finite Ha; \<forall>j\<in>I - Ha. xa j = \<zero>\<^bsub>A j\<^esub>; finite (H \<union> Ha); j \<in> I - (H \<union> Ha)\<rbrakk> \<Longrightarrow> prod_pOp I A x xa j = \<zero>\<^bsub>A j\<^esub>
[PROOF STEP]
apply (simp, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa H Ha j. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_prodag I A; xa \<in> carr_prodag I A; H \<subseteq> I; Ha \<subseteq> I; finite H; \<forall>j\<in>I - H. x j = \<zero>\<^bsub>A j\<^esub>; finite Ha; \<forall>j\<in>I - Ha. xa j = \<zero>\<^bsub>A j\<^esub>; j \<in> I; j \<notin> H; j \<notin> Ha\<rbrakk> \<Longrightarrow> prod_pOp I A x xa j = \<zero>\<^bsub>A j\<^esub>
[PROOF STEP]
apply (frule_tac x = j in bspec, assumption,
         thin_tac "\<forall>k\<in>I. aGroup (A k)",
        frule_tac x = j in bspec, simp,
         thin_tac "\<forall>j\<in>I - H. x j = \<zero>\<^bsub>A j\<^esub>",
        frule_tac x = j in bspec, simp,
         thin_tac "\<forall>j\<in>I - Ha. xa j = \<zero>\<^bsub>A j\<^esub>")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa H Ha j. \<lbrakk>x \<in> carr_prodag I A; xa \<in> carr_prodag I A; H \<subseteq> I; Ha \<subseteq> I; finite H; finite Ha; j \<in> I; j \<notin> H; j \<notin> Ha; aGroup (A j); x j = \<zero>\<^bsub>A j\<^esub>; xa j = \<zero>\<^bsub>A j\<^esub>\<rbrakk> \<Longrightarrow> prod_pOp I A x xa j = \<zero>\<^bsub>A j\<^esub>
[PROOF STEP]
apply (simp add:prod_pOp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa H Ha j. \<lbrakk>x \<in> carr_prodag I A; xa \<in> carr_prodag I A; H \<subseteq> I; Ha \<subseteq> I; finite H; finite Ha; j \<in> I; j \<notin> H; j \<notin> Ha; aGroup (A j); x j = \<zero>\<^bsub>A j\<^esub>; xa j = \<zero>\<^bsub>A j\<^esub>\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>A j\<^esub> \<plusminus>\<^bsub>A j\<^esub> \<zero>\<^bsub>A j\<^esub> = \<zero>\<^bsub>A j\<^esub>
[PROOF STEP]
apply (rule aGroup.ag_l_zero)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa H Ha j. \<lbrakk>x \<in> carr_prodag I A; xa \<in> carr_prodag I A; H \<subseteq> I; Ha \<subseteq> I; finite H; finite Ha; j \<in> I; j \<notin> H; j \<notin> Ha; aGroup (A j); x j = \<zero>\<^bsub>A j\<^esub>; xa j = \<zero>\<^bsub>A j\<^esub>\<rbrakk> \<Longrightarrow> aGroup (A j)
 2. \<And>x xa H Ha j. \<lbrakk>x \<in> carr_prodag I A; xa \<in> carr_prodag I A; H \<subseteq> I; Ha \<subseteq> I; finite H; finite Ha; j \<in> I; j \<notin> H; j \<notin> Ha; aGroup (A j); x j = \<zero>\<^bsub>A j\<^esub>; xa j = \<zero>\<^bsub>A j\<^esub>\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>A j\<^esub> \<in> carrier (A j)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa H Ha j. \<lbrakk>x \<in> carr_prodag I A; xa \<in> carr_prodag I A; H \<subseteq> I; Ha \<subseteq> I; finite H; finite Ha; j \<in> I; j \<notin> H; j \<notin> Ha; aGroup (A j); x j = \<zero>\<^bsub>A j\<^esub>; xa j = \<zero>\<^bsub>A j\<^esub>\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>A j\<^esub> \<in> carrier (A j)
[PROOF STEP]
apply (rule aGroup.ex_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa H Ha j. \<lbrakk>x \<in> carr_prodag I A; xa \<in> carr_prodag I A; H \<subseteq> I; Ha \<subseteq> I; finite H; finite Ha; j \<in> I; j \<notin> H; j \<notin> Ha; aGroup (A j); x j = \<zero>\<^bsub>A j\<^esub>; xa j = \<zero>\<^bsub>A j\<^esub>\<rbrakk> \<Longrightarrow> aGroup (A j)
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


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


[STATEMENT]
lemma dsum_iOp_func:"\<forall>k\<in>I. aGroup (A k) \<Longrightarrow>
                  prod_mOp I A \<in> carr_dsumag I A \<rightarrow> carr_dsumag I A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> prod_mOp I A \<in> carr_dsumag I A \<rightarrow> carr_dsumag I A
[PROOF STEP]
apply (rule Pi_I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> prod_mOp I A x \<in> carr_dsumag I A
[PROOF STEP]
apply (simp add:carr_dsumag_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); finiteHom I A x\<rbrakk> \<Longrightarrow> finiteHom I A (prod_mOp I A x)
[PROOF STEP]
apply (simp add:finiteHom_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_prodag I A \<and> (\<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. x j = \<zero>\<^bsub>A j\<^esub>))\<rbrakk> \<Longrightarrow> prod_mOp I A x \<in> carr_prodag I A \<and> (\<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_mOp I A x j = \<zero>\<^bsub>A j\<^esub>))
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_prodag I A; \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. x j = \<zero>\<^bsub>A j\<^esub>)\<rbrakk> \<Longrightarrow> prod_mOp I A x \<in> carr_prodag I A \<and> (\<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_mOp I A x j = \<zero>\<^bsub>A j\<^esub>))
[PROOF STEP]
apply (simp add:prod_mOp_mem)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_prodag I A; \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. x j = \<zero>\<^bsub>A j\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_mOp I A x j = \<zero>\<^bsub>A j\<^esub>)
[PROOF STEP]
apply (erule exE, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x H. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_prodag I A; H \<subseteq> I; finite H; \<forall>j\<in>I - H. x j = \<zero>\<^bsub>A j\<^esub>\<rbrakk> \<Longrightarrow> \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_mOp I A x j = \<zero>\<^bsub>A j\<^esub>)
[PROOF STEP]
apply (simp add:prod_mOp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x H. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_prodag I A; H \<subseteq> I; finite H; \<forall>j\<in>I - H. x j = \<zero>\<^bsub>A j\<^esub>\<rbrakk> \<Longrightarrow> \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. -\<^sub>a\<^bsub>A j\<^esub> x j = \<zero>\<^bsub>A j\<^esub>)
[PROOF STEP]
apply (subgoal_tac "\<forall>j\<in>I - H. -\<^sub>a\<^bsub>A j\<^esub> (x j) = \<zero>\<^bsub>A j\<^esub>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x H. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_prodag I A; H \<subseteq> I; finite H; \<forall>j\<in>I - H. x j = \<zero>\<^bsub>A j\<^esub>; \<forall>j\<in>I - H. -\<^sub>a\<^bsub>A j\<^esub> x j = \<zero>\<^bsub>A j\<^esub>\<rbrakk> \<Longrightarrow> \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. -\<^sub>a\<^bsub>A j\<^esub> x j = \<zero>\<^bsub>A j\<^esub>)
 2. \<And>x H. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_prodag I A; H \<subseteq> I; finite H; \<forall>j\<in>I - H. x j = \<zero>\<^bsub>A j\<^esub>\<rbrakk> \<Longrightarrow> \<forall>j\<in>I - H. -\<^sub>a\<^bsub>A j\<^esub> x j = \<zero>\<^bsub>A j\<^esub>
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x H. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_prodag I A; H \<subseteq> I; finite H; \<forall>j\<in>I - H. x j = \<zero>\<^bsub>A j\<^esub>\<rbrakk> \<Longrightarrow> \<forall>j\<in>I - H. -\<^sub>a\<^bsub>A j\<^esub> x j = \<zero>\<^bsub>A j\<^esub>
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x H j. \<lbrakk>\<forall>k\<in>I. aGroup (A k); x \<in> carr_prodag I A; H \<subseteq> I; finite H; \<forall>j\<in>I - H. x j = \<zero>\<^bsub>A j\<^esub>; j \<in> I - H\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>A j\<^esub> x j = \<zero>\<^bsub>A j\<^esub>
[PROOF STEP]
apply (frule_tac x = j in bspec, simp,
        thin_tac "\<forall>k\<in>I. aGroup (A k)",
        frule_tac x = j in bspec, simp,
        thin_tac "\<forall>j\<in>I - H. x j = \<zero>\<^bsub>A j\<^esub>", simp add:aGroup.ag_inv_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


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


[STATEMENT]
lemma dsum_zero_func:"\<forall>k\<in>I. aGroup (A k) \<Longrightarrow>
                           prod_zero I A \<in> carr_dsumag I A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> prod_zero I A \<in> carr_dsumag I A
[PROOF STEP]
apply (simp add:carr_dsumag_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> finiteHom I A (prod_zero I A)
[PROOF STEP]
apply (simp add:finiteHom_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> prod_zero I A \<in> carr_prodag I A \<and> (\<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_zero I A j = \<zero>\<^bsub>A j\<^esub>))
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> prod_zero I A \<in> carr_prodag I A
 2. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_zero I A j = \<zero>\<^bsub>A j\<^esub>)
[PROOF STEP]
apply (simp add:prod_zero_func)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_zero I A j = \<zero>\<^bsub>A j\<^esub>)
[PROOF STEP]
apply (subgoal_tac "{} \<subseteq> I")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); {} \<subseteq> I\<rbrakk> \<Longrightarrow> \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_zero I A j = \<zero>\<^bsub>A j\<^esub>)
 2. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> {} \<subseteq> I
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> {} \<subseteq> I
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); {} \<subseteq> I\<rbrakk> \<Longrightarrow> \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_zero I A j = \<zero>\<^bsub>A j\<^esub>)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); {} \<subseteq> I\<rbrakk> \<Longrightarrow> \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_zero I A j = \<zero>\<^bsub>A j\<^esub>)
[PROOF STEP]
apply (subgoal_tac "finite {}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); {} \<subseteq> I; finite {}\<rbrakk> \<Longrightarrow> \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_zero I A j = \<zero>\<^bsub>A j\<^esub>)
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); {} \<subseteq> I\<rbrakk> \<Longrightarrow> finite {}
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); {} \<subseteq> I\<rbrakk> \<Longrightarrow> finite {}
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); {} \<subseteq> I; finite {}\<rbrakk> \<Longrightarrow> \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_zero I A j = \<zero>\<^bsub>A j\<^esub>)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); {} \<subseteq> I; finite {}\<rbrakk> \<Longrightarrow> \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_zero I A j = \<zero>\<^bsub>A j\<^esub>)
[PROOF STEP]
apply (subgoal_tac "\<forall>j\<in>I - {}. prod_zero I A j = \<zero>\<^bsub>A j\<^esub>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); {} \<subseteq> I; finite {}; \<forall>j\<in>I - {}. prod_zero I A j = \<zero>\<^bsub>A j\<^esub>\<rbrakk> \<Longrightarrow> \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. prod_zero I A j = \<zero>\<^bsub>A j\<^esub>)
 2. \<lbrakk>\<forall>k\<in>I. aGroup (A k); {} \<subseteq> I; finite {}\<rbrakk> \<Longrightarrow> \<forall>j\<in>I - {}. prod_zero I A j = \<zero>\<^bsub>A j\<^esub>
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); {} \<subseteq> I; finite {}\<rbrakk> \<Longrightarrow> \<forall>j\<in>I - {}. prod_zero I A j = \<zero>\<^bsub>A j\<^esub>
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<forall>k\<in>I. aGroup (A k); {} \<subseteq> I; finite {}; j \<in> I - {}\<rbrakk> \<Longrightarrow> prod_zero I A j = \<zero>\<^bsub>A j\<^esub>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<forall>k\<in>I. aGroup (A k); j \<in> I\<rbrakk> \<Longrightarrow> prod_zero I A j = \<zero>\<^bsub>A j\<^esub>
[PROOF STEP]
apply (simp add:prod_zero_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma dsumag_sub_prodag:"\<forall>k\<in>I. aGroup (A k) \<Longrightarrow>
                              carr_dsumag I A \<subseteq> carr_prodag I A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> carr_dsumag I A \<subseteq> carr_prodag I A
[PROOF STEP]
by (rule subsetI,
       simp add:carr_dsumag_def finiteHom_def)


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


[STATEMENT]
lemma dsumag_elemfun:"\<lbrakk>\<forall>k\<in>I. aGroup (A k); f \<in> carrier (dsumag I A)\<rbrakk> \<Longrightarrow>
         f \<in> extensional I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); f \<in> carrier (a\<Oplus>\<^bsub>I\<^esub> A)\<rbrakk> \<Longrightarrow> f \<in> extensional I
[PROOF STEP]
apply (simp add:carrier_dsumag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); f \<in> carr_dsumag I A\<rbrakk> \<Longrightarrow> f \<in> extensional I
[PROOF STEP]
apply (simp add:carr_dsumag_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); finiteHom I A f\<rbrakk> \<Longrightarrow> f \<in> extensional I
[PROOF STEP]
apply (simp add:finiteHom_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); f \<in> carr_prodag I A \<and> (\<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. f j = \<zero>\<^bsub>A j\<^esub>))\<rbrakk> \<Longrightarrow> f \<in> extensional I
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>k\<in>I. aGroup (A k); f \<in> carr_prodag I A; \<exists>H\<subseteq>I. finite H \<and> (\<forall>j\<in>I - H. f j = \<zero>\<^bsub>A j\<^esub>)\<rbrakk> \<Longrightarrow> f \<in> extensional I
[PROOF STEP]
apply (simp add:carr_prodag_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done