[STATEMENT]
lemma (in Corps) ApproximationTr2:"\<lbrakk>valuation K v; aa \<in> carrier K; aa \<noteq> \<zero>;
     0 \<le> (v aa)\<rbrakk> \<Longrightarrow> (int N) *\<^sub>a(v aa) \<le> (v (1\<^sub>r \<plusminus> -\<^sub>a ((1\<^sub>r \<plusminus> -\<^sub>a (aa^\<^bsup>K N\<^esup>))^\<^bsup>K N\<^esup>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; aa \<in> carrier K; aa \<noteq> \<zero>; 0 \<le> v aa\<rbrakk> \<Longrightarrow> int N *\<^sub>a v aa \<le> v (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a aa^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)
[PROOF STEP]
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"],
       case_tac "N = 0",
       frule val_nonzero_z[of v "aa"], assumption+, erule exE, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>valuation K v; aa \<in> carrier K; aa \<noteq> \<zero>; 0 \<le> ant z; Ring K; aGroup K; N = 0; v aa = ant z\<rbrakk> \<Longrightarrow> 0 \<le> v (1\<^sub>r \<plusminus> -\<^sub>a 1\<^sub>r)
 2. \<lbrakk>valuation K v; aa \<in> carrier K; aa \<noteq> \<zero>; 0 \<le> v aa; Ring K; aGroup K; N \<noteq> 0\<rbrakk> \<Longrightarrow> int N *\<^sub>a v aa \<le> v (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a aa^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)
[PROOF STEP]
apply(frule Ring.ring_one[of "K"], simp add:aGroup.ag_r_inv1,
       simp add:value_of_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; aa \<in> carrier K; aa \<noteq> \<zero>; 0 \<le> v aa; Ring K; aGroup K; N \<noteq> 0\<rbrakk> \<Longrightarrow> int N *\<^sub>a v aa \<le> v (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a aa^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)
[PROOF STEP]
apply (frule_tac n = N in Ring.npClose[of "K" "aa"], assumption+,
       frule ApproximationTr[of v "-\<^sub>a (aa^\<^bsup>K N\<^esup>)" "N - Suc 0"],
       rule aGroup.ag_mOp_closed, assumption+, simp add:val_minus_eq,
       subst val_exp_ring[THEN sym, of v], assumption+,
       simp add:asprod_pos_pos)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; aa \<in> carrier K; aa \<noteq> \<zero>; 0 \<le> v aa; Ring K; aGroup K; N \<noteq> 0; aa^\<^bsup>K N\<^esup> \<in> carrier K; v (-\<^sub>a aa^\<^bsup>K N\<^esup>) \<le> v (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a aa^\<^bsup>K N\<^esup>)^\<^bsup>K Suc (N - Suc 0)\<^esup>)\<rbrakk> \<Longrightarrow> int N *\<^sub>a v aa \<le> v (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a aa^\<^bsup>K N\<^esup>)^\<^bsup>K N\<^esup>)
[PROOF STEP]
apply (simp add:val_minus_eq, simp add:val_exp_ring[THEN sym])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) eSum_tr:"
( \<forall>j \<le> n. (x j) \<in> carrier K) \<and>
 ( \<forall>j \<le> n. (b j) \<in> carrier K) \<and> l \<le> n \<and>
 ( \<forall>j\<in>({h. h \<le> n} -{l}). (g j = (x j) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (b j)))) \<and>
  g l = (x l) \<cdot>\<^sub>r (-\<^sub>a (b l))
\<longrightarrow> (nsum K (\<lambda>j \<in> {h. h \<le> n}. (x j) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (b j))) n) \<plusminus> (-\<^sub>a (x l)) =
                       nsum K g n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n
[PROOF STEP]
apply (cut_tac field_is_ring, frule Ring.ring_is_ag[of "K"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring K; aGroup K\<rbrakk> \<Longrightarrow> (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring K; aGroup K\<rbrakk> \<Longrightarrow> (\<forall>j\<le>0. x j \<in> carrier K) \<and> (\<forall>j\<le>0. b j \<in> carrier K) \<and> l \<le> 0 \<and> (\<forall>j\<in>{h. h \<le> 0} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> 0}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) 0 \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g 0
 2. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n\<rbrakk> \<Longrightarrow> (\<forall>j\<le>Suc n. x j \<in> carrier K) \<and> (\<forall>j\<le>Suc n. b j \<in> carrier K) \<and> l \<le> Suc n \<and> (\<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) Suc n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g Suc n
[PROOF STEP]
apply (simp, rule impI, (erule conjE)+,
       simp, frule Ring.ring_one[of "K"], subst Ring.ring_distrib1,
       assumption+,
       simp add:aGroup.ag_mOp_closed, simp add:Ring.ring_r_one,
       frule aGroup.ag_mOp_closed[of K "b 0"], assumption+,
       frule Ring.ring_tOp_closed[of "K" "x 0" "-\<^sub>a (b 0)"], assumption+,
       subst aGroup.ag_pOp_commute[of "K" "x 0" _], assumption+,
       subst aGroup.ag_pOp_assoc, assumption+,
       frule aGroup.ag_mOp_closed[of "K"],
       assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring K; aGroup K; x 0 \<in> carrier K; b 0 \<in> carrier K; l = 0; g 0 = x 0 \<cdot>\<^sub>r (-\<^sub>a b 0); 1\<^sub>r \<in> carrier K; -\<^sub>a b 0 \<in> carrier K; x 0 \<cdot>\<^sub>r (-\<^sub>a b 0) \<in> carrier K\<rbrakk> \<Longrightarrow> x 0 \<cdot>\<^sub>r (-\<^sub>a b 0) \<plusminus> (x 0 \<plusminus> -\<^sub>a x 0) = x 0 \<cdot>\<^sub>r (-\<^sub>a b 0)
 2. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n\<rbrakk> \<Longrightarrow> (\<forall>j\<le>Suc n. x j \<in> carrier K) \<and> (\<forall>j\<le>Suc n. b j \<in> carrier K) \<and> l \<le> Suc n \<and> (\<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) Suc n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g Suc n
[PROOF STEP]
apply (simp add:aGroup.ag_r_inv1, subst aGroup.ag_r_zero, assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n\<rbrakk> \<Longrightarrow> (\<forall>j\<le>Suc n. x j \<in> carrier K) \<and> (\<forall>j\<le>Suc n. b j \<in> carrier K) \<and> l \<le> Suc n \<and> (\<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) Suc n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g Suc n
[PROOF STEP]
apply (rule impI, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) Suc n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g Suc n
[PROOF STEP]
apply (subgoal_tac "\<forall>j \<le> (Suc n).  ((x j) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (b j))) \<in> carrier K")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) Suc n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g Suc n
 2. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l)\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K
[PROOF STEP]
apply (case_tac "l = Suc n", simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<in>{h. h \<le> Suc n} - {Suc n}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>a. if a \<le> Suc n then x a \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b a) else undefined) n \<plusminus> x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n)) \<plusminus> -\<^sub>a x (Suc n) = \<Sigma>\<^sub>e K g n \<plusminus> x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n))
 2. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) Suc n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g Suc n
 3. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l)\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K
[PROOF STEP]
apply (subgoal_tac "\<Sigma>\<^sub>e K g n \<in> carrier K",
        subgoal_tac "{h. h \<le> (Suc n)} - {Suc n} = {h. h \<le> n}", simp,
        subgoal_tac "\<forall>j. j \<le> n \<longrightarrow> j \<le> (Suc n)",
        frule_tac f = "\<lambda>u. if u \<le> Suc n then (x u) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (b u)) else
        undefined" and n = n in aGroup.nsum_eq[of "K" _ _ "g"])
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}; \<forall>j\<le>n. j \<le> Suc n\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (if j \<le> Suc n then x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) else undefined) \<in> carrier K
 2. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}; \<forall>j\<le>n. j \<le> Suc n\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. g j \<in> carrier K
 3. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}; \<forall>j\<le>n. j \<le> Suc n\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (if j \<le> Suc n then x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) else undefined) = g j
 4. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}; \<forall>j\<le>n. j \<le> Suc n; \<Sigma>\<^sub>e K (\<lambda>u. if u \<le> Suc n then x u \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b u) else undefined) n = \<Sigma>\<^sub>e K g n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>a. if a \<le> Suc n then x a \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b a) else undefined) n \<plusminus> x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n)) \<plusminus> -\<^sub>a x (Suc n) = \<Sigma>\<^sub>e K g n \<plusminus> x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n))
 5. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. j \<le> Suc n
 6. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<in>{h. h \<le> Suc n} - {Suc n}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K\<rbrakk> \<Longrightarrow> {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}
 7. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<in>{h. h \<le> Suc n} - {Suc n}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K g n \<in> carrier K
 8. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) Suc n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g Suc n
 9. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l)\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K
[PROOF STEP]
apply (rule allI, rule impI, simp,
        rule allI, simp, rule allI, rule impI, simp, simp)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}; \<Sigma>\<^sub>e K (\<lambda>u. if u \<le> Suc n then x u \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b u) else undefined) n = \<Sigma>\<^sub>e K g n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K g n \<plusminus> x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n)) \<plusminus> -\<^sub>a x (Suc n) = \<Sigma>\<^sub>e K g n \<plusminus> x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n))
 2. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. j \<le> Suc n
 3. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<in>{h. h \<le> Suc n} - {Suc n}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K\<rbrakk> \<Longrightarrow> {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}
 4. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<in>{h. h \<le> Suc n} - {Suc n}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K g n \<in> carrier K
 5. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) Suc n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g Suc n
 6. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l)\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K
[PROOF STEP]
apply (cut_tac a = "x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (b (Suc n))) \<plusminus> -\<^sub>a (x (Suc n))" and
       b = "x (Suc n) \<cdot>\<^sub>r (-\<^sub>a (b (Suc n)))" and
       c = "\<Sigma>\<^sub>e K g n" in aGroup.ag_pOp_add_l[of K], assumption)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}; \<Sigma>\<^sub>e K (\<lambda>u. if u \<le> Suc n then x u \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b u) else undefined) n = \<Sigma>\<^sub>e K g n\<rbrakk> \<Longrightarrow> x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n)) \<plusminus> -\<^sub>a x (Suc n) \<in> carrier K
 2. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}; \<Sigma>\<^sub>e K (\<lambda>u. if u \<le> Suc n then x u \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b u) else undefined) n = \<Sigma>\<^sub>e K g n\<rbrakk> \<Longrightarrow> x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)) \<in> carrier K
 3. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}; \<Sigma>\<^sub>e K (\<lambda>u. if u \<le> Suc n then x u \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b u) else undefined) n = \<Sigma>\<^sub>e K g n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K g n \<in> carrier K
 4. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}; \<Sigma>\<^sub>e K (\<lambda>u. if u \<le> Suc n then x u \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b u) else undefined) n = \<Sigma>\<^sub>e K g n\<rbrakk> \<Longrightarrow> x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n)) \<plusminus> -\<^sub>a x (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n))
 5. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}; \<Sigma>\<^sub>e K (\<lambda>u. if u \<le> Suc n then x u \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b u) else undefined) n = \<Sigma>\<^sub>e K g n; \<Sigma>\<^sub>e K g n \<plusminus> (x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n)) \<plusminus> -\<^sub>a x (Suc n)) = \<Sigma>\<^sub>e K g n \<plusminus> x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n))\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K g n \<plusminus> x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n)) \<plusminus> -\<^sub>a x (Suc n) = \<Sigma>\<^sub>e K g n \<plusminus> x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n))
 6. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. j \<le> Suc n
 7. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<in>{h. h \<le> Suc n} - {Suc n}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K\<rbrakk> \<Longrightarrow> {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}
 8. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<in>{h. h \<le> Suc n} - {Suc n}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K g n \<in> carrier K
 9. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) Suc n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g Suc n
 10. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l)\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K
[PROOF STEP]
apply (rule aGroup.ag_pOp_closed, assumption+,
        rule Ring.ring_tOp_closed, assumption+, simp,
        rule aGroup.ag_pOp_closed, assumption+, simp add:Ring.ring_one,
        rule aGroup.ag_mOp_closed, assumption, simp,
        rule aGroup.ag_mOp_closed, assumption, simp,
        rule Ring.ring_tOp_closed, assumption+, simp,
        rule aGroup.ag_mOp_closed, assumption+, simp, assumption)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}; \<Sigma>\<^sub>e K (\<lambda>u. if u \<le> Suc n then x u \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b u) else undefined) n = \<Sigma>\<^sub>e K g n\<rbrakk> \<Longrightarrow> x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n)) \<plusminus> -\<^sub>a x (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n))
 2. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}; \<Sigma>\<^sub>e K (\<lambda>u. if u \<le> Suc n then x u \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b u) else undefined) n = \<Sigma>\<^sub>e K g n; \<Sigma>\<^sub>e K g n \<plusminus> (x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n)) \<plusminus> -\<^sub>a x (Suc n)) = \<Sigma>\<^sub>e K g n \<plusminus> x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n))\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K g n \<plusminus> x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n)) \<plusminus> -\<^sub>a x (Suc n) = \<Sigma>\<^sub>e K g n \<plusminus> x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n))
 3. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. j \<le> Suc n
 4. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<in>{h. h \<le> Suc n} - {Suc n}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K\<rbrakk> \<Longrightarrow> {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}
 5. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<in>{h. h \<le> Suc n} - {Suc n}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K g n \<in> carrier K
 6. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) Suc n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g Suc n
 7. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l)\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K
[PROOF STEP]
apply (subst Ring.ring_distrib1, assumption+, simp, simp add:Ring.ring_one,
        simp add:aGroup.ag_mOp_closed,
        simp add:Ring.ring_r_one)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}; \<Sigma>\<^sub>e K (\<lambda>u. if u \<le> Suc n then x u \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b u) else undefined) n = \<Sigma>\<^sub>e K g n\<rbrakk> \<Longrightarrow> x (Suc n) \<plusminus> x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)) \<plusminus> -\<^sub>a x (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n))
 2. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}; \<Sigma>\<^sub>e K (\<lambda>u. if u \<le> Suc n then x u \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b u) else undefined) n = \<Sigma>\<^sub>e K g n; \<Sigma>\<^sub>e K g n \<plusminus> (x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n)) \<plusminus> -\<^sub>a x (Suc n)) = \<Sigma>\<^sub>e K g n \<plusminus> x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n))\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K g n \<plusminus> x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n)) \<plusminus> -\<^sub>a x (Suc n) = \<Sigma>\<^sub>e K g n \<plusminus> x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n))
 3. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. j \<le> Suc n
 4. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<in>{h. h \<le> Suc n} - {Suc n}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K\<rbrakk> \<Longrightarrow> {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}
 5. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<in>{h. h \<le> Suc n} - {Suc n}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K g n \<in> carrier K
 6. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) Suc n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g Suc n
 7. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l)\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K
[PROOF STEP]
apply (
        frule_tac x = "x (Suc n)" and y = "x (Suc n) \<cdot>\<^sub>r (-\<^sub>a (b (Suc n)))" in
        aGroup.ag_pOp_commute [of "K"], simp,
        simp add:Ring.ring_tOp_closed aGroup.ag_mOp_closed,
        simp)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}; \<Sigma>\<^sub>e K (\<lambda>u. if u \<le> Suc n then x u \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b u) else undefined) n = \<Sigma>\<^sub>e K g n; x (Suc n) \<plusminus> x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)) \<plusminus> x (Suc n)\<rbrakk> \<Longrightarrow> x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)) \<plusminus> x (Suc n) \<plusminus> -\<^sub>a x (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n))
 2. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}; \<Sigma>\<^sub>e K (\<lambda>u. if u \<le> Suc n then x u \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b u) else undefined) n = \<Sigma>\<^sub>e K g n; \<Sigma>\<^sub>e K g n \<plusminus> (x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n)) \<plusminus> -\<^sub>a x (Suc n)) = \<Sigma>\<^sub>e K g n \<plusminus> x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n))\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K g n \<plusminus> x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n)) \<plusminus> -\<^sub>a x (Suc n) = \<Sigma>\<^sub>e K g n \<plusminus> x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n))
 3. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. j \<le> Suc n
 4. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<in>{h. h \<le> Suc n} - {Suc n}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K\<rbrakk> \<Longrightarrow> {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}
 5. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<in>{h. h \<le> Suc n} - {Suc n}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K g n \<in> carrier K
 6. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) Suc n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g Suc n
 7. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l)\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K
[PROOF STEP]
apply (
        subst aGroup.ag_pOp_assoc[of "K"], assumption+,
        rule Ring.ring_tOp_closed, assumption+, simp,
        (simp add:aGroup.ag_mOp_closed)+,
        subst aGroup.ag_r_inv1, assumption+, simp,
        subst aGroup.ag_r_zero, assumption+,
        simp add:Ring.ring_tOp_closed aGroup.ag_mOp_closed, simp,
        rotate_tac -1, drule sym, simp)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}; \<Sigma>\<^sub>e K (\<lambda>u. if u \<le> Suc n then x u \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b u) else undefined) n = \<Sigma>\<^sub>e K g n; \<Sigma>\<^sub>e K g n \<plusminus> x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)) = \<Sigma>\<^sub>e K g n \<plusminus> (x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n)) \<plusminus> -\<^sub>a x (Suc n))\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K g n \<plusminus> x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n)) \<plusminus> -\<^sub>a x (Suc n) = \<Sigma>\<^sub>e K g n \<plusminus> (x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n)) \<plusminus> -\<^sub>a x (Suc n))
 2. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. j \<le> Suc n
 3. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<in>{h. h \<le> Suc n} - {Suc n}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K\<rbrakk> \<Longrightarrow> {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}
 4. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<in>{h. h \<le> Suc n} - {Suc n}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K g n \<in> carrier K
 5. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) Suc n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g Suc n
 6. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l)\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K
[PROOF STEP]
apply (
        thin_tac "\<Sigma>\<^sub>e K g n \<plusminus> x (Suc n) \<cdot>\<^sub>r (-\<^sub>a (b (Suc n))) =
         \<Sigma>\<^sub>e K g n \<plusminus> (x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (b (Suc n))) \<plusminus> -\<^sub>a (x (Suc n)))")
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}; \<Sigma>\<^sub>e K (\<lambda>u. if u \<le> Suc n then x u \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b u) else undefined) n = \<Sigma>\<^sub>e K g n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K g n \<plusminus> x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n)) \<plusminus> -\<^sub>a x (Suc n) = \<Sigma>\<^sub>e K g n \<plusminus> (x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n)) \<plusminus> -\<^sub>a x (Suc n))
 2. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<le>n. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K; {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. j \<le> Suc n
 3. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<in>{h. h \<le> Suc n} - {Suc n}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n; \<Sigma>\<^sub>e K g n \<in> carrier K\<rbrakk> \<Longrightarrow> {h. h \<le> Suc n} - {Suc n} = {h. h \<le> n}
 4. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<in>{h. h \<le> Suc n} - {Suc n}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K g n \<in> carrier K
 5. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) Suc n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g Suc n
 6. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l)\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K
[PROOF STEP]
apply (subst aGroup.ag_pOp_assoc[THEN sym], assumption+,
          rule Ring.ring_tOp_closed, assumption+, simp,
          rule aGroup.ag_pOp_closed, assumption+, simp add:Ring.ring_one,
          rule aGroup.ag_mOp_closed, assumption+, simp,
          rule aGroup.ag_mOp_closed, assumption+, simp, simp,
          simp, rule equalityI, rule subsetI, simp, rule subsetI, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>Ring K; aGroup K; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; \<forall>j\<in>{h. h \<le> Suc n} - {Suc n}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g (Suc n) = x (Suc n) \<cdot>\<^sub>r (-\<^sub>a b (Suc n)); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l = Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K g n \<in> carrier K
 2. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) Suc n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g Suc n
 3. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l)\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K
[PROOF STEP]
apply (rule aGroup.nsum_mem, assumption+,
         rule allI, rule impI, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) Suc n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g Suc n
 2. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l)\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l)\<rbrakk> \<Longrightarrow> \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K
 2. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) Suc n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g Suc n
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n j. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l); j \<le> Suc n\<rbrakk> \<Longrightarrow> x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K
 2. \<And>n. \<lbrakk>Ring K; aGroup K; (\<forall>j\<le>n. x j \<in> carrier K) \<and> (\<forall>j\<le>n. b j \<in> carrier K) \<and> l \<le> n \<and> (\<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) \<and> g l = x l \<cdot>\<^sub>r (-\<^sub>a b l) \<longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> Suc n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) Suc n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g Suc n
[PROOF STEP]
apply (case_tac "j = l", simp,
         rule Ring.ring_tOp_closed, assumption, simp,
         rule aGroup.ag_pOp_closed, assumption+, simp add:Ring.ring_one,
         rule aGroup.ag_mOp_closed, assumption, simp, simp,
         rule Ring.ring_tOp_closed, assumption, simp,
         rule aGroup.ag_pOp_closed, assumption+, simp add:Ring.ring_one,
         rule aGroup.ag_mOp_closed, assumption, simp, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ring K; aGroup K; \<Sigma>\<^sub>e K (\<lambda>a. if a \<le> n then x a \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b a) else undefined) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>a. if a \<le> Suc n then x a \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b a) else undefined) n \<plusminus> x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n)) \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n \<plusminus> x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n))
[PROOF STEP]
(* end defer *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ring K; aGroup K; \<Sigma>\<^sub>e K (\<lambda>a. if a \<le> n then x a \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b a) else undefined) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>a. if a \<le> Suc n then x a \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b a) else undefined) n \<plusminus> x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n)) \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n \<plusminus> x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n))
[PROOF STEP]
apply (subst aGroup.ag_pOp_assoc, assumption+,
        rule aGroup.nsum_mem, assumption+,
        rule allI, simp, rule Ring.ring_tOp_closed, assumption+, simp,
        rule aGroup.ag_pOp_closed, assumption+, simp add:Ring.ring_one,
        rule aGroup.ag_mOp_closed, assumption, simp,
        rule aGroup.ag_mOp_closed, assumption, simp,
        subst aGroup.ag_pOp_commute[of K _ "-\<^sub>a (x l)"], assumption+,
        rule Ring.ring_tOp_closed, assumption, simp,
        rule aGroup.ag_pOp_closed, assumption+, simp add:Ring.ring_one)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>Ring K; aGroup K; \<Sigma>\<^sub>e K (\<lambda>a. if a \<le> n then x a \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b a) else undefined) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l \<noteq> Suc n\<rbrakk> \<Longrightarrow> -\<^sub>a b (Suc n) \<in> carrier K
 2. \<And>n. \<lbrakk>Ring K; aGroup K; \<Sigma>\<^sub>e K (\<lambda>a. if a \<le> n then x a \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b a) else undefined) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l \<noteq> Suc n\<rbrakk> \<Longrightarrow> -\<^sub>a x l \<in> carrier K
 3. \<And>n. \<lbrakk>Ring K; aGroup K; \<Sigma>\<^sub>e K (\<lambda>a. if a \<le> n then x a \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b a) else undefined) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>a. if a \<le> Suc n then x a \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b a) else undefined) n \<plusminus> (-\<^sub>a x l \<plusminus> x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n))) = \<Sigma>\<^sub>e K g n \<plusminus> x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n))
[PROOF STEP]
apply (rule aGroup.ag_mOp_closed, assumption+, simp,
        rule aGroup.ag_mOp_closed, assumption+, simp,
        subst aGroup.ag_pOp_assoc[THEN sym], assumption+,
        rule aGroup.nsum_mem, assumption+,
        rule allI, rule impI, simp,
        rule aGroup.ag_mOp_closed, assumption, simp,
        rule Ring.ring_tOp_closed, assumption, simp,
         rule aGroup.ag_pOp_closed, assumption+, simp add:Ring.ring_one,
         rule aGroup.ag_mOp_closed, assumption, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ring K; aGroup K; \<Sigma>\<^sub>e K (\<lambda>a. if a \<le> n then x a \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b a) else undefined) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>a. if a \<le> Suc n then x a \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b a) else undefined) n \<plusminus> -\<^sub>a x l \<plusminus> x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n)) = \<Sigma>\<^sub>e K g n \<plusminus> x (Suc n) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b (Suc n))
[PROOF STEP]
apply (subgoal_tac "\<Sigma>\<^sub>e K (\<lambda>a. if a \<le> (Suc n) then x a \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (b a))
         else undefined) n \<plusminus> -\<^sub>a (x l) =
         \<Sigma>\<^sub>e K (\<lambda>a. if a \<le> n then x a \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (b a)) else undefined) n \<plusminus>
         -\<^sub>a (x l)", simp,
         rule aGroup.ag_pOp_add_r[of K _ _ "-\<^sub>a (x l)"], assumption+,
         rule aGroup.nsum_mem, assumption+,
         rule allI, rule impI, simp,
         rule aGroup.nsum_mem, assumption+,
         rule allI, rule impI, simp,
         rule aGroup.ag_mOp_closed, assumption, simp,
         rule aGroup.nsum_eq, assumption+,
         rule allI, rule impI, simp, rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n j. \<lbrakk>Ring K; aGroup K; \<Sigma>\<^sub>e K (\<lambda>a. if a \<le> n then x a \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b a) else undefined) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l \<noteq> Suc n; j \<le> n\<rbrakk> \<Longrightarrow> (if j \<le> n then x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) else undefined) \<in> carrier K
 2. \<And>n. \<lbrakk>Ring K; aGroup K; \<Sigma>\<^sub>e K (\<lambda>a. if a \<le> n then x a \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b a) else undefined) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (if j \<le> Suc n then x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) else undefined) = (if j \<le> n then x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) else undefined)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ring K; aGroup K; \<Sigma>\<^sub>e K (\<lambda>a. if a \<le> n then x a \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b a) else undefined) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n; \<forall>j\<le>Suc n. x j \<in> carrier K; \<forall>j\<le>Suc n. b j \<in> carrier K; l \<le> Suc n; \<forall>j\<in>{h. h \<le> Suc n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l); \<forall>j\<le>Suc n. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) \<in> carrier K; l \<noteq> Suc n\<rbrakk> \<Longrightarrow> \<forall>j\<le>n. (if j \<le> Suc n then x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) else undefined) = (if j \<le> n then x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j) else undefined)
[PROOF STEP]
apply (rule allI, rule impI, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) eSum_minus_x:"\<lbrakk>\<forall>j \<le> n. (x j) \<in> carrier K;
       \<forall>j \<le> n. (b j) \<in> carrier K; l \<le> n;
       \<forall>j\<in>({h. h \<le> n} -{l}). (g j = (x j) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (b j)));
       g l = (x l) \<cdot>\<^sub>r (-\<^sub>a (b l)) \<rbrakk> \<Longrightarrow>
       (nsum K (\<lambda>j\<in>{h. h \<le> n}. (x j) \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a (b j))) n) \<plusminus> (-\<^sub>a (x l)) =
                        nsum K g n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<le>n. x j \<in> carrier K; \<forall>j\<le>n. b j \<in> carrier K; l \<le> n; \<forall>j\<in>{h. h \<le> n} - {l}. g j = x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j); g l = x l \<cdot>\<^sub>r (-\<^sub>a b l)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K (\<lambda>j\<in>{h. h \<le> n}. x j \<cdot>\<^sub>r (1\<^sub>r \<plusminus> -\<^sub>a b j)) n \<plusminus> -\<^sub>a x l = \<Sigma>\<^sub>e K g n
[PROOF STEP]
by (cut_tac eSum_tr[of "n" "x" "b" "l" "g"], simp)


[STATEMENT]
lemma (in Ring) one_m_x_times:"x \<in> carrier R \<Longrightarrow>
 (1\<^sub>r \<plusminus> -\<^sub>a x) \<cdot>\<^sub>r (nsum R (\<lambda>j. x^\<^bsup>R j\<^esup>) n) = 1\<^sub>r \<plusminus> -\<^sub>a (x^\<^bsup>R (Suc n)\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier R \<Longrightarrow> (1\<^sub>r \<plusminus> -\<^sub>a x) \<cdot>\<^sub>r \<Sigma>\<^sub>e R NPOW x R n = 1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>R Suc n\<^esup>
[PROOF STEP]
apply (cut_tac ring_one, cut_tac ring_is_ag,
       frule aGroup.ag_mOp_closed[of "R" "x"], assumption+,
       frule aGroup.ag_pOp_closed[of "R" "1\<^sub>r" "-\<^sub>a x"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; 1\<^sub>r \<in> carrier R; aGroup R; -\<^sub>a x \<in> carrier R; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier R\<rbrakk> \<Longrightarrow> (1\<^sub>r \<plusminus> -\<^sub>a x) \<cdot>\<^sub>r \<Sigma>\<^sub>e R NPOW x R n = 1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>R Suc n\<^esup>
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; 1\<^sub>r \<in> carrier R; aGroup R; -\<^sub>a x \<in> carrier R; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier R\<rbrakk> \<Longrightarrow> (1\<^sub>r \<plusminus> -\<^sub>a x) \<cdot>\<^sub>r \<Sigma>\<^sub>e R NPOW x R 0 = 1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>R Suc 0\<^esup>
 2. \<And>n. \<lbrakk>x \<in> carrier R; 1\<^sub>r \<in> carrier R; aGroup R; -\<^sub>a x \<in> carrier R; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier R; (1\<^sub>r \<plusminus> -\<^sub>a x) \<cdot>\<^sub>r \<Sigma>\<^sub>e R NPOW x R n = 1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>R Suc n\<^esup>\<rbrakk> \<Longrightarrow> (1\<^sub>r \<plusminus> -\<^sub>a x) \<cdot>\<^sub>r \<Sigma>\<^sub>e R NPOW x R Suc n = 1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>R Suc (Suc n)\<^esup>
[PROOF STEP]
apply (simp add:ring_r_one ring_l_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; 1\<^sub>r \<in> carrier R; aGroup R; -\<^sub>a x \<in> carrier R; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier R; (1\<^sub>r \<plusminus> -\<^sub>a x) \<cdot>\<^sub>r \<Sigma>\<^sub>e R NPOW x R n = 1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>R Suc n\<^esup>\<rbrakk> \<Longrightarrow> (1\<^sub>r \<plusminus> -\<^sub>a x) \<cdot>\<^sub>r \<Sigma>\<^sub>e R NPOW x R Suc n = 1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>R Suc (Suc n)\<^esup>
[PROOF STEP]
apply (simp del:npow_suc,
        frule_tac n = "Suc n" in npClose[of "x"],
        subst ring_distrib1, assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier R; 1\<^sub>r \<in> carrier R; aGroup R; -\<^sub>a x \<in> carrier R; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier R; (1\<^sub>r \<plusminus> -\<^sub>a x) \<cdot>\<^sub>r \<Sigma>\<^sub>e R NPOW x R n = 1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>R Suc n\<^esup>; x^\<^bsup>R Suc n\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R NPOW x R n \<in> carrier R
 2. \<And>n. \<lbrakk>x \<in> carrier R; 1\<^sub>r \<in> carrier R; aGroup R; -\<^sub>a x \<in> carrier R; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier R; (1\<^sub>r \<plusminus> -\<^sub>a x) \<cdot>\<^sub>r \<Sigma>\<^sub>e R NPOW x R n = 1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>R Suc n\<^esup>; x^\<^bsup>R Suc n\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> x^\<^bsup>R Suc n\<^esup> \<in> carrier R
 3. \<And>n. \<lbrakk>x \<in> carrier R; 1\<^sub>r \<in> carrier R; aGroup R; -\<^sub>a x \<in> carrier R; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier R; (1\<^sub>r \<plusminus> -\<^sub>a x) \<cdot>\<^sub>r \<Sigma>\<^sub>e R NPOW x R n = 1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>R Suc n\<^esup>; x^\<^bsup>R Suc n\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> (1\<^sub>r \<plusminus> -\<^sub>a x) \<cdot>\<^sub>r \<Sigma>\<^sub>e R NPOW x R n \<plusminus> (1\<^sub>r \<plusminus> -\<^sub>a x) \<cdot>\<^sub>r x^\<^bsup>R Suc n\<^esup> = 1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>R Suc (Suc n)\<^esup>
[PROOF STEP]
apply (rule aGroup.nsum_mem, assumption, rule allI, rule impI,
        simp add:npClose, rule npClose, assumption+,
        simp del:npow_suc,
        thin_tac "(1\<^sub>r \<plusminus> -\<^sub>a x) \<cdot>\<^sub>r \<Sigma>\<^sub>e R (npow R x) n = 1\<^sub>r \<plusminus> -\<^sub>a (x^\<^bsup>R (Suc n)\<^esup>)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; 1\<^sub>r \<in> carrier R; aGroup R; -\<^sub>a x \<in> carrier R; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier R; x^\<^bsup>R Suc n\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>R Suc n\<^esup> \<plusminus> (1\<^sub>r \<plusminus> -\<^sub>a x) \<cdot>\<^sub>r x^\<^bsup>R Suc n\<^esup> = 1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>R Suc (Suc n)\<^esup>
[PROOF STEP]
apply (subst ring_distrib2, assumption+,
        simp del:npow_suc add:ring_l_one,
        subst aGroup.pOp_assocTr43[of R], assumption+,
        rule_tac x = "x^\<^bsup>R (Suc n)\<^esup>" in aGroup.ag_mOp_closed[of R], assumption+,
        rule ring_tOp_closed, rule aGroup.ag_mOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; 1\<^sub>r \<in> carrier R; aGroup R; -\<^sub>a x \<in> carrier R; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier R; x^\<^bsup>R Suc n\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> (-\<^sub>a x^\<^bsup>R Suc n\<^esup> \<plusminus> x^\<^bsup>R Suc n\<^esup>) \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r x^\<^bsup>R Suc n\<^esup> = 1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>R Suc (Suc n)\<^esup>
[PROOF STEP]
apply (subst aGroup.ag_l_inv1, assumption+, simp del:npow_suc
        add:aGroup.ag_r_zero,
        frule_tac x = "-\<^sub>a x" and y = "x^\<^bsup>R (Suc n)\<^esup>" in ring_tOp_closed,
        assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; 1\<^sub>r \<in> carrier R; aGroup R; -\<^sub>a x \<in> carrier R; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier R; x^\<^bsup>R Suc n\<^esup> \<in> carrier R; (-\<^sub>a x) \<cdot>\<^sub>r x^\<^bsup>R Suc n\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> 1\<^sub>r \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r x^\<^bsup>R Suc n\<^esup> = 1\<^sub>r \<plusminus> -\<^sub>a x^\<^bsup>R Suc (Suc n)\<^esup>
[PROOF STEP]
apply (rule aGroup.ag_pOp_add_l[of R _ _ "1\<^sub>r"], assumption+,
        rule aGroup.ag_mOp_closed, assumption+,
        rule npClose, assumption+,
        subst ring_inv1_1[THEN sym, of x], assumption,
        rule npClose, assumption,
        simp,
        subst ring_tOp_commute[of x], assumption+, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) x_pow_fSum_in_Vr:"\<lbrakk>valuation K v; x \<in> carrier (Vr K v)\<rbrakk> \<Longrightarrow>
   (nsum K (npow K x) n) \<in> carrier (Vr K v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier (Vr K v)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K NPOW x K n \<in> carrier (Vr K v)
[PROOF STEP]
apply (frule Vr_ring[of v])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier (Vr K v); Ring (Vr K v)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K NPOW x K n \<in> carrier (Vr K v)
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valuation K v; x \<in> carrier (Vr K v); Ring (Vr K v)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K NPOW x K 0 \<in> carrier (Vr K v)
 2. \<And>n. \<lbrakk>valuation K v; x \<in> carrier (Vr K v); Ring (Vr K v); \<Sigma>\<^sub>e K NPOW x K n \<in> carrier (Vr K v)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K NPOW x K Suc n \<in> carrier (Vr K v)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valuation K v; x \<in> carrier (Vr K v); Ring (Vr K v)\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> carrier (Vr K v)
 2. \<And>n. \<lbrakk>valuation K v; x \<in> carrier (Vr K v); Ring (Vr K v); \<Sigma>\<^sub>e K NPOW x K n \<in> carrier (Vr K v)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K NPOW x K Suc n \<in> carrier (Vr K v)
[PROOF STEP]
apply (frule Ring.ring_one[of "Vr K v"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valuation K v; x \<in> carrier (Vr K v); Ring (Vr K v); 1\<^sub>r\<^bsub>Vr K v\<^esub> \<in> carrier (Vr K v)\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> carrier (Vr K v)
 2. \<And>n. \<lbrakk>valuation K v; x \<in> carrier (Vr K v); Ring (Vr K v); \<Sigma>\<^sub>e K NPOW x K n \<in> carrier (Vr K v)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K NPOW x K Suc n \<in> carrier (Vr K v)
[PROOF STEP]
apply (simp add:Vr_1_f_1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>valuation K v; x \<in> carrier (Vr K v); Ring (Vr K v); \<Sigma>\<^sub>e K NPOW x K n \<in> carrier (Vr K v)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K NPOW x K Suc n \<in> carrier (Vr K v)
[PROOF STEP]
apply (simp del:npow_suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>valuation K v; x \<in> carrier (Vr K v); Ring (Vr K v); \<Sigma>\<^sub>e K NPOW x K n \<in> carrier (Vr K v)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K NPOW x K n \<plusminus> x^\<^bsup>K Suc n\<^esup> \<in> carrier (Vr K v)
[PROOF STEP]
apply (frule Ring.ring_is_ag[of "Vr K v"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>valuation K v; x \<in> carrier (Vr K v); Ring (Vr K v); \<Sigma>\<^sub>e K NPOW x K n \<in> carrier (Vr K v); aGroup (Vr K v)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K NPOW x K n \<plusminus> x^\<^bsup>K Suc n\<^esup> \<in> carrier (Vr K v)
[PROOF STEP]
apply (subst Vr_pOp_f_pOp[THEN sym, of v], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>valuation K v; x \<in> carrier (Vr K v); Ring (Vr K v); \<Sigma>\<^sub>e K NPOW x K n \<in> carrier (Vr K v); aGroup (Vr K v)\<rbrakk> \<Longrightarrow> x^\<^bsup>K Suc n\<^esup> \<in> carrier (Vr K v)
 2. \<And>n. \<lbrakk>valuation K v; x \<in> carrier (Vr K v); Ring (Vr K v); \<Sigma>\<^sub>e K NPOW x K n \<in> carrier (Vr K v); aGroup (Vr K v)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K NPOW x K n \<plusminus>\<^bsub>Vr K v\<^esub> x^\<^bsup>K Suc n\<^esup> \<in> carrier (Vr K v)
[PROOF STEP]
apply (subst Vr_exp_f_exp[THEN sym, of v], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>valuation K v; x \<in> carrier (Vr K v); Ring (Vr K v); \<Sigma>\<^sub>e K NPOW x K n \<in> carrier (Vr K v); aGroup (Vr K v)\<rbrakk> \<Longrightarrow> x^\<^bsup>Vr K v Suc n\<^esup> \<in> carrier (Vr K v)
 2. \<And>n. \<lbrakk>valuation K v; x \<in> carrier (Vr K v); Ring (Vr K v); \<Sigma>\<^sub>e K NPOW x K n \<in> carrier (Vr K v); aGroup (Vr K v)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K NPOW x K n \<plusminus>\<^bsub>Vr K v\<^esub> x^\<^bsup>K Suc n\<^esup> \<in> carrier (Vr K v)
[PROOF STEP]
apply (rule Ring.npClose[of "Vr K v"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>valuation K v; x \<in> carrier (Vr K v); Ring (Vr K v); \<Sigma>\<^sub>e K NPOW x K n \<in> carrier (Vr K v); aGroup (Vr K v)\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e K NPOW x K n \<plusminus>\<^bsub>Vr K v\<^esub> x^\<^bsup>K Suc n\<^esup> \<in> carrier (Vr K v)
[PROOF STEP]
apply (rule aGroup.ag_pOp_closed[of "Vr K v"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>valuation K v; x \<in> carrier (Vr K v); Ring (Vr K v); \<Sigma>\<^sub>e K NPOW x K n \<in> carrier (Vr K v); aGroup (Vr K v)\<rbrakk> \<Longrightarrow> x^\<^bsup>K Suc n\<^esup> \<in> carrier (Vr K v)
[PROOF STEP]
apply (subst Vr_exp_f_exp[THEN sym, of v], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>valuation K v; x \<in> carrier (Vr K v); Ring (Vr K v); \<Sigma>\<^sub>e K NPOW x K n \<in> carrier (Vr K v); aGroup (Vr K v)\<rbrakk> \<Longrightarrow> x^\<^bsup>Vr K v Suc n\<^esup> \<in> carrier (Vr K v)
[PROOF STEP]
apply (rule Ring.npClose[of "Vr K v"], assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Corps) val_1mx_pos:"\<lbrakk>valuation K v; x \<in> carrier K;
         0 < (v (1\<^sub>r \<plusminus> -\<^sub>a x))\<rbrakk> \<Longrightarrow>  v x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x)\<rbrakk> \<Longrightarrow> v x = 0
[PROOF STEP]
apply (cut_tac field_is_ring, frule Ring.ring_one[of "K"],
       frule Ring.ring_is_ag[of "K"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; 1\<^sub>r \<in> carrier K; aGroup K\<rbrakk> \<Longrightarrow> v x = 0
[PROOF STEP]
apply (frule aGroup.ag_mOp_closed[of "K" "x"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; 1\<^sub>r \<in> carrier K; aGroup K; -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> v x = 0
[PROOF STEP]
apply (frule aGroup.ag_pOp_closed[of "K" "1\<^sub>r" "-\<^sub>a x"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; 1\<^sub>r \<in> carrier K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K\<rbrakk> \<Longrightarrow> v x = 0
[PROOF STEP]
apply (frule aGroup.ag_mOp_closed[of "K" "1\<^sub>r \<plusminus> -\<^sub>a x"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; 1\<^sub>r \<in> carrier K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K\<rbrakk> \<Longrightarrow> v x = 0
[PROOF STEP]
apply (cut_tac x = x and y = "1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a x)" and f = v in
        eq_elems_eq_val)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; 1\<^sub>r \<in> carrier K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K\<rbrakk> \<Longrightarrow> x = 1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a x)
 2. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; 1\<^sub>r \<in> carrier K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; v x = v (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a x))\<rbrakk> \<Longrightarrow> v x = 0
[PROOF STEP]
apply (subst aGroup.ag_p_inv, assumption+,
       subst aGroup.ag_pOp_assoc[THEN sym], assumption+,
       rule aGroup.ag_mOp_closed, assumption+,
       subst aGroup.ag_inv_inv, assumption+,
       subst aGroup.ag_r_inv1, assumption+,
       subst aGroup.ag_l_zero, assumption+,
       (simp add:aGroup.ag_inv_inv)+,
       frule  value_less_eq[of v  "1\<^sub>r" "-\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a x)"],
        assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; 1\<^sub>r \<in> carrier K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; v x = v (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a x))\<rbrakk> \<Longrightarrow> v 1\<^sub>r < v (-\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a x))
 2. \<lbrakk>valuation K v; x \<in> carrier K; 0 < v (1\<^sub>r \<plusminus> -\<^sub>a x); Ring K; 1\<^sub>r \<in> carrier K; aGroup K; -\<^sub>a x \<in> carrier K; 1\<^sub>r \<plusminus> -\<^sub>a x \<in> carrier K; -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a x) \<in> carrier K; v x = v (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a x)); v 1\<^sub>r = v (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a x))\<rbrakk> \<Longrightarrow> v (1\<^sub>r \<plusminus> -\<^sub>a (1\<^sub>r \<plusminus> -\<^sub>a x)) = 0
[PROOF STEP]
apply (simp add:val_minus_eq value_of_one,
        simp add:value_of_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done