[STATEMENT]
lemma (in Ring) Sr_ring:"sr R S \<Longrightarrow> Ring (Sr R S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sr R S \<Longrightarrow> Ring (Sr R S)
[PROOF STEP]
apply (simp add:Ring_def [of "Sr R S"],
       cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<plusminus>\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<plusminus>\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> c = a \<plusminus>\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<plusminus>\<^bsub>Sr R S\<^esub> b = b \<plusminus>\<^bsub>Sr R S\<^esub> a)) \<and> mop (Sr R S) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> -\<^sub>a\<^bsub>Sr R S\<^esub> a \<plusminus>\<^bsub>Sr R S\<^esub> a = \<zero>\<^bsub>Sr R S\<^esub>) \<and> \<zero>\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<plusminus>\<^bsub>Sr R S\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<plusminus>\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S)
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<plusminus>\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> c = a \<plusminus>\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<plusminus>\<^bsub>Sr R S\<^esub> b = b \<plusminus>\<^bsub>Sr R S\<^esub> a)) \<and> mop (Sr R S) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> -\<^sub>a\<^bsub>Sr R S\<^esub> a \<plusminus>\<^bsub>Sr R S\<^esub> a = \<zero>\<^bsub>Sr R S\<^esub>) \<and> \<zero>\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<plusminus>\<^bsub>Sr R S\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (simp add:Sr_def Sr_pOp_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<plusminus>\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> c = a \<plusminus>\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<plusminus>\<^bsub>Sr R S\<^esub> b = b \<plusminus>\<^bsub>Sr R S\<^esub> a)) \<and> mop (Sr R S) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> -\<^sub>a\<^bsub>Sr R S\<^esub> a \<plusminus>\<^bsub>Sr R S\<^esub> a = \<zero>\<^bsub>Sr R S\<^esub>) \<and> \<zero>\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<plusminus>\<^bsub>Sr R S\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<plusminus>\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> c = a \<plusminus>\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c)))
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<plusminus>\<^bsub>Sr R S\<^esub> b = b \<plusminus>\<^bsub>Sr R S\<^esub> a)) \<and> mop (Sr R S) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> -\<^sub>a\<^bsub>Sr R S\<^esub> a \<plusminus>\<^bsub>Sr R S\<^esub> a = \<zero>\<^bsub>Sr R S\<^esub>) \<and> \<zero>\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<plusminus>\<^bsub>Sr R S\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (rule allI, rule impI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>sr R S; aGroup R; a \<in> carrier (Sr R S); b \<in> carrier (Sr R S); c \<in> carrier (Sr R S)\<rbrakk> \<Longrightarrow> a \<plusminus>\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> c = a \<plusminus>\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c)
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<plusminus>\<^bsub>Sr R S\<^esub> b = b \<plusminus>\<^bsub>Sr R S\<^esub> a)) \<and> mop (Sr R S) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> -\<^sub>a\<^bsub>Sr R S\<^esub> a \<plusminus>\<^bsub>Sr R S\<^esub> a = \<zero>\<^bsub>Sr R S\<^esub>) \<and> \<zero>\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<plusminus>\<^bsub>Sr R S\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (simp add:Sr_def,
        frule_tac x = a and y = b in Sr_pOp_closed, assumption+,
        frule_tac x = b and y = c in Sr_pOp_closed, assumption+,
        simp add:Sr_def sr_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>aGroup R; a \<in> S; b \<in> S; c \<in> S; a \<plusminus> b \<in> S; b \<plusminus> c \<in> S; S \<subseteq> carrier R; 1\<^sub>r \<in> S; \<forall>x\<in>S. \<forall>y\<in>S. x \<plusminus> -\<^sub>a y \<in> S \<and> x \<cdot>\<^sub>r y \<in> S\<rbrakk> \<Longrightarrow> a \<plusminus> b \<plusminus> c = a \<plusminus> (b \<plusminus> c)
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<plusminus>\<^bsub>Sr R S\<^esub> b = b \<plusminus>\<^bsub>Sr R S\<^esub> a)) \<and> mop (Sr R S) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> -\<^sub>a\<^bsub>Sr R S\<^esub> a \<plusminus>\<^bsub>Sr R S\<^esub> a = \<zero>\<^bsub>Sr R S\<^esub>) \<and> \<zero>\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<plusminus>\<^bsub>Sr R S\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (frule_tac c = a in subsetD[of "S" "carrier R"], assumption+,
        frule_tac c = b in subsetD[of "S" "carrier R"], assumption+,
        frule_tac c = c in subsetD[of "S" "carrier R"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>aGroup R; a \<in> S; b \<in> S; c \<in> S; a \<plusminus> b \<in> S; b \<plusminus> c \<in> S; S \<subseteq> carrier R; 1\<^sub>r \<in> S; \<forall>x\<in>S. \<forall>y\<in>S. x \<plusminus> -\<^sub>a y \<in> S \<and> x \<cdot>\<^sub>r y \<in> S; a \<in> carrier R; b \<in> carrier R; c \<in> carrier R\<rbrakk> \<Longrightarrow> a \<plusminus> b \<plusminus> c = a \<plusminus> (b \<plusminus> c)
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<plusminus>\<^bsub>Sr R S\<^esub> b = b \<plusminus>\<^bsub>Sr R S\<^esub> a)) \<and> mop (Sr R S) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> -\<^sub>a\<^bsub>Sr R S\<^esub> a \<plusminus>\<^bsub>Sr R S\<^esub> a = \<zero>\<^bsub>Sr R S\<^esub>) \<and> \<zero>\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<plusminus>\<^bsub>Sr R S\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (simp add:aGroup.ag_pOp_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<plusminus>\<^bsub>Sr R S\<^esub> b = b \<plusminus>\<^bsub>Sr R S\<^esub> a)) \<and> mop (Sr R S) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> -\<^sub>a\<^bsub>Sr R S\<^esub> a \<plusminus>\<^bsub>Sr R S\<^esub> a = \<zero>\<^bsub>Sr R S\<^esub>) \<and> \<zero>\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<plusminus>\<^bsub>Sr R S\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<plusminus>\<^bsub>Sr R S\<^esub> b = b \<plusminus>\<^bsub>Sr R S\<^esub> a)
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> mop (Sr R S) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> -\<^sub>a\<^bsub>Sr R S\<^esub> a \<plusminus>\<^bsub>Sr R S\<^esub> a = \<zero>\<^bsub>Sr R S\<^esub>) \<and> \<zero>\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<plusminus>\<^bsub>Sr R S\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (rule allI, rule impI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>sr R S; aGroup R; a \<in> carrier (Sr R S); b \<in> carrier (Sr R S)\<rbrakk> \<Longrightarrow> a \<plusminus>\<^bsub>Sr R S\<^esub> b = b \<plusminus>\<^bsub>Sr R S\<^esub> a
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> mop (Sr R S) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> -\<^sub>a\<^bsub>Sr R S\<^esub> a \<plusminus>\<^bsub>Sr R S\<^esub> a = \<zero>\<^bsub>Sr R S\<^esub>) \<and> \<zero>\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<plusminus>\<^bsub>Sr R S\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (simp add:Sr_def sr_def, (erule conjE)+,
        frule_tac c = a in subsetD[of "S" "carrier R"], assumption+,
        frule_tac c = b in subsetD[of "S" "carrier R"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>aGroup R; a \<in> S; b \<in> S; S \<subseteq> carrier R; 1\<^sub>r \<in> S; \<forall>x\<in>S. \<forall>y\<in>S. x \<plusminus> -\<^sub>a y \<in> S \<and> x \<cdot>\<^sub>r y \<in> S; a \<in> carrier R; b \<in> carrier R\<rbrakk> \<Longrightarrow> a \<plusminus> b = b \<plusminus> a
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> mop (Sr R S) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> -\<^sub>a\<^bsub>Sr R S\<^esub> a \<plusminus>\<^bsub>Sr R S\<^esub> a = \<zero>\<^bsub>Sr R S\<^esub>) \<and> \<zero>\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<plusminus>\<^bsub>Sr R S\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (simp add:aGroup.ag_pOp_commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> mop (Sr R S) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> -\<^sub>a\<^bsub>Sr R S\<^esub> a \<plusminus>\<^bsub>Sr R S\<^esub> a = \<zero>\<^bsub>Sr R S\<^esub>) \<and> \<zero>\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<plusminus>\<^bsub>Sr R S\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> mop (Sr R S) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S)
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> -\<^sub>a\<^bsub>Sr R S\<^esub> a \<plusminus>\<^bsub>Sr R S\<^esub> a = \<zero>\<^bsub>Sr R S\<^esub>) \<and> \<zero>\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<plusminus>\<^bsub>Sr R S\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply ((subst Sr_def)+, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> restrict (mop R) S \<in> S \<rightarrow> S
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> -\<^sub>a\<^bsub>Sr R S\<^esub> a \<plusminus>\<^bsub>Sr R S\<^esub> a = \<zero>\<^bsub>Sr R S\<^esub>) \<and> \<zero>\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<plusminus>\<^bsub>Sr R S\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (simp add:Sr_mOp_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> -\<^sub>a\<^bsub>Sr R S\<^esub> a \<plusminus>\<^bsub>Sr R S\<^esub> a = \<zero>\<^bsub>Sr R S\<^esub>) \<and> \<zero>\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<plusminus>\<^bsub>Sr R S\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> -\<^sub>a\<^bsub>Sr R S\<^esub> a \<plusminus>\<^bsub>Sr R S\<^esub> a = \<zero>\<^bsub>Sr R S\<^esub>
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<plusminus>\<^bsub>Sr R S\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> a \<in> carrier (Sr R S) \<longrightarrow> -\<^sub>a\<^bsub>Sr R S\<^esub> a \<plusminus>\<^bsub>Sr R S\<^esub> a = \<zero>\<^bsub>Sr R S\<^esub>
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<plusminus>\<^bsub>Sr R S\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply ((subst Sr_def)+, simp add:Sr_mOp_closed, rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>sr R S; aGroup R; a \<in> S\<rbrakk> \<Longrightarrow> -\<^sub>a a \<plusminus> a = \<zero>
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<plusminus>\<^bsub>Sr R S\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (unfold sr_def, frule conjunct1, fold sr_def,
         frule_tac c = a in subsetD[of "S" "carrier R"], assumption+,
         simp add:aGroup.ag_l_inv1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<plusminus>\<^bsub>Sr R S\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S)
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<plusminus>\<^bsub>Sr R S\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (simp add:Sr_def Sr_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<plusminus>\<^bsub>Sr R S\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> \<zero>\<^bsub>Sr R S\<^esub> \<plusminus>\<^bsub>Sr R S\<^esub> a = a
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (rule allI, simp add:Sr_def Sr_zero)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> a \<in> S \<longrightarrow> \<zero> \<plusminus> a = a
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>sr R S; aGroup R; a \<in> S\<rbrakk> \<Longrightarrow> \<zero> \<plusminus> a = a
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (unfold sr_def, frule conjunct1, fold sr_def,
         frule_tac c = a in subsetD[of "S" "carrier R"], assumption+,
         simp add:aGroup.ag_l_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<cdot>\<^sub>r\<^bsub>Sr R S\<^esub>) \<in> carrier (Sr R S) \<rightarrow> carrier (Sr R S) \<rightarrow> carrier (Sr R S)
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (simp add:Sr_def Sr_tOp_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)))
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (rule allI, rule impI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>sr R S; aGroup R; a \<in> carrier (Sr R S); b \<in> carrier (Sr R S); c \<in> carrier (Sr R S)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c)
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (simp add:Sr_def Sr_tOp_closed)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>sr R S; aGroup R; a \<in> S; b \<in> S; c \<in> S\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<cdot>\<^sub>r c = a \<cdot>\<^sub>r (b \<cdot>\<^sub>r c)
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (unfold sr_def, frule conjunct1, fold sr_def,
         frule_tac c = a in subsetD[of "S" "carrier R"], assumption+,
         frule_tac c = b in subsetD[of "S" "carrier R"], assumption+,
         frule_tac c = c in subsetD[of "S" "carrier R"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>sr R S; aGroup R; a \<in> S; b \<in> S; c \<in> S; S \<subseteq> carrier R; a \<in> carrier R; b \<in> carrier R; c \<in> carrier R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b \<cdot>\<^sub>r c = a \<cdot>\<^sub>r (b \<cdot>\<^sub>r c)
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (simp add:ring_tOp_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)) \<and> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b = b \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a)
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply ((rule allI, rule impI)+, simp add:Sr_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>sr R S; aGroup R; a \<in> S; b \<in> S\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b = b \<cdot>\<^sub>r a
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (unfold sr_def, frule conjunct1, fold sr_def,
         frule_tac c = a in subsetD[of "S" "carrier R"], assumption+,
         frule_tac c = b in subsetD[of "S" "carrier R"], assumption+,
         simp add:ring_tOp_commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<in> carrier (Sr R S)
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (simp add:Sr_def Sr_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))) \<and> (\<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> (\<forall>b. b \<in> carrier (Sr R S) \<longrightarrow> (\<forall>c. c \<in> carrier (Sr R S) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> (b \<plusminus>\<^bsub>Sr R S\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> b \<plusminus>\<^bsub>Sr R S\<^esub> a \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> c))
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a
[PROOF STEP]
apply (simp add:Sr_def Sr_pOp_closed Sr_tOp_closed)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> S \<longrightarrow> (\<forall>b. b \<in> S \<longrightarrow> (\<forall>c. c \<in> S \<longrightarrow> a \<cdot>\<^sub>r (b \<plusminus> c) = a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r c))
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a
[PROOF STEP]
apply (rule allI, rule impI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>sr R S; aGroup R; a \<in> S; b \<in> S; c \<in> S\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r (b \<plusminus> c) = a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r c
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a
[PROOF STEP]
apply (unfold sr_def, frule conjunct1, fold sr_def,
         frule_tac c = a in subsetD[of "S" "carrier R"], assumption+,
         frule_tac c = b in subsetD[of "S" "carrier R"], assumption+,
         frule_tac c = c in subsetD[of "S" "carrier R"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>sr R S; aGroup R; a \<in> S; b \<in> S; c \<in> S; S \<subseteq> carrier R; a \<in> carrier R; b \<in> carrier R; c \<in> carrier R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r (b \<plusminus> c) = a \<cdot>\<^sub>r b \<plusminus> a \<cdot>\<^sub>r c
 2. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a
[PROOF STEP]
apply (simp add:ring_distrib1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (Sr R S) \<longrightarrow> 1\<^sub>r\<^bsub>Sr R S\<^esub> \<cdot>\<^sub>r\<^bsub>Sr R S\<^esub> a = a
[PROOF STEP]
apply (simp add:Sr_def Sr_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sr R S; aGroup R\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> S \<longrightarrow> 1\<^sub>r \<cdot>\<^sub>r a = a
[PROOF STEP]
apply (rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>sr R S; aGroup R; a \<in> S\<rbrakk> \<Longrightarrow> 1\<^sub>r \<cdot>\<^sub>r a = a
[PROOF STEP]
apply (unfold sr_def, frule conjunct1, fold sr_def,
         frule_tac c = a in subsetD[of "S" "carrier R"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>sr R S; aGroup R; a \<in> S; S \<subseteq> carrier R; a \<in> carrier R\<rbrakk> \<Longrightarrow> 1\<^sub>r \<cdot>\<^sub>r a = a
[PROOF STEP]
apply (simp add:ring_l_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ring_tOp_rel:"\<lbrakk>x\<in>carrier R; xa\<in>carrier R; y\<in>carrier R;
ya \<in> carrier R \<rbrakk> \<Longrightarrow> (x \<cdot>\<^sub>r xa) \<cdot>\<^sub>r (y \<cdot>\<^sub>r ya) = (x \<cdot>\<^sub>r y) \<cdot>\<^sub>r (xa \<cdot>\<^sub>r ya)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; xa \<in> carrier R; y \<in> carrier R; ya \<in> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r xa \<cdot>\<^sub>r (y \<cdot>\<^sub>r ya) = x \<cdot>\<^sub>r y \<cdot>\<^sub>r (xa \<cdot>\<^sub>r ya)
[PROOF STEP]
apply (frule ring_tOp_closed[of "y" "ya"], assumption+,
       simp add:ring_tOp_assoc[of "x" "xa"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; xa \<in> carrier R; y \<in> carrier R; ya \<in> carrier R; y \<cdot>\<^sub>r ya \<in> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r (xa \<cdot>\<^sub>r (y \<cdot>\<^sub>r ya)) = x \<cdot>\<^sub>r y \<cdot>\<^sub>r (xa \<cdot>\<^sub>r ya)
[PROOF STEP]
apply (simp add:ring_tOp_assoc[THEN sym, of "xa" "y" "ya"],
       simp add:ring_tOp_commute[of "xa" "y"],
       simp add:ring_tOp_assoc[of "y" "xa" "ya"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; xa \<in> carrier R; y \<in> carrier R; ya \<in> carrier R; y \<cdot>\<^sub>r ya \<in> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r (y \<cdot>\<^sub>r (xa \<cdot>\<^sub>r ya)) = x \<cdot>\<^sub>r y \<cdot>\<^sub>r (xa \<cdot>\<^sub>r ya)
[PROOF STEP]
apply (frule ring_tOp_closed[of "xa" "ya"], assumption+,
       simp add:ring_tOp_assoc[THEN sym, of "x" "y"])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) nsClose:
  "\<And> n. \<lbrakk> x \<in> carrier R \<rbrakk>  \<Longrightarrow> nscal R x n \<in> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. x \<in> carrier R \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> x \<in> carrier R
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. x \<in> carrier R \<Longrightarrow>  0 \<times>\<^bsub>R\<^esub> x \<in> carrier R
 2. \<And>n na. \<lbrakk>x \<in> carrier R;  na \<times>\<^bsub>R\<^esub> x \<in> carrier R\<rbrakk> \<Longrightarrow>  Suc na \<times>\<^bsub>R\<^esub> x \<in> carrier R
[PROOF STEP]
apply (simp add:ring_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>x \<in> carrier R;  na \<times>\<^bsub>R\<^esub> x \<in> carrier R\<rbrakk> \<Longrightarrow>  Suc na \<times>\<^bsub>R\<^esub> x \<in> carrier R
[PROOF STEP]
apply (cut_tac ring_is_ag, simp add:aGroup.ag_pOp_closed)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) nsZero:
             "nscal R \<zero> n = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  n \<times>\<^bsub>R\<^esub> \<zero> = \<zero>
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aGroup R \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> \<zero> = \<zero>
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. aGroup R \<Longrightarrow>  0 \<times>\<^bsub>R\<^esub> \<zero> = \<zero>
 2. \<And>n. \<lbrakk>aGroup R;  n \<times>\<^bsub>R\<^esub> \<zero> = \<zero>\<rbrakk> \<Longrightarrow>  Suc n \<times>\<^bsub>R\<^esub> \<zero> = \<zero>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>aGroup R;  n \<times>\<^bsub>R\<^esub> \<zero> = \<zero>\<rbrakk> \<Longrightarrow>  Suc n \<times>\<^bsub>R\<^esub> \<zero> = \<zero>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>aGroup R;  n \<times>\<^bsub>R\<^esub> \<zero> = \<zero>\<rbrakk> \<Longrightarrow> \<zero> \<plusminus> \<zero> = \<zero>
[PROOF STEP]
apply (cut_tac ring_zero, simp add:aGroup.ag_l_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) nsZeroI: "\<And> n.  x = \<zero>  \<Longrightarrow> nscal R x n = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. x = \<zero> \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> x = \<zero>
[PROOF STEP]
by (simp only:nsZero)


[STATEMENT]
lemma (in Ring) nsEqElm:  "\<lbrakk> x \<in> carrier R; y \<in> carrier R; x = y \<rbrakk>
        \<Longrightarrow> (nscal R x n) = (nscal R y n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x = y\<rbrakk> \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> x =  n \<times>\<^bsub>R\<^esub> y
[PROOF STEP]
by simp


[STATEMENT]
lemma (in Ring) nsDistr:  "x \<in> carrier R
        \<Longrightarrow> (nscal R x n) \<plusminus> (nscal R x m) = nscal R x (n + m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier R \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> x \<plusminus>  m \<times>\<^bsub>R\<^esub> x =  (n + m) \<times>\<^bsub>R\<^esub> x
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> x \<plusminus>  m \<times>\<^bsub>R\<^esub> x =  (n + m) \<times>\<^bsub>R\<^esub> x
[PROOF STEP]
apply (induct_tac m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> x \<plusminus>  0 \<times>\<^bsub>R\<^esub> x =  (n + 0) \<times>\<^bsub>R\<^esub> x
 2. \<And>na. \<lbrakk>x \<in> carrier R; aGroup R;  n \<times>\<^bsub>R\<^esub> x \<plusminus>  na \<times>\<^bsub>R\<^esub> x =  (n + na) \<times>\<^bsub>R\<^esub> x\<rbrakk> \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> x \<plusminus>  Suc na \<times>\<^bsub>R\<^esub> x =  (n + Suc na) \<times>\<^bsub>R\<^esub> x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> x \<plusminus> \<zero> =  n \<times>\<^bsub>R\<^esub> x
 2. \<And>na. \<lbrakk>x \<in> carrier R; aGroup R;  n \<times>\<^bsub>R\<^esub> x \<plusminus>  na \<times>\<^bsub>R\<^esub> x =  (n + na) \<times>\<^bsub>R\<^esub> x\<rbrakk> \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> x \<plusminus>  Suc na \<times>\<^bsub>R\<^esub> x =  (n + Suc na) \<times>\<^bsub>R\<^esub> x
[PROOF STEP]
apply (frule nsClose[of "x" "n"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; aGroup R;  n \<times>\<^bsub>R\<^esub> x \<in> carrier R\<rbrakk> \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> x \<plusminus> \<zero> =  n \<times>\<^bsub>R\<^esub> x
 2. \<And>na. \<lbrakk>x \<in> carrier R; aGroup R;  n \<times>\<^bsub>R\<^esub> x \<plusminus>  na \<times>\<^bsub>R\<^esub> x =  (n + na) \<times>\<^bsub>R\<^esub> x\<rbrakk> \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> x \<plusminus>  Suc na \<times>\<^bsub>R\<^esub> x =  (n + Suc na) \<times>\<^bsub>R\<^esub> x
[PROOF STEP]
apply ( simp add:aGroup.ag_r_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>x \<in> carrier R; aGroup R;  n \<times>\<^bsub>R\<^esub> x \<plusminus>  na \<times>\<^bsub>R\<^esub> x =  (n + na) \<times>\<^bsub>R\<^esub> x\<rbrakk> \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> x \<plusminus>  Suc na \<times>\<^bsub>R\<^esub> x =  (n + Suc na) \<times>\<^bsub>R\<^esub> x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>x \<in> carrier R; aGroup R;  n \<times>\<^bsub>R\<^esub> x \<plusminus>  na \<times>\<^bsub>R\<^esub> x =  (n + na) \<times>\<^bsub>R\<^esub> x\<rbrakk> \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> x \<plusminus> ( na \<times>\<^bsub>R\<^esub> x \<plusminus> x) =  (n + na) \<times>\<^bsub>R\<^esub> x \<plusminus> x
[PROOF STEP]
apply (frule_tac x = x and n = n in nsClose,
         frule_tac x = x and n = na in nsClose)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>x \<in> carrier R; aGroup R;  n \<times>\<^bsub>R\<^esub> x \<plusminus>  na \<times>\<^bsub>R\<^esub> x =  (n + na) \<times>\<^bsub>R\<^esub> x;  n \<times>\<^bsub>R\<^esub> x \<in> carrier R;  na \<times>\<^bsub>R\<^esub> x \<in> carrier R\<rbrakk> \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> x \<plusminus> ( na \<times>\<^bsub>R\<^esub> x \<plusminus> x) =  (n + na) \<times>\<^bsub>R\<^esub> x \<plusminus> x
[PROOF STEP]
apply (subst aGroup.ag_pOp_assoc[THEN sym], assumption+, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) nsDistrL:  "\<lbrakk>x \<in> carrier R; y \<in> carrier R \<rbrakk>
        \<Longrightarrow> (nscal R x n) \<plusminus> (nscal R y n) = nscal R (x \<plusminus> y) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> x \<plusminus>  n \<times>\<^bsub>R\<^esub> y =  n \<times>\<^bsub>R\<^esub> (x \<plusminus> y)
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> x \<plusminus>  n \<times>\<^bsub>R\<^esub> y =  n \<times>\<^bsub>R\<^esub> (x \<plusminus> y)
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R\<rbrakk> \<Longrightarrow>  0 \<times>\<^bsub>R\<^esub> x \<plusminus>  0 \<times>\<^bsub>R\<^esub> y =  0 \<times>\<^bsub>R\<^esub> (x \<plusminus> y)
 2. \<And>n. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R;  n \<times>\<^bsub>R\<^esub> x \<plusminus>  n \<times>\<^bsub>R\<^esub> y =  n \<times>\<^bsub>R\<^esub> (x \<plusminus> y)\<rbrakk> \<Longrightarrow>  Suc n \<times>\<^bsub>R\<^esub> x \<plusminus>  Suc n \<times>\<^bsub>R\<^esub> y =  Suc n \<times>\<^bsub>R\<^esub> (x \<plusminus> y)
[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> \<zero> \<plusminus> \<zero> = \<zero>
 2. \<And>n. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R;  n \<times>\<^bsub>R\<^esub> x \<plusminus>  n \<times>\<^bsub>R\<^esub> y =  n \<times>\<^bsub>R\<^esub> (x \<plusminus> y)\<rbrakk> \<Longrightarrow>  Suc n \<times>\<^bsub>R\<^esub> x \<plusminus>  Suc n \<times>\<^bsub>R\<^esub> y =  Suc n \<times>\<^bsub>R\<^esub> (x \<plusminus> y)
[PROOF STEP]
apply (cut_tac ring_zero,
         simp add:aGroup.ag_l_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R;  n \<times>\<^bsub>R\<^esub> x \<plusminus>  n \<times>\<^bsub>R\<^esub> y =  n \<times>\<^bsub>R\<^esub> (x \<plusminus> y)\<rbrakk> \<Longrightarrow>  Suc n \<times>\<^bsub>R\<^esub> x \<plusminus>  Suc n \<times>\<^bsub>R\<^esub> y =  Suc n \<times>\<^bsub>R\<^esub> (x \<plusminus> y)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R;  n \<times>\<^bsub>R\<^esub> x \<plusminus>  n \<times>\<^bsub>R\<^esub> y =  n \<times>\<^bsub>R\<^esub> (x \<plusminus> y)\<rbrakk> \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> x \<plusminus> x \<plusminus> ( n \<times>\<^bsub>R\<^esub> y \<plusminus> y) =  n \<times>\<^bsub>R\<^esub> (x \<plusminus> y) \<plusminus> (x \<plusminus> y)
[PROOF STEP]
apply (frule_tac x = x and n = n in nsClose,
         frule_tac x = y and n = n in nsClose)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R;  n \<times>\<^bsub>R\<^esub> x \<plusminus>  n \<times>\<^bsub>R\<^esub> y =  n \<times>\<^bsub>R\<^esub> (x \<plusminus> y);  n \<times>\<^bsub>R\<^esub> x \<in> carrier R;  n \<times>\<^bsub>R\<^esub> y \<in> carrier R\<rbrakk> \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> x \<plusminus> x \<plusminus> ( n \<times>\<^bsub>R\<^esub> y \<plusminus> y) =  n \<times>\<^bsub>R\<^esub> (x \<plusminus> y) \<plusminus> (x \<plusminus> y)
[PROOF STEP]
apply (subst aGroup.pOp_assocTr43[of R _ x _ y], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R;  n \<times>\<^bsub>R\<^esub> x \<plusminus>  n \<times>\<^bsub>R\<^esub> y =  n \<times>\<^bsub>R\<^esub> (x \<plusminus> y);  n \<times>\<^bsub>R\<^esub> x \<in> carrier R;  n \<times>\<^bsub>R\<^esub> y \<in> carrier R\<rbrakk> \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> x \<plusminus> (x \<plusminus>  n \<times>\<^bsub>R\<^esub> y) \<plusminus> y =  n \<times>\<^bsub>R\<^esub> (x \<plusminus> y) \<plusminus> (x \<plusminus> y)
[PROOF STEP]
apply (frule_tac x = x and y = "n \<times>\<^bsub>R\<^esub> y" in aGroup.ag_pOp_commute[of "R"],
         assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R;  n \<times>\<^bsub>R\<^esub> x \<plusminus>  n \<times>\<^bsub>R\<^esub> y =  n \<times>\<^bsub>R\<^esub> (x \<plusminus> y);  n \<times>\<^bsub>R\<^esub> x \<in> carrier R;  n \<times>\<^bsub>R\<^esub> y \<in> carrier R; x \<plusminus>  n \<times>\<^bsub>R\<^esub> y =  n \<times>\<^bsub>R\<^esub> y \<plusminus> x\<rbrakk> \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> x \<plusminus> (x \<plusminus>  n \<times>\<^bsub>R\<^esub> y) \<plusminus> y =  n \<times>\<^bsub>R\<^esub> (x \<plusminus> y) \<plusminus> (x \<plusminus> y)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R;  n \<times>\<^bsub>R\<^esub> x \<plusminus>  n \<times>\<^bsub>R\<^esub> y =  n \<times>\<^bsub>R\<^esub> (x \<plusminus> y);  n \<times>\<^bsub>R\<^esub> x \<in> carrier R;  n \<times>\<^bsub>R\<^esub> y \<in> carrier R; x \<plusminus>  n \<times>\<^bsub>R\<^esub> y =  n \<times>\<^bsub>R\<^esub> y \<plusminus> x\<rbrakk> \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> x \<plusminus> ( n \<times>\<^bsub>R\<^esub> y \<plusminus> x) \<plusminus> y =  n \<times>\<^bsub>R\<^esub> (x \<plusminus> y) \<plusminus> (x \<plusminus> y)
[PROOF STEP]
apply (subst aGroup.pOp_assocTr43[THEN sym, of R _ _ x y], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; y \<in> carrier R; aGroup R;  n \<times>\<^bsub>R\<^esub> x \<plusminus>  n \<times>\<^bsub>R\<^esub> y =  n \<times>\<^bsub>R\<^esub> (x \<plusminus> y);  n \<times>\<^bsub>R\<^esub> x \<in> carrier R;  n \<times>\<^bsub>R\<^esub> y \<in> carrier R; x \<plusminus>  n \<times>\<^bsub>R\<^esub> y =  n \<times>\<^bsub>R\<^esub> y \<plusminus> x\<rbrakk> \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> x \<plusminus>  n \<times>\<^bsub>R\<^esub> y \<plusminus> (x \<plusminus> y) =  n \<times>\<^bsub>R\<^esub> (x \<plusminus> y) \<plusminus> (x \<plusminus> y)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) nsMulDistrL:"\<lbrakk> x \<in> carrier R; y \<in> carrier R \<rbrakk>
        \<Longrightarrow> x \<cdot>\<^sub>r (nscal R y n) = nscal R (x \<cdot>\<^sub>r y) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r  n \<times>\<^bsub>R\<^esub> y =  n \<times>\<^bsub>R\<^esub> (x \<cdot>\<^sub>r y)
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r  0 \<times>\<^bsub>R\<^esub> y =  0 \<times>\<^bsub>R\<^esub> (x \<cdot>\<^sub>r y)
 2. \<And>n. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r  n \<times>\<^bsub>R\<^esub> y =  n \<times>\<^bsub>R\<^esub> (x \<cdot>\<^sub>r y)\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r  Suc n \<times>\<^bsub>R\<^esub> y =  Suc n \<times>\<^bsub>R\<^esub> (x \<cdot>\<^sub>r y)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r \<zero> = \<zero>
 2. \<And>n. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r  n \<times>\<^bsub>R\<^esub> y =  n \<times>\<^bsub>R\<^esub> (x \<cdot>\<^sub>r y)\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r  Suc n \<times>\<^bsub>R\<^esub> y =  Suc n \<times>\<^bsub>R\<^esub> (x \<cdot>\<^sub>r y)
[PROOF STEP]
apply (simp add:ring_times_x_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r  n \<times>\<^bsub>R\<^esub> y =  n \<times>\<^bsub>R\<^esub> (x \<cdot>\<^sub>r y)\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r  Suc n \<times>\<^bsub>R\<^esub> y =  Suc n \<times>\<^bsub>R\<^esub> (x \<cdot>\<^sub>r y)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r  n \<times>\<^bsub>R\<^esub> y =  n \<times>\<^bsub>R\<^esub> (x \<cdot>\<^sub>r y)\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r ( n \<times>\<^bsub>R\<^esub> y \<plusminus> y) =  n \<times>\<^bsub>R\<^esub> (x \<cdot>\<^sub>r y) \<plusminus> x \<cdot>\<^sub>r y
[PROOF STEP]
apply (subst ring_distrib1, assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r  n \<times>\<^bsub>R\<^esub> y =  n \<times>\<^bsub>R\<^esub> (x \<cdot>\<^sub>r y)\<rbrakk> \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> y \<in> carrier R
 2. \<And>n. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r  n \<times>\<^bsub>R\<^esub> y =  n \<times>\<^bsub>R\<^esub> (x \<cdot>\<^sub>r y)\<rbrakk> \<Longrightarrow> y \<in> carrier R
 3. \<And>n. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r  n \<times>\<^bsub>R\<^esub> y =  n \<times>\<^bsub>R\<^esub> (x \<cdot>\<^sub>r y)\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r  n \<times>\<^bsub>R\<^esub> y \<plusminus> x \<cdot>\<^sub>r y =  n \<times>\<^bsub>R\<^esub> (x \<cdot>\<^sub>r y) \<plusminus> x \<cdot>\<^sub>r y
[PROOF STEP]
apply (rule nsClose, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r  n \<times>\<^bsub>R\<^esub> y =  n \<times>\<^bsub>R\<^esub> (x \<cdot>\<^sub>r y)\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r  n \<times>\<^bsub>R\<^esub> y \<plusminus> x \<cdot>\<^sub>r y =  n \<times>\<^bsub>R\<^esub> (x \<cdot>\<^sub>r y) \<plusminus> x \<cdot>\<^sub>r y
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) nsMulDistrR:"\<lbrakk> x \<in> carrier R; y \<in> carrier R\<rbrakk>
        \<Longrightarrow> (nscal R y n) \<cdot>\<^sub>r x = nscal R (y \<cdot>\<^sub>r x) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier R; y \<in> carrier R\<rbrakk> \<Longrightarrow>  n \<times>\<^bsub>R\<^esub> y \<cdot>\<^sub>r x =  n \<times>\<^bsub>R\<^esub> (y \<cdot>\<^sub>r x)
[PROOF STEP]
apply (frule_tac x = y and n = n in nsClose,
         simp add:ring_tOp_commute[of "n \<times>\<^bsub>R\<^esub> y" "x"],
         simp add:nsMulDistrL,
         simp add:ring_tOp_commute[of "y" "x"])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) npClose:"x \<in> carrier R \<Longrightarrow> npow R x n \<in> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier R \<Longrightarrow> x^\<^bsup>R n\<^esup> \<in> carrier R
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x \<in> carrier R \<Longrightarrow> x^\<^bsup>R 0\<^esup> \<in> carrier R
 2. \<And>n. \<lbrakk>x \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> x^\<^bsup>R Suc n\<^esup> \<in> carrier R
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x \<in> carrier R \<Longrightarrow> 1\<^sub>r \<in> carrier R
 2. \<And>n. \<lbrakk>x \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> x^\<^bsup>R Suc n\<^esup> \<in> carrier R
[PROOF STEP]
apply (simp add:ring_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> x^\<^bsup>R Suc n\<^esup> \<in> carrier R
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x \<in> carrier R
[PROOF STEP]
apply (rule ring_tOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) npMulDistr:"\<And> n m. x \<in> carrier R  \<Longrightarrow>
                 (npow R x n) \<cdot>\<^sub>r (npow R x m) = npow R x (n + m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n m. x \<in> carrier R \<Longrightarrow> x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x^\<^bsup>R m\<^esup> = x^\<^bsup>R (n + m)\<^esup>
[PROOF STEP]
apply (induct_tac m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n m. x \<in> carrier R \<Longrightarrow> x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x^\<^bsup>R 0\<^esup> = x^\<^bsup>R (n + 0)\<^esup>
 2. \<And>n m na. \<lbrakk>x \<in> carrier R; x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x^\<^bsup>R na\<^esup> = x^\<^bsup>R (n + na)\<^esup>\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x^\<^bsup>R Suc na\<^esup> = x^\<^bsup>R (n + Suc na)\<^esup>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. x \<in> carrier R \<Longrightarrow> x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r 1\<^sub>r = x^\<^bsup>R n\<^esup>
 2. \<And>n m na. \<lbrakk>x \<in> carrier R; x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x^\<^bsup>R na\<^esup> = x^\<^bsup>R (n + na)\<^esup>\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x^\<^bsup>R Suc na\<^esup> = x^\<^bsup>R (n + Suc na)\<^esup>
[PROOF STEP]
apply (rule ring_r_one, simp add:npClose)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n m na. \<lbrakk>x \<in> carrier R; x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x^\<^bsup>R na\<^esup> = x^\<^bsup>R (n + na)\<^esup>\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x^\<^bsup>R Suc na\<^esup> = x^\<^bsup>R (n + Suc na)\<^esup>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x^\<^bsup>R na\<^esup> = x^\<^bsup>R (n + na)\<^esup>\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r (x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x) = x^\<^bsup>R (n + na)\<^esup> \<cdot>\<^sub>r x
[PROOF STEP]
apply (frule_tac x = x and n = n in npClose,
         frule_tac x = x and n = na in npClose)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x^\<^bsup>R na\<^esup> = x^\<^bsup>R (n + na)\<^esup>; x^\<^bsup>R n\<^esup> \<in> carrier R; x^\<^bsup>R na\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r (x^\<^bsup>R na\<^esup> \<cdot>\<^sub>r x) = x^\<^bsup>R (n + na)\<^esup> \<cdot>\<^sub>r x
[PROOF STEP]
apply (simp add:ring_tOp_assoc[THEN sym])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) npMulExp:"\<And>n m. x \<in> carrier R
        \<Longrightarrow>  npow R (npow R x n) m = npow R x (n * m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n m. x \<in> carrier R \<Longrightarrow> x^\<^bsup>R n\<^esup>^\<^bsup>R m\<^esup> = x^\<^bsup>R (n * m)\<^esup>
[PROOF STEP]
apply (induct_tac m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n m. x \<in> carrier R \<Longrightarrow> x^\<^bsup>R n\<^esup>^\<^bsup>R 0\<^esup> = x^\<^bsup>R (n * 0)\<^esup>
 2. \<And>n m na. \<lbrakk>x \<in> carrier R; x^\<^bsup>R n\<^esup>^\<^bsup>R na\<^esup> = x^\<^bsup>R (n * na)\<^esup>\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup>^\<^bsup>R Suc na\<^esup> = x^\<^bsup>R (n * Suc na)\<^esup>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n m na. \<lbrakk>x \<in> carrier R; x^\<^bsup>R n\<^esup>^\<^bsup>R na\<^esup> = x^\<^bsup>R (n * na)\<^esup>\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup>^\<^bsup>R Suc na\<^esup> = x^\<^bsup>R (n * Suc na)\<^esup>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; x^\<^bsup>R n\<^esup>^\<^bsup>R na\<^esup> = x^\<^bsup>R (n * na)\<^esup>\<rbrakk> \<Longrightarrow> x^\<^bsup>R (n * na)\<^esup> \<cdot>\<^sub>r x^\<^bsup>R n\<^esup> = x^\<^bsup>R (n + n * na)\<^esup>
[PROOF STEP]
apply (simp add:npMulDistr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>x \<in> carrier R; x^\<^bsup>R n\<^esup>^\<^bsup>R na\<^esup> = x^\<^bsup>R (n * na)\<^esup>\<rbrakk> \<Longrightarrow> x^\<^bsup>R (n * na + n)\<^esup> = x^\<^bsup>R (n + n * na)\<^esup>
[PROOF STEP]
apply (simp add:add.commute)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) npGTPowZero_sub:
  " \<And> n. \<lbrakk> x \<in> carrier R; npow R x m = \<zero> \<rbrakk>
        \<Longrightarrow>(m \<le> n) \<longrightarrow> (npow R x n = \<zero> )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>\<rbrakk> \<Longrightarrow> m \<le> n \<longrightarrow> x^\<^bsup>R n\<^esup> = \<zero>
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; m \<le> n\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> = \<zero>
[PROOF STEP]
apply (subgoal_tac "npow R x n = (npow R x (n-m)) \<cdot>\<^sub>r (npow R x m)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; m \<le> n; x^\<^bsup>R n\<^esup> = x^\<^bsup>R (n - m)\<^esup> \<cdot>\<^sub>r x^\<^bsup>R m\<^esup>\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> = \<zero>
 2. \<And>n. \<lbrakk>x \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; m \<le> n\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> = x^\<^bsup>R (n - m)\<^esup> \<cdot>\<^sub>r x^\<^bsup>R m\<^esup>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; m \<le> n; x^\<^bsup>R n\<^esup> = x^\<^bsup>R (n - m)\<^esup> \<cdot>\<^sub>r \<zero>\<rbrakk> \<Longrightarrow> x^\<^bsup>R (n - m)\<^esup> \<cdot>\<^sub>r \<zero> = \<zero>
 2. \<And>n. \<lbrakk>x \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; m \<le> n\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> = x^\<^bsup>R (n - m)\<^esup> \<cdot>\<^sub>r x^\<^bsup>R m\<^esup>
[PROOF STEP]
apply (rule ring_times_x_0)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>x \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; m \<le> n; x^\<^bsup>R n\<^esup> = x^\<^bsup>R (n - m)\<^esup> \<cdot>\<^sub>r \<zero>\<rbrakk> \<Longrightarrow> x^\<^bsup>R (n - m)\<^esup> \<in> carrier R
 2. \<And>n. \<lbrakk>x \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; m \<le> n\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> = x^\<^bsup>R (n - m)\<^esup> \<cdot>\<^sub>r x^\<^bsup>R m\<^esup>
[PROOF STEP]
apply (simp add:npClose)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; m \<le> n\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> = x^\<^bsup>R (n - m)\<^esup> \<cdot>\<^sub>r x^\<^bsup>R m\<^esup>
[PROOF STEP]
apply (thin_tac "x^\<^bsup>R m\<^esup> = \<zero>")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; m \<le> n\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> = x^\<^bsup>R (n - m)\<^esup> \<cdot>\<^sub>r x^\<^bsup>R m\<^esup>
[PROOF STEP]
apply (subst npMulDistr, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; m \<le> n\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> = x^\<^bsup>R (n - m + m)\<^esup>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) npGTPowZero:
  "\<And> n. \<lbrakk> x \<in> carrier R; npow R x m = \<zero>; m \<le> n \<rbrakk>
        \<Longrightarrow> npow R x n = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; m \<le> n\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> = \<zero>
[PROOF STEP]
apply (cut_tac x = x and m = m and n = n in npGTPowZero_sub, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; x^\<^bsup>R m\<^esup> = \<zero>; m \<le> n; m \<le> n \<longrightarrow> x^\<^bsup>R n\<^esup> = \<zero>\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> = \<zero>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) npOne: " npow R (1\<^sub>r) n = 1\<^sub>r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1\<^sub>r^\<^bsup>R n\<^esup> = 1\<^sub>r
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 1\<^sub>r^\<^bsup>R 0\<^esup> = 1\<^sub>r
 2. \<And>n. 1\<^sub>r^\<^bsup>R n\<^esup> = 1\<^sub>r \<Longrightarrow> 1\<^sub>r^\<^bsup>R Suc n\<^esup> = 1\<^sub>r
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. 1\<^sub>r^\<^bsup>R n\<^esup> = 1\<^sub>r \<Longrightarrow> 1\<^sub>r^\<^bsup>R Suc n\<^esup> = 1\<^sub>r
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. 1\<^sub>r^\<^bsup>R n\<^esup> = 1\<^sub>r \<Longrightarrow> 1\<^sub>r \<cdot>\<^sub>r 1\<^sub>r = 1\<^sub>r
[PROOF STEP]
apply (rule ring_r_one, simp add:ring_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) npZero_sub: "0 < n \<longrightarrow> npow R \<zero> n = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<longrightarrow> \<zero>^\<^bsup>R n\<^esup> = \<zero>
[PROOF STEP]
apply (induct_tac "n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 < 0 \<longrightarrow> \<zero>^\<^bsup>R 0\<^esup> = \<zero>
 2. \<And>n. 0 < n \<longrightarrow> \<zero>^\<^bsup>R n\<^esup> = \<zero> \<Longrightarrow> 0 < Suc n \<longrightarrow> \<zero>^\<^bsup>R Suc n\<^esup> = \<zero>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. 0 < n \<longrightarrow> \<zero>^\<^bsup>R n\<^esup> = \<zero> \<Longrightarrow> 0 < Suc n \<longrightarrow> \<zero>^\<^bsup>R Suc n\<^esup> = \<zero>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. 0 < n \<longrightarrow> \<zero>^\<^bsup>R n\<^esup> = \<zero> \<Longrightarrow> \<zero>^\<^bsup>R n\<^esup> \<cdot>\<^sub>r \<zero> = \<zero>
[PROOF STEP]
apply (cut_tac ring_zero,
           frule_tac n = n in npClose[of "\<zero>"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>0 < n \<longrightarrow> \<zero>^\<^bsup>R n\<^esup> = \<zero>; \<zero> \<in> carrier R; \<zero>^\<^bsup>R n\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> \<zero>^\<^bsup>R n\<^esup> \<cdot>\<^sub>r \<zero> = \<zero>
[PROOF STEP]
apply (simp add:ring_times_x_0)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) npZero: "0 < n  \<Longrightarrow> npow R \<zero> n = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> \<zero>^\<^bsup>R n\<^esup> = \<zero>
[PROOF STEP]
apply (simp add:npZero_sub)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) npMulElmL: "\<And> n. \<lbrakk> x \<in> carrier R; 0 \<le> n\<rbrakk>
        \<Longrightarrow> x \<cdot>\<^sub>r (npow R x n) = npow R x (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; 0 \<le> n\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r x^\<^bsup>R n\<^esup> = x^\<^bsup>R Suc n\<^esup>
[PROOF STEP]
apply (simp only:npow_suc,
       frule_tac n = n and x = x in npClose,
       simp add:ring_tOp_commute)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) npMulEleL: "\<And> n. x \<in> carrier R
        \<Longrightarrow> (npow R x n) \<cdot>\<^sub>r x =  npow R x (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. x \<in> carrier R \<Longrightarrow> x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x = x^\<^bsup>R Suc n\<^esup>
[PROOF STEP]
by (simp add:npMulElmL[THEN sym])


[STATEMENT]
lemma (in Ring) npMulElmR: "\<And> n. x \<in> carrier R
        \<Longrightarrow> (npow R x n) \<cdot>\<^sub>r x =  npow R x (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. x \<in> carrier R \<Longrightarrow> x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x = x^\<^bsup>R Suc n\<^esup>
[PROOF STEP]
apply ( frule_tac n = n in npClose[of "x"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<in> carrier R; x^\<^bsup>R n\<^esup> \<in> carrier R\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x = x^\<^bsup>R Suc n\<^esup>
[PROOF STEP]
apply (simp only:ring_tOp_commute,
          subst npMulElmL, assumption, simp, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done