[STATEMENT]
lemma (in Ring) npeSum2:
  "\<And> n. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk>
        \<Longrightarrow> npow R (x \<plusminus> y) n =
                nsum R (\<lambda> i. nscal R ((npow R x (n-i)) \<cdot>\<^sub>r (npow R y i))
                                       ( n choose i) ) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R n\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R n\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) n
[PROOF STEP]
apply (induct_tac "n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R 0\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (0 choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (0 - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) 0
 2. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R Suc na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (Suc na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) Suc na
[PROOF STEP]
(*1*)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R 0\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (0 choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (0 - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) 0
 2. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R Suc na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (Suc na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) Suc na
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow> 1\<^sub>r = \<zero> \<plusminus> 1\<^sub>r \<cdot>\<^sub>r 1\<^sub>r
 2. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R Suc na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (Suc na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) Suc na
[PROOF STEP]
apply (cut_tac ring_one, simp add:ring_r_one, simp add:aGroup.ag_l_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R Suc na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (Suc na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) Suc na
[PROOF STEP]
(*1:done*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R Suc na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (Suc na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) Suc na
[PROOF STEP]
apply (subst aGroup.nsumElmTail, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<forall>i.  (Suc na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>) \<in> carrier R
 2. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R Suc na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (Suc na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus>  (Suc na choose 0) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - 0)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>)
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n na i. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow>  (Suc na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>) \<in> carrier R
 2. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R Suc na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (Suc na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus>  (Suc na choose 0) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - 0)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>)
[PROOF STEP]
apply (simp add:nsClose ring_tOp_closed npClose)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R Suc na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (Suc na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus>  (Suc na choose 0) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - 0)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>)
[PROOF STEP]
(**
thm binomial_Suc_Suc
**)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R Suc na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (Suc na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus>  (Suc na choose 0) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - 0)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>)
[PROOF STEP]
apply (simp only:binomial_Suc_Suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R Suc na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i + (na choose Suc i)) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus>  (Suc na choose 0) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - 0)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>)
[PROOF STEP]
apply (simp only: nsDistr [THEN sym] add:npClose ring_tOp_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R Suc na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>) \<plusminus>  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus>  (Suc na choose 0) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - 0)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>)
[PROOF STEP]
apply (subst aGroup.nsumElmAdd, assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<forall>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>) \<in> carrier R
 2. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<forall>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>) \<in> carrier R
 3. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R Suc na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus>  (Suc na choose 0) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - 0)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>)
[PROOF STEP]
apply (rule allI,
           simp add:nsClose ring_tOp_closed npClose)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<forall>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>) \<in> carrier R
 2. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R Suc na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus>  (Suc na choose 0) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - 0)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>)
[PROOF STEP]
apply (rule allI,
           simp add:nsClose add:ring_tOp_closed npClose)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R Suc na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus>  (Suc na choose 0) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - 0)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>)
[PROOF STEP]
apply (subst aGroup.ag_pOp_assoc, assumption)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<in> carrier R
 2. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<in> carrier R
 3. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow>  (Suc na choose 0) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - 0)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>) \<in> carrier R
 4. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R Suc na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus> (\<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus>  (Suc na choose 0) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - 0)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>))
[PROOF STEP]
apply (rule aGroup.nsum_mem, assumption,
           rule allI, rule impI,  simp add:nsClose ring_tOp_closed npClose)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<in> carrier R
 2. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow>  (Suc na choose 0) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - 0)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>) \<in> carrier R
 3. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R Suc na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus> (\<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus>  (Suc na choose 0) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - 0)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>))
[PROOF STEP]
apply (rule aGroup.nsum_mem, assumption,
           rule allI, rule impI,  simp add:nsClose ring_tOp_closed npClose)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow>  (Suc na choose 0) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - 0)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>) \<in> carrier R
 2. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R Suc na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus> (\<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus>  (Suc na choose 0) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - 0)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>))
[PROOF STEP]
apply (simp add:nsClose ring_tOp_closed npClose)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<zero> \<plusminus> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r \<in> carrier R
 2. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R Suc na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus> (\<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus>  (Suc na choose 0) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - 0)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>))
[PROOF STEP]
apply (rule aGroup.ag_pOp_closed, assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<zero> \<in> carrier R
 2. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r \<in> carrier R
 3. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R Suc na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus> (\<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus>  (Suc na choose 0) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - 0)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>))
[PROOF STEP]
apply (simp add:aGroup.ag_inc_zero)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r \<in> carrier R
 2. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R Suc na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus> (\<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus>  (Suc na choose 0) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - 0)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>))
[PROOF STEP]
apply (rule ring_tOp_closed)+
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> x^\<^bsup>R na\<^esup> \<in> carrier R
 2. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> x \<in> carrier R
 3. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> carrier R
 4. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R Suc na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus> (\<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus>  (Suc na choose 0) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - 0)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>))
[PROOF STEP]
apply (simp add:npClose, assumption, simp add:ring_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R Suc na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus> (\<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus>  (Suc na choose 0) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - 0)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>))
[PROOF STEP]
apply (subst npMulElmL [THEN sym, of "x \<plusminus> y"],
         simp add:aGroup.ag_pOp_closed, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> (x \<plusminus> y) \<cdot>\<^sub>r (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus> (\<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - Suc i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc i\<^esup>)) na \<plusminus>  (Suc na choose 0) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (Suc na - 0)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> (x \<plusminus> y) \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na \<plusminus> (\<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na \<plusminus> (\<zero> \<plusminus> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r))
[PROOF STEP]
apply (subst ring_distrib2 [of _ "x" "y"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na \<in> carrier R
 2. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> x \<in> carrier R
 3. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> y \<in> carrier R
 4. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na \<plusminus> y \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na \<plusminus> (\<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na \<plusminus> (\<zero> \<plusminus> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r))
[PROOF STEP]
apply (rule aGroup.nsum_mem,assumption,
         rule allI, rule impI, rule nsClose, rule ring_tOp_closed,
         simp add:npClose, simp add:npClose, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na \<plusminus> y \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na \<plusminus> (\<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na \<plusminus> (\<zero> \<plusminus> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r))
[PROOF STEP]
apply (rule aGroup.gEQAddcross [THEN sym], assumption+,
         rule aGroup.nsum_mem, assumption, rule allI, rule impI, rule nsClose,
         (rule ring_tOp_closed)+, simp add:npClose,
         rule ring_tOp_closed, simp add:npClose, assumption)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na \<plusminus> (\<zero> \<plusminus> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r) \<in> carrier R
 2. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na \<in> carrier R
 3. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na \<in> carrier R
 4. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na = y \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na
 5. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na \<plusminus> (\<zero> \<plusminus> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r) = x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na
[PROOF STEP]
apply (rule aGroup.ag_pOp_closed, assumption)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na \<in> carrier R
 2. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<zero> \<plusminus> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r \<in> carrier R
 3. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na \<in> carrier R
 4. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na \<in> carrier R
 5. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na = y \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na
 6. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na \<plusminus> (\<zero> \<plusminus> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r) = x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na
[PROOF STEP]
apply (rule aGroup.nsum_mem, assumption,
           rule allI, rule impI, rule nsClose, rule ring_tOp_closed,
          simp add:npClose, rule ring_tOp_closed, simp add:npClose, assumption)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<zero> \<plusminus> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r \<in> carrier R
 2. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na \<in> carrier R
 3. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na \<in> carrier R
 4. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na = y \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na
 5. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na \<plusminus> (\<zero> \<plusminus> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r) = x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na
[PROOF STEP]
apply (rule aGroup.ag_pOp_closed, assumption, simp add:ring_zero)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r \<in> carrier R
 2. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na \<in> carrier R
 3. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na \<in> carrier R
 4. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na = y \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na
 5. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na \<plusminus> (\<zero> \<plusminus> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r) = x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na
[PROOF STEP]
apply ((rule ring_tOp_closed)+,
           simp add:npClose,assumption, simp add:ring_one)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na \<in> carrier R
 2. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na \<in> carrier R
 3. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na = y \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na
 4. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na \<plusminus> (\<zero> \<plusminus> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r) = x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na
[PROOF STEP]
apply (rule ring_tOp_closed, assumption,
           rule aGroup.nsum_mem, assumption, rule allI, rule impI,
           rule nsClose, rule ring_tOp_closed,
           (simp add:npClose)+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na \<in> carrier R
 2. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na = y \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na
 3. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na \<plusminus> (\<zero> \<plusminus> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r) = x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na
[PROOF STEP]
apply (rule ring_tOp_closed, assumption+,
           rule aGroup.nsum_mem, assumption, rule allI, rule impI,
           rule nsClose,
           rule ring_tOp_closed,
           simp add:npClose, simp add:npClose)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na = y \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na
 2. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na \<plusminus> (\<zero> \<plusminus> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r) = x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na
[PROOF STEP]
apply (subst npeSum2_sub_muly [of "x" "y"], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na \<plusminus> (\<zero> \<plusminus> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r) = x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na
[PROOF STEP]
(* final part *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na \<plusminus> (\<zero> \<plusminus> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r) = x \<cdot>\<^sub>r \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na
[PROOF STEP]
apply (subst npeSum2_sub_mulx2 [of x y], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R; (x \<plusminus> y)^\<^bsup>R na\<^esup> = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) na\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na \<plusminus> (\<zero> \<plusminus> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r 1\<^sub>r) = \<Sigma>\<^sub>e R (\<lambda>i.  (na choose Suc i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (na - i)\<^esup> \<cdot>\<^sub>r (y^\<^bsup>R i\<^esup> \<cdot>\<^sub>r y))) na \<plusminus> (\<zero> \<plusminus> x \<cdot>\<^sub>r x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r 1\<^sub>r)
[PROOF STEP]
apply (frule_tac n = na in npClose[of x],
         simp add:ring_tOp_commute[of _ x])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in aGroup) nsum_zeroTr:
  "\<And> n. (\<forall> i. i \<le> n \<longrightarrow>  f i = \<zero>) \<longrightarrow> (nsum A f n = \<zero>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. (\<forall>i\<le>n. f i = \<zero>) \<longrightarrow> \<Sigma>\<^sub>e A f n = \<zero>
[PROOF STEP]
apply (induct_tac "n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. (\<forall>i\<le>0. f i = \<zero>) \<longrightarrow> \<Sigma>\<^sub>e A f 0 = \<zero>
 2. \<And>n na. (\<forall>i\<le>na. f i = \<zero>) \<longrightarrow> \<Sigma>\<^sub>e A f na = \<zero> \<Longrightarrow> (\<forall>i\<le>Suc na. f i = \<zero>) \<longrightarrow> \<Sigma>\<^sub>e A f Suc na = \<zero>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. (\<forall>i\<le>na. f i = \<zero>) \<longrightarrow> \<Sigma>\<^sub>e A f na = \<zero> \<Longrightarrow> (\<forall>i\<le>Suc na. f i = \<zero>) \<longrightarrow> \<Sigma>\<^sub>e A f Suc na = \<zero>
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>(\<forall>i\<le>na. f i = \<zero>) \<longrightarrow> \<Sigma>\<^sub>e A f na = \<zero>; \<forall>i\<le>Suc na. f i = \<zero>\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e A f Suc na = \<zero>
[PROOF STEP]
apply (cut_tac n = na in Nsetn_sub_mem1, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<Sigma>\<^sub>e A f na = \<zero>; \<forall>i\<le>Suc na. f i = \<zero>\<rbrakk> \<Longrightarrow> \<zero> \<plusminus> \<zero> = \<zero>
[PROOF STEP]
apply (subst aGroup.ag_l_zero, rule aGroup_axioms)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>\<Sigma>\<^sub>e A f na = \<zero>; \<forall>i\<le>Suc na. f i = \<zero>\<rbrakk> \<Longrightarrow> \<zero> \<in> carrier A
 2. \<And>na. \<lbrakk>\<Sigma>\<^sub>e A f na = \<zero>; \<forall>i\<le>Suc na. f i = \<zero>\<rbrakk> \<Longrightarrow> \<zero> = \<zero>
[PROOF STEP]
apply (simp add:ag_inc_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<Sigma>\<^sub>e A f na = \<zero>; \<forall>i\<le>Suc na. f i = \<zero>\<rbrakk> \<Longrightarrow> \<zero> = \<zero>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) npAdd:
  "\<lbrakk> x \<in> carrier R; y \<in> carrier R;
     npow R x m = \<zero>; npow R y n = \<zero> \<rbrakk>
        \<Longrightarrow> npow R (x \<plusminus> y) (m + n) = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; y^\<^bsup>R n\<^esup> = \<zero>\<rbrakk> \<Longrightarrow> (x \<plusminus> y)^\<^bsup>R (m + n)\<^esup> = \<zero>
[PROOF STEP]
apply (subst npeSum2, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; y^\<^bsup>R n\<^esup> = \<zero>\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R (\<lambda>i.  (m + n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (m + n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>)) (m + n) = \<zero>
[PROOF STEP]
apply (rule aGroup.nsum_zeroTr [THEN mp])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; y^\<^bsup>R n\<^esup> = \<zero>\<rbrakk> \<Longrightarrow> aGroup R
 2. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; y^\<^bsup>R n\<^esup> = \<zero>\<rbrakk> \<Longrightarrow> \<forall>i\<le>m + n.  (m + n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (m + n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>) = \<zero>
[PROOF STEP]
apply (simp add:ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; y^\<^bsup>R n\<^esup> = \<zero>\<rbrakk> \<Longrightarrow> \<forall>i\<le>m + n.  (m + n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (m + n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>) = \<zero>
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; y^\<^bsup>R n\<^esup> = \<zero>; i \<le> m + n\<rbrakk> \<Longrightarrow>  (m + n choose i) \<times>\<^bsub>R\<^esub> (x^\<^bsup>R (m + n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup>) = \<zero>
[PROOF STEP]
apply (rule nsZeroI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; y^\<^bsup>R n\<^esup> = \<zero>; i \<le> m + n\<rbrakk> \<Longrightarrow> x^\<^bsup>R (m + n - i)\<^esup> \<cdot>\<^sub>r y^\<^bsup>R i\<^esup> = \<zero>
[PROOF STEP]
apply (rule rMulZeroDiv, simp add:npClose, simp add:npClose)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; y^\<^bsup>R n\<^esup> = \<zero>; i \<le> m + n\<rbrakk> \<Longrightarrow> x^\<^bsup>R (m + n - i)\<^esup> = \<zero> \<or> y^\<^bsup>R i\<^esup> = \<zero>
[PROOF STEP]
apply (case_tac "i \<le> n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; y^\<^bsup>R n\<^esup> = \<zero>; i \<le> m + n; i \<le> n\<rbrakk> \<Longrightarrow> x^\<^bsup>R (m + n - i)\<^esup> = \<zero> \<or> y^\<^bsup>R i\<^esup> = \<zero>
 2. \<And>i. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; y^\<^bsup>R n\<^esup> = \<zero>; i \<le> m + n; \<not> i \<le> n\<rbrakk> \<Longrightarrow> x^\<^bsup>R (m + n - i)\<^esup> = \<zero> \<or> y^\<^bsup>R i\<^esup> = \<zero>
[PROOF STEP]
apply (rule disjI1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; y^\<^bsup>R n\<^esup> = \<zero>; i \<le> m + n; i \<le> n\<rbrakk> \<Longrightarrow> x^\<^bsup>R (m + n - i)\<^esup> = \<zero>
 2. \<And>i. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; y^\<^bsup>R n\<^esup> = \<zero>; i \<le> m + n; \<not> i \<le> n\<rbrakk> \<Longrightarrow> x^\<^bsup>R (m + n - i)\<^esup> = \<zero> \<or> y^\<^bsup>R i\<^esup> = \<zero>
[PROOF STEP]
apply (rule npGTPowZero [of "x" "m"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; y^\<^bsup>R n\<^esup> = \<zero>; i \<le> m + n; i \<le> n\<rbrakk> \<Longrightarrow> m \<le> m + n - i
 2. \<And>i. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; y^\<^bsup>R n\<^esup> = \<zero>; i \<le> m + n; \<not> i \<le> n\<rbrakk> \<Longrightarrow> x^\<^bsup>R (m + n - i)\<^esup> = \<zero> \<or> y^\<^bsup>R i\<^esup> = \<zero>
[PROOF STEP]
apply arith
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; y^\<^bsup>R n\<^esup> = \<zero>; i \<le> m + n; \<not> i \<le> n\<rbrakk> \<Longrightarrow> x^\<^bsup>R (m + n - i)\<^esup> = \<zero> \<or> y^\<^bsup>R i\<^esup> = \<zero>
[PROOF STEP]
apply (rule disjI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; y^\<^bsup>R n\<^esup> = \<zero>; i \<le> m + n; \<not> i \<le> n\<rbrakk> \<Longrightarrow> y^\<^bsup>R i\<^esup> = \<zero>
[PROOF STEP]
apply (rule npGTPowZero [of "y" "n"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; y^\<^bsup>R n\<^esup> = \<zero>; i \<le> m + n; \<not> i \<le> n\<rbrakk> \<Longrightarrow> n \<le> i
[PROOF STEP]
apply (arith)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) npInverse:
  "\<And>n. x \<in> carrier R
        \<Longrightarrow> npow R (-\<^sub>a x) n = npow R x n
            \<or> npow R (-\<^sub>a x) n = -\<^sub>a (npow R x n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. x \<in> carrier R \<Longrightarrow> (-\<^sub>a x)^\<^bsup>R n\<^esup> = x^\<^bsup>R n\<^esup> \<or> (-\<^sub>a x)^\<^bsup>R n\<^esup> = -\<^sub>a x^\<^bsup>R n\<^esup>
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. x \<in> carrier R \<Longrightarrow> (-\<^sub>a x)^\<^bsup>R 0\<^esup> = x^\<^bsup>R 0\<^esup> \<or> (-\<^sub>a x)^\<^bsup>R 0\<^esup> = -\<^sub>a x^\<^bsup>R 0\<^esup>
 2. \<And>n na. \<lbrakk>x \<in> carrier R; (-\<^sub>a x)^\<^bsup>R na\<^esup> = x^\<^bsup>R na\<^esup> \<or> (-\<^sub>a x)^\<^bsup>R na\<^esup> = -\<^sub>a x^\<^bsup>R na\<^esup>\<rbrakk> \<Longrightarrow> (-\<^sub>a x)^\<^bsup>R Suc na\<^esup> = x^\<^bsup>R Suc na\<^esup> \<or> (-\<^sub>a x)^\<^bsup>R Suc na\<^esup> = -\<^sub>a x^\<^bsup>R Suc na\<^esup>
[PROOF STEP]
(* n=0 *)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. x \<in> carrier R \<Longrightarrow> (-\<^sub>a x)^\<^bsup>R 0\<^esup> = x^\<^bsup>R 0\<^esup> \<or> (-\<^sub>a x)^\<^bsup>R 0\<^esup> = -\<^sub>a x^\<^bsup>R 0\<^esup>
 2. \<And>n na. \<lbrakk>x \<in> carrier R; (-\<^sub>a x)^\<^bsup>R na\<^esup> = x^\<^bsup>R na\<^esup> \<or> (-\<^sub>a x)^\<^bsup>R na\<^esup> = -\<^sub>a x^\<^bsup>R na\<^esup>\<rbrakk> \<Longrightarrow> (-\<^sub>a x)^\<^bsup>R Suc na\<^esup> = x^\<^bsup>R Suc na\<^esup> \<or> (-\<^sub>a x)^\<^bsup>R Suc na\<^esup> = -\<^sub>a x^\<^bsup>R Suc na\<^esup>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; (-\<^sub>a x)^\<^bsup>R na\<^esup> = x^\<^bsup>R na\<^esup> \<or> (-\<^sub>a x)^\<^bsup>R na\<^esup> = -\<^sub>a x^\<^bsup>R na\<^esup>\<rbrakk> \<Longrightarrow> (-\<^sub>a x)^\<^bsup>R Suc na\<^esup> = x^\<^bsup>R Suc na\<^esup> \<or> (-\<^sub>a x)^\<^bsup>R Suc na\<^esup> = -\<^sub>a x^\<^bsup>R Suc na\<^esup>
[PROOF STEP]
apply (erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; (-\<^sub>a x)^\<^bsup>R na\<^esup> = x^\<^bsup>R na\<^esup>\<rbrakk> \<Longrightarrow> (-\<^sub>a x)^\<^bsup>R Suc na\<^esup> = x^\<^bsup>R Suc na\<^esup> \<or> (-\<^sub>a x)^\<^bsup>R Suc na\<^esup> = -\<^sub>a x^\<^bsup>R Suc na\<^esup>
 2. \<And>n na. \<lbrakk>x \<in> carrier R; (-\<^sub>a x)^\<^bsup>R na\<^esup> = -\<^sub>a x^\<^bsup>R na\<^esup>\<rbrakk> \<Longrightarrow> (-\<^sub>a x)^\<^bsup>R Suc na\<^esup> = x^\<^bsup>R Suc na\<^esup> \<or> (-\<^sub>a x)^\<^bsup>R Suc na\<^esup> = -\<^sub>a x^\<^bsup>R Suc na\<^esup>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>x \<in> carrier R; (-\<^sub>a x)^\<^bsup>R na\<^esup> = x^\<^bsup>R na\<^esup>\<rbrakk> \<Longrightarrow> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r (-\<^sub>a x) = x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<or> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r (-\<^sub>a x) = -\<^sub>a x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x
 2. \<And>n na. \<lbrakk>x \<in> carrier R; (-\<^sub>a x)^\<^bsup>R na\<^esup> = -\<^sub>a x^\<^bsup>R na\<^esup>\<rbrakk> \<Longrightarrow> (-\<^sub>a x)^\<^bsup>R Suc na\<^esup> = x^\<^bsup>R Suc na\<^esup> \<or> (-\<^sub>a x)^\<^bsup>R Suc na\<^esup> = -\<^sub>a x^\<^bsup>R Suc na\<^esup>
[PROOF STEP]
apply (subst ring_inv1_2,
        simp add:npClose, assumption, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; (-\<^sub>a x)^\<^bsup>R na\<^esup> = -\<^sub>a x^\<^bsup>R na\<^esup>\<rbrakk> \<Longrightarrow> (-\<^sub>a x)^\<^bsup>R Suc na\<^esup> = x^\<^bsup>R Suc na\<^esup> \<or> (-\<^sub>a x)^\<^bsup>R Suc na\<^esup> = -\<^sub>a x^\<^bsup>R Suc na\<^esup>
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; (-\<^sub>a x)^\<^bsup>R na\<^esup> = -\<^sub>a x^\<^bsup>R na\<^esup>; aGroup R\<rbrakk> \<Longrightarrow> (-\<^sub>a x)^\<^bsup>R Suc na\<^esup> = x^\<^bsup>R Suc na\<^esup> \<or> (-\<^sub>a x)^\<^bsup>R Suc na\<^esup> = -\<^sub>a x^\<^bsup>R Suc na\<^esup>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>x \<in> carrier R; (-\<^sub>a x)^\<^bsup>R na\<^esup> = -\<^sub>a x^\<^bsup>R na\<^esup>; aGroup R\<rbrakk> \<Longrightarrow> (-\<^sub>a x^\<^bsup>R na\<^esup>) \<cdot>\<^sub>r (-\<^sub>a x) = x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<or> (-\<^sub>a x^\<^bsup>R na\<^esup>) \<cdot>\<^sub>r (-\<^sub>a x) = -\<^sub>a x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x
[PROOF STEP]
apply (subst ring_inv1_2[THEN sym, of _ x])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>na. \<lbrakk>x \<in> carrier R; (-\<^sub>a x)^\<^bsup>R na\<^esup> = -\<^sub>a x^\<^bsup>R na\<^esup>; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a x^\<^bsup>R na\<^esup> \<in> carrier R
 2. \<And>na. \<lbrakk>x \<in> carrier R; (-\<^sub>a x)^\<^bsup>R na\<^esup> = -\<^sub>a x^\<^bsup>R na\<^esup>; aGroup R\<rbrakk> \<Longrightarrow> x \<in> carrier R
 3. \<And>na. \<lbrakk>x \<in> carrier R; (-\<^sub>a x)^\<^bsup>R na\<^esup> = -\<^sub>a x^\<^bsup>R na\<^esup>; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a (-\<^sub>a x^\<^bsup>R na\<^esup>) \<cdot>\<^sub>r x = x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<or> (-\<^sub>a x^\<^bsup>R na\<^esup>) \<cdot>\<^sub>r (-\<^sub>a x) = -\<^sub>a x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x
[PROOF STEP]
apply (rule aGroup.ag_mOp_closed, assumption+,
        simp add:npClose, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>x \<in> carrier R; (-\<^sub>a x)^\<^bsup>R na\<^esup> = -\<^sub>a x^\<^bsup>R na\<^esup>; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a (-\<^sub>a x^\<^bsup>R na\<^esup>) \<cdot>\<^sub>r x = x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<or> (-\<^sub>a x^\<^bsup>R na\<^esup>) \<cdot>\<^sub>r (-\<^sub>a x) = -\<^sub>a x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x
[PROOF STEP]
apply (thin_tac "(-\<^sub>a x)^\<^bsup>R na\<^esup> = -\<^sub>a (x^\<^bsup>R na\<^esup>)",
        frule_tac n = na in npClose[of x],
        frule_tac x = "x^\<^bsup>R na\<^esup>" in aGroup.ag_mOp_closed[of R], simp add:npClose)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>x \<in> carrier R; aGroup R; x^\<^bsup>R na\<^esup> \<in> carrier R; -\<^sub>a x^\<^bsup>R na\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> -\<^sub>a (-\<^sub>a x^\<^bsup>R na\<^esup>) \<cdot>\<^sub>r x = x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<or> (-\<^sub>a x^\<^bsup>R na\<^esup>) \<cdot>\<^sub>r (-\<^sub>a x) = -\<^sub>a x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x
[PROOF STEP]
apply (simp add: ring_inv1_1[of _ x])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>x \<in> carrier R; aGroup R; x^\<^bsup>R na\<^esup> \<in> carrier R; -\<^sub>a x^\<^bsup>R na\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> (-\<^sub>a (-\<^sub>a x^\<^bsup>R na\<^esup>)) \<cdot>\<^sub>r x = x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<or> (-\<^sub>a x^\<^bsup>R na\<^esup>) \<cdot>\<^sub>r (-\<^sub>a x) = (-\<^sub>a x^\<^bsup>R na\<^esup>) \<cdot>\<^sub>r x
[PROOF STEP]
apply (simp add:aGroup.ag_inv_inv[of R])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) npMul:
  "\<And> n. \<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk>
        \<Longrightarrow> npow R (x \<cdot>\<^sub>r y) n = (npow R x n) \<cdot>\<^sub>r (npow R y n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> (x \<cdot>\<^sub>r y)^\<^bsup>R n\<^esup> = x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r y^\<^bsup>R n\<^esup>
[PROOF STEP]
apply (induct_tac "n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> (x \<cdot>\<^sub>r y)^\<^bsup>R 0\<^esup> = x^\<^bsup>R 0\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>
 2. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; (x \<cdot>\<^sub>r y)^\<^bsup>R na\<^esup> = x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r y^\<^bsup>R na\<^esup>\<rbrakk> \<Longrightarrow> (x \<cdot>\<^sub>r y)^\<^bsup>R Suc na\<^esup> = x^\<^bsup>R Suc na\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc na\<^esup>
[PROOF STEP]
(* n=0 *)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> (x \<cdot>\<^sub>r y)^\<^bsup>R 0\<^esup> = x^\<^bsup>R 0\<^esup> \<cdot>\<^sub>r y^\<^bsup>R 0\<^esup>
 2. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; (x \<cdot>\<^sub>r y)^\<^bsup>R na\<^esup> = x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r y^\<^bsup>R na\<^esup>\<rbrakk> \<Longrightarrow> (x \<cdot>\<^sub>r y)^\<^bsup>R Suc na\<^esup> = x^\<^bsup>R Suc na\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc na\<^esup>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> 1\<^sub>r = 1\<^sub>r \<cdot>\<^sub>r 1\<^sub>r
 2. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; (x \<cdot>\<^sub>r y)^\<^bsup>R na\<^esup> = x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r y^\<^bsup>R na\<^esup>\<rbrakk> \<Longrightarrow> (x \<cdot>\<^sub>r y)^\<^bsup>R Suc na\<^esup> = x^\<^bsup>R Suc na\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc na\<^esup>
[PROOF STEP]
apply (rule ring_r_one [THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> carrier R
 2. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; (x \<cdot>\<^sub>r y)^\<^bsup>R na\<^esup> = x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r y^\<^bsup>R na\<^esup>\<rbrakk> \<Longrightarrow> (x \<cdot>\<^sub>r y)^\<^bsup>R Suc na\<^esup> = x^\<^bsup>R Suc na\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc na\<^esup>
[PROOF STEP]
apply (simp add:ring_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; (x \<cdot>\<^sub>r y)^\<^bsup>R na\<^esup> = x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r y^\<^bsup>R na\<^esup>\<rbrakk> \<Longrightarrow> (x \<cdot>\<^sub>r y)^\<^bsup>R Suc na\<^esup> = x^\<^bsup>R Suc na\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc na\<^esup>
[PROOF STEP]
(* n>0 *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; (x \<cdot>\<^sub>r y)^\<^bsup>R na\<^esup> = x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r y^\<^bsup>R na\<^esup>\<rbrakk> \<Longrightarrow> (x \<cdot>\<^sub>r y)^\<^bsup>R Suc na\<^esup> = x^\<^bsup>R Suc na\<^esup> \<cdot>\<^sub>r y^\<^bsup>R Suc na\<^esup>
[PROOF STEP]
apply (simp only:npow_suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; (x \<cdot>\<^sub>r y)^\<^bsup>R na\<^esup> = x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r y^\<^bsup>R na\<^esup>\<rbrakk> \<Longrightarrow> x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r y^\<^bsup>R na\<^esup> \<cdot>\<^sub>r (x \<cdot>\<^sub>r y) = x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x \<cdot>\<^sub>r (y^\<^bsup>R na\<^esup> \<cdot>\<^sub>r y)
[PROOF STEP]
apply (rule ring_tOp_rel[THEN sym])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; (x \<cdot>\<^sub>r y)^\<^bsup>R na\<^esup> = x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r y^\<^bsup>R na\<^esup>\<rbrakk> \<Longrightarrow> x^\<^bsup>R na\<^esup> \<in> carrier R
 2. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; (x \<cdot>\<^sub>r y)^\<^bsup>R na\<^esup> = x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r y^\<^bsup>R na\<^esup>\<rbrakk> \<Longrightarrow> x \<in> carrier R
 3. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; (x \<cdot>\<^sub>r y)^\<^bsup>R na\<^esup> = x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r y^\<^bsup>R na\<^esup>\<rbrakk> \<Longrightarrow> y^\<^bsup>R na\<^esup> \<in> carrier R
 4. \<And>n na. \<lbrakk>x \<in> carrier R; y \<in> carrier R; (x \<cdot>\<^sub>r y)^\<^bsup>R na\<^esup> = x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r y^\<^bsup>R na\<^esup>\<rbrakk> \<Longrightarrow> y \<in> carrier R
[PROOF STEP]
apply (rule npClose, assumption+)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ridmap_surjec:"Ring A \<Longrightarrow> surjec\<^bsub>A,A\<^esub> (ridmap A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ring A \<Longrightarrow> surjec\<^bsub>A,A\<^esub> ridmap A
[PROOF STEP]
by(simp add:surjec_def aHom_def ridmap_def Ring.ring_is_ag aGroup.ag_pOp_closed surj_to_def)


[STATEMENT]
lemma rHom_aHom:"f \<in> rHom A R \<Longrightarrow> f \<in> aHom A R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> rHom A R \<Longrightarrow> f \<in> aHom A R
[PROOF STEP]
by (simp add:rHom_def)


[STATEMENT]
lemma rimg_carrier:"f \<in> rHom A R \<Longrightarrow> carrier (rimg A R f) = f ` (carrier A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> rHom A R \<Longrightarrow> carrier (rimg A R f) = f ` carrier A
[PROOF STEP]
by (simp add:rimg_def)


[STATEMENT]
lemma rHom_mem:"\<lbrakk> f \<in> rHom A R; a \<in> carrier A \<rbrakk> \<Longrightarrow> f a \<in> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> rHom A R; a \<in> carrier A\<rbrakk> \<Longrightarrow> f a \<in> carrier R
[PROOF STEP]
apply (simp add:rHom_def, frule conjunct1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> aHom A R \<and> (\<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y) \<and> f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>; a \<in> carrier A; f \<in> aHom A R\<rbrakk> \<Longrightarrow> f a \<in> carrier R
[PROOF STEP]
apply (thin_tac "f \<in> aHom A R \<and>
     (\<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y) \<and> f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; f \<in> aHom A R\<rbrakk> \<Longrightarrow> f a \<in> carrier R
[PROOF STEP]
apply (simp add:aHom_def, frule conjunct1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; f \<in> carrier A \<rightarrow> carrier R \<and> f \<in> extensional (carrier A) \<and> (\<forall>a\<in>carrier A. \<forall>b\<in>carrier A. f (a \<plusminus>\<^bsub>A\<^esub> b) = f a \<plusminus>\<^bsub>R\<^esub> f b); f \<in> carrier A \<rightarrow> carrier R\<rbrakk> \<Longrightarrow> f a \<in> carrier R
[PROOF STEP]
apply (thin_tac "f \<in> carrier A \<rightarrow> carrier R \<and>
     f \<in> extensional (carrier A) \<and>
     (\<forall>a\<in>carrier A. \<forall>b\<in>carrier A. f (a \<plusminus>\<^bsub>A\<^esub> b) = f a \<plusminus>\<^bsub>R\<^esub> f b)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier A; f \<in> carrier A \<rightarrow> carrier R\<rbrakk> \<Longrightarrow> f a \<in> carrier R
[PROOF STEP]
apply (simp add:funcset_mem)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rHom_func:"f \<in> rHom A R \<Longrightarrow> f \<in> carrier A \<rightarrow> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> rHom A R \<Longrightarrow> f \<in> carrier A \<rightarrow> carrier R
[PROOF STEP]
by (simp add:rHom_def aHom_def)


[STATEMENT]
lemma ringhom1:"\<lbrakk> Ring A; Ring R; x \<in> carrier A; y \<in> carrier A;
                    f \<in> rHom A R \<rbrakk> \<Longrightarrow> f (x \<plusminus>\<^bsub>A\<^esub> y) = (f x) \<plusminus>\<^bsub>R\<^esub> (f y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; x \<in> carrier A; y \<in> carrier A; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f (x \<plusminus>\<^bsub>A\<^esub> y) = f x \<plusminus>\<^bsub>R\<^esub> f y
[PROOF STEP]
apply (simp add:rHom_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; x \<in> carrier A; y \<in> carrier A; f \<in> aHom A R \<and> (\<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y) \<and> f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> f (x \<plusminus>\<^bsub>A\<^esub> y) = f x \<plusminus>\<^bsub>R\<^esub> f y
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; x \<in> carrier A; y \<in> carrier A; f \<in> aHom A R; (\<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y) \<and> f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> f (x \<plusminus>\<^bsub>A\<^esub> y) = f x \<plusminus>\<^bsub>R\<^esub> f y
[PROOF STEP]
apply (frule Ring.ring_is_ag [of "A"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; x \<in> carrier A; y \<in> carrier A; f \<in> aHom A R; (\<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y) \<and> f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>; aGroup A\<rbrakk> \<Longrightarrow> f (x \<plusminus>\<^bsub>A\<^esub> y) = f x \<plusminus>\<^bsub>R\<^esub> f y
[PROOF STEP]
apply (frule Ring.ring_is_ag [of "R"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; x \<in> carrier A; y \<in> carrier A; f \<in> aHom A R; (\<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y) \<and> f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> f (x \<plusminus>\<^bsub>A\<^esub> y) = f x \<plusminus>\<^bsub>R\<^esub> f y
[PROOF STEP]
apply (rule aHom_add, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rHom_inv_inv:"\<lbrakk> Ring A; Ring R; x \<in> carrier A; f \<in> rHom A R \<rbrakk>
 \<Longrightarrow> f (-\<^sub>a\<^bsub>A\<^esub> x) = -\<^sub>a\<^bsub>R\<^esub> (f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; x \<in> carrier A; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f (-\<^sub>a\<^bsub>A\<^esub> x) = -\<^sub>a\<^bsub>R\<^esub> f x
[PROOF STEP]
apply (frule Ring.ring_is_ag [of "A"],
       frule Ring.ring_is_ag [of "R"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; x \<in> carrier A; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> f (-\<^sub>a\<^bsub>A\<^esub> x) = -\<^sub>a\<^bsub>R\<^esub> f x
[PROOF STEP]
apply (simp add:rHom_def, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; x \<in> carrier A; aGroup A; aGroup R; f \<in> aHom A R; (\<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y) \<and> f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> f (-\<^sub>a\<^bsub>A\<^esub> x) = -\<^sub>a\<^bsub>R\<^esub> f x
[PROOF STEP]
apply (simp add:aHom_inv_inv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rHom_0_0:"\<lbrakk> Ring A; Ring R; f \<in> rHom A R \<rbrakk>  \<Longrightarrow> f (\<zero>\<^bsub>A\<^esub>) = \<zero>\<^bsub>R\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f \<zero>\<^bsub>A\<^esub> = \<zero>\<^bsub>R\<^esub>
[PROOF STEP]
apply (frule Ring.ring_is_ag [of "A"], frule Ring.ring_is_ag [of "R"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> f \<zero>\<^bsub>A\<^esub> = \<zero>\<^bsub>R\<^esub>
[PROOF STEP]
apply (simp add:rHom_def, (erule conjE)+, simp add:aHom_0_0)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rHom_tOp:"\<lbrakk> Ring A; Ring R; x \<in> carrier A; y \<in> carrier A;
 f \<in> rHom A R \<rbrakk> \<Longrightarrow> f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = (f x) \<cdot>\<^sub>r\<^bsub>R\<^esub> (f y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; x \<in> carrier A; y \<in> carrier A; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y
[PROOF STEP]
by (simp add:rHom_def)


[STATEMENT]
lemma rHom_add:"\<lbrakk>f \<in> rHom A R; x \<in> carrier A; y \<in> carrier A\<rbrakk> \<Longrightarrow>
                   f (x \<plusminus>\<^bsub>A\<^esub> y) = (f x) \<plusminus>\<^bsub>R\<^esub> (f y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> rHom A R; x \<in> carrier A; y \<in> carrier A\<rbrakk> \<Longrightarrow> f (x \<plusminus>\<^bsub>A\<^esub> y) = f x \<plusminus>\<^bsub>R\<^esub> f y
[PROOF STEP]
by (simp add:rHom_def aHom_def)


[STATEMENT]
lemma rHom_one:"\<lbrakk> Ring A; Ring R;f \<in> rHom A R \<rbrakk> \<Longrightarrow> f (1\<^sub>r\<^bsub>A\<^esub>) = (1\<^sub>r\<^bsub>R\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>
[PROOF STEP]
by (simp add:rHom_def)


[STATEMENT]
lemma rHom_npow:"\<lbrakk> Ring A; Ring R; x \<in> carrier A; f \<in> rHom A R \<rbrakk> \<Longrightarrow>
                    f (x^\<^bsup>A n\<^esup>) = (f x)^\<^bsup>R n\<^esup>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; x \<in> carrier A; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f (x^\<^bsup>A n\<^esup>) = f x^\<^bsup>R n\<^esup>
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; x \<in> carrier A; f \<in> rHom A R\<rbrakk> \<Longrightarrow> f (x^\<^bsup>A 0\<^esup>) = f x^\<^bsup>R 0\<^esup>
 2. \<And>n. \<lbrakk>Ring A; Ring R; x \<in> carrier A; f \<in> rHom A R; f (x^\<^bsup>A n\<^esup>) = f x^\<^bsup>R n\<^esup>\<rbrakk> \<Longrightarrow> f (x^\<^bsup>A Suc n\<^esup>) = f x^\<^bsup>R Suc n\<^esup>
[PROOF STEP]
apply (simp add:rHom_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Ring A; Ring R; x \<in> carrier A; f \<in> rHom A R; f (x^\<^bsup>A n\<^esup>) = f x^\<^bsup>R n\<^esup>\<rbrakk> \<Longrightarrow> f (x^\<^bsup>A Suc n\<^esup>) = f x^\<^bsup>R Suc n\<^esup>
[PROOF STEP]
apply (simp,
      frule_tac n = n in Ring.npClose[of "A" "x"], assumption+,
      subst rHom_tOp[of "A" "R" _ "x" "f"], assumption+, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rHom_compos:"\<lbrakk>Ring A; Ring B; Ring C; f \<in> rHom A B; g \<in> rHom B C\<rbrakk> \<Longrightarrow>
                   compos A g f \<in> rHom A C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring B; Ring C; f \<in> rHom A B; g \<in> rHom B C\<rbrakk> \<Longrightarrow> compos A g f \<in> rHom A C
[PROOF STEP]
apply (subst rHom_def, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring B; Ring C; f \<in> rHom A B; g \<in> rHom B C\<rbrakk> \<Longrightarrow> compos A g f \<in> aHom A C \<and> (\<forall>x\<in>carrier A. \<forall>y\<in>carrier A. compos A g f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = compos A g f x \<cdot>\<^sub>r\<^bsub>C\<^esub> compos A g f y) \<and> compos A g f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>C\<^esub>
[PROOF STEP]
apply (frule Ring.ring_is_ag[of "A"], frule Ring.ring_is_ag[of "B"],
       frule Ring.ring_is_ag[of "C"],
       frule rHom_aHom[of "f" "A" "B"], frule rHom_aHom[of "g" "B" "C"],
       simp add:aHom_compos)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring B; Ring C; f \<in> rHom A B; g \<in> rHom B C; aGroup A; aGroup B; aGroup C; f \<in> aHom A B; g \<in> aHom B C\<rbrakk> \<Longrightarrow> (\<forall>x\<in>carrier A. \<forall>y\<in>carrier A. compos A g f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = compos A g f x \<cdot>\<^sub>r\<^bsub>C\<^esub> compos A g f y) \<and> compos A g f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>C\<^esub>
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring B; Ring C; f \<in> rHom A B; g \<in> rHom B C; aGroup A; aGroup B; aGroup C; f \<in> aHom A B; g \<in> aHom B C\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. compos A g f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = compos A g f x \<cdot>\<^sub>r\<^bsub>C\<^esub> compos A g f y
 2. \<lbrakk>Ring A; Ring B; Ring C; f \<in> rHom A B; g \<in> rHom B C; aGroup A; aGroup B; aGroup C; f \<in> aHom A B; g \<in> aHom B C\<rbrakk> \<Longrightarrow> compos A g f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>C\<^esub>
[PROOF STEP]
apply ((rule ballI)+, simp add:compos_def compose_def,
        frule_tac x = x and y = y in Ring.ring_tOp_closed[of "A"], assumption+,
        simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring A; Ring B; Ring C; f \<in> rHom A B; g \<in> rHom B C; aGroup A; aGroup B; aGroup C; f \<in> aHom A B; g \<in> aHom B C; x \<in> carrier A; y \<in> carrier A; x \<cdot>\<^sub>r\<^bsub>A\<^esub> y \<in> carrier A\<rbrakk> \<Longrightarrow> g (f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y)) = g (f x) \<cdot>\<^sub>r\<^bsub>C\<^esub> g (f y)
 2. \<lbrakk>Ring A; Ring B; Ring C; f \<in> rHom A B; g \<in> rHom B C; aGroup A; aGroup B; aGroup C; f \<in> aHom A B; g \<in> aHom B C\<rbrakk> \<Longrightarrow> compos A g f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>C\<^esub>
[PROOF STEP]
apply (simp add:rHom_tOp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>Ring A; Ring B; Ring C; f \<in> rHom A B; g \<in> rHom B C; aGroup A; aGroup B; aGroup C; f \<in> aHom A B; g \<in> aHom B C; x \<in> carrier A; y \<in> carrier A; x \<cdot>\<^sub>r\<^bsub>A\<^esub> y \<in> carrier A\<rbrakk> \<Longrightarrow> g (f x \<cdot>\<^sub>r\<^bsub>B\<^esub> f y) = g (f x) \<cdot>\<^sub>r\<^bsub>C\<^esub> g (f y)
 2. \<lbrakk>Ring A; Ring B; Ring C; f \<in> rHom A B; g \<in> rHom B C; aGroup A; aGroup B; aGroup C; f \<in> aHom A B; g \<in> aHom B C\<rbrakk> \<Longrightarrow> compos A g f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>C\<^esub>
[PROOF STEP]
apply (frule_tac a = x in rHom_mem[of "f" "A" "B"], assumption+,
        frule_tac a = y in rHom_mem[of "f" "A" "B"], assumption+,
         simp add:rHom_tOp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring B; Ring C; f \<in> rHom A B; g \<in> rHom B C; aGroup A; aGroup B; aGroup C; f \<in> aHom A B; g \<in> aHom B C\<rbrakk> \<Longrightarrow> compos A g f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>C\<^esub>
[PROOF STEP]
apply (frule Ring.ring_one[of "A"], frule Ring.ring_one[of "B"],
        simp add:compos_def compose_def, simp add:rHom_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done