[STATEMENT]
lemma (in Ring) ex_contid_maximal:"\<lbrakk> S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {};
T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply (cut_tac A="{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}" in Zorn_Lemma2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}\<rbrakk> \<Longrightarrow> \<forall>C\<in>chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<exists>U\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>C. X \<subseteq> U
 2. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}\<rbrakk> \<Longrightarrow> \<exists>U\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>C. X \<subseteq> U
 2. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply (case_tac "C = {}")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C = {}\<rbrakk> \<Longrightarrow> \<exists>U\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>C. X \<subseteq> U
 2. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>U\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>C. X \<subseteq> U
 3. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
(** case C = {} **)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C = {}\<rbrakk> \<Longrightarrow> \<exists>U\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>C. X \<subseteq> U
 2. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>U\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>C. X \<subseteq> U
 3. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>U\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>C. X \<subseteq> U
 2. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
(** case C = {} done **)
     (** existence of sup in C **)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>U\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>C. X \<subseteq> U
 2. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply (subgoal_tac "\<Union>C\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J} \<and>
                                         (\<forall>x\<in>C. x \<subseteq>  \<Union>C)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<noteq> {}; \<Union> C \<in> {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J} \<and> (\<forall>x\<in>C. x \<subseteq> \<Union> C)\<rbrakk> \<Longrightarrow> \<exists>U\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>C. X \<subseteq> U
 2. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<Union> C \<in> {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J} \<and> (\<forall>x\<in>C. x \<subseteq> \<Union> C)
 3. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<Union> C \<in> {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J} \<and> (\<forall>x\<in>C. x \<subseteq> \<Union> C)
 2. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply (rule conjI,
       simp add:CollectI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> ideal R (\<Union> C) \<and> (\<forall>x\<in>C. 1\<^sub>r \<notin> x) \<and> I \<subseteq> \<Union> C
 2. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>C. x \<subseteq> \<Union> C
 3. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply (subgoal_tac "C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}\<rbrakk> \<Longrightarrow> ideal R (\<Union> C) \<and> (\<forall>x\<in>C. 1\<^sub>r \<notin> x) \<and> I \<subseteq> \<Union> C
 2. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}
 3. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>C. x \<subseteq> \<Union> C
 4. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply (rule conjI,
       simp add:chains_un)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}\<rbrakk> \<Longrightarrow> (\<forall>x\<in>C. 1\<^sub>r \<notin> x) \<and> I \<subseteq> \<Union> C
 2. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}
 3. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>C. x \<subseteq> \<Union> C
 4. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}\<rbrakk> \<Longrightarrow> \<forall>x\<in>C. 1\<^sub>r \<notin> x
 2. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}\<rbrakk> \<Longrightarrow> I \<subseteq> \<Union> C
 3. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}
 4. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>C. x \<subseteq> \<Union> C
 5. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply (rule contrapos_pp, simp+, erule bexE)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>C x. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; x \<in> C; 1\<^sub>r \<in> x\<rbrakk> \<Longrightarrow> False
 2. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}\<rbrakk> \<Longrightarrow> I \<subseteq> \<Union> C
 3. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}
 4. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>C. x \<subseteq> \<Union> C
 5. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply (thin_tac " C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>C x. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}; x \<in> C; 1\<^sub>r \<in> x\<rbrakk> \<Longrightarrow> False
 2. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}\<rbrakk> \<Longrightarrow> I \<subseteq> \<Union> C
 3. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}
 4. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>C. x \<subseteq> \<Union> C
 5. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply (simp add:chains_def, erule conjE)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>C x. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}; x \<in> C; 1\<^sub>r \<in> x; C \<subseteq> {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; chain\<^sub>\<subseteq> C\<rbrakk> \<Longrightarrow> False
 2. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}\<rbrakk> \<Longrightarrow> I \<subseteq> \<Union> C
 3. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}
 4. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>C. x \<subseteq> \<Union> C
 5. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply (frule_tac c = x and A = C and B = "{J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}"
         in subsetD, assumption+, simp,
        thin_tac "C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> I \<subseteq> \<Union> C
 2. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}
 3. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>C. x \<subseteq> \<Union> C
 4. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply (frule_tac A = C in nonempty_ex, erule exE, simp add:chains_def,
        erule conjE,
        frule_tac c = x and A = C and B = "{J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}" in
                  subsetD, assumption+, simp, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>C x. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}; x \<in> C; C \<subseteq> {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; chain\<^sub>\<subseteq> C; ideal R x; 1\<^sub>r \<notin> x; I \<subseteq> x\<rbrakk> \<Longrightarrow> I \<subseteq> \<Union> C
 2. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}
 3. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>C. x \<subseteq> \<Union> C
 4. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply (rule_tac A = I and B = x and C = "\<Union>C" in subset_trans, assumption,
        rule_tac B = x and A = C in Union_upper, assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}
 2. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>C. x \<subseteq> \<Union> C
 3. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply (simp add:chains_def, erule conjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}; C \<subseteq> {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; chain\<^sub>\<subseteq> C\<rbrakk> \<Longrightarrow> C \<subseteq> {I. ideal R I \<and> I \<subset> carrier R}
 2. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>C. x \<subseteq> \<Union> C
 3. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply (rule subsetI, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C x. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}; C \<subseteq> {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; chain\<^sub>\<subseteq> C; x \<in> C\<rbrakk> \<Longrightarrow> ideal R x \<and> x \<subset> carrier R
 2. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>C. x \<subseteq> \<Union> C
 3. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply (frule_tac c = x and A = C and B = "{J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}"
        in subsetD, assumption+, simp, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C x. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}; C \<subseteq> {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; chain\<^sub>\<subseteq> C; x \<in> C; ideal R x; 1\<^sub>r \<notin> x; I \<subseteq> x\<rbrakk> \<Longrightarrow> x \<subset> carrier R
 2. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>C. x \<subseteq> \<Union> C
 3. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply (subst psubset_eq, simp add:ideal_subset1)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C x. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; C \<noteq> {}; C \<subseteq> {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; chain\<^sub>\<subseteq> C; x \<in> C; ideal R x; 1\<^sub>r \<notin> x; I \<subseteq> x\<rbrakk> \<Longrightarrow> x \<noteq> carrier R
 2. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>C. x \<subseteq> \<Union> C
 3. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply (rule contrapos_pp, simp+, simp add:ring_one)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>C. x \<subseteq> \<Union> C
 2. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C x. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<in> chains {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; C \<noteq> {}; x \<in> C\<rbrakk> \<Longrightarrow> x \<subseteq> \<Union> C
 2. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply (rule Union_upper, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<exists>M\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply (erule bexE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; M \<in> {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; \<forall>X\<in>{J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_set T mx
[PROOF STEP]
apply (simp add:maximal_set_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; ideal R M \<and> 1\<^sub>r \<notin> M \<and> I \<subseteq> M; \<forall>X. ideal R X \<and> 1\<^sub>r \<notin> X \<and> I \<subseteq> X \<longrightarrow> M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>mx. ideal R mx \<and> 1\<^sub>r \<notin> mx \<and> I \<subseteq> mx \<and> (\<forall>s. ideal R s \<and> 1\<^sub>r \<notin> s \<and> I \<subseteq> s \<longrightarrow> mx \<subseteq> s \<longrightarrow> s = mx)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) contid_maximal:"\<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {};
             T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; maximal_set T mx\<rbrakk> \<Longrightarrow>
                                                maximal_ideal R mx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S = {1\<^sub>r}; \<zero> \<notin> S; ideal R I; I \<inter> S = {}; T = {J. ideal R J \<and> S \<inter> J = {} \<and> I \<subseteq> J}; maximal_set T mx\<rbrakk> \<Longrightarrow> maximal_ideal R mx
[PROOF STEP]
apply (simp add:maximal_set_def maximal_ideal_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; ideal R mx \<and> 1\<^sub>r \<notin> mx \<and> I \<subseteq> mx \<and> (\<forall>s. ideal R s \<and> 1\<^sub>r \<notin> s \<and> I \<subseteq> s \<longrightarrow> mx \<subseteq> s \<longrightarrow> s = mx)\<rbrakk> \<Longrightarrow> {J. ideal R J \<and> mx \<subseteq> J} = {mx, carrier R}
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; ideal R mx; 1\<^sub>r \<notin> mx; I \<subseteq> mx; \<forall>s. ideal R s \<and> 1\<^sub>r \<notin> s \<and> I \<subseteq> s \<longrightarrow> mx \<subseteq> s \<longrightarrow> s = mx\<rbrakk> \<Longrightarrow> {J. ideal R J \<and> mx \<subseteq> J} = {mx, carrier R}
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; ideal R mx; 1\<^sub>r \<notin> mx; I \<subseteq> mx; \<forall>s. ideal R s \<and> 1\<^sub>r \<notin> s \<and> I \<subseteq> s \<longrightarrow> mx \<subseteq> s \<longrightarrow> s = mx\<rbrakk> \<Longrightarrow> {J. ideal R J \<and> mx \<subseteq> J} \<subseteq> {mx, carrier R}
 2. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; ideal R mx; 1\<^sub>r \<notin> mx; I \<subseteq> mx; \<forall>s. ideal R s \<and> 1\<^sub>r \<notin> s \<and> I \<subseteq> s \<longrightarrow> mx \<subseteq> s \<longrightarrow> s = mx\<rbrakk> \<Longrightarrow> {mx, carrier R} \<subseteq> {J. ideal R J \<and> mx \<subseteq> J}
[PROOF STEP]
(** {J. ideal R J \<and> mx \<subseteq> J} \<subseteq> {mx, carrier R} **)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; ideal R mx; 1\<^sub>r \<notin> mx; I \<subseteq> mx; \<forall>s. ideal R s \<and> 1\<^sub>r \<notin> s \<and> I \<subseteq> s \<longrightarrow> mx \<subseteq> s \<longrightarrow> s = mx\<rbrakk> \<Longrightarrow> {J. ideal R J \<and> mx \<subseteq> J} \<subseteq> {mx, carrier R}
 2. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; ideal R mx; 1\<^sub>r \<notin> mx; I \<subseteq> mx; \<forall>s. ideal R s \<and> 1\<^sub>r \<notin> s \<and> I \<subseteq> s \<longrightarrow> mx \<subseteq> s \<longrightarrow> s = mx\<rbrakk> \<Longrightarrow> {mx, carrier R} \<subseteq> {J. ideal R J \<and> mx \<subseteq> J}
[PROOF STEP]
apply (rule subsetI, simp add:CollectI, erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; ideal R mx; 1\<^sub>r \<notin> mx; I \<subseteq> mx; \<forall>s. ideal R s \<and> 1\<^sub>r \<notin> s \<and> I \<subseteq> s \<longrightarrow> mx \<subseteq> s \<longrightarrow> s = mx; ideal R x; mx \<subseteq> x\<rbrakk> \<Longrightarrow> x = mx \<or> x = carrier R
 2. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; ideal R mx; 1\<^sub>r \<notin> mx; I \<subseteq> mx; \<forall>s. ideal R s \<and> 1\<^sub>r \<notin> s \<and> I \<subseteq> s \<longrightarrow> mx \<subseteq> s \<longrightarrow> s = mx\<rbrakk> \<Longrightarrow> {mx, carrier R} \<subseteq> {J. ideal R J \<and> mx \<subseteq> J}
[PROOF STEP]
apply (case_tac "x = mx", simp, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; ideal R mx; 1\<^sub>r \<notin> mx; I \<subseteq> mx; \<forall>s. ideal R s \<and> 1\<^sub>r \<notin> s \<and> I \<subseteq> s \<longrightarrow> mx \<subseteq> s \<longrightarrow> s = mx; ideal R x; mx \<subseteq> x; x \<noteq> mx\<rbrakk> \<Longrightarrow> x = carrier R
 2. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; ideal R mx; 1\<^sub>r \<notin> mx; I \<subseteq> mx; \<forall>s. ideal R s \<and> 1\<^sub>r \<notin> s \<and> I \<subseteq> s \<longrightarrow> mx \<subseteq> s \<longrightarrow> s = mx\<rbrakk> \<Longrightarrow> {mx, carrier R} \<subseteq> {J. ideal R J \<and> mx \<subseteq> J}
[PROOF STEP]
apply (subgoal_tac "1\<^sub>r \<in> x")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; ideal R mx; 1\<^sub>r \<notin> mx; I \<subseteq> mx; \<forall>s. ideal R s \<and> 1\<^sub>r \<notin> s \<and> I \<subseteq> s \<longrightarrow> mx \<subseteq> s \<longrightarrow> s = mx; ideal R x; mx \<subseteq> x; x \<noteq> mx; 1\<^sub>r \<in> x\<rbrakk> \<Longrightarrow> x = carrier R
 2. \<And>x. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; ideal R mx; 1\<^sub>r \<notin> mx; I \<subseteq> mx; \<forall>s. ideal R s \<and> 1\<^sub>r \<notin> s \<and> I \<subseteq> s \<longrightarrow> mx \<subseteq> s \<longrightarrow> s = mx; ideal R x; mx \<subseteq> x; x \<noteq> mx\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> x
 3. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; ideal R mx; 1\<^sub>r \<notin> mx; I \<subseteq> mx; \<forall>s. ideal R s \<and> 1\<^sub>r \<notin> s \<and> I \<subseteq> s \<longrightarrow> mx \<subseteq> s \<longrightarrow> s = mx\<rbrakk> \<Longrightarrow> {mx, carrier R} \<subseteq> {J. ideal R J \<and> mx \<subseteq> J}
[PROOF STEP]
apply (rule_tac  I = x in ideal_inc_one, assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; ideal R mx; 1\<^sub>r \<notin> mx; I \<subseteq> mx; \<forall>s. ideal R s \<and> 1\<^sub>r \<notin> s \<and> I \<subseteq> s \<longrightarrow> mx \<subseteq> s \<longrightarrow> s = mx; ideal R x; mx \<subseteq> x; x \<noteq> mx\<rbrakk> \<Longrightarrow> 1\<^sub>r \<in> x
 2. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; ideal R mx; 1\<^sub>r \<notin> mx; I \<subseteq> mx; \<forall>s. ideal R s \<and> 1\<^sub>r \<notin> s \<and> I \<subseteq> s \<longrightarrow> mx \<subseteq> s \<longrightarrow> s = mx\<rbrakk> \<Longrightarrow> {mx, carrier R} \<subseteq> {J. ideal R J \<and> mx \<subseteq> J}
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; ideal R mx; 1\<^sub>r \<notin> mx; I \<subseteq> mx; \<forall>s. ideal R s \<and> 1\<^sub>r \<notin> s \<and> I \<subseteq> s \<longrightarrow> mx \<subseteq> s \<longrightarrow> s = mx\<rbrakk> \<Longrightarrow> ideal R (carrier R) \<and> mx \<subseteq> carrier R
[PROOF STEP]
apply (drule spec[of _ mx])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S = {1\<^sub>r}; \<zero> \<noteq> 1\<^sub>r; ideal R I; 1\<^sub>r \<notin> I; T = {J. ideal R J \<and> 1\<^sub>r \<notin> J \<and> I \<subseteq> J}; ideal R mx; 1\<^sub>r \<notin> mx; I \<subseteq> mx; ideal R mx \<and> 1\<^sub>r \<notin> mx \<and> I \<subseteq> mx \<longrightarrow> mx \<subseteq> mx \<longrightarrow> mx = mx\<rbrakk> \<Longrightarrow> ideal R (carrier R) \<and> mx \<subseteq> carrier R
[PROOF STEP]
apply (simp add:whole_ideal,
        rule subsetI, rule ideal_subset[of "mx"], assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_contained_maxid:"\<lbrakk>\<not>(zeroring R); ideal R I; 1\<^sub>r \<notin> I\<rbrakk> \<Longrightarrow>
                    \<exists>mx. maximal_ideal R mx \<and> I \<subseteq> mx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_ideal R mx \<and> I \<subseteq> mx
[PROOF STEP]
apply (cut_tac ex_contid_maximal[of "{1\<^sub>r}" "I"
                      "{J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J}"])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I; \<exists>mx. maximal_set {J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J} mx\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_ideal R mx \<and> I \<subseteq> mx
 2. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I\<rbrakk> \<Longrightarrow> {1\<^sub>r} = {1\<^sub>r}
 3. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I\<rbrakk> \<Longrightarrow> \<zero> \<notin> {1\<^sub>r}
 4. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I\<rbrakk> \<Longrightarrow> ideal R I
 5. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I\<rbrakk> \<Longrightarrow> I \<inter> {1\<^sub>r} = {}
 6. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I\<rbrakk> \<Longrightarrow> {J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J} = {J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J}
[PROOF STEP]
apply (erule exE,
       cut_tac mx = mx in contid_maximal[of "{1\<^sub>r}" "I"
                         "{J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J}"])
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. \<And>mx. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I; maximal_set {J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J} mx\<rbrakk> \<Longrightarrow> {1\<^sub>r} = {1\<^sub>r}
 2. \<And>mx. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I; maximal_set {J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J} mx\<rbrakk> \<Longrightarrow> \<zero> \<notin> {1\<^sub>r}
 3. \<And>mx. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I; maximal_set {J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J} mx\<rbrakk> \<Longrightarrow> ideal R I
 4. \<And>mx. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I; maximal_set {J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J} mx\<rbrakk> \<Longrightarrow> I \<inter> {1\<^sub>r} = {}
 5. \<And>mx. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I; maximal_set {J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J} mx\<rbrakk> \<Longrightarrow> {J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J} = {J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J}
 6. \<And>mx. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I; maximal_set {J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J} mx\<rbrakk> \<Longrightarrow> maximal_set {J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J} mx
 7. \<And>mx. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I; maximal_set {J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J} mx; maximal_ideal R mx\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_ideal R mx \<and> I \<subseteq> mx
 8. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I\<rbrakk> \<Longrightarrow> {1\<^sub>r} = {1\<^sub>r}
 9. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I\<rbrakk> \<Longrightarrow> \<zero> \<notin> {1\<^sub>r}
 10. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I\<rbrakk> \<Longrightarrow> ideal R I
A total of 12 subgoals...
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<And>mx. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I; maximal_set {J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J} mx\<rbrakk> \<Longrightarrow> \<zero> \<notin> {1\<^sub>r}
 2. \<And>mx. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I; maximal_set {J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J} mx\<rbrakk> \<Longrightarrow> ideal R I
 3. \<And>mx. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I; maximal_set {J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J} mx\<rbrakk> \<Longrightarrow> I \<inter> {1\<^sub>r} = {}
 4. \<And>mx. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I; maximal_set {J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J} mx\<rbrakk> \<Longrightarrow> {J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J} = {J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J}
 5. \<And>mx. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I; maximal_set {J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J} mx\<rbrakk> \<Longrightarrow> maximal_set {J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J} mx
 6. \<And>mx. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I; maximal_set {J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J} mx; maximal_ideal R mx\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_ideal R mx \<and> I \<subseteq> mx
 7. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I\<rbrakk> \<Longrightarrow> {1\<^sub>r} = {1\<^sub>r}
 8. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I\<rbrakk> \<Longrightarrow> \<zero> \<notin> {1\<^sub>r}
 9. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I\<rbrakk> \<Longrightarrow> ideal R I
 10. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I\<rbrakk> \<Longrightarrow> I \<inter> {1\<^sub>r} = {}
A total of 11 subgoals...
[PROOF STEP]
apply (frule Zero_ring1, simp,
        assumption, simp, simp, simp,
        simp add:maximal_set_def, (erule conjE)+, blast,
        simp, frule Zero_ring1, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I\<rbrakk> \<Longrightarrow> ideal R I
 2. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I\<rbrakk> \<Longrightarrow> I \<inter> {1\<^sub>r} = {}
 3. \<lbrakk>\<not> zeroring R; ideal R I; 1\<^sub>r \<notin> I\<rbrakk> \<Longrightarrow> {J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J} = {J. ideal R J \<and> {1\<^sub>r} \<inter> J = {} \<and> I \<subseteq> J}
[PROOF STEP]
apply (assumption, simp, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) nonunit_principal_id:"\<lbrakk>a \<in> carrier R; \<not> (Unit R a)\<rbrakk> \<Longrightarrow>
                                             (R \<diamondsuit>\<^sub>p a) \<noteq> (carrier R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; \<not> Unit R a\<rbrakk> \<Longrightarrow> R \<diamondsuit>\<^sub>p a \<noteq> carrier R
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; \<not> Unit R a; R \<diamondsuit>\<^sub>p a = carrier R\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule sym, thin_tac "R \<diamondsuit>\<^sub>p a = carrier R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; \<not> Unit R a; carrier R = R \<diamondsuit>\<^sub>p a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cut_tac ring_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; \<not> Unit R a; carrier R = R \<diamondsuit>\<^sub>p a; 1\<^sub>r \<in> carrier R\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule eq_set_inc[of "1\<^sub>r" "carrier R" "R \<diamondsuit>\<^sub>p a"], assumption,
        thin_tac "carrier R = R \<diamondsuit>\<^sub>p a", thin_tac "1\<^sub>r \<in> carrier R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> carrier R; \<not> Unit R a; 1\<^sub>r \<in> R \<diamondsuit>\<^sub>p a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:Rxa_def, erule bexE, simp add:ring_tOp_commute[of _ "a"],
       frule sym, thin_tac "1\<^sub>r = a \<cdot>\<^sub>r r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>a \<in> carrier R; \<not> Unit R a; r \<in> carrier R; a \<cdot>\<^sub>r r = 1\<^sub>r\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:Unit_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) nonunit_contained_maxid:"\<lbrakk>\<not>(zeroring R); a \<in> carrier R;
                \<not> Unit R a \<rbrakk>  \<Longrightarrow>  \<exists>mx. maximal_ideal R mx \<and> a \<in>  mx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> zeroring R; a \<in> carrier R; \<not> Unit R a\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_ideal R mx \<and> a \<in> mx
[PROOF STEP]
apply (frule principal_ideal[of "a"],
       frule ideal_contained_maxid[of "R \<diamondsuit>\<^sub>p a"], assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> zeroring R; a \<in> carrier R; \<not> Unit R a; ideal R (R \<diamondsuit>\<^sub>p a)\<rbrakk> \<Longrightarrow> 1\<^sub>r \<notin> R \<diamondsuit>\<^sub>p a
 2. \<lbrakk>\<not> zeroring R; a \<in> carrier R; \<not> Unit R a; ideal R (R \<diamondsuit>\<^sub>p a); \<exists>mx. maximal_ideal R mx \<and> R \<diamondsuit>\<^sub>p a \<subseteq> mx\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_ideal R mx \<and> a \<in> mx
[PROOF STEP]
apply (rule contrapos_pp, simp+,
        frule ideal_inc_one[of "R \<diamondsuit>\<^sub>p a"], assumption,
        simp add:nonunit_principal_id)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> zeroring R; a \<in> carrier R; \<not> Unit R a; ideal R (R \<diamondsuit>\<^sub>p a); \<exists>mx. maximal_ideal R mx \<and> R \<diamondsuit>\<^sub>p a \<subseteq> mx\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_ideal R mx \<and> a \<in> mx
[PROOF STEP]
apply (erule exE, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>mx. \<lbrakk>\<not> zeroring R; a \<in> carrier R; \<not> Unit R a; ideal R (R \<diamondsuit>\<^sub>p a); maximal_ideal R mx; R \<diamondsuit>\<^sub>p a \<subseteq> mx\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_ideal R mx \<and> a \<in> mx
[PROOF STEP]
apply (frule a_in_principal[of "a"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>mx. \<lbrakk>\<not> zeroring R; a \<in> carrier R; \<not> Unit R a; ideal R (R \<diamondsuit>\<^sub>p a); maximal_ideal R mx; R \<diamondsuit>\<^sub>p a \<subseteq> mx; a \<in> R \<diamondsuit>\<^sub>p a\<rbrakk> \<Longrightarrow> \<exists>mx. maximal_ideal R mx \<and> a \<in> mx
[PROOF STEP]
apply (frule_tac B = mx in subsetD[of "R \<diamondsuit>\<^sub>p a" _ "a"], assumption, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) local_ring_diff:"\<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R;
  \<forall>a\<in> (carrier R - mx). Unit R a \<rbrakk> \<Longrightarrow> local_ring R \<and> maximal_ideal R mx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a\<rbrakk> \<Longrightarrow> local_ring R \<and> maximal_ideal R mx
[PROOF STEP]
apply (subgoal_tac "{mx} = {m. maximal_ideal R m}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a; {mx} = {m. maximal_ideal R m}\<rbrakk> \<Longrightarrow> local_ring R \<and> maximal_ideal R mx
 2. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a\<rbrakk> \<Longrightarrow> {mx} = {m. maximal_ideal R m}
[PROOF STEP]
apply (cut_tac singletonI[of "mx"], simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a; {mx} = {m. maximal_ideal R m}; maximal_ideal R mx\<rbrakk> \<Longrightarrow> local_ring R
 2. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a\<rbrakk> \<Longrightarrow> {mx} = {m. maximal_ideal R m}
[PROOF STEP]
apply (frule sym, thin_tac "{mx} = {m. maximal_ideal R m}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a; maximal_ideal R mx; {m. maximal_ideal R m} = {mx}\<rbrakk> \<Longrightarrow> local_ring R
 2. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a\<rbrakk> \<Longrightarrow> {mx} = {m. maximal_ideal R m}
[PROOF STEP]
apply (simp add:local_ring_def, simp add:Ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a\<rbrakk> \<Longrightarrow> {mx} = {m. maximal_ideal R m}
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a\<rbrakk> \<Longrightarrow> {mx} \<subseteq> {m. maximal_ideal R m}
 2. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a\<rbrakk> \<Longrightarrow> {m. maximal_ideal R m} \<subseteq> {mx}
[PROOF STEP]
apply (rule subsetI, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a; x = mx\<rbrakk> \<Longrightarrow> maximal_ideal R mx
 2. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a\<rbrakk> \<Longrightarrow> {m. maximal_ideal R m} \<subseteq> {mx}
[PROOF STEP]
apply (simp add:maximal_ideal_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a; x = mx\<rbrakk> \<Longrightarrow> 1\<^sub>r \<notin> mx \<and> {J. ideal R J \<and> mx \<subseteq> J} = {mx, carrier R}
 2. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a\<rbrakk> \<Longrightarrow> {m. maximal_ideal R m} \<subseteq> {mx}
[PROOF STEP]
apply (simp add:ideal_inc_one1[of "mx", THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; \<forall>a\<in>carrier R - mx. Unit R a; x = mx\<rbrakk> \<Longrightarrow> {J. ideal R J \<and> mx \<subseteq> J} = {mx, carrier R}
 2. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a\<rbrakk> \<Longrightarrow> {m. maximal_ideal R m} \<subseteq> {mx}
[PROOF STEP]
apply (thin_tac "x = mx", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; Ball (carrier R - mx) (Unit R)\<rbrakk> \<Longrightarrow> {J. ideal R J \<and> mx \<subseteq> J} = {mx, carrier R}
 2. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a\<rbrakk> \<Longrightarrow> {m. maximal_ideal R m} \<subseteq> {mx}
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; Ball (carrier R - mx) (Unit R)\<rbrakk> \<Longrightarrow> {J. ideal R J \<and> mx \<subseteq> J} \<subseteq> {mx, carrier R}
 2. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; Ball (carrier R - mx) (Unit R)\<rbrakk> \<Longrightarrow> {mx, carrier R} \<subseteq> {J. ideal R J \<and> mx \<subseteq> J}
 3. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a\<rbrakk> \<Longrightarrow> {m. maximal_ideal R m} \<subseteq> {mx}
[PROOF STEP]
apply (rule subsetI, simp, erule conjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; \<forall>x\<in>carrier R - mx. Unit R x; ideal R x; mx \<subseteq> x\<rbrakk> \<Longrightarrow> x = mx \<or> x = carrier R
 2. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; Ball (carrier R - mx) (Unit R)\<rbrakk> \<Longrightarrow> {mx, carrier R} \<subseteq> {J. ideal R J \<and> mx \<subseteq> J}
 3. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a\<rbrakk> \<Longrightarrow> {m. maximal_ideal R m} \<subseteq> {mx}
[PROOF STEP]
apply (case_tac "x \<noteq> mx")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; \<forall>x\<in>carrier R - mx. Unit R x; ideal R x; mx \<subseteq> x; x \<noteq> mx\<rbrakk> \<Longrightarrow> x = mx \<or> x = carrier R
 2. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; \<forall>x\<in>carrier R - mx. Unit R x; ideal R x; mx \<subseteq> x; \<not> x \<noteq> mx\<rbrakk> \<Longrightarrow> x = mx \<or> x = carrier R
 3. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; Ball (carrier R - mx) (Unit R)\<rbrakk> \<Longrightarrow> {mx, carrier R} \<subseteq> {J. ideal R J \<and> mx \<subseteq> J}
 4. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a\<rbrakk> \<Longrightarrow> {m. maximal_ideal R m} \<subseteq> {mx}
[PROOF STEP]
apply (frule_tac A = x and B = mx in sets_not_eq, assumption)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; \<forall>x\<in>carrier R - mx. Unit R x; ideal R x; mx \<subseteq> x; x \<noteq> mx; \<exists>a\<in>x. a \<notin> mx\<rbrakk> \<Longrightarrow> x = mx \<or> x = carrier R
 2. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; \<forall>x\<in>carrier R - mx. Unit R x; ideal R x; mx \<subseteq> x; \<not> x \<noteq> mx\<rbrakk> \<Longrightarrow> x = mx \<or> x = carrier R
 3. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; Ball (carrier R - mx) (Unit R)\<rbrakk> \<Longrightarrow> {mx, carrier R} \<subseteq> {J. ideal R J \<and> mx \<subseteq> J}
 4. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a\<rbrakk> \<Longrightarrow> {m. maximal_ideal R m} \<subseteq> {mx}
[PROOF STEP]
apply (erule bexE)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x a. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; \<forall>x\<in>carrier R - mx. Unit R x; ideal R x; mx \<subseteq> x; x \<noteq> mx; a \<in> x; a \<notin> mx\<rbrakk> \<Longrightarrow> x = mx \<or> x = carrier R
 2. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; \<forall>x\<in>carrier R - mx. Unit R x; ideal R x; mx \<subseteq> x; \<not> x \<noteq> mx\<rbrakk> \<Longrightarrow> x = mx \<or> x = carrier R
 3. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; Ball (carrier R - mx) (Unit R)\<rbrakk> \<Longrightarrow> {mx, carrier R} \<subseteq> {J. ideal R J \<and> mx \<subseteq> J}
 4. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a\<rbrakk> \<Longrightarrow> {m. maximal_ideal R m} \<subseteq> {mx}
[PROOF STEP]
apply (frule_tac h = a and I = x in ideal_subset, assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x a. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; \<forall>x\<in>carrier R - mx. Unit R x; ideal R x; mx \<subseteq> x; x \<noteq> mx; a \<in> x; a \<notin> mx; a \<in> carrier R\<rbrakk> \<Longrightarrow> x = mx \<or> x = carrier R
 2. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; \<forall>x\<in>carrier R - mx. Unit R x; ideal R x; mx \<subseteq> x; \<not> x \<noteq> mx\<rbrakk> \<Longrightarrow> x = mx \<or> x = carrier R
 3. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; Ball (carrier R - mx) (Unit R)\<rbrakk> \<Longrightarrow> {mx, carrier R} \<subseteq> {J. ideal R J \<and> mx \<subseteq> J}
 4. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a\<rbrakk> \<Longrightarrow> {m. maximal_ideal R m} \<subseteq> {mx}
[PROOF STEP]
apply (frule_tac x = a in bspec, simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x a. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; \<forall>x\<in>carrier R - mx. Unit R x; ideal R x; mx \<subseteq> x; x \<noteq> mx; a \<in> x; a \<notin> mx; a \<in> carrier R; Unit R a\<rbrakk> \<Longrightarrow> x = mx \<or> x = carrier R
 2. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; \<forall>x\<in>carrier R - mx. Unit R x; ideal R x; mx \<subseteq> x; \<not> x \<noteq> mx\<rbrakk> \<Longrightarrow> x = mx \<or> x = carrier R
 3. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; Ball (carrier R - mx) (Unit R)\<rbrakk> \<Longrightarrow> {mx, carrier R} \<subseteq> {J. ideal R J \<and> mx \<subseteq> J}
 4. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a\<rbrakk> \<Longrightarrow> {m. maximal_ideal R m} \<subseteq> {mx}
[PROOF STEP]
apply (frule_tac I = x and a = a in ideal_inc_unit1, assumption+,
        simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; \<forall>x\<in>carrier R - mx. Unit R x; ideal R x; mx \<subseteq> x; \<not> x \<noteq> mx\<rbrakk> \<Longrightarrow> x = mx \<or> x = carrier R
 2. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; Ball (carrier R - mx) (Unit R)\<rbrakk> \<Longrightarrow> {mx, carrier R} \<subseteq> {J. ideal R J \<and> mx \<subseteq> J}
 3. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a\<rbrakk> \<Longrightarrow> {m. maximal_ideal R m} \<subseteq> {mx}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; Ball (carrier R - mx) (Unit R)\<rbrakk> \<Longrightarrow> {mx, carrier R} \<subseteq> {J. ideal R J \<and> mx \<subseteq> J}
 2. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a\<rbrakk> \<Longrightarrow> {m. maximal_ideal R m} \<subseteq> {mx}
[PROOF STEP]
apply (rule subsetI, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; \<forall>x\<in>carrier R - mx. Unit R x; x = mx \<or> x = carrier R\<rbrakk> \<Longrightarrow> ideal R x \<and> mx \<subseteq> x
 2. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a\<rbrakk> \<Longrightarrow> {m. maximal_ideal R m} \<subseteq> {mx}
[PROOF STEP]
apply (erule disjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; \<forall>x\<in>carrier R - mx. Unit R x; x = mx\<rbrakk> \<Longrightarrow> ideal R x \<and> mx \<subseteq> x
 2. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; \<forall>x\<in>carrier R - mx. Unit R x; x = carrier R\<rbrakk> \<Longrightarrow> ideal R x \<and> mx \<subseteq> x
 3. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a\<rbrakk> \<Longrightarrow> {m. maximal_ideal R m} \<subseteq> {mx}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; 1\<^sub>r \<notin> mx; \<forall>x\<in>carrier R - mx. Unit R x; x = carrier R\<rbrakk> \<Longrightarrow> ideal R x \<and> mx \<subseteq> x
 2. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a\<rbrakk> \<Longrightarrow> {m. maximal_ideal R m} \<subseteq> {mx}
[PROOF STEP]
apply (simp add:whole_ideal ideal_subset1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a\<rbrakk> \<Longrightarrow> {m. maximal_ideal R m} \<subseteq> {mx}
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a; x \<in> {m. maximal_ideal R m}\<rbrakk> \<Longrightarrow> x \<in> {mx}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a; maximal_ideal R x\<rbrakk> \<Longrightarrow> x = mx
[PROOF STEP]
apply (subgoal_tac "x \<subseteq> mx",
        thin_tac "\<forall>a\<in>carrier R - mx. Unit R a",
        simp add:maximal_ideal_def, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; x \<subseteq> mx; ideal R x; 1\<^sub>r \<notin> x; {J. ideal R J \<and> x \<subseteq> J} = {x, carrier R}\<rbrakk> \<Longrightarrow> x = mx
 2. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a; maximal_ideal R x\<rbrakk> \<Longrightarrow> x \<subseteq> mx
[PROOF STEP]
apply (subgoal_tac "mx \<in> {J. ideal R J \<and> x \<subseteq> J}", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; x \<subseteq> mx; ideal R x; 1\<^sub>r \<notin> x; {J. ideal R J \<and> x \<subseteq> J} = {x, carrier R}\<rbrakk> \<Longrightarrow> mx \<in> {J. ideal R J \<and> x \<subseteq> J}
 2. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a; maximal_ideal R x\<rbrakk> \<Longrightarrow> x \<subseteq> mx
[PROOF STEP]
apply (thin_tac "{J. ideal R J \<and> x \<subseteq> J} = {x, carrier R}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; x \<subseteq> mx; ideal R x; 1\<^sub>r \<notin> x\<rbrakk> \<Longrightarrow> mx \<in> {J. ideal R J \<and> x \<subseteq> J}
 2. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a; maximal_ideal R x\<rbrakk> \<Longrightarrow> x \<subseteq> mx
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a; maximal_ideal R x\<rbrakk> \<Longrightarrow> x \<subseteq> mx
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a; maximal_ideal R x; \<not> x \<subseteq> mx\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:subset_eq, erule bexE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a; maximal_ideal R x; xa \<in> x; xa \<notin> mx\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac mx = x in maximal_ideal_ideal,
        frule_tac x = xa in bspec,
        thin_tac "\<forall>a\<in>carrier R - mx. Unit R a", simp,
        simp add:ideal_subset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<not> zeroring R; ideal R mx; mx \<noteq> carrier R; \<forall>a\<in>carrier R - mx. Unit R a; maximal_ideal R x; xa \<in> x; xa \<notin> mx; ideal R x; Unit R xa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac I = x and a = xa in ideal_inc_unit, assumption+,
                  simp add:maximal_ideal_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) localring_unit:"\<lbrakk>\<not> zeroring R; maximal_ideal R mx;
                \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r) \<rbrakk> \<Longrightarrow> local_ring R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r)\<rbrakk> \<Longrightarrow> local_ring R
[PROOF STEP]
apply (frule maximal_ideal_ideal[of "mx"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx\<rbrakk> \<Longrightarrow> local_ring R
[PROOF STEP]
apply (frule local_ring_diff[of "mx"], assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx\<rbrakk> \<Longrightarrow> mx \<noteq> carrier R
 2. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier R - mx. Unit R a
 3. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx; local_ring R \<and> maximal_ideal R mx\<rbrakk> \<Longrightarrow> local_ring R
[PROOF STEP]
apply (simp add:maximal_ideal_def, erule conjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<not> zeroring R; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx; 1\<^sub>r \<notin> mx; {J. ideal R J \<and> mx \<subseteq> J} = {mx, carrier R}\<rbrakk> \<Longrightarrow> mx \<noteq> carrier R
 2. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier R - mx. Unit R a
 3. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx; local_ring R \<and> maximal_ideal R mx\<rbrakk> \<Longrightarrow> local_ring R
[PROOF STEP]
apply (simp add:ideal_inc_one1[THEN sym, of "mx"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx\<rbrakk> \<Longrightarrow> \<forall>a\<in>carrier R - mx. Unit R a
 2. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx; local_ring R \<and> maximal_ideal R mx\<rbrakk> \<Longrightarrow> local_ring R
[PROOF STEP]
apply (rule ballI, simp, erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx; a \<in> carrier R; a \<notin> mx\<rbrakk> \<Longrightarrow> Unit R a
 2. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx; local_ring R \<and> maximal_ideal R mx\<rbrakk> \<Longrightarrow> local_ring R
[PROOF STEP]
apply (frule_tac x = a in maximal_prime_Tr0[of "mx"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx; a \<in> carrier R; a \<notin> mx; mx \<minusplus> R \<diamondsuit>\<^sub>p a = carrier R\<rbrakk> \<Longrightarrow> Unit R a
 2. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx; local_ring R \<and> maximal_ideal R mx\<rbrakk> \<Longrightarrow> local_ring R
[PROOF STEP]
apply (frule sym, thin_tac "mx \<minusplus> R \<diamondsuit>\<^sub>p a = carrier R",
        cut_tac ring_one,
        frule_tac a = "1\<^sub>r" and A = "carrier R" and B = "mx \<minusplus> R \<diamondsuit>\<^sub>p a" in
                  eq_set_inc, assumption+,
        thin_tac "carrier R = mx \<minusplus> R \<diamondsuit>\<^sub>p a")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx; a \<in> carrier R; a \<notin> mx; 1\<^sub>r \<in> carrier R; 1\<^sub>r \<in> mx \<minusplus> R \<diamondsuit>\<^sub>p a\<rbrakk> \<Longrightarrow> Unit R a
 2. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx; local_ring R \<and> maximal_ideal R mx\<rbrakk> \<Longrightarrow> local_ring R
[PROOF STEP]
apply (frule_tac a = a in principal_ideal,
       frule ideal_subset1[of mx],
       frule_tac I = "R \<diamondsuit>\<^sub>p a" in ideal_subset1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx; a \<in> carrier R; a \<notin> mx; 1\<^sub>r \<in> carrier R; 1\<^sub>r \<in> mx \<minusplus> R \<diamondsuit>\<^sub>p a; ideal R (R \<diamondsuit>\<^sub>p a); mx \<subseteq> carrier R; R \<diamondsuit>\<^sub>p a \<subseteq> carrier R\<rbrakk> \<Longrightarrow> Unit R a
 2. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx; local_ring R \<and> maximal_ideal R mx\<rbrakk> \<Longrightarrow> local_ring R
[PROOF STEP]
apply (cut_tac ring_is_ag,
        simp add:aGroup.set_sum, (erule bexE)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a h k. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx; a \<in> carrier R; a \<notin> mx; 1\<^sub>r \<in> carrier R; ideal R (R \<diamondsuit>\<^sub>p a); mx \<subseteq> carrier R; R \<diamondsuit>\<^sub>p a \<subseteq> carrier R; aGroup R; h \<in> mx; k \<in> R \<diamondsuit>\<^sub>p a; 1\<^sub>r = h \<plusminus> k\<rbrakk> \<Longrightarrow> Unit R a
 2. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx; local_ring R \<and> maximal_ideal R mx\<rbrakk> \<Longrightarrow> local_ring R
[PROOF STEP]
apply (simp add:Rxa_def, erule bexE, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a h k r. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> (h \<plusminus> r \<cdot>\<^sub>r a)); ideal R mx; a \<in> carrier R; a \<notin> mx; h \<plusminus> r \<cdot>\<^sub>r a \<in> carrier R; ideal R {x. \<exists>r\<in>carrier R. x = r \<cdot>\<^sub>r a}; mx \<subseteq> carrier R; {x. \<exists>r\<in>carrier R. x = r \<cdot>\<^sub>r a} \<subseteq> carrier R; aGroup R; h \<in> mx; 1\<^sub>r = h \<plusminus> r \<cdot>\<^sub>r a; r \<in> carrier R; k = r \<cdot>\<^sub>r a\<rbrakk> \<Longrightarrow> Unit R a
 2. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx; local_ring R \<and> maximal_ideal R mx\<rbrakk> \<Longrightarrow> local_ring R
[PROOF STEP]
apply (frule sym, thin_tac "1\<^sub>r = h \<plusminus> r \<cdot>\<^sub>r a",
        frule_tac x = r and y = a in ring_tOp_closed, assumption+,
        frule_tac h = h in ideal_subset[of "mx"], assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a h k r. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> (h \<plusminus> r \<cdot>\<^sub>r a)); ideal R mx; a \<in> carrier R; a \<notin> mx; h \<plusminus> r \<cdot>\<^sub>r a \<in> carrier R; ideal R {x. \<exists>r\<in>carrier R. x = r \<cdot>\<^sub>r a}; mx \<subseteq> carrier R; {x. \<exists>r\<in>carrier R. x = r \<cdot>\<^sub>r a} \<subseteq> carrier R; aGroup R; h \<in> mx; r \<in> carrier R; k = r \<cdot>\<^sub>r a; h \<plusminus> r \<cdot>\<^sub>r a = 1\<^sub>r; r \<cdot>\<^sub>r a \<in> carrier R; h \<in> carrier R\<rbrakk> \<Longrightarrow> Unit R a
 2. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx; local_ring R \<and> maximal_ideal R mx\<rbrakk> \<Longrightarrow> local_ring R
[PROOF STEP]
apply (frule_tac I = mx and x = h in ideal_inv1_closed, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a h k r. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> (h \<plusminus> r \<cdot>\<^sub>r a)); ideal R mx; a \<in> carrier R; a \<notin> mx; h \<plusminus> r \<cdot>\<^sub>r a \<in> carrier R; ideal R {x. \<exists>r\<in>carrier R. x = r \<cdot>\<^sub>r a}; mx \<subseteq> carrier R; {x. \<exists>r\<in>carrier R. x = r \<cdot>\<^sub>r a} \<subseteq> carrier R; aGroup R; h \<in> mx; r \<in> carrier R; k = r \<cdot>\<^sub>r a; h \<plusminus> r \<cdot>\<^sub>r a = 1\<^sub>r; r \<cdot>\<^sub>r a \<in> carrier R; h \<in> carrier R; -\<^sub>a h \<in> mx\<rbrakk> \<Longrightarrow> Unit R a
 2. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx; local_ring R \<and> maximal_ideal R mx\<rbrakk> \<Longrightarrow> local_ring R
[PROOF STEP]
apply (frule_tac a = "-\<^sub>a h" in forall_spec, assumption,
        thin_tac "\<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> (h \<plusminus> r \<cdot>\<^sub>r a))",
        thin_tac "h \<plusminus> r \<cdot>\<^sub>r a = 1\<^sub>r")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a h k r. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; ideal R mx; a \<in> carrier R; a \<notin> mx; h \<plusminus> r \<cdot>\<^sub>r a \<in> carrier R; ideal R {x. \<exists>r\<in>carrier R. x = r \<cdot>\<^sub>r a}; mx \<subseteq> carrier R; {x. \<exists>r\<in>carrier R. x = r \<cdot>\<^sub>r a} \<subseteq> carrier R; aGroup R; h \<in> mx; r \<in> carrier R; k = r \<cdot>\<^sub>r a; r \<cdot>\<^sub>r a \<in> carrier R; h \<in> carrier R; -\<^sub>a h \<in> mx; Unit R (-\<^sub>a h \<plusminus> (h \<plusminus> r \<cdot>\<^sub>r a))\<rbrakk> \<Longrightarrow> Unit R a
 2. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx; local_ring R \<and> maximal_ideal R mx\<rbrakk> \<Longrightarrow> local_ring R
[PROOF STEP]
apply (frule_tac h = "-\<^sub>a h" in ideal_subset[of "mx"], assumption,
        frule_tac x1 = "-\<^sub>a h" and y1 = h and z1 = "r \<cdot>\<^sub>r a" in
        aGroup.ag_pOp_assoc[THEN sym], assumption+,
        simp add:aGroup.ag_l_inv1 aGroup.ag_l_zero,
        thin_tac "k = r \<cdot>\<^sub>r a", thin_tac "h \<plusminus> r \<cdot>\<^sub>r a \<in> carrier R",
        thin_tac "h \<in> carrier R", thin_tac "-\<^sub>a h \<in> mx",
        thin_tac "-\<^sub>a h \<plusminus> (h \<plusminus> r \<cdot>\<^sub>r a) = r \<cdot>\<^sub>r a")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a h k r. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; ideal R mx; a \<in> carrier R; a \<notin> mx; ideal R {x. \<exists>r\<in>carrier R. x = r \<cdot>\<^sub>r a}; mx \<subseteq> carrier R; {x. \<exists>r\<in>carrier R. x = r \<cdot>\<^sub>r a} \<subseteq> carrier R; aGroup R; h \<in> mx; r \<in> carrier R; r \<cdot>\<^sub>r a \<in> carrier R; Unit R (r \<cdot>\<^sub>r a); -\<^sub>a h \<in> carrier R\<rbrakk> \<Longrightarrow> Unit R a
 2. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx; local_ring R \<and> maximal_ideal R mx\<rbrakk> \<Longrightarrow> local_ring R
[PROOF STEP]
apply (simp add:ring_tOp_commute, simp add:Unit_def, erule bexE,
        simp add:ring_tOp_assoc,
        frule_tac x = r and y = b in ring_tOp_closed, assumption+, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> zeroring R; maximal_ideal R mx; \<forall>x. x \<in> mx \<longrightarrow> Unit R (x \<plusminus> 1\<^sub>r); ideal R mx; local_ring R \<and> maximal_ideal R mx\<rbrakk> \<Longrightarrow> local_ring R
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) zeroring_J_rad_empty:"zeroring R \<Longrightarrow> J_rad R = carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zeroring R \<Longrightarrow> J_rad R = carrier R
[PROOF STEP]
by (simp add:J_rad_def)


[STATEMENT]
lemma (in Ring) J_rad_mem:"x \<in> J_rad R \<Longrightarrow> x \<in> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> J_rad R \<Longrightarrow> x \<in> carrier R
[PROOF STEP]
apply (simp add:J_rad_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> (if zeroring R then carrier R else \<Inter> {mx. maximal_ideal R mx}) \<Longrightarrow> x \<in> carrier R
[PROOF STEP]
apply (case_tac "zeroring R", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> (if zeroring R then carrier R else \<Inter> {mx. maximal_ideal R mx}); \<not> zeroring R\<rbrakk> \<Longrightarrow> x \<in> carrier R
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>xa. maximal_ideal R xa \<longrightarrow> x \<in> xa; \<not> zeroring R\<rbrakk> \<Longrightarrow> x \<in> carrier R
[PROOF STEP]
apply (frule id_maximal_Exist, erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>I. \<lbrakk>\<forall>xa. maximal_ideal R xa \<longrightarrow> x \<in> xa; \<not> zeroring R; maximal_ideal R I\<rbrakk> \<Longrightarrow> x \<in> carrier R
[PROOF STEP]
apply (frule_tac a = I in forall_spec, assumption,
        thin_tac "\<forall>xa. maximal_ideal R xa \<longrightarrow> x \<in> xa")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>I. \<lbrakk>\<not> zeroring R; maximal_ideal R I; x \<in> I\<rbrakk> \<Longrightarrow> x \<in> carrier R
[PROOF STEP]
apply (frule maximal_ideal_ideal,
        simp add:ideal_subset)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) J_rad_unit:"\<lbrakk>\<not> zeroring R; x \<in> J_rad R\<rbrakk> \<Longrightarrow>
            \<forall>y. (y\<in> carrier R \<longrightarrow> Unit R (1\<^sub>r \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> zeroring R; x \<in> J_rad R\<rbrakk> \<Longrightarrow> \<forall>y. y \<in> carrier R \<longrightarrow> Unit R (1\<^sub>r \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r y)
[PROOF STEP]
apply (cut_tac ring_is_ag,
       rule allI, rule impI,
       rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>\<not> zeroring R; x \<in> J_rad R; aGroup R; y \<in> carrier R; \<not> Unit R (1\<^sub>r \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r y)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule J_rad_mem[of "x"],
       frule_tac x = x and y = y in ring_tOp_closed, assumption,
       frule_tac x = "x \<cdot>\<^sub>r y" in aGroup.ag_mOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>\<not> zeroring R; x \<in> J_rad R; aGroup R; y \<in> carrier R; \<not> Unit R (1\<^sub>r \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r y); x \<in> carrier R; x \<cdot>\<^sub>r y \<in> carrier R; -\<^sub>a x \<cdot>\<^sub>r y \<in> carrier R\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cut_tac ring_one,
      frule_tac x = "1\<^sub>r" and y = "-\<^sub>a (x \<cdot>\<^sub>r y)" in aGroup.ag_pOp_closed,
      assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>\<not> zeroring R; x \<in> J_rad R; aGroup R; y \<in> carrier R; \<not> Unit R (1\<^sub>r \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r y); x \<in> carrier R; x \<cdot>\<^sub>r y \<in> carrier R; -\<^sub>a x \<cdot>\<^sub>r y \<in> carrier R; 1\<^sub>r \<in> carrier R; 1\<^sub>r \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y \<in> carrier R\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac a = "1\<^sub>r \<plusminus> -\<^sub>a (x \<cdot>\<^sub>r y)" in nonunit_contained_maxid,
        assumption+, simp add:ring_inv1_1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>\<not> zeroring R; x \<in> J_rad R; aGroup R; y \<in> carrier R; \<not> Unit R (1\<^sub>r \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r y); x \<in> carrier R; x \<cdot>\<^sub>r y \<in> carrier R; -\<^sub>a x \<cdot>\<^sub>r y \<in> carrier R; 1\<^sub>r \<in> carrier R; 1\<^sub>r \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y \<in> carrier R; \<exists>mx. maximal_ideal R mx \<and> 1\<^sub>r \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y \<in> mx\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule exE, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y mx. \<lbrakk>\<not> zeroring R; x \<in> J_rad R; aGroup R; y \<in> carrier R; \<not> Unit R (1\<^sub>r \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r y); x \<in> carrier R; x \<cdot>\<^sub>r y \<in> carrier R; -\<^sub>a x \<cdot>\<^sub>r y \<in> carrier R; 1\<^sub>r \<in> carrier R; 1\<^sub>r \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y \<in> carrier R; maximal_ideal R mx; 1\<^sub>r \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y \<in> mx\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:J_rad_def,
        frule_tac a = mx in forall_spec, assumption,
        thin_tac "\<forall>xa. maximal_ideal R xa \<longrightarrow> x \<in> xa",
        frule_tac mx = mx in maximal_ideal_ideal,
        frule_tac I = mx and x = x and r = y in ideal_ring_multiple1,
        assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y mx. \<lbrakk>\<not> zeroring R; aGroup R; y \<in> carrier R; \<not> Unit R (1\<^sub>r \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r y); x \<in> carrier R; x \<cdot>\<^sub>r y \<in> carrier R; -\<^sub>a x \<cdot>\<^sub>r y \<in> carrier R; 1\<^sub>r \<in> carrier R; 1\<^sub>r \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y \<in> carrier R; maximal_ideal R mx; 1\<^sub>r \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y \<in> mx; x \<in> mx; ideal R mx; x \<cdot>\<^sub>r y \<in> mx\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac I = mx and x = "x \<cdot>\<^sub>r y" in ideal_inv1_closed,
           assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y mx. \<lbrakk>\<not> zeroring R; aGroup R; y \<in> carrier R; \<not> Unit R (1\<^sub>r \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r y); x \<in> carrier R; x \<cdot>\<^sub>r y \<in> carrier R; -\<^sub>a x \<cdot>\<^sub>r y \<in> carrier R; 1\<^sub>r \<in> carrier R; 1\<^sub>r \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y \<in> carrier R; maximal_ideal R mx; 1\<^sub>r \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y \<in> mx; x \<in> mx; ideal R mx; x \<cdot>\<^sub>r y \<in> mx; -\<^sub>a x \<cdot>\<^sub>r y \<in> mx\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac I = mx and a = "1\<^sub>r" and b = "-\<^sub>a (x \<cdot>\<^sub>r y)" in ideal_ele_sumTr2,
        assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y mx. \<lbrakk>\<not> zeroring R; aGroup R; y \<in> carrier R; \<not> Unit R (1\<^sub>r \<plusminus> (-\<^sub>a x) \<cdot>\<^sub>r y); x \<in> carrier R; x \<cdot>\<^sub>r y \<in> carrier R; -\<^sub>a x \<cdot>\<^sub>r y \<in> carrier R; 1\<^sub>r \<in> carrier R; 1\<^sub>r \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y \<in> carrier R; maximal_ideal R mx; 1\<^sub>r \<plusminus> -\<^sub>a x \<cdot>\<^sub>r y \<in> mx; x \<in> mx; ideal R mx; x \<cdot>\<^sub>r y \<in> mx; -\<^sub>a x \<cdot>\<^sub>r y \<in> mx; 1\<^sub>r \<in> mx\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:maximal_ideal_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_solution_imp_solve_system:
  fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
  assumes xAb:"is_solution x A b"
  shows "is_solution x (fst (solve_system A b)) (snd (solve_system A b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_solution x (fst (solve_system A b)) (snd (solve_system A b))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_solution x (fst (solve_system A b)) (snd (solve_system A b))
[PROOF STEP]
have "(fst (Gauss_Jordan_PA A)*v(A *v x) = fst (Gauss_Jordan_PA A) *v b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Gauss_Jordan_PA A) *v (A *v x) = fst (Gauss_Jordan_PA A) *v b
[PROOF STEP]
using xAb
[PROOF STATE]
proof (prove)
using this:
is_solution x A b

goal (1 subgoal):
 1. fst (Gauss_Jordan_PA A) *v (A *v x) = fst (Gauss_Jordan_PA A) *v b
[PROOF STEP]
unfolding is_solution_def
[PROOF STATE]
proof (prove)
using this:
A *v x = b

goal (1 subgoal):
 1. fst (Gauss_Jordan_PA A) *v (A *v x) = fst (Gauss_Jordan_PA A) *v b
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
fst (Gauss_Jordan_PA A) *v (A *v x) = fst (Gauss_Jordan_PA A) *v b

goal (1 subgoal):
 1. is_solution x (fst (solve_system A b)) (snd (solve_system A b))
[PROOF STEP]
hence "(snd (Gauss_Jordan_PA A) *v x = fst (Gauss_Jordan_PA A) *v b)"
[PROOF STATE]
proof (prove)
using this:
fst (Gauss_Jordan_PA A) *v (A *v x) = fst (Gauss_Jordan_PA A) *v b

goal (1 subgoal):
 1. snd (Gauss_Jordan_PA A) *v x = fst (Gauss_Jordan_PA A) *v b
[PROOF STEP]
unfolding matrix_vector_mul_assoc
[PROOF STATE]
proof (prove)
using this:
fst (Gauss_Jordan_PA A) ** A *v x = fst (Gauss_Jordan_PA A) *v b

goal (1 subgoal):
 1. snd (Gauss_Jordan_PA A) *v x = fst (Gauss_Jordan_PA A) *v b
[PROOF STEP]
unfolding fst_Gauss_Jordan_PA[of A]
[PROOF STATE]
proof (prove)
using this:
snd (Gauss_Jordan_PA A) *v x = fst (Gauss_Jordan_PA A) *v b

goal (1 subgoal):
 1. snd (Gauss_Jordan_PA A) *v x = fst (Gauss_Jordan_PA A) *v b
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
snd (Gauss_Jordan_PA A) *v x = fst (Gauss_Jordan_PA A) *v b

goal (1 subgoal):
 1. is_solution x (fst (solve_system A b)) (snd (solve_system A b))
[PROOF STEP]
thus "is_solution x (fst (solve_system A b)) (snd (solve_system A b))"
[PROOF STATE]
proof (prove)
using this:
snd (Gauss_Jordan_PA A) *v x = fst (Gauss_Jordan_PA A) *v b

goal (1 subgoal):
 1. is_solution x (fst (solve_system A b)) (snd (solve_system A b))
[PROOF STEP]
unfolding is_solution_def solve_system_def Let_def
[PROOF STATE]
proof (prove)
using this:
snd (Gauss_Jordan_PA A) *v x = fst (Gauss_Jordan_PA A) *v b

goal (1 subgoal):
 1. fst (snd (Gauss_Jordan_PA A), fst (Gauss_Jordan_PA A) *v b) *v x = snd (snd (Gauss_Jordan_PA A), fst (Gauss_Jordan_PA A) *v b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_solution x (fst (solve_system A b)) (snd (solve_system A b))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma solve_system_imp_is_solution:
  fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
  assumes xAb: "is_solution x (fst (solve_system A b)) (snd (solve_system A b))"
  shows "is_solution x A b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_solution x A b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_solution x A b
[PROOF STEP]
have "fst (solve_system A b) *v x = snd (solve_system A b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (solve_system A b) *v x = snd (solve_system A b)
[PROOF STEP]
using xAb
[PROOF STATE]
proof (prove)
using this:
is_solution x (fst (solve_system A b)) (snd (solve_system A b))

goal (1 subgoal):
 1. fst (solve_system A b) *v x = snd (solve_system A b)
[PROOF STEP]
unfolding is_solution_def
[PROOF STATE]
proof (prove)
using this:
fst (solve_system A b) *v x = snd (solve_system A b)

goal (1 subgoal):
 1. fst (solve_system A b) *v x = snd (solve_system A b)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
fst (solve_system A b) *v x = snd (solve_system A b)

goal (1 subgoal):
 1. is_solution x A b
[PROOF STEP]
hence "snd (Gauss_Jordan_PA A) *v x = fst (Gauss_Jordan_PA A) *v b"
[PROOF STATE]
proof (prove)
using this:
fst (solve_system A b) *v x = snd (solve_system A b)

goal (1 subgoal):
 1. snd (Gauss_Jordan_PA A) *v x = fst (Gauss_Jordan_PA A) *v b
[PROOF STEP]
unfolding solve_system_def Let_def fst_conv snd_conv
[PROOF STATE]
proof (prove)
using this:
snd (Gauss_Jordan_PA A) *v x = fst (Gauss_Jordan_PA A) *v b

goal (1 subgoal):
 1. snd (Gauss_Jordan_PA A) *v x = fst (Gauss_Jordan_PA A) *v b
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
snd (Gauss_Jordan_PA A) *v x = fst (Gauss_Jordan_PA A) *v b

goal (1 subgoal):
 1. is_solution x A b
[PROOF STEP]
hence "(fst (Gauss_Jordan_PA A) ** A) *v x = fst (Gauss_Jordan_PA A) *v b"
[PROOF STATE]
proof (prove)
using this:
snd (Gauss_Jordan_PA A) *v x = fst (Gauss_Jordan_PA A) *v b

goal (1 subgoal):
 1. fst (Gauss_Jordan_PA A) ** A *v x = fst (Gauss_Jordan_PA A) *v b
[PROOF STEP]
unfolding fst_Gauss_Jordan_PA
[PROOF STATE]
proof (prove)
using this:
snd (Gauss_Jordan_PA A) *v x = fst (Gauss_Jordan_PA A) *v b

goal (1 subgoal):
 1. snd (Gauss_Jordan_PA A) *v x = fst (Gauss_Jordan_PA A) *v b
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
fst (Gauss_Jordan_PA A) ** A *v x = fst (Gauss_Jordan_PA A) *v b

goal (1 subgoal):
 1. is_solution x A b
[PROOF STEP]
hence "fst (Gauss_Jordan_PA A) *v (A *v x) = fst (Gauss_Jordan_PA A) *v b"
[PROOF STATE]
proof (prove)
using this:
fst (Gauss_Jordan_PA A) ** A *v x = fst (Gauss_Jordan_PA A) *v b

goal (1 subgoal):
 1. fst (Gauss_Jordan_PA A) *v (A *v x) = fst (Gauss_Jordan_PA A) *v b
[PROOF STEP]
unfolding matrix_vector_mul_assoc
[PROOF STATE]
proof (prove)
using this:
fst (Gauss_Jordan_PA A) ** A *v x = fst (Gauss_Jordan_PA A) *v b

goal (1 subgoal):
 1. fst (Gauss_Jordan_PA A) ** A *v x = fst (Gauss_Jordan_PA A) *v b
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
fst (Gauss_Jordan_PA A) *v (A *v x) = fst (Gauss_Jordan_PA A) *v b

goal (1 subgoal):
 1. is_solution x A b
[PROOF STEP]
hence "matrix_inv (fst (Gauss_Jordan_PA A)) *v (fst (Gauss_Jordan_PA A) *v (A *v x))
  = matrix_inv (fst (Gauss_Jordan_PA A)) *v (fst (Gauss_Jordan_PA A) *v b)"
[PROOF STATE]
proof (prove)
using this:
fst (Gauss_Jordan_PA A) *v (A *v x) = fst (Gauss_Jordan_PA A) *v b

goal (1 subgoal):
 1. matrix_inv (fst (Gauss_Jordan_PA A)) *v (fst (Gauss_Jordan_PA A) *v (A *v x)) = matrix_inv (fst (Gauss_Jordan_PA A)) *v (fst (Gauss_Jordan_PA A) *v b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
matrix_inv (fst (Gauss_Jordan_PA A)) *v (fst (Gauss_Jordan_PA A) *v (A *v x)) = matrix_inv (fst (Gauss_Jordan_PA A)) *v (fst (Gauss_Jordan_PA A) *v b)

goal (1 subgoal):
 1. is_solution x A b
[PROOF STEP]
hence "(A *v x) = b"
[PROOF STATE]
proof (prove)
using this:
matrix_inv (fst (Gauss_Jordan_PA A)) *v (fst (Gauss_Jordan_PA A) *v (A *v x)) = matrix_inv (fst (Gauss_Jordan_PA A)) *v (fst (Gauss_Jordan_PA A) *v b)

goal (1 subgoal):
 1. A *v x = b
[PROOF STEP]
unfolding matrix_vector_mul_assoc[of "matrix_inv (fst (Gauss_Jordan_PA A))"]
[PROOF STATE]
proof (prove)
using this:
matrix_inv (fst (Gauss_Jordan_PA A)) ** fst (Gauss_Jordan_PA A) *v (A *v x) = matrix_inv (fst (Gauss_Jordan_PA A)) ** fst (Gauss_Jordan_PA A) *v b

goal (1 subgoal):
 1. A *v x = b
[PROOF STEP]
unfolding matrix_inv_left[OF invertible_fst_Gauss_Jordan_PA]
[PROOF STATE]
proof (prove)
using this:
mat (1::'a) *v (A *v x) = mat (1::'a) *v b

goal (1 subgoal):
 1. A *v x = b
[PROOF STEP]
unfolding matrix_vector_mul_lid
[PROOF STATE]
proof (prove)
using this:
A *v x = b

goal (1 subgoal):
 1. A *v x = b
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A *v x = b

goal (1 subgoal):
 1. is_solution x A b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A *v x = b

goal (1 subgoal):
 1. is_solution x A b
[PROOF STEP]
unfolding is_solution_def
[PROOF STATE]
proof (prove)
using this:
A *v x = b

goal (1 subgoal):
 1. A *v x = b
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
is_solution x A b

goal:
No subgoals!
[PROOF STEP]
qed