[STATEMENT]
lemma rimg_ag:"\<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> aGroup (rimg A R f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> aGroup (rimg A R f)
[PROOF STEP]
apply (frule Ring.ring_is_ag [of "A"],
       frule Ring.ring_is_ag [of "R"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> aGroup (rimg A R f)
[PROOF STEP]
apply (simp add:rHom_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> aGroup (rimg A R f)
[PROOF STEP]
apply (subst aGroup_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> ((\<plusminus>\<^bsub>rimg A R f\<^esub>) \<in> carrier (rimg A R f) \<rightarrow> carrier (rimg A R f) \<rightarrow> carrier (rimg A R f) \<and> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<plusminus>\<^bsub>rimg A R f\<^esub> b \<plusminus>\<^bsub>rimg A R f\<^esub> c = a \<plusminus>\<^bsub>rimg A R f\<^esub> (b \<plusminus>\<^bsub>rimg A R f\<^esub> c)) \<and> (\<forall>a b. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> a \<plusminus>\<^bsub>rimg A R f\<^esub> b = b \<plusminus>\<^bsub>rimg A R f\<^esub> a)) \<and> (mop (rimg A R f) \<in> carrier (rimg A R f) \<rightarrow> carrier (rimg A R f) \<and> (\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> -\<^sub>a\<^bsub>rimg A R f\<^esub> a \<plusminus>\<^bsub>rimg A R f\<^esub> a = \<zero>\<^bsub>rimg A R f\<^esub>)) \<and> \<zero>\<^bsub>rimg A R f\<^esub> \<in> carrier (rimg A R f) \<and> (\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> \<zero>\<^bsub>rimg A R f\<^esub> \<plusminus>\<^bsub>rimg A R f\<^esub> a = a)
[PROOF STEP]
apply (simp add:rimg_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> (\<plusminus>\<^bsub>R\<^esub>) \<in> f ` carrier A \<rightarrow> f ` carrier A \<rightarrow> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> (\<forall>b. b \<in> f ` carrier A \<longrightarrow> (\<forall>c. c \<in> f ` carrier A \<longrightarrow> a \<plusminus>\<^bsub>R\<^esub> b \<plusminus>\<^bsub>R\<^esub> c = a \<plusminus>\<^bsub>R\<^esub> (b \<plusminus>\<^bsub>R\<^esub> c)))) \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> (\<forall>b. b \<in> f ` carrier A \<longrightarrow> a \<plusminus>\<^bsub>R\<^esub> b = b \<plusminus>\<^bsub>R\<^esub> a)) \<and> mop R \<in> f ` carrier A \<rightarrow> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> -\<^sub>a\<^bsub>R\<^esub> a \<plusminus>\<^bsub>R\<^esub> a = \<zero>\<^bsub>R\<^esub>) \<and> \<zero>\<^bsub>R\<^esub> \<in> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> (\<plusminus>\<^bsub>R\<^esub>) \<in> f ` carrier A \<rightarrow> f ` carrier A \<rightarrow> f ` carrier A
 2. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> (\<forall>b. b \<in> f ` carrier A \<longrightarrow> (\<forall>c. c \<in> f ` carrier A \<longrightarrow> a \<plusminus>\<^bsub>R\<^esub> b \<plusminus>\<^bsub>R\<^esub> c = a \<plusminus>\<^bsub>R\<^esub> (b \<plusminus>\<^bsub>R\<^esub> c)))) \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> (\<forall>b. b \<in> f ` carrier A \<longrightarrow> a \<plusminus>\<^bsub>R\<^esub> b = b \<plusminus>\<^bsub>R\<^esub> a)) \<and> mop R \<in> f ` carrier A \<rightarrow> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> -\<^sub>a\<^bsub>R\<^esub> a \<plusminus>\<^bsub>R\<^esub> a = \<zero>\<^bsub>R\<^esub>) \<and> \<zero>\<^bsub>R\<^esub> \<in> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a)
[PROOF STEP]
apply (rule Pi_I)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>; x \<in> f ` carrier A; xa \<in> f ` carrier A\<rbrakk> \<Longrightarrow> x \<plusminus>\<^bsub>R\<^esub> xa \<in> f ` carrier A
 2. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> (\<forall>b. b \<in> f ` carrier A \<longrightarrow> (\<forall>c. c \<in> f ` carrier A \<longrightarrow> a \<plusminus>\<^bsub>R\<^esub> b \<plusminus>\<^bsub>R\<^esub> c = a \<plusminus>\<^bsub>R\<^esub> (b \<plusminus>\<^bsub>R\<^esub> c)))) \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> (\<forall>b. b \<in> f ` carrier A \<longrightarrow> a \<plusminus>\<^bsub>R\<^esub> b = b \<plusminus>\<^bsub>R\<^esub> a)) \<and> mop R \<in> f ` carrier A \<rightarrow> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> -\<^sub>a\<^bsub>R\<^esub> a \<plusminus>\<^bsub>R\<^esub> a = \<zero>\<^bsub>R\<^esub>) \<and> \<zero>\<^bsub>R\<^esub> \<in> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a)
[PROOF STEP]
apply (simp add:image_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>; \<exists>xa\<in>carrier A. x = f xa; \<exists>x\<in>carrier A. xa = f x\<rbrakk> \<Longrightarrow> \<exists>xb\<in>carrier A. x \<plusminus>\<^bsub>R\<^esub> xa = f xb
 2. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> (\<forall>b. b \<in> f ` carrier A \<longrightarrow> (\<forall>c. c \<in> f ` carrier A \<longrightarrow> a \<plusminus>\<^bsub>R\<^esub> b \<plusminus>\<^bsub>R\<^esub> c = a \<plusminus>\<^bsub>R\<^esub> (b \<plusminus>\<^bsub>R\<^esub> c)))) \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> (\<forall>b. b \<in> f ` carrier A \<longrightarrow> a \<plusminus>\<^bsub>R\<^esub> b = b \<plusminus>\<^bsub>R\<^esub> a)) \<and> mop R \<in> f ` carrier A \<rightarrow> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> -\<^sub>a\<^bsub>R\<^esub> a \<plusminus>\<^bsub>R\<^esub> a = \<zero>\<^bsub>R\<^esub>) \<and> \<zero>\<^bsub>R\<^esub> \<in> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a)
[PROOF STEP]
apply (erule bexE)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa xb xc. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>; xb \<in> carrier A; x = f xb; xc \<in> carrier A; xa = f xc\<rbrakk> \<Longrightarrow> \<exists>xb\<in>carrier A. x \<plusminus>\<^bsub>R\<^esub> xa = f xb
 2. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> (\<forall>b. b \<in> f ` carrier A \<longrightarrow> (\<forall>c. c \<in> f ` carrier A \<longrightarrow> a \<plusminus>\<^bsub>R\<^esub> b \<plusminus>\<^bsub>R\<^esub> c = a \<plusminus>\<^bsub>R\<^esub> (b \<plusminus>\<^bsub>R\<^esub> c)))) \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> (\<forall>b. b \<in> f ` carrier A \<longrightarrow> a \<plusminus>\<^bsub>R\<^esub> b = b \<plusminus>\<^bsub>R\<^esub> a)) \<and> mop R \<in> f ` carrier A \<rightarrow> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> -\<^sub>a\<^bsub>R\<^esub> a \<plusminus>\<^bsub>R\<^esub> a = \<zero>\<^bsub>R\<^esub>) \<and> \<zero>\<^bsub>R\<^esub> \<in> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa xb xc. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>; xb \<in> carrier A; x = f xb; xc \<in> carrier A; xa = f xc\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier A. f xb \<plusminus>\<^bsub>R\<^esub> f xc = f x
 2. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> (\<forall>b. b \<in> f ` carrier A \<longrightarrow> (\<forall>c. c \<in> f ` carrier A \<longrightarrow> a \<plusminus>\<^bsub>R\<^esub> b \<plusminus>\<^bsub>R\<^esub> c = a \<plusminus>\<^bsub>R\<^esub> (b \<plusminus>\<^bsub>R\<^esub> c)))) \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> (\<forall>b. b \<in> f ` carrier A \<longrightarrow> a \<plusminus>\<^bsub>R\<^esub> b = b \<plusminus>\<^bsub>R\<^esub> a)) \<and> mop R \<in> f ` carrier A \<rightarrow> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> -\<^sub>a\<^bsub>R\<^esub> a \<plusminus>\<^bsub>R\<^esub> a = \<zero>\<^bsub>R\<^esub>) \<and> \<zero>\<^bsub>R\<^esub> \<in> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a)
[PROOF STEP]
apply (subst aHom_add [THEN sym, of "A" "R" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa xb xc. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>; xb \<in> carrier A; x = f xb; xc \<in> carrier A; xa = f xc\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier A. f (xb \<plusminus>\<^bsub>A\<^esub> xc) = f x
 2. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> (\<forall>b. b \<in> f ` carrier A \<longrightarrow> (\<forall>c. c \<in> f ` carrier A \<longrightarrow> a \<plusminus>\<^bsub>R\<^esub> b \<plusminus>\<^bsub>R\<^esub> c = a \<plusminus>\<^bsub>R\<^esub> (b \<plusminus>\<^bsub>R\<^esub> c)))) \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> (\<forall>b. b \<in> f ` carrier A \<longrightarrow> a \<plusminus>\<^bsub>R\<^esub> b = b \<plusminus>\<^bsub>R\<^esub> a)) \<and> mop R \<in> f ` carrier A \<rightarrow> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> -\<^sub>a\<^bsub>R\<^esub> a \<plusminus>\<^bsub>R\<^esub> a = \<zero>\<^bsub>R\<^esub>) \<and> \<zero>\<^bsub>R\<^esub> \<in> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a)
[PROOF STEP]
apply (blast dest: aGroup.ag_pOp_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> (\<forall>b. b \<in> f ` carrier A \<longrightarrow> (\<forall>c. c \<in> f ` carrier A \<longrightarrow> a \<plusminus>\<^bsub>R\<^esub> b \<plusminus>\<^bsub>R\<^esub> c = a \<plusminus>\<^bsub>R\<^esub> (b \<plusminus>\<^bsub>R\<^esub> c)))) \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> (\<forall>b. b \<in> f ` carrier A \<longrightarrow> a \<plusminus>\<^bsub>R\<^esub> b = b \<plusminus>\<^bsub>R\<^esub> a)) \<and> mop R \<in> f ` carrier A \<rightarrow> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> -\<^sub>a\<^bsub>R\<^esub> a \<plusminus>\<^bsub>R\<^esub> a = \<zero>\<^bsub>R\<^esub>) \<and> \<zero>\<^bsub>R\<^esub> \<in> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> f ` carrier A \<longrightarrow> (\<forall>b. b \<in> f ` carrier A \<longrightarrow> (\<forall>c. c \<in> f ` carrier A \<longrightarrow> a \<plusminus>\<^bsub>R\<^esub> b \<plusminus>\<^bsub>R\<^esub> c = a \<plusminus>\<^bsub>R\<^esub> (b \<plusminus>\<^bsub>R\<^esub> c)))
 2. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> (\<forall>b. b \<in> f ` carrier A \<longrightarrow> a \<plusminus>\<^bsub>R\<^esub> b = b \<plusminus>\<^bsub>R\<^esub> a)) \<and> mop R \<in> f ` carrier A \<rightarrow> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> -\<^sub>a\<^bsub>R\<^esub> a \<plusminus>\<^bsub>R\<^esub> a = \<zero>\<^bsub>R\<^esub>) \<and> \<zero>\<^bsub>R\<^esub> \<in> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a)
[PROOF STEP]
apply ((rule allI, rule impI)+, simp add:image_def, (erule bexE)+, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c x xa xb. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>; x \<in> carrier A; a = f x; xa \<in> carrier A; b = f xa; xb \<in> carrier A; c = f xb\<rbrakk> \<Longrightarrow> f x \<plusminus>\<^bsub>R\<^esub> f xa \<plusminus>\<^bsub>R\<^esub> f xb = f x \<plusminus>\<^bsub>R\<^esub> (f xa \<plusminus>\<^bsub>R\<^esub> f xb)
 2. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> (\<forall>b. b \<in> f ` carrier A \<longrightarrow> a \<plusminus>\<^bsub>R\<^esub> b = b \<plusminus>\<^bsub>R\<^esub> a)) \<and> mop R \<in> f ` carrier A \<rightarrow> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> -\<^sub>a\<^bsub>R\<^esub> a \<plusminus>\<^bsub>R\<^esub> a = \<zero>\<^bsub>R\<^esub>) \<and> \<zero>\<^bsub>R\<^esub> \<in> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a)
[PROOF STEP]
apply (frule_tac x = x and y = xa in aGroup.ag_pOp_closed, assumption+,
        frule_tac x = xa and y = xb in aGroup.ag_pOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c x xa xb. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>; x \<in> carrier A; a = f x; xa \<in> carrier A; b = f xa; xb \<in> carrier A; c = f xb; x \<plusminus>\<^bsub>A\<^esub> xa \<in> carrier A; xa \<plusminus>\<^bsub>A\<^esub> xb \<in> carrier A\<rbrakk> \<Longrightarrow> f x \<plusminus>\<^bsub>R\<^esub> f xa \<plusminus>\<^bsub>R\<^esub> f xb = f x \<plusminus>\<^bsub>R\<^esub> (f xa \<plusminus>\<^bsub>R\<^esub> f xb)
 2. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> (\<forall>b. b \<in> f ` carrier A \<longrightarrow> a \<plusminus>\<^bsub>R\<^esub> b = b \<plusminus>\<^bsub>R\<^esub> a)) \<and> mop R \<in> f ` carrier A \<rightarrow> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> -\<^sub>a\<^bsub>R\<^esub> a \<plusminus>\<^bsub>R\<^esub> a = \<zero>\<^bsub>R\<^esub>) \<and> \<zero>\<^bsub>R\<^esub> \<in> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a)
[PROOF STEP]
apply (simp add:aHom_add[of "A" "R" "f", THEN sym] aGroup.ag_pOp_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> (\<forall>b. b \<in> f ` carrier A \<longrightarrow> a \<plusminus>\<^bsub>R\<^esub> b = b \<plusminus>\<^bsub>R\<^esub> a)) \<and> mop R \<in> f ` carrier A \<rightarrow> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> -\<^sub>a\<^bsub>R\<^esub> a \<plusminus>\<^bsub>R\<^esub> a = \<zero>\<^bsub>R\<^esub>) \<and> \<zero>\<^bsub>R\<^esub> \<in> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> f ` carrier A \<longrightarrow> (\<forall>b. b \<in> f ` carrier A \<longrightarrow> a \<plusminus>\<^bsub>R\<^esub> b = b \<plusminus>\<^bsub>R\<^esub> a)
 2. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> mop R \<in> f ` carrier A \<rightarrow> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> -\<^sub>a\<^bsub>R\<^esub> a \<plusminus>\<^bsub>R\<^esub> a = \<zero>\<^bsub>R\<^esub>) \<and> \<zero>\<^bsub>R\<^esub> \<in> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a)
[PROOF STEP]
apply ((rule allI, rule impI)+, simp add:image_def, (erule bexE)+, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b x xa. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>; x \<in> carrier A; a = f x; xa \<in> carrier A; b = f xa\<rbrakk> \<Longrightarrow> f x \<plusminus>\<^bsub>R\<^esub> f xa = f xa \<plusminus>\<^bsub>R\<^esub> f x
 2. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> mop R \<in> f ` carrier A \<rightarrow> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> -\<^sub>a\<^bsub>R\<^esub> a \<plusminus>\<^bsub>R\<^esub> a = \<zero>\<^bsub>R\<^esub>) \<and> \<zero>\<^bsub>R\<^esub> \<in> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a)
[PROOF STEP]
apply (simp add:aHom_add[of "A" "R" "f", THEN sym] aGroup.ag_pOp_commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> mop R \<in> f ` carrier A \<rightarrow> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> -\<^sub>a\<^bsub>R\<^esub> a \<plusminus>\<^bsub>R\<^esub> a = \<zero>\<^bsub>R\<^esub>) \<and> \<zero>\<^bsub>R\<^esub> \<in> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> mop R \<in> f ` carrier A \<rightarrow> f ` carrier A
 2. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> -\<^sub>a\<^bsub>R\<^esub> a \<plusminus>\<^bsub>R\<^esub> a = \<zero>\<^bsub>R\<^esub>) \<and> \<zero>\<^bsub>R\<^esub> \<in> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a)
[PROOF STEP]
apply (rule Pi_I)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>; x \<in> f ` carrier A\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>R\<^esub> x \<in> f ` carrier A
 2. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> -\<^sub>a\<^bsub>R\<^esub> a \<plusminus>\<^bsub>R\<^esub> a = \<zero>\<^bsub>R\<^esub>) \<and> \<zero>\<^bsub>R\<^esub> \<in> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a)
[PROOF STEP]
apply (simp add:image_def, erule bexE, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>; xa \<in> carrier A; x = f xa\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier A. -\<^sub>a\<^bsub>R\<^esub> f xa = f x
 2. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> -\<^sub>a\<^bsub>R\<^esub> a \<plusminus>\<^bsub>R\<^esub> a = \<zero>\<^bsub>R\<^esub>) \<and> \<zero>\<^bsub>R\<^esub> \<in> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a)
[PROOF STEP]
apply (simp add:aHom_inv_inv[THEN sym],
        frule_tac x = xa in aGroup.ag_mOp_closed[of "A"], assumption+, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> -\<^sub>a\<^bsub>R\<^esub> a \<plusminus>\<^bsub>R\<^esub> a = \<zero>\<^bsub>R\<^esub>) \<and> \<zero>\<^bsub>R\<^esub> \<in> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> f ` carrier A \<longrightarrow> -\<^sub>a\<^bsub>R\<^esub> a \<plusminus>\<^bsub>R\<^esub> a = \<zero>\<^bsub>R\<^esub>
 2. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>R\<^esub> \<in> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a)
[PROOF STEP]
apply (rule allI, rule impI, simp add:image_def, (erule bexE)+, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a x. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>; x \<in> carrier A; a = f x\<rbrakk> \<Longrightarrow> -\<^sub>a\<^bsub>R\<^esub> f x \<plusminus>\<^bsub>R\<^esub> f x = \<zero>\<^bsub>R\<^esub>
 2. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>R\<^esub> \<in> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a)
[PROOF STEP]
apply (simp add:aHom_inv_inv[THEN sym],
        frule_tac x = x in aGroup.ag_mOp_closed[of "A"], assumption+,
        simp add:aHom_add[of "A" "R" "f", THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a x. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>; x \<in> carrier A; a = f x; -\<^sub>a\<^bsub>A\<^esub> x \<in> carrier A\<rbrakk> \<Longrightarrow> f (-\<^sub>a\<^bsub>A\<^esub> x \<plusminus>\<^bsub>A\<^esub> x) = \<zero>\<^bsub>R\<^esub>
 2. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>R\<^esub> \<in> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a)
[PROOF STEP]
apply (simp add:aGroup.ag_l_inv1 aHom_0_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>R\<^esub> \<in> f ` carrier A \<and> (\<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>R\<^esub> \<in> f ` carrier A
 2. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a
[PROOF STEP]
apply (simp add:image_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier A. \<zero>\<^bsub>R\<^esub> = f x
 2. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a
[PROOF STEP]
apply (frule aHom_0_0[THEN sym, of "A" "R" "f"], assumption+,
        frule Ring.ring_zero[of "A"], blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> f ` carrier A \<longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> a = a
[PROOF STEP]
apply (rule allI, rule impI,
       simp add:image_def, erule bexE,
       frule_tac a = x in aHom_mem[of "A" "R" "f"], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a x. \<lbrakk>Ring A; Ring R; aGroup A; aGroup R; f \<in> aHom A R; \<forall>x\<in>carrier A. \<forall>y\<in>carrier A. f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> y) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f y; f 1\<^sub>r\<^bsub>A\<^esub> = 1\<^sub>r\<^bsub>R\<^esub>; x \<in> carrier A; a = f x; f x \<in> carrier R\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>R\<^esub> \<plusminus>\<^bsub>R\<^esub> f x = f x
[PROOF STEP]
apply (simp add:aGroup.ag_l_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rimg_ring:"\<lbrakk>Ring A; Ring R; f \<in> rHom A R \<rbrakk> \<Longrightarrow> Ring (rimg A R f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> Ring (rimg A R f)
[PROOF STEP]
apply (unfold Ring_def [of "rimg A R f"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> (((\<plusminus>\<^bsub>rimg A R f\<^esub>) \<in> carrier (rimg A R f) \<rightarrow> carrier (rimg A R f) \<rightarrow> carrier (rimg A R f) \<and> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<plusminus>\<^bsub>rimg A R f\<^esub> b \<plusminus>\<^bsub>rimg A R f\<^esub> c = a \<plusminus>\<^bsub>rimg A R f\<^esub> (b \<plusminus>\<^bsub>rimg A R f\<^esub> c)) \<and> (\<forall>a b. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> a \<plusminus>\<^bsub>rimg A R f\<^esub> b = b \<plusminus>\<^bsub>rimg A R f\<^esub> a)) \<and> mop (rimg A R f) \<in> carrier (rimg A R f) \<rightarrow> carrier (rimg A R f) \<and> (\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> -\<^sub>a\<^bsub>rimg A R f\<^esub> a \<plusminus>\<^bsub>rimg A R f\<^esub> a = \<zero>\<^bsub>rimg A R f\<^esub>) \<and> \<zero>\<^bsub>rimg A R f\<^esub> \<in> carrier (rimg A R f)) \<and> ((\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> \<zero>\<^bsub>rimg A R f\<^esub> \<plusminus>\<^bsub>rimg A R f\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub>) \<in> carrier (rimg A R f) \<rightarrow> carrier (rimg A R f) \<rightarrow> carrier (rimg A R f) \<and> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c))) \<and> ((\<forall>a b. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b = b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a) \<and> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<in> carrier (rimg A R f)) \<and> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<plusminus>\<^bsub>rimg A R f\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<plusminus>\<^bsub>rimg A R f\<^esub> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c) \<and> (\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a = a)
[PROOF STEP]
apply (frule rimg_ag[of "A" "R" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> (((\<plusminus>\<^bsub>rimg A R f\<^esub>) \<in> carrier (rimg A R f) \<rightarrow> carrier (rimg A R f) \<rightarrow> carrier (rimg A R f) \<and> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<plusminus>\<^bsub>rimg A R f\<^esub> b \<plusminus>\<^bsub>rimg A R f\<^esub> c = a \<plusminus>\<^bsub>rimg A R f\<^esub> (b \<plusminus>\<^bsub>rimg A R f\<^esub> c)) \<and> (\<forall>a b. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> a \<plusminus>\<^bsub>rimg A R f\<^esub> b = b \<plusminus>\<^bsub>rimg A R f\<^esub> a)) \<and> mop (rimg A R f) \<in> carrier (rimg A R f) \<rightarrow> carrier (rimg A R f) \<and> (\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> -\<^sub>a\<^bsub>rimg A R f\<^esub> a \<plusminus>\<^bsub>rimg A R f\<^esub> a = \<zero>\<^bsub>rimg A R f\<^esub>) \<and> \<zero>\<^bsub>rimg A R f\<^esub> \<in> carrier (rimg A R f)) \<and> ((\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> \<zero>\<^bsub>rimg A R f\<^esub> \<plusminus>\<^bsub>rimg A R f\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub>) \<in> carrier (rimg A R f) \<rightarrow> carrier (rimg A R f) \<rightarrow> carrier (rimg A R f) \<and> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c))) \<and> ((\<forall>a b. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b = b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a) \<and> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<in> carrier (rimg A R f)) \<and> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<plusminus>\<^bsub>rimg A R f\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<plusminus>\<^bsub>rimg A R f\<^esub> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c) \<and> (\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a = a)
[PROOF STEP]
apply (rule conjI, simp add:aGroup_def[of "rimg A R f"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> ((\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> \<zero>\<^bsub>rimg A R f\<^esub> \<plusminus>\<^bsub>rimg A R f\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub>) \<in> carrier (rimg A R f) \<rightarrow> carrier (rimg A R f) \<rightarrow> carrier (rimg A R f) \<and> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c))) \<and> ((\<forall>a b. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b = b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a) \<and> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<in> carrier (rimg A R f)) \<and> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<plusminus>\<^bsub>rimg A R f\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<plusminus>\<^bsub>rimg A R f\<^esub> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c) \<and> (\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a = a)
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> (\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> \<zero>\<^bsub>rimg A R f\<^esub> \<plusminus>\<^bsub>rimg A R f\<^esub> a = a) \<and> (\<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub>) \<in> carrier (rimg A R f) \<rightarrow> carrier (rimg A R f) \<rightarrow> carrier (rimg A R f) \<and> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c))
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> ((\<forall>a b. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b = b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a) \<and> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<in> carrier (rimg A R f)) \<and> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<plusminus>\<^bsub>rimg A R f\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<plusminus>\<^bsub>rimg A R f\<^esub> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c) \<and> (\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a = a)
[PROOF STEP]
apply (rule conjI, rule allI, rule impI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f); a \<in> carrier (rimg A R f)\<rbrakk> \<Longrightarrow> \<zero>\<^bsub>rimg A R f\<^esub> \<plusminus>\<^bsub>rimg A R f\<^esub> a = a
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> (\<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub>) \<in> carrier (rimg A R f) \<rightarrow> carrier (rimg A R f) \<rightarrow> carrier (rimg A R f) \<and> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c))
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> ((\<forall>a b. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b = b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a) \<and> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<in> carrier (rimg A R f)) \<and> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<plusminus>\<^bsub>rimg A R f\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<plusminus>\<^bsub>rimg A R f\<^esub> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c) \<and> (\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a = a)
[PROOF STEP]
apply (frule aGroup.ag_inc_zero[of "rimg A R f"],
        subst aGroup.ag_pOp_commute, assumption+,
        simp add:aGroup.ag_r_zero[of "rimg A R f"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> (\<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub>) \<in> carrier (rimg A R f) \<rightarrow> carrier (rimg A R f) \<rightarrow> carrier (rimg A R f) \<and> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c))
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> ((\<forall>a b. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b = b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a) \<and> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<in> carrier (rimg A R f)) \<and> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<plusminus>\<^bsub>rimg A R f\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<plusminus>\<^bsub>rimg A R f\<^esub> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c) \<and> (\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a = a)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> (\<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub>) \<in> carrier (rimg A R f) \<rightarrow> carrier (rimg A R f) \<rightarrow> carrier (rimg A R f)
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> \<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c)
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> ((\<forall>a b. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b = b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a) \<and> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<in> carrier (rimg A R f)) \<and> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<plusminus>\<^bsub>rimg A R f\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<plusminus>\<^bsub>rimg A R f\<^esub> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c) \<and> (\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a = a)
[PROOF STEP]
apply (rule Pi_I)+
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f); x \<in> carrier (rimg A R f); xa \<in> carrier (rimg A R f)\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> xa \<in> carrier (rimg A R f)
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> \<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c)
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> ((\<forall>a b. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b = b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a) \<and> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<in> carrier (rimg A R f)) \<and> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<plusminus>\<^bsub>rimg A R f\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<plusminus>\<^bsub>rimg A R f\<^esub> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c) \<and> (\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a = a)
[PROOF STEP]
apply (thin_tac "aGroup (rimg A R f)",
       simp add:rimg_def, simp add:image_def, (erule bexE)+,
       simp add:rHom_tOp[THEN sym])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa xb xc. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; xb \<in> carrier A; x = f xb; xc \<in> carrier A; xa = f xc\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier A. f (xb \<cdot>\<^sub>r\<^bsub>A\<^esub> xc) = f x
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> \<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c)
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> ((\<forall>a b. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b = b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a) \<and> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<in> carrier (rimg A R f)) \<and> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<plusminus>\<^bsub>rimg A R f\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<plusminus>\<^bsub>rimg A R f\<^esub> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c) \<and> (\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a = a)
[PROOF STEP]
apply (blast dest:Ring.ring_tOp_closed)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> \<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c)
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> ((\<forall>a b. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b = b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a) \<and> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<in> carrier (rimg A R f)) \<and> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<plusminus>\<^bsub>rimg A R f\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<plusminus>\<^bsub>rimg A R f\<^esub> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c) \<and> (\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a = a)
[PROOF STEP]
apply ((rule allI)+, (rule impI)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f); a \<in> carrier (rimg A R f); b \<in> carrier (rimg A R f); c \<in> carrier (rimg A R f)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c)
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> ((\<forall>a b. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b = b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a) \<and> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<in> carrier (rimg A R f)) \<and> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<plusminus>\<^bsub>rimg A R f\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<plusminus>\<^bsub>rimg A R f\<^esub> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c) \<and> (\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a = a)
[PROOF STEP]
apply (thin_tac "aGroup (rimg A R f)", simp add:rimg_def,
        simp add:image_def, (erule bexE)+, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c x xa xb. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; x \<in> carrier A; a = f x; xa \<in> carrier A; b = f xa; xb \<in> carrier A; c = f xb\<rbrakk> \<Longrightarrow> f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f xa \<cdot>\<^sub>r\<^bsub>R\<^esub> f xb = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f xa \<cdot>\<^sub>r\<^bsub>R\<^esub> f xb)
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> ((\<forall>a b. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b = b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a) \<and> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<in> carrier (rimg A R f)) \<and> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<plusminus>\<^bsub>rimg A R f\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<plusminus>\<^bsub>rimg A R f\<^esub> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c) \<and> (\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a = a)
[PROOF STEP]
apply (frule_tac x = x and y = xa in Ring.ring_tOp_closed, assumption+,
        frule_tac x = xa and y = xb in Ring.ring_tOp_closed, assumption+,
        simp add:rHom_tOp[THEN sym],
        simp add:Ring.ring_tOp_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> ((\<forall>a b. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b = b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a) \<and> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<in> carrier (rimg A R f)) \<and> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<plusminus>\<^bsub>rimg A R f\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<plusminus>\<^bsub>rimg A R f\<^esub> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c) \<and> (\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a = a)
[PROOF STEP]
apply (rule conjI, rule conjI, (rule allI)+, (rule impI)+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f); a \<in> carrier (rimg A R f); b \<in> carrier (rimg A R f)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b = b \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<in> carrier (rimg A R f)
 3. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<plusminus>\<^bsub>rimg A R f\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<plusminus>\<^bsub>rimg A R f\<^esub> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c) \<and> (\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a = a)
[PROOF STEP]
apply (thin_tac "aGroup (rimg A R f)", simp add:rimg_def,
        simp add:image_def, (erule bexE)+, simp,
        simp add:rHom_tOp[THEN sym],
        simp add:Ring.ring_tOp_commute)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<in> carrier (rimg A R f)
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<plusminus>\<^bsub>rimg A R f\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<plusminus>\<^bsub>rimg A R f\<^esub> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c) \<and> (\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a = a)
[PROOF STEP]
apply (thin_tac "aGroup (rimg A R f)", simp add:rimg_def,
         simp add:image_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R\<rbrakk> \<Longrightarrow> \<exists>x\<in>carrier A. 1\<^sub>r\<^bsub>R\<^esub> = f x
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<plusminus>\<^bsub>rimg A R f\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<plusminus>\<^bsub>rimg A R f\<^esub> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c) \<and> (\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a = a)
[PROOF STEP]
apply (subst rHom_one [THEN sym, of "A" "R" "f"], assumption+,
         frule Ring.ring_one[of "A"], blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> (\<forall>a b c. a \<in> carrier (rimg A R f) \<longrightarrow> b \<in> carrier (rimg A R f) \<longrightarrow> c \<in> carrier (rimg A R f) \<longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<plusminus>\<^bsub>rimg A R f\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<plusminus>\<^bsub>rimg A R f\<^esub> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c) \<and> (\<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a = a)
[PROOF STEP]
apply (rule conjI, (rule allI)+, (rule impI)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f); a \<in> carrier (rimg A R f); b \<in> carrier (rimg A R f); c \<in> carrier (rimg A R f)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> (b \<plusminus>\<^bsub>rimg A R f\<^esub> c) = a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> b \<plusminus>\<^bsub>rimg A R f\<^esub> a \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> c
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a = a
[PROOF STEP]
apply (simp add:rimg_def, fold rimg_def,
       simp add:image_def, (erule bexE)+, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c x xa xb. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f); x \<in> carrier A; a = f x; xa \<in> carrier A; b = f xa; xb \<in> carrier A; c = f xb\<rbrakk> \<Longrightarrow> f x \<cdot>\<^sub>r\<^bsub>R\<^esub> (f xa \<plusminus>\<^bsub>R\<^esub> f xb) = f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f xa \<plusminus>\<^bsub>R\<^esub> f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f xb
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a = a
[PROOF STEP]
apply (frule rHom_aHom[of "f" "A" "R"],
        frule Ring.ring_is_ag [of "A"],
        frule Ring.ring_is_ag [of "R"],
        simp add:aHom_add[THEN sym],
        simp add:rHom_tOp[THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c x xa xb. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f); x \<in> carrier A; a = f x; xa \<in> carrier A; b = f xa; xb \<in> carrier A; c = f xb; f \<in> aHom A R; aGroup A; aGroup R\<rbrakk> \<Longrightarrow> f x \<cdot>\<^sub>r\<^bsub>R\<^esub> f (xa \<plusminus>\<^bsub>A\<^esub> xb) = f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> xa) \<plusminus>\<^bsub>R\<^esub> f (x \<cdot>\<^sub>r\<^bsub>A\<^esub> xb)
 2. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a = a
[PROOF STEP]
apply (frule_tac x = xa and y = xb in aGroup.ag_pOp_closed[of "A"],
          assumption+,
        frule_tac x = x and y = xa in Ring.ring_tOp_closed[of "A"],
          assumption+,
        frule_tac x = x and y = xb in Ring.ring_tOp_closed[of "A"],
          assumption+,
        simp add:aHom_add[THEN sym],
        simp add:rHom_tOp[THEN sym],
        simp add:Ring.ring_distrib1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; aGroup (rimg A R f)\<rbrakk> \<Longrightarrow> \<forall>a. a \<in> carrier (rimg A R f) \<longrightarrow> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a = a
[PROOF STEP]
apply (rule allI, rule impI,
        thin_tac "aGroup (rimg A R f)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>Ring A; Ring R; f \<in> rHom A R; a \<in> carrier (rimg A R f)\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>rimg A R f\<^esub> \<cdot>\<^sub>r\<^bsub>rimg A R f\<^esub> a = a
[PROOF STEP]
apply (simp add:rimg_def,
        simp add:image_def, erule bexE, simp add:rHom_tOp[THEN sym],
        frule_tac a = x in rHom_mem[of "f" "A" "R"], assumption+,
         simp add:Ring.ring_l_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_asubg:"ideal R I \<Longrightarrow> R +> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> R +> I
[PROOF STEP]
by (simp add:ideal_def)


[STATEMENT]
lemma (in Ring) ideal_pOp_closed:"\<lbrakk>ideal R I; x \<in> I; y \<in> I \<rbrakk>
                                                   \<Longrightarrow> x \<plusminus> y \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; x \<in> I; y \<in> I\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> I
[PROOF STEP]
apply (unfold ideal_def, frule conjunct1, fold ideal_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; x \<in> I; y \<in> I; R +> I\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> I
[PROOF STEP]
apply (cut_tac ring_is_ag,
       simp add:aGroup.asubg_pOp_closed)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_nsum_closedTr:"ideal R I \<Longrightarrow>
                                      (\<forall>j \<le> n. f j \<in> I) \<longrightarrow>  nsum R f n \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> (\<forall>j\<le>n. f j \<in> I) \<longrightarrow> \<Sigma>\<^sub>e R f n \<in> I
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ideal R I \<Longrightarrow> (\<forall>j\<le>0. f j \<in> I) \<longrightarrow> \<Sigma>\<^sub>e R f 0 \<in> I
 2. \<And>n. \<lbrakk>ideal R I; (\<forall>j\<le>n. f j \<in> I) \<longrightarrow> \<Sigma>\<^sub>e R f n \<in> I\<rbrakk> \<Longrightarrow> (\<forall>j\<le>Suc n. f j \<in> I) \<longrightarrow> \<Sigma>\<^sub>e R f Suc n \<in> I
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ideal R I; \<forall>j\<le>0. f j \<in> I\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f 0 \<in> I
 2. \<And>n. \<lbrakk>ideal R I; (\<forall>j\<le>n. f j \<in> I) \<longrightarrow> \<Sigma>\<^sub>e R f n \<in> I\<rbrakk> \<Longrightarrow> (\<forall>j\<le>Suc n. f j \<in> I) \<longrightarrow> \<Sigma>\<^sub>e R f Suc n \<in> I
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>ideal R I; (\<forall>j\<le>n. f j \<in> I) \<longrightarrow> \<Sigma>\<^sub>e R f n \<in> I\<rbrakk> \<Longrightarrow> (\<forall>j\<le>Suc n. f j \<in> I) \<longrightarrow> \<Sigma>\<^sub>e R f Suc n \<in> I
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>ideal R I; (\<forall>j\<le>n. f j \<in> I) \<longrightarrow> \<Sigma>\<^sub>e R f n \<in> I; \<forall>j\<le>Suc n. f j \<in> I\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f Suc n \<in> I
[PROOF STEP]
apply (cut_tac n = n in Nsetn_sub_mem1, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>ideal R I; \<Sigma>\<^sub>e R f n \<in> I; \<forall>j\<le>Suc n. f j \<in> I\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f n \<plusminus> f (Suc n) \<in> I
[PROOF STEP]
apply (rule ideal_pOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>ideal R I; \<Sigma>\<^sub>e R f n \<in> I; \<forall>j\<le>Suc n. f j \<in> I\<rbrakk> \<Longrightarrow> f (Suc n) \<in> I
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_nsum_closed:"\<lbrakk>ideal R I; \<forall>j \<le> n. f j \<in> I\<rbrakk> \<Longrightarrow>
                                             nsum R f n \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; \<forall>j\<le>n. f j \<in> I\<rbrakk> \<Longrightarrow> \<Sigma>\<^sub>e R f n \<in> I
[PROOF STEP]
by (simp add:ideal_nsum_closedTr)


[STATEMENT]
lemma (in Ring) ideal_subset1:"ideal R I \<Longrightarrow> I \<subseteq> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> I \<subseteq> carrier R
[PROOF STEP]
apply (unfold ideal_def, frule conjunct1, fold ideal_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; R +> I\<rbrakk> \<Longrightarrow> I \<subseteq> carrier R
[PROOF STEP]
apply (simp add:asubGroup_def sg_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; I \<noteq> {}; I \<subseteq> carrier (b_ag R); \<forall>a\<in>I. \<forall>b\<in>I. a \<cdot>\<^bsub>b_ag R\<^esub> \<rho>\<^bsub>b_ag R\<^esub> b \<in> I\<rbrakk> \<Longrightarrow> I \<subseteq> carrier R
[PROOF STEP]
apply (cut_tac ring_is_ag,
         simp add:aGroup.ag_carrier_carrier)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_subset:"\<lbrakk>ideal R I; h \<in> I\<rbrakk> \<Longrightarrow> h \<in> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; h \<in> I\<rbrakk> \<Longrightarrow> h \<in> carrier R
[PROOF STEP]
by (frule ideal_subset1[of "I"],
       simp add:subsetD)


[STATEMENT]
lemma (in Ring) ideal_ring_multiple:"\<lbrakk>ideal R I; x \<in> I; r \<in> carrier R\<rbrakk> \<Longrightarrow>
       r \<cdot>\<^sub>r x \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; x \<in> I; r \<in> carrier R\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r x \<in> I
[PROOF STEP]
by (simp add:ideal_def)


[STATEMENT]
lemma (in Ring) ideal_ring_multiple1:"\<lbrakk>ideal R I; x \<in> I; r \<in> carrier R \<rbrakk> \<Longrightarrow>
       x \<cdot>\<^sub>r r \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; x \<in> I; r \<in> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r r \<in> I
[PROOF STEP]
apply (frule ideal_subset[of "I" "x"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; x \<in> I; r \<in> carrier R; x \<in> carrier R\<rbrakk> \<Longrightarrow> x \<cdot>\<^sub>r r \<in> I
[PROOF STEP]
apply (simp add:ring_tOp_commute ideal_ring_multiple)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_npow_closedTr:"\<lbrakk>ideal R I; x \<in> I\<rbrakk> \<Longrightarrow>
                                        0 < n \<longrightarrow> x^\<^bsup>R n\<^esup> \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; x \<in> I\<rbrakk> \<Longrightarrow> 0 < n \<longrightarrow> x^\<^bsup>R n\<^esup> \<in> I
[PROOF STEP]
apply (induct_tac n,
       simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>ideal R I; x \<in> I; 0 < n \<longrightarrow> x^\<^bsup>R n\<^esup> \<in> I\<rbrakk> \<Longrightarrow> 0 < Suc n \<longrightarrow> x^\<^bsup>R Suc n\<^esup> \<in> I
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>ideal R I; x \<in> I; 0 < n \<longrightarrow> x^\<^bsup>R n\<^esup> \<in> I; 0 < Suc n\<rbrakk> \<Longrightarrow> x^\<^bsup>R Suc n\<^esup> \<in> I
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>ideal R I; x \<in> I; 0 < n \<longrightarrow> x^\<^bsup>R n\<^esup> \<in> I\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x \<in> I
[PROOF STEP]
apply (case_tac "n = 0", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>ideal R I; x \<in> I; n = 0\<rbrakk> \<Longrightarrow> 1\<^sub>r \<cdot>\<^sub>r x \<in> I
 2. \<And>n. \<lbrakk>ideal R I; x \<in> I; 0 < n \<longrightarrow> x^\<^bsup>R n\<^esup> \<in> I; n \<noteq> 0\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x \<in> I
[PROOF STEP]
apply (frule ideal_subset[of "I" "x"], assumption+,
        simp add:ring_l_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>ideal R I; x \<in> I; 0 < n \<longrightarrow> x^\<^bsup>R n\<^esup> \<in> I; n \<noteq> 0\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x \<in> I
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>ideal R I; x \<in> I; x^\<^bsup>R n\<^esup> \<in> I; 0 < n\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> \<cdot>\<^sub>r x \<in> I
[PROOF STEP]
apply (frule ideal_subset[of "I" "x"], assumption+,
       rule ideal_ring_multiple, assumption+,
       simp add:ideal_subset)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_npow_closed:"\<lbrakk>ideal R I; x \<in> I; 0 < n\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; x \<in> I; 0 < n\<rbrakk> \<Longrightarrow> x^\<^bsup>R n\<^esup> \<in> I
[PROOF STEP]
by (simp add:ideal_npow_closedTr)


[STATEMENT]
lemma (in Ring) times_modTr:"\<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R;
 b' \<in> carrier R; ideal R I; a \<plusminus> (-\<^sub>a b) \<in> I; a' \<plusminus> (-\<^sub>a b') \<in> I\<rbrakk> \<Longrightarrow>
                           a \<cdot>\<^sub>r a' \<plusminus> (-\<^sub>a (b \<cdot>\<^sub>r b')) \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b' \<in> I
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b' \<in> I
[PROOF STEP]
apply (subgoal_tac "a \<cdot>\<^sub>r a' \<plusminus> (-\<^sub>a (b \<cdot>\<^sub>r b')) = a \<cdot>\<^sub>r a' \<plusminus> (-\<^sub>a (a \<cdot>\<^sub>r b'))
                       \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> (-\<^sub>a (b \<cdot>\<^sub>r b')))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R; a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b' = a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b' \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b')\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b' \<in> I
 2. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b' = a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b' \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R; a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b' = a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b' \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b')\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b' \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b') \<in> I
 2. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b' = a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b' \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b')
[PROOF STEP]
apply (simp add:ring_inv1_2[of "a" "b'"], simp add:ring_inv1_1[of "b" "b'"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R; a \<cdot>\<^sub>r a' \<plusminus> (-\<^sub>a b) \<cdot>\<^sub>r b' = a \<cdot>\<^sub>r a' \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a b') \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> (-\<^sub>a b) \<cdot>\<^sub>r b')\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r a' \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a b') \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> (-\<^sub>a b) \<cdot>\<^sub>r b') \<in> I
 2. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b' = a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b' \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b')
[PROOF STEP]
apply (frule aGroup.ag_mOp_closed[of "R" "b'"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R; a \<cdot>\<^sub>r a' \<plusminus> (-\<^sub>a b) \<cdot>\<^sub>r b' = a \<cdot>\<^sub>r a' \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a b') \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> (-\<^sub>a b) \<cdot>\<^sub>r b'); -\<^sub>a b' \<in> carrier R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r a' \<plusminus> a \<cdot>\<^sub>r (-\<^sub>a b') \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> (-\<^sub>a b) \<cdot>\<^sub>r b') \<in> I
 2. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b' = a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b' \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b')
[PROOF STEP]
apply (simp add:ring_distrib1[THEN sym, of "a" "a'" "-\<^sub>a b'"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R; a \<cdot>\<^sub>r a' \<plusminus> (-\<^sub>a b) \<cdot>\<^sub>r b' = a \<cdot>\<^sub>r (a' \<plusminus> -\<^sub>a b') \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> (-\<^sub>a b) \<cdot>\<^sub>r b'); -\<^sub>a b' \<in> carrier R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r (a' \<plusminus> -\<^sub>a b') \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> (-\<^sub>a b) \<cdot>\<^sub>r b') \<in> I
 2. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b' = a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b' \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b')
[PROOF STEP]
apply (frule aGroup.ag_mOp_closed[of "R" "b"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R; a \<cdot>\<^sub>r a' \<plusminus> (-\<^sub>a b) \<cdot>\<^sub>r b' = a \<cdot>\<^sub>r (a' \<plusminus> -\<^sub>a b') \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> (-\<^sub>a b) \<cdot>\<^sub>r b'); -\<^sub>a b' \<in> carrier R; -\<^sub>a b \<in> carrier R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r (a' \<plusminus> -\<^sub>a b') \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> (-\<^sub>a b) \<cdot>\<^sub>r b') \<in> I
 2. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b' = a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b' \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b')
[PROOF STEP]
apply (frule ring_distrib2[THEN sym, of "b'" "a" "-\<^sub>a b" ], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R; a \<cdot>\<^sub>r a' \<plusminus> (-\<^sub>a b) \<cdot>\<^sub>r b' = a \<cdot>\<^sub>r (a' \<plusminus> -\<^sub>a b') \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> (-\<^sub>a b) \<cdot>\<^sub>r b'); -\<^sub>a b' \<in> carrier R; -\<^sub>a b \<in> carrier R; a \<cdot>\<^sub>r b' \<plusminus> (-\<^sub>a b) \<cdot>\<^sub>r b' = (a \<plusminus> -\<^sub>a b) \<cdot>\<^sub>r b'\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r (a' \<plusminus> -\<^sub>a b') \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> (-\<^sub>a b) \<cdot>\<^sub>r b') \<in> I
 2. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b' = a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b' \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R; a \<cdot>\<^sub>r a' \<plusminus> (-\<^sub>a b) \<cdot>\<^sub>r b' = a \<cdot>\<^sub>r (a' \<plusminus> -\<^sub>a b') \<plusminus> (a \<plusminus> -\<^sub>a b) \<cdot>\<^sub>r b'; -\<^sub>a b' \<in> carrier R; -\<^sub>a b \<in> carrier R; a \<cdot>\<^sub>r b' \<plusminus> (-\<^sub>a b) \<cdot>\<^sub>r b' = (a \<plusminus> -\<^sub>a b) \<cdot>\<^sub>r b'\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r (a' \<plusminus> -\<^sub>a b') \<plusminus> (a \<plusminus> -\<^sub>a b) \<cdot>\<^sub>r b' \<in> I
 2. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b' = a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b' \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b')
[PROOF STEP]
apply (thin_tac "a \<cdot>\<^sub>r a' \<plusminus> (-\<^sub>a b) \<cdot>\<^sub>r b' = a \<cdot>\<^sub>r (a' \<plusminus> -\<^sub>a b') \<plusminus> (a \<plusminus> -\<^sub>a b) \<cdot>\<^sub>r b'",
       thin_tac "a \<cdot>\<^sub>r b' \<plusminus> (-\<^sub>a b) \<cdot>\<^sub>r b' = (a \<plusminus> -\<^sub>a b) \<cdot>\<^sub>r b'")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R; -\<^sub>a b' \<in> carrier R; -\<^sub>a b \<in> carrier R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r (a' \<plusminus> -\<^sub>a b') \<plusminus> (a \<plusminus> -\<^sub>a b) \<cdot>\<^sub>r b' \<in> I
 2. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b' = a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b' \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b')
[PROOF STEP]
apply (frule ideal_ring_multiple[of "I" "a' \<plusminus> (-\<^sub>a b')" "a"], assumption+,
        frule ideal_ring_multiple1[of "I" "a \<plusminus> (-\<^sub>a b)" "b'"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R; -\<^sub>a b' \<in> carrier R; -\<^sub>a b \<in> carrier R; a \<cdot>\<^sub>r (a' \<plusminus> -\<^sub>a b') \<in> I; (a \<plusminus> -\<^sub>a b) \<cdot>\<^sub>r b' \<in> I\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r (a' \<plusminus> -\<^sub>a b') \<plusminus> (a \<plusminus> -\<^sub>a b) \<cdot>\<^sub>r b' \<in> I
 2. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b' = a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b' \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b')
[PROOF STEP]
apply (simp add:ideal_pOp_closed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b' = a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b' \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b')
[PROOF STEP]
apply (frule ring_tOp_closed[of "a" "a'"], assumption+,
       frule ring_tOp_closed[of "a" "b'"], assumption+,
       frule ring_tOp_closed[of "b" "b'"], assumption+,
       frule aGroup.ag_mOp_closed[of "R" "b \<cdot>\<^sub>r b'"], assumption+,
       frule aGroup.ag_mOp_closed[of "R" "a \<cdot>\<^sub>r b'"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R; a \<cdot>\<^sub>r a' \<in> carrier R; a \<cdot>\<^sub>r b' \<in> carrier R; b \<cdot>\<^sub>r b' \<in> carrier R; -\<^sub>a b \<cdot>\<^sub>r b' \<in> carrier R; -\<^sub>a a \<cdot>\<^sub>r b' \<in> carrier R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b' = a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a a \<cdot>\<^sub>r b' \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b')
[PROOF STEP]
apply (subst aGroup.ag_pOp_assoc[of "R"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R; a \<cdot>\<^sub>r a' \<in> carrier R; a \<cdot>\<^sub>r b' \<in> carrier R; b \<cdot>\<^sub>r b' \<in> carrier R; -\<^sub>a b \<cdot>\<^sub>r b' \<in> carrier R; -\<^sub>a a \<cdot>\<^sub>r b' \<in> carrier R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r b' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b' \<in> carrier R
 2. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R; a \<cdot>\<^sub>r a' \<in> carrier R; a \<cdot>\<^sub>r b' \<in> carrier R; b \<cdot>\<^sub>r b' \<in> carrier R; -\<^sub>a b \<cdot>\<^sub>r b' \<in> carrier R; -\<^sub>a a \<cdot>\<^sub>r b' \<in> carrier R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b' = a \<cdot>\<^sub>r a' \<plusminus> (-\<^sub>a a \<cdot>\<^sub>r b' \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b'))
[PROOF STEP]
apply (rule aGroup.ag_pOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; a' \<in> carrier R; b \<in> carrier R; b' \<in> carrier R; ideal R I; a \<plusminus> -\<^sub>a b \<in> I; a' \<plusminus> -\<^sub>a b' \<in> I; aGroup R; a \<cdot>\<^sub>r a' \<in> carrier R; a \<cdot>\<^sub>r b' \<in> carrier R; b \<cdot>\<^sub>r b' \<in> carrier R; -\<^sub>a b \<cdot>\<^sub>r b' \<in> carrier R; -\<^sub>a a \<cdot>\<^sub>r b' \<in> carrier R\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>r a' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b' = a \<cdot>\<^sub>r a' \<plusminus> (-\<^sub>a a \<cdot>\<^sub>r b' \<plusminus> (a \<cdot>\<^sub>r b' \<plusminus> -\<^sub>a b \<cdot>\<^sub>r b'))
[PROOF STEP]
apply (simp add:aGroup.ag_pOp_assoc[THEN sym, of "R" "-\<^sub>a (a \<cdot>\<^sub>r b')" "a \<cdot>\<^sub>r b'"
                          "-\<^sub>a (b \<cdot>\<^sub>r b')"],
        simp add:aGroup.ag_l_inv1 aGroup.ag_l_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_inv1_closed:"\<lbrakk> ideal R I; x \<in> I \<rbrakk> \<Longrightarrow> -\<^sub>a x \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; x \<in> I\<rbrakk> \<Longrightarrow> -\<^sub>a x \<in> I
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; x \<in> I; aGroup R\<rbrakk> \<Longrightarrow> -\<^sub>a x \<in> I
[PROOF STEP]
apply (unfold ideal_def, frule conjunct1, fold ideal_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; x \<in> I; aGroup R; R +> I\<rbrakk> \<Longrightarrow> -\<^sub>a x \<in> I
[PROOF STEP]
apply (simp add:aGroup.asubg_mOp_closed[of "R" "I"])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_zero:"ideal R I  \<Longrightarrow> \<zero> \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ideal R I \<Longrightarrow> \<zero> \<in> I
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; aGroup R\<rbrakk> \<Longrightarrow> \<zero> \<in> I
[PROOF STEP]
apply (unfold ideal_def, frule conjunct1, fold ideal_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; aGroup R; R +> I\<rbrakk> \<Longrightarrow> \<zero> \<in> I
[PROOF STEP]
apply (simp add:aGroup.asubg_inc_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_zero_forall:"\<forall>I. ideal R I \<longrightarrow>  \<zero> \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>I. ideal R I \<longrightarrow> \<zero> \<in> I
[PROOF STEP]
by (simp add:ideal_zero)


[STATEMENT]
lemma (in Ring) ideal_ele_sumTr1:"\<lbrakk> ideal R I; a \<in> carrier R; b \<in> carrier R;
          a \<plusminus> b \<in> I; a \<in> I \<rbrakk> \<Longrightarrow> b \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; a \<plusminus> b \<in> I; a \<in> I\<rbrakk> \<Longrightarrow> b \<in> I
[PROOF STEP]
apply (frule ideal_inv1_closed[of "I" "a"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; a \<plusminus> b \<in> I; a \<in> I; -\<^sub>a a \<in> I\<rbrakk> \<Longrightarrow> b \<in> I
[PROOF STEP]
apply (frule ideal_pOp_closed[of "I" "-\<^sub>a a" "a \<plusminus> b"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; a \<plusminus> b \<in> I; a \<in> I; -\<^sub>a a \<in> I; -\<^sub>a a \<plusminus> (a \<plusminus> b) \<in> I\<rbrakk> \<Longrightarrow> b \<in> I
[PROOF STEP]
apply (frule ideal_subset[of "I" "-\<^sub>a a"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; a \<plusminus> b \<in> I; a \<in> I; -\<^sub>a a \<in> I; -\<^sub>a a \<plusminus> (a \<plusminus> b) \<in> I; -\<^sub>a a \<in> carrier R\<rbrakk> \<Longrightarrow> b \<in> I
[PROOF STEP]
apply (cut_tac ring_is_ag,
       simp add:aGroup.ag_pOp_assoc[THEN sym],
       simp add:aGroup.ag_l_inv1,
       simp add:aGroup.ag_l_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_ele_sumTr2:"\<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R;
                a \<plusminus> b \<in> I; b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; a \<plusminus> b \<in> I; b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I
[PROOF STEP]
apply (cut_tac ring_is_ag,
       simp add:aGroup.ag_pOp_commute[of "R" "a" "b"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; a \<in> carrier R; b \<in> carrier R; b \<plusminus> a \<in> I; b \<in> I; aGroup R\<rbrakk> \<Longrightarrow> a \<in> I
[PROOF STEP]
apply (simp add:ideal_ele_sumTr1[of "I" "b" "a"])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_condition:"\<lbrakk>I \<subseteq> carrier R; I \<noteq> {};
       \<forall>x\<in>I. \<forall>y\<in>I. x \<plusminus> (-\<^sub>a y) \<in> I; \<forall>r\<in>carrier R. \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I \<rbrakk> \<Longrightarrow>
                                   ideal R I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I \<subseteq> carrier R; I \<noteq> {}; \<forall>x\<in>I. \<forall>y\<in>I. x \<plusminus> -\<^sub>a y \<in> I; \<forall>r\<in>carrier R. \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I\<rbrakk> \<Longrightarrow> ideal R I
[PROOF STEP]
apply (simp add:ideal_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I \<subseteq> carrier R; I \<noteq> {}; \<forall>x\<in>I. \<forall>y\<in>I. x \<plusminus> -\<^sub>a y \<in> I; \<forall>r\<in>carrier R. \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I\<rbrakk> \<Longrightarrow> R +> I
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I \<subseteq> carrier R; I \<noteq> {}; \<forall>x\<in>I. \<forall>y\<in>I. x \<plusminus> -\<^sub>a y \<in> I; \<forall>r\<in>carrier R. \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I; aGroup R\<rbrakk> \<Longrightarrow> R +> I
[PROOF STEP]
apply (rule aGroup.asubg_test[of "R" "I"], assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_condition1:"\<lbrakk>I \<subseteq> carrier R; I \<noteq> {};
  \<forall>x\<in>I. \<forall>y\<in>I. x \<plusminus> y \<in> I; \<forall>r\<in>carrier R. \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I \<rbrakk> \<Longrightarrow> ideal R I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>I \<subseteq> carrier R; I \<noteq> {}; \<forall>x\<in>I. \<forall>y\<in>I. x \<plusminus> y \<in> I; \<forall>r\<in>carrier R. \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I\<rbrakk> \<Longrightarrow> ideal R I
[PROOF STEP]
apply (rule ideal_condition[of "I"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>I \<subseteq> carrier R; I \<noteq> {}; \<forall>x\<in>I. \<forall>y\<in>I. x \<plusminus> y \<in> I; \<forall>r\<in>carrier R. \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I\<rbrakk> \<Longrightarrow> \<forall>x\<in>I. \<forall>y\<in>I. x \<plusminus> -\<^sub>a y \<in> I
 2. \<lbrakk>I \<subseteq> carrier R; I \<noteq> {}; \<forall>x\<in>I. \<forall>y\<in>I. x \<plusminus> y \<in> I; \<forall>r\<in>carrier R. \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>I \<subseteq> carrier R; I \<noteq> {}; \<forall>x\<in>I. \<forall>y\<in>I. x \<plusminus> y \<in> I; \<forall>r\<in>carrier R. \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I; x \<in> I; y \<in> I\<rbrakk> \<Longrightarrow> x \<plusminus> -\<^sub>a y \<in> I
 2. \<lbrakk>I \<subseteq> carrier R; I \<noteq> {}; \<forall>x\<in>I. \<forall>y\<in>I. x \<plusminus> y \<in> I; \<forall>r\<in>carrier R. \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I
[PROOF STEP]
apply (cut_tac ring_is_ag,
       cut_tac ring_one,
       frule aGroup.ag_mOp_closed[of "R" "1\<^sub>r"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>I \<subseteq> carrier R; I \<noteq> {}; \<forall>x\<in>I. \<forall>y\<in>I. x \<plusminus> y \<in> I; \<forall>r\<in>carrier R. \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I; x \<in> I; y \<in> I; aGroup R; 1\<^sub>r \<in> carrier R; -\<^sub>a 1\<^sub>r \<in> carrier R\<rbrakk> \<Longrightarrow> x \<plusminus> -\<^sub>a y \<in> I
 2. \<lbrakk>I \<subseteq> carrier R; I \<noteq> {}; \<forall>x\<in>I. \<forall>y\<in>I. x \<plusminus> y \<in> I; \<forall>r\<in>carrier R. \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I
[PROOF STEP]
apply (frule_tac x = "-\<^sub>a 1\<^sub>r " in bspec, assumption+,
        thin_tac "\<forall>r\<in>carrier R. \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I",
        rotate_tac -1,
        frule_tac x = y in bspec, assumption,
        thin_tac "\<forall>x\<in>I. (-\<^sub>a 1\<^sub>r) \<cdot>\<^sub>r x \<in> I")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>I \<subseteq> carrier R; I \<noteq> {}; \<forall>x\<in>I. \<forall>y\<in>I. x \<plusminus> y \<in> I; x \<in> I; y \<in> I; aGroup R; 1\<^sub>r \<in> carrier R; -\<^sub>a 1\<^sub>r \<in> carrier R; (-\<^sub>a 1\<^sub>r) \<cdot>\<^sub>r y \<in> I\<rbrakk> \<Longrightarrow> x \<plusminus> -\<^sub>a y \<in> I
 2. \<lbrakk>I \<subseteq> carrier R; I \<noteq> {}; \<forall>x\<in>I. \<forall>y\<in>I. x \<plusminus> y \<in> I; \<forall>r\<in>carrier R. \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>I. r \<cdot>\<^sub>r x \<in> I
[PROOF STEP]
apply (frule_tac c = y in subsetD[of "I" "carrier R"], assumption+,
        simp add:ring_times_minusl[THEN sym], simp add:ideal_pOp_closed)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done