[STATEMENT]
lemma (in Ring) maximal_prime:"maximal_ideal R mx \<Longrightarrow> prime_ideal R mx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maximal_ideal R mx \<Longrightarrow> prime_ideal R mx
[PROOF STEP]
apply (cut_tac ring_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maximal_ideal R mx; aGroup R\<rbrakk> \<Longrightarrow> prime_ideal R mx
[PROOF STEP]
apply (simp add:prime_ideal_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maximal_ideal R mx; aGroup R\<rbrakk> \<Longrightarrow> ideal R mx \<and> 1\<^sub>r \<notin> mx \<and> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> mx \<longrightarrow> x \<in> mx \<or> y \<in> mx)
[PROOF STEP]
apply (simp add:maximal_ideal_ideal)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maximal_ideal R mx; aGroup R\<rbrakk> \<Longrightarrow> 1\<^sub>r \<notin> mx \<and> (\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> mx \<longrightarrow> x \<in> mx \<or> y \<in> mx)
[PROOF STEP]
apply (simp add:maximal_ideal_proper)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maximal_ideal R mx; aGroup R\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier R. \<forall>y\<in>carrier R. x \<cdot>\<^sub>r y \<in> mx \<longrightarrow> x \<in> mx \<or> y \<in> mx
[PROOF STEP]
apply ((rule ballI)+, rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx\<rbrakk> \<Longrightarrow> x \<in> mx \<or> y \<in> mx
[PROOF STEP]
apply (rule contrapos_pp, simp+, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac x = x in maximal_prime_Tr0[of "mx"], assumption+,
       frule_tac x = y in maximal_prime_Tr0[of "mx"], assumption+,
       frule maximal_ideal_ideal[of mx],
       frule ideal_subset1[of mx],
       frule_tac a = x in principal_ideal,
       frule_tac a = y in principal_ideal,
       frule_tac I = "R \<diamondsuit>\<^sub>p x" in ideal_subset1,
       frule_tac I = "R \<diamondsuit>\<^sub>p y" in ideal_subset1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; mx \<minusplus> R \<diamondsuit>\<^sub>p x = carrier R; mx \<minusplus> R \<diamondsuit>\<^sub>p y = carrier R; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:aGroup.set_sum)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; {xa. \<exists>h\<in>mx. \<exists>k\<in>R \<diamondsuit>\<^sub>p x. xa = h \<plusminus> k} = carrier R; {x. \<exists>h\<in>mx. \<exists>k\<in>R \<diamondsuit>\<^sub>p y. x = h \<plusminus> k} = carrier R; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cut_tac ring_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; {xa. \<exists>h\<in>mx. \<exists>k\<in>R \<diamondsuit>\<^sub>p x. xa = h \<plusminus> k} = carrier R; {x. \<exists>h\<in>mx. \<exists>k\<in>R \<diamondsuit>\<^sub>p y. x = h \<plusminus> k} = carrier R; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; 1\<^sub>r \<in> carrier R\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule sym,
        thin_tac "{xa. \<exists>h\<in>mx. \<exists>k\<in>R \<diamondsuit>\<^sub>p x. xa = h \<plusminus> k} = carrier R",
        frule sym,
        thin_tac "{x. \<exists>h\<in>mx. \<exists>k\<in>R \<diamondsuit>\<^sub>p y. x = h \<plusminus> k} = carrier R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; 1\<^sub>r \<in> carrier R; carrier R = {xa. \<exists>h\<in>mx. \<exists>k\<in>R \<diamondsuit>\<^sub>p x. xa = h \<plusminus> k}; carrier R = {x. \<exists>h\<in>mx. \<exists>k\<in>R \<diamondsuit>\<^sub>p y. x = h \<plusminus> k}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac a = "1\<^sub>r" and B = "{xa. \<exists>i\<in>mx. \<exists>j\<in>(Rxa R x). xa = i \<plusminus> j}" in
                         eq_set_inc[of _ "carrier R"], assumption,
        frule_tac a = "1\<^sub>r" and B = "{xa. \<exists>i\<in>mx. \<exists>j\<in>(Rxa R y). xa = i \<plusminus> j}" in
                         eq_set_inc[of _ "carrier R"], assumption,
        thin_tac "carrier R = {xa. \<exists>i\<in>mx. \<exists>j\<in>(Rxa R x). xa = i \<plusminus> j}",
        thin_tac "carrier R = {x. \<exists>i\<in>mx. \<exists>j\<in>(Rxa R y). x = i \<plusminus> j}")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; 1\<^sub>r \<in> carrier R; 1\<^sub>r \<in> {xa. \<exists>i\<in>mx. \<exists>j\<in>R \<diamondsuit>\<^sub>p x. xa = i \<plusminus> j}; 1\<^sub>r \<in> {xa. \<exists>i\<in>mx. \<exists>j\<in>R \<diamondsuit>\<^sub>p y. xa = i \<plusminus> j}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule CollectD, (erule bexE)+,
        frule sym, thin_tac "1\<^sub>r = i \<plusminus> j")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y i j. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; 1\<^sub>r \<in> carrier R; 1\<^sub>r \<in> {xa. \<exists>i\<in>mx. \<exists>j\<in>R \<diamondsuit>\<^sub>p y. xa = i \<plusminus> j}; i \<in> mx; j \<in> R \<diamondsuit>\<^sub>p x; i \<plusminus> j = 1\<^sub>r\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule CollectD, (erule bexE)+, rotate_tac -1,
        frule sym, thin_tac "1\<^sub>r = ia \<plusminus> ja")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y i j ia ja. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; 1\<^sub>r \<in> carrier R; i \<in> mx; j \<in> R \<diamondsuit>\<^sub>p x; i \<plusminus> j = 1\<^sub>r; ia \<in> mx; ja \<in> R \<diamondsuit>\<^sub>p y; ia \<plusminus> ja = 1\<^sub>r\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac h = i in ideal_subset[of mx], assumption,
        frule_tac h = ia in ideal_subset[of mx], assumption,
        frule_tac h = j in ideal_subset, assumption+,
        frule_tac h = ja in ideal_subset, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y i j ia ja. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; 1\<^sub>r \<in> carrier R; i \<in> mx; j \<in> R \<diamondsuit>\<^sub>p x; i \<plusminus> j = 1\<^sub>r; ia \<in> mx; ja \<in> R \<diamondsuit>\<^sub>p y; ia \<plusminus> ja = 1\<^sub>r; i \<in> carrier R; ia \<in> carrier R; j \<in> carrier R; ja \<in> carrier R\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cut_tac ring_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y i j ia ja. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; 1\<^sub>r \<in> carrier R; i \<in> mx; j \<in> R \<diamondsuit>\<^sub>p x; i \<plusminus> j = 1\<^sub>r; ia \<in> mx; ja \<in> R \<diamondsuit>\<^sub>p y; ia \<plusminus> ja = 1\<^sub>r; i \<in> carrier R; ia \<in> carrier R; j \<in> carrier R; ja \<in> carrier R; 1\<^sub>r \<in> carrier R\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac x = i and y = j in aGroup.ag_pOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y i j ia ja. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; 1\<^sub>r \<in> carrier R; i \<in> mx; j \<in> R \<diamondsuit>\<^sub>p x; i \<plusminus> j = 1\<^sub>r; ia \<in> mx; ja \<in> R \<diamondsuit>\<^sub>p y; ia \<plusminus> ja = 1\<^sub>r; i \<in> carrier R; ia \<in> carrier R; j \<in> carrier R; ja \<in> carrier R; 1\<^sub>r \<in> carrier R; i \<plusminus> j \<in> carrier R\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac x = "i \<plusminus> j" and y = ia and z = ja in ring_distrib1,
           assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y i j ia ja. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; 1\<^sub>r \<in> carrier R; i \<in> mx; j \<in> R \<diamondsuit>\<^sub>p x; i \<plusminus> j = 1\<^sub>r; ia \<in> mx; ja \<in> R \<diamondsuit>\<^sub>p y; ia \<plusminus> ja = 1\<^sub>r; i \<in> carrier R; ia \<in> carrier R; j \<in> carrier R; ja \<in> carrier R; 1\<^sub>r \<in> carrier R; i \<plusminus> j \<in> carrier R; (i \<plusminus> j) \<cdot>\<^sub>r (ia \<plusminus> ja) = (i \<plusminus> j) \<cdot>\<^sub>r ia \<plusminus> (i \<plusminus> j) \<cdot>\<^sub>r ja\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac x = ia and y = i and z = j in ring_distrib2, assumption+,
        frule_tac x = ja and y = i and z = j in ring_distrib2, assumption+,
        simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y i j ia ja. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; i \<in> mx; j \<in> R \<diamondsuit>\<^sub>p x; i \<plusminus> j = 1\<^sub>r; ia \<in> mx; ja \<in> R \<diamondsuit>\<^sub>p y; ia \<plusminus> ja = 1\<^sub>r; i \<in> carrier R; ia \<in> carrier R; j \<in> carrier R; ja \<in> carrier R; 1\<^sub>r \<in> carrier R; 1\<^sub>r \<cdot>\<^sub>r 1\<^sub>r = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); 1\<^sub>r \<cdot>\<^sub>r ia = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia; 1\<^sub>r \<cdot>\<^sub>r ja = i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (thin_tac "1\<^sub>r \<cdot>\<^sub>r ia = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia",
        thin_tac "1\<^sub>r \<cdot>\<^sub>r ja = i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja",
        simp add:ring_l_one[of "1\<^sub>r"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y i j ia ja. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; i \<in> mx; j \<in> R \<diamondsuit>\<^sub>p x; i \<plusminus> j = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); ia \<in> mx; ja \<in> R \<diamondsuit>\<^sub>p y; ia \<plusminus> ja = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); i \<in> carrier R; ia \<in> carrier R; j \<in> carrier R; ja \<in> carrier R; i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja) \<in> carrier R; 1\<^sub>r = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac x = ia and r = i in ideal_ring_multiple[of mx], assumption+,
        frule_tac x = i and r = j in ideal_ring_multiple1[of mx], assumption+,
        frule_tac x = i and r = ja in ideal_ring_multiple1[of mx], assumption+,
        frule_tac r = j and x = ia in ideal_ring_multiple[of mx], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y i j ia ja. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; i \<in> mx; j \<in> R \<diamondsuit>\<^sub>p x; i \<plusminus> j = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); ia \<in> mx; ja \<in> R \<diamondsuit>\<^sub>p y; ia \<plusminus> ja = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); i \<in> carrier R; ia \<in> carrier R; j \<in> carrier R; ja \<in> carrier R; i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja) \<in> carrier R; 1\<^sub>r = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); i \<cdot>\<^sub>r ia \<in> mx; i \<cdot>\<^sub>r j \<in> mx; i \<cdot>\<^sub>r ja \<in> mx; j \<cdot>\<^sub>r ia \<in> mx\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (subgoal_tac "j \<cdot>\<^sub>r ja \<in> mx")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y i j ia ja. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; i \<in> mx; j \<in> R \<diamondsuit>\<^sub>p x; i \<plusminus> j = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); ia \<in> mx; ja \<in> R \<diamondsuit>\<^sub>p y; ia \<plusminus> ja = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); i \<in> carrier R; ia \<in> carrier R; j \<in> carrier R; ja \<in> carrier R; i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja) \<in> carrier R; 1\<^sub>r = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); i \<cdot>\<^sub>r ia \<in> mx; i \<cdot>\<^sub>r j \<in> mx; i \<cdot>\<^sub>r ja \<in> mx; j \<cdot>\<^sub>r ia \<in> mx; j \<cdot>\<^sub>r ja \<in> mx\<rbrakk> \<Longrightarrow> False
 2. \<And>x y i j ia ja. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; i \<in> mx; j \<in> R \<diamondsuit>\<^sub>p x; i \<plusminus> j = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); ia \<in> mx; ja \<in> R \<diamondsuit>\<^sub>p y; ia \<plusminus> ja = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); i \<in> carrier R; ia \<in> carrier R; j \<in> carrier R; ja \<in> carrier R; i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja) \<in> carrier R; 1\<^sub>r = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); i \<cdot>\<^sub>r ia \<in> mx; i \<cdot>\<^sub>r j \<in> mx; i \<cdot>\<^sub>r ja \<in> mx; j \<cdot>\<^sub>r ia \<in> mx\<rbrakk> \<Longrightarrow> j \<cdot>\<^sub>r ja \<in> mx
[PROOF STEP]
apply (frule_tac x = "i \<cdot>\<^sub>r ia" and y = "j \<cdot>\<^sub>r ia" in ideal_pOp_closed[of mx],
                   assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y i j ia ja. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; i \<in> mx; j \<in> R \<diamondsuit>\<^sub>p x; i \<plusminus> j = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); ia \<in> mx; ja \<in> R \<diamondsuit>\<^sub>p y; ia \<plusminus> ja = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); i \<in> carrier R; ia \<in> carrier R; j \<in> carrier R; ja \<in> carrier R; i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja) \<in> carrier R; 1\<^sub>r = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); i \<cdot>\<^sub>r ia \<in> mx; i \<cdot>\<^sub>r j \<in> mx; i \<cdot>\<^sub>r ja \<in> mx; j \<cdot>\<^sub>r ia \<in> mx; j \<cdot>\<^sub>r ja \<in> mx; i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<in> mx\<rbrakk> \<Longrightarrow> False
 2. \<And>x y i j ia ja. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; i \<in> mx; j \<in> R \<diamondsuit>\<^sub>p x; i \<plusminus> j = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); ia \<in> mx; ja \<in> R \<diamondsuit>\<^sub>p y; ia \<plusminus> ja = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); i \<in> carrier R; ia \<in> carrier R; j \<in> carrier R; ja \<in> carrier R; i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja) \<in> carrier R; 1\<^sub>r = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); i \<cdot>\<^sub>r ia \<in> mx; i \<cdot>\<^sub>r j \<in> mx; i \<cdot>\<^sub>r ja \<in> mx; j \<cdot>\<^sub>r ia \<in> mx\<rbrakk> \<Longrightarrow> j \<cdot>\<^sub>r ja \<in> mx
[PROOF STEP]
apply (
        frule_tac x = "i \<cdot>\<^sub>r ja" and y = "j \<cdot>\<^sub>r ja" in ideal_pOp_closed[of mx],
           assumption+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y i j ia ja. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; i \<in> mx; j \<in> R \<diamondsuit>\<^sub>p x; i \<plusminus> j = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); ia \<in> mx; ja \<in> R \<diamondsuit>\<^sub>p y; ia \<plusminus> ja = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); i \<in> carrier R; ia \<in> carrier R; j \<in> carrier R; ja \<in> carrier R; i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja) \<in> carrier R; 1\<^sub>r = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); i \<cdot>\<^sub>r ia \<in> mx; i \<cdot>\<^sub>r j \<in> mx; i \<cdot>\<^sub>r ja \<in> mx; j \<cdot>\<^sub>r ia \<in> mx; j \<cdot>\<^sub>r ja \<in> mx; i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<in> mx; i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja \<in> mx\<rbrakk> \<Longrightarrow> False
 2. \<And>x y i j ia ja. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; i \<in> mx; j \<in> R \<diamondsuit>\<^sub>p x; i \<plusminus> j = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); ia \<in> mx; ja \<in> R \<diamondsuit>\<^sub>p y; ia \<plusminus> ja = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); i \<in> carrier R; ia \<in> carrier R; j \<in> carrier R; ja \<in> carrier R; i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja) \<in> carrier R; 1\<^sub>r = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); i \<cdot>\<^sub>r ia \<in> mx; i \<cdot>\<^sub>r j \<in> mx; i \<cdot>\<^sub>r ja \<in> mx; j \<cdot>\<^sub>r ia \<in> mx\<rbrakk> \<Longrightarrow> j \<cdot>\<^sub>r ja \<in> mx
[PROOF STEP]
apply (frule_tac x = "i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia" and y = "i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja" in
          ideal_pOp_closed[of mx], assumption+,
        thin_tac "i \<plusminus> j = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja)",
        thin_tac "ia \<plusminus> ja = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y i j ia ja. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; i \<in> mx; j \<in> R \<diamondsuit>\<^sub>p x; ia \<in> mx; ja \<in> R \<diamondsuit>\<^sub>p y; i \<in> carrier R; ia \<in> carrier R; j \<in> carrier R; ja \<in> carrier R; i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja) \<in> carrier R; 1\<^sub>r = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); i \<cdot>\<^sub>r ia \<in> mx; i \<cdot>\<^sub>r j \<in> mx; i \<cdot>\<^sub>r ja \<in> mx; j \<cdot>\<^sub>r ia \<in> mx; j \<cdot>\<^sub>r ja \<in> mx; i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<in> mx; i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja \<in> mx; i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja) \<in> mx\<rbrakk> \<Longrightarrow> False
 2. \<And>x y i j ia ja. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; i \<in> mx; j \<in> R \<diamondsuit>\<^sub>p x; i \<plusminus> j = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); ia \<in> mx; ja \<in> R \<diamondsuit>\<^sub>p y; ia \<plusminus> ja = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); i \<in> carrier R; ia \<in> carrier R; j \<in> carrier R; ja \<in> carrier R; i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja) \<in> carrier R; 1\<^sub>r = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); i \<cdot>\<^sub>r ia \<in> mx; i \<cdot>\<^sub>r j \<in> mx; i \<cdot>\<^sub>r ja \<in> mx; j \<cdot>\<^sub>r ia \<in> mx\<rbrakk> \<Longrightarrow> j \<cdot>\<^sub>r ja \<in> mx
[PROOF STEP]
apply (frule sym, thin_tac "1\<^sub>r = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja)",
       simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y i j ia ja. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; i \<in> mx; j \<in> R \<diamondsuit>\<^sub>p x; ia \<in> mx; ja \<in> R \<diamondsuit>\<^sub>p y; i \<in> carrier R; ia \<in> carrier R; j \<in> carrier R; ja \<in> carrier R; 1\<^sub>r \<in> carrier R; i \<cdot>\<^sub>r ia \<in> mx; i \<cdot>\<^sub>r j \<in> mx; i \<cdot>\<^sub>r ja \<in> mx; j \<cdot>\<^sub>r ia \<in> mx; j \<cdot>\<^sub>r ja \<in> mx; i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<in> mx; i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja \<in> mx; 1\<^sub>r \<in> mx; i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja) = 1\<^sub>r\<rbrakk> \<Longrightarrow> False
 2. \<And>x y i j ia ja. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; i \<in> mx; j \<in> R \<diamondsuit>\<^sub>p x; i \<plusminus> j = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); ia \<in> mx; ja \<in> R \<diamondsuit>\<^sub>p y; ia \<plusminus> ja = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); i \<in> carrier R; ia \<in> carrier R; j \<in> carrier R; ja \<in> carrier R; i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja) \<in> carrier R; 1\<^sub>r = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); i \<cdot>\<^sub>r ia \<in> mx; i \<cdot>\<^sub>r j \<in> mx; i \<cdot>\<^sub>r ja \<in> mx; j \<cdot>\<^sub>r ia \<in> mx\<rbrakk> \<Longrightarrow> j \<cdot>\<^sub>r ja \<in> mx
[PROOF STEP]
apply (simp add:maximal_ideal_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y i j ia ja. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; ideal R (R \<diamondsuit>\<^sub>p x); ideal R (R \<diamondsuit>\<^sub>p y); R \<diamondsuit>\<^sub>p x \<subseteq> carrier R; R \<diamondsuit>\<^sub>p y \<subseteq> carrier R; i \<in> mx; j \<in> R \<diamondsuit>\<^sub>p x; i \<plusminus> j = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); ia \<in> mx; ja \<in> R \<diamondsuit>\<^sub>p y; ia \<plusminus> ja = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); i \<in> carrier R; ia \<in> carrier R; j \<in> carrier R; ja \<in> carrier R; i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja) \<in> carrier R; 1\<^sub>r = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja); i \<cdot>\<^sub>r ia \<in> mx; i \<cdot>\<^sub>r j \<in> mx; i \<cdot>\<^sub>r ja \<in> mx; j \<cdot>\<^sub>r ia \<in> mx\<rbrakk> \<Longrightarrow> j \<cdot>\<^sub>r ja \<in> mx
[PROOF STEP]
apply (thin_tac "i \<plusminus> j = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja)",
       thin_tac "ia \<plusminus> ja = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja)",
       thin_tac "i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja) \<in> carrier R",
       thin_tac "1\<^sub>r = i \<cdot>\<^sub>r ia \<plusminus> j \<cdot>\<^sub>r ia \<plusminus> (i \<cdot>\<^sub>r ja \<plusminus> j \<cdot>\<^sub>r ja)",
       thin_tac "i \<cdot>\<^sub>r j \<in> mx", thin_tac "i \<cdot>\<^sub>r ja \<in> mx",
       thin_tac "R \<diamondsuit>\<^sub>p y \<subseteq> carrier R", thin_tac "R \<diamondsuit>\<^sub>p x \<subseteq> carrier R",
       thin_tac "ideal R (R \<diamondsuit>\<^sub>p y)", thin_tac "ideal R (R \<diamondsuit>\<^sub>p x)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y i j ia ja. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; i \<in> mx; j \<in> R \<diamondsuit>\<^sub>p x; ia \<in> mx; ja \<in> R \<diamondsuit>\<^sub>p y; i \<in> carrier R; ia \<in> carrier R; j \<in> carrier R; ja \<in> carrier R; i \<cdot>\<^sub>r ia \<in> mx; j \<cdot>\<^sub>r ia \<in> mx\<rbrakk> \<Longrightarrow> j \<cdot>\<^sub>r ja \<in> mx
[PROOF STEP]
apply (simp add:Rxa_def, (erule bexE)+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y i j ia ja r ra. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; i \<in> mx; ia \<in> mx; i \<in> carrier R; ia \<in> carrier R; r \<cdot>\<^sub>r x \<in> carrier R; ra \<cdot>\<^sub>r y \<in> carrier R; i \<cdot>\<^sub>r ia \<in> mx; r \<cdot>\<^sub>r x \<cdot>\<^sub>r ia \<in> mx; r \<in> carrier R; j = r \<cdot>\<^sub>r x; ra \<in> carrier R; ja = ra \<cdot>\<^sub>r y\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r x \<cdot>\<^sub>r (ra \<cdot>\<^sub>r y) \<in> mx
[PROOF STEP]
apply (simp add:ring_tOp_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y i j ia ja r ra. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; i \<in> mx; ia \<in> mx; i \<in> carrier R; ia \<in> carrier R; r \<cdot>\<^sub>r x \<in> carrier R; ra \<cdot>\<^sub>r y \<in> carrier R; i \<cdot>\<^sub>r ia \<in> mx; r \<cdot>\<^sub>r (x \<cdot>\<^sub>r ia) \<in> mx; r \<in> carrier R; j = r \<cdot>\<^sub>r x; ra \<in> carrier R; ja = ra \<cdot>\<^sub>r y\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r (x \<cdot>\<^sub>r (ra \<cdot>\<^sub>r y)) \<in> mx
[PROOF STEP]
apply (simp add:ring_tOp_assoc[THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y i j ia ja r ra. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; i \<in> mx; ia \<in> mx; i \<in> carrier R; ia \<in> carrier R; r \<cdot>\<^sub>r x \<in> carrier R; ra \<cdot>\<^sub>r y \<in> carrier R; i \<cdot>\<^sub>r ia \<in> mx; r \<cdot>\<^sub>r x \<cdot>\<^sub>r ia \<in> mx; r \<in> carrier R; j = r \<cdot>\<^sub>r x; ra \<in> carrier R; ja = ra \<cdot>\<^sub>r y\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r (x \<cdot>\<^sub>r ra \<cdot>\<^sub>r y) \<in> mx
[PROOF STEP]
apply (frule_tac x = x and y = ra in ring_tOp_commute, assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y i j ia ja r ra. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; i \<in> mx; ia \<in> mx; i \<in> carrier R; ia \<in> carrier R; r \<cdot>\<^sub>r x \<in> carrier R; ra \<cdot>\<^sub>r y \<in> carrier R; i \<cdot>\<^sub>r ia \<in> mx; r \<cdot>\<^sub>r x \<cdot>\<^sub>r ia \<in> mx; r \<in> carrier R; j = r \<cdot>\<^sub>r x; ra \<in> carrier R; ja = ra \<cdot>\<^sub>r y; x \<cdot>\<^sub>r ra = ra \<cdot>\<^sub>r x\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r (ra \<cdot>\<^sub>r x \<cdot>\<^sub>r y) \<in> mx
[PROOF STEP]
apply (simp add:ring_tOp_assoc,
        frule_tac x = x and y = y in ring_tOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y i j ia ja r ra. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; i \<in> mx; ia \<in> mx; i \<in> carrier R; ia \<in> carrier R; r \<cdot>\<^sub>r x \<in> carrier R; ra \<cdot>\<^sub>r y \<in> carrier R; i \<cdot>\<^sub>r ia \<in> mx; r \<cdot>\<^sub>r (x \<cdot>\<^sub>r ia) \<in> mx; r \<in> carrier R; j = r \<cdot>\<^sub>r x; ra \<in> carrier R; ja = ra \<cdot>\<^sub>r y; x \<cdot>\<^sub>r ra = ra \<cdot>\<^sub>r x; x \<cdot>\<^sub>r y \<in> carrier R\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r (ra \<cdot>\<^sub>r (x \<cdot>\<^sub>r y)) \<in> mx
[PROOF STEP]
apply (frule_tac x1 = r and y1 = ra and z1 = "x \<cdot>\<^sub>r y" in
        ring_tOp_assoc[THEN sym], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y i j ia ja r ra. \<lbrakk>maximal_ideal R mx; aGroup R; x \<in> carrier R; y \<in> carrier R; x \<cdot>\<^sub>r y \<in> mx; x \<notin> mx; y \<notin> mx; ideal R mx; mx \<subseteq> carrier R; i \<in> mx; ia \<in> mx; i \<in> carrier R; ia \<in> carrier R; r \<cdot>\<^sub>r x \<in> carrier R; ra \<cdot>\<^sub>r y \<in> carrier R; i \<cdot>\<^sub>r ia \<in> mx; r \<cdot>\<^sub>r (x \<cdot>\<^sub>r ia) \<in> mx; r \<in> carrier R; j = r \<cdot>\<^sub>r x; ra \<in> carrier R; ja = ra \<cdot>\<^sub>r y; x \<cdot>\<^sub>r ra = ra \<cdot>\<^sub>r x; x \<cdot>\<^sub>r y \<in> carrier R; r \<cdot>\<^sub>r (ra \<cdot>\<^sub>r (x \<cdot>\<^sub>r y)) = r \<cdot>\<^sub>r ra \<cdot>\<^sub>r (x \<cdot>\<^sub>r y)\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r ra \<cdot>\<^sub>r (x \<cdot>\<^sub>r y) \<in> mx
[PROOF STEP]
apply (frule_tac x = r and y = ra in ring_tOp_closed, assumption+,
        rule ideal_ring_multiple[of mx], assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) chains_un:"\<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk>
       \<Longrightarrow> ideal R (\<Union>c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> ideal R (\<Union> c)
[PROOF STEP]
apply (rule ideal_condition1)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<Union> c \<subseteq> carrier R
 2. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<Union> c \<noteq> {}
 3. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>\<Union> c. \<forall>y\<in>\<Union> c. x \<plusminus> y \<in> \<Union> c
 4. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Union> c. r \<cdot>\<^sub>r x \<in> \<Union> c
[PROOF STEP]
apply (rule Union_least[of "c" "carrier R"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>X. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}; X \<in> c\<rbrakk> \<Longrightarrow> X \<subseteq> carrier R
 2. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<Union> c \<noteq> {}
 3. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>\<Union> c. \<forall>y\<in>\<Union> c. x \<plusminus> y \<in> \<Union> c
 4. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Union> c. r \<cdot>\<^sub>r x \<in> \<Union> c
[PROOF STEP]
apply (simp add:chains_def,
       erule conjE,
       frule_tac c = X in subsetD[of "c" "{I. ideal R I \<and> I \<subset> carrier R}"],
       assumption+, simp add:psubset_imp_subset)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<Union> c \<noteq> {}
 2. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>\<Union> c. \<forall>y\<in>\<Union> c. x \<plusminus> y \<in> \<Union> c
 3. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Union> c. r \<cdot>\<^sub>r x \<in> \<Union> c
[PROOF STEP]
apply (simp add:chains_def,
       erule conjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>c \<noteq> {}; c \<subseteq> {I. ideal R I \<and> I \<subset> carrier R}; chain\<^sub>\<subseteq> c\<rbrakk> \<Longrightarrow> \<exists>x\<in>c. x \<noteq> {}
 2. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>\<Union> c. \<forall>y\<in>\<Union> c. x \<plusminus> y \<in> \<Union> c
 3. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Union> c. r \<cdot>\<^sub>r x \<in> \<Union> c
[PROOF STEP]
apply (frule nonempty_ex[of "c"], erule exE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>c \<noteq> {}; c \<subseteq> {I. ideal R I \<and> I \<subset> carrier R}; chain\<^sub>\<subseteq> c; x \<in> c\<rbrakk> \<Longrightarrow> \<exists>x\<in>c. x \<noteq> {}
 2. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>\<Union> c. \<forall>y\<in>\<Union> c. x \<plusminus> y \<in> \<Union> c
 3. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Union> c. r \<cdot>\<^sub>r x \<in> \<Union> c
[PROOF STEP]
apply (frule_tac c = x in subsetD[of "c" "{I. ideal R I \<and> I \<subset> carrier R}"],
        assumption+, simp, erule conjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>c \<noteq> {}; c \<subseteq> {I. ideal R I \<and> I \<subset> carrier R}; chain\<^sub>\<subseteq> c; x \<in> c; ideal R x; x \<subset> carrier R\<rbrakk> \<Longrightarrow> \<exists>x\<in>c. x \<noteq> {}
 2. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>\<Union> c. \<forall>y\<in>\<Union> c. x \<plusminus> y \<in> \<Union> c
 3. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Union> c. r \<cdot>\<^sub>r x \<in> \<Union> c
[PROOF STEP]
apply (frule_tac I = x in ideal_zero, blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>\<Union> c. \<forall>y\<in>\<Union> c. x \<plusminus> y \<in> \<Union> c
 2. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Union> c. r \<cdot>\<^sub>r x \<in> \<Union> c
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}; x \<in> \<Union> c; y \<in> \<Union> c\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> \<Union> c
 2. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Union> c. r \<cdot>\<^sub>r x \<in> \<Union> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}; \<exists>X\<in>c. x \<in> X; \<exists>X\<in>c. y \<in> X\<rbrakk> \<Longrightarrow> \<exists>X\<in>c. x \<plusminus> y \<in> X
 2. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Union> c. r \<cdot>\<^sub>r x \<in> \<Union> c
[PROOF STEP]
apply (erule bexE)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y X Xa. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}; X \<in> c; x \<in> X; Xa \<in> c; y \<in> Xa\<rbrakk> \<Longrightarrow> \<exists>X\<in>c. x \<plusminus> y \<in> X
 2. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Union> c. r \<cdot>\<^sub>r x \<in> \<Union> c
[PROOF STEP]
apply (simp add: chains_def chain_subset_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y X Xa. \<lbrakk>c \<subseteq> {I. ideal R I \<and> I \<subset> carrier R} \<and> (\<forall>A\<in>c. \<forall>B\<in>c. A \<subseteq> B \<or> B \<subseteq> A); c \<noteq> {}; X \<in> c; x \<in> X; Xa \<in> c; y \<in> Xa\<rbrakk> \<Longrightarrow> \<exists>X\<in>c. x \<plusminus> y \<in> X
 2. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Union> c. r \<cdot>\<^sub>r x \<in> \<Union> c
[PROOF STEP]
apply (frule conjunct1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y X Xa. \<lbrakk>c \<subseteq> {I. ideal R I \<and> I \<subset> carrier R} \<and> (\<forall>A\<in>c. \<forall>B\<in>c. A \<subseteq> B \<or> B \<subseteq> A); c \<noteq> {}; X \<in> c; x \<in> X; Xa \<in> c; y \<in> Xa; c \<subseteq> {I. ideal R I \<and> I \<subset> carrier R}\<rbrakk> \<Longrightarrow> \<exists>X\<in>c. x \<plusminus> y \<in> X
 2. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Union> c. r \<cdot>\<^sub>r x \<in> \<Union> c
[PROOF STEP]
apply (frule conjunct2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y X Xa. \<lbrakk>c \<subseteq> {I. ideal R I \<and> I \<subset> carrier R} \<and> (\<forall>A\<in>c. \<forall>B\<in>c. A \<subseteq> B \<or> B \<subseteq> A); c \<noteq> {}; X \<in> c; x \<in> X; Xa \<in> c; y \<in> Xa; c \<subseteq> {I. ideal R I \<and> I \<subset> carrier R}; \<forall>A\<in>c. \<forall>B\<in>c. A \<subseteq> B \<or> B \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>X\<in>c. x \<plusminus> y \<in> X
 2. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Union> c. r \<cdot>\<^sub>r x \<in> \<Union> c
[PROOF STEP]
apply (thin_tac "c \<subseteq> {I. ideal R I \<and> I \<subset> carrier R} \<and> (\<forall>x\<in>c. \<forall>y\<in>c. x \<subseteq> y \<or> y \<subseteq> x)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y X Xa. \<lbrakk>c \<noteq> {}; X \<in> c; x \<in> X; Xa \<in> c; y \<in> Xa; c \<subseteq> {I. ideal R I \<and> I \<subset> carrier R}; \<forall>A\<in>c. \<forall>B\<in>c. A \<subseteq> B \<or> B \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>X\<in>c. x \<plusminus> y \<in> X
 2. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Union> c. r \<cdot>\<^sub>r x \<in> \<Union> c
[PROOF STEP]
apply (frule_tac x = X in bspec, assumption,
        thin_tac "\<forall>x\<in>c. \<forall>y\<in>c. x \<subseteq> y \<or> y \<subseteq> x",
        frule_tac x = Xa in bspec, assumption,
        thin_tac "\<forall>y\<in>c. X \<subseteq> y \<or> y \<subseteq> X")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y X Xa. \<lbrakk>c \<noteq> {}; X \<in> c; x \<in> X; Xa \<in> c; y \<in> Xa; c \<subseteq> {I. ideal R I \<and> I \<subset> carrier R}; X \<subseteq> Xa \<or> Xa \<subseteq> X\<rbrakk> \<Longrightarrow> \<exists>X\<in>c. x \<plusminus> y \<in> X
 2. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Union> c. r \<cdot>\<^sub>r x \<in> \<Union> c
[PROOF STEP]
apply (frule_tac c = Xa in subsetD[of "c" "{I. ideal R I \<and> I \<subset> carrier R}"],
          assumption+,
        frule_tac c = X in subsetD[of "c" "{I. ideal R I \<and> I \<subset> carrier R}"],
          assumption+, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y X Xa. \<lbrakk>c \<noteq> {}; X \<in> c; x \<in> X; Xa \<in> c; y \<in> Xa; c \<subseteq> {I. ideal R I \<and> I \<subset> carrier R}; X \<subseteq> Xa \<or> Xa \<subseteq> X; ideal R Xa \<and> Xa \<subset> carrier R; ideal R X \<and> X \<subset> carrier R\<rbrakk> \<Longrightarrow> \<exists>X\<in>c. x \<plusminus> y \<in> X
 2. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Union> c. r \<cdot>\<^sub>r x \<in> \<Union> c
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y X Xa. \<lbrakk>c \<noteq> {}; X \<in> c; x \<in> X; Xa \<in> c; y \<in> Xa; c \<subseteq> {I. ideal R I \<and> I \<subset> carrier R}; X \<subseteq> Xa \<or> Xa \<subseteq> X; ideal R Xa; Xa \<subset> carrier R; ideal R X; X \<subset> carrier R\<rbrakk> \<Longrightarrow> \<exists>X\<in>c. x \<plusminus> y \<in> X
 2. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Union> c. r \<cdot>\<^sub>r x \<in> \<Union> c
[PROOF STEP]
apply (erule disjE,
        frule_tac c = x and A = X and B = Xa in subsetD, assumption+,
        frule_tac x = x and y = y and I = Xa in ideal_pOp_closed, assumption+,
        blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y X Xa. \<lbrakk>c \<noteq> {}; X \<in> c; x \<in> X; Xa \<in> c; y \<in> Xa; c \<subseteq> {I. ideal R I \<and> I \<subset> carrier R}; ideal R Xa; Xa \<subset> carrier R; ideal R X; X \<subset> carrier R; Xa \<subseteq> X\<rbrakk> \<Longrightarrow> \<exists>X\<in>c. x \<plusminus> y \<in> X
 2. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Union> c. r \<cdot>\<^sub>r x \<in> \<Union> c
[PROOF STEP]
apply (frule_tac c = y and A = Xa and B = X in subsetD, assumption+,
        frule_tac x = x and y = y and I = X in ideal_pOp_closed, assumption+,
        blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Union> c. r \<cdot>\<^sub>r x \<in> \<Union> c
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}; r \<in> carrier R; x \<in> \<Union> c\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r x \<in> \<Union> c
[PROOF STEP]
apply (simp, erule bexE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x X. \<lbrakk>c \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; c \<noteq> {}; r \<in> carrier R; X \<in> c; x \<in> X\<rbrakk> \<Longrightarrow> \<exists>X\<in>c. r \<cdot>\<^sub>r x \<in> X
[PROOF STEP]
apply (simp add:chains_def, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x X. \<lbrakk>c \<noteq> {}; r \<in> carrier R; X \<in> c; x \<in> X; c \<subseteq> {I. ideal R I \<and> I \<subset> carrier R}; chain\<^sub>\<subseteq> c\<rbrakk> \<Longrightarrow> \<exists>X\<in>c. r \<cdot>\<^sub>r x \<in> X
[PROOF STEP]
apply (frule_tac c = X in subsetD[of "c" "{I. ideal R I \<and> I \<subset> carrier R}"],
        assumption+, simp, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x X. \<lbrakk>c \<noteq> {}; r \<in> carrier R; X \<in> c; x \<in> X; c \<subseteq> {I. ideal R I \<and> I \<subset> carrier R}; chain\<^sub>\<subseteq> c; ideal R X; X \<subset> carrier R\<rbrakk> \<Longrightarrow> \<exists>X\<in>c. r \<cdot>\<^sub>r x \<in> X
[PROOF STEP]
apply (frule_tac I = X and x = x and r = r in ideal_ring_multiple,
        assumption+, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) zeroring_no_maximal:"zeroring R \<Longrightarrow> \<not> (\<exists>I. maximal_ideal R I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zeroring R \<Longrightarrow> \<nexists>I. maximal_ideal R I
[PROOF STEP]
apply (rule contrapos_pp, simp+, erule exE,
       frule_tac mx = x in maximal_ideal_ideal)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>zeroring R; maximal_ideal R x; ideal R x\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac I = x in ideal_zero)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>zeroring R; maximal_ideal R x; ideal R x; \<zero> \<in> x\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:zeroring_def, erule conjE,
       cut_tac ring_one, simp, thin_tac "carrier R = {\<zero>}",
        frule sym, thin_tac "1\<^sub>r = \<zero>", simp, thin_tac "\<zero> = 1\<^sub>r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>maximal_ideal R x; ideal R x; 1\<^sub>r \<in> x; Ring R\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:maximal_ideal_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) id_maximal_Exist:"\<not>(zeroring R) \<Longrightarrow> \<exists>I. maximal_ideal R I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> zeroring R \<Longrightarrow> \<exists>I. maximal_ideal R I
[PROOF STEP]
apply (cut_tac A="{ I. ideal R I \<and> I \<subset> carrier R }" in Zorn_Lemma2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<not> zeroring R \<Longrightarrow> \<forall>C\<in>chains {I. ideal R I \<and> I \<subset> carrier R}. \<exists>U\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>C. X \<subseteq> U
 2. \<lbrakk>\<not> zeroring R; \<exists>M\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>{I. ideal R I \<and> I \<subset> carrier R}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>I. maximal_ideal R I
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C. \<lbrakk>\<not> zeroring R; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}\<rbrakk> \<Longrightarrow> \<exists>U\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>C. X \<subseteq> U
 2. \<lbrakk>\<not> zeroring R; \<exists>M\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>{I. ideal R I \<and> I \<subset> carrier R}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>I. maximal_ideal R I
[PROOF STEP]
apply (case_tac "C={}", simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C. \<lbrakk>\<not> zeroring R; {} \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; C = {}\<rbrakk> \<Longrightarrow> \<exists>U. ideal R U \<and> U \<subset> carrier R
 2. \<And>C. \<lbrakk>\<not> zeroring R; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>U\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>C. X \<subseteq> U
 3. \<lbrakk>\<not> zeroring R; \<exists>M\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>{I. ideal R I \<and> I \<subset> carrier R}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>I. maximal_ideal R I
[PROOF STEP]
apply (cut_tac zero_ideal)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C. \<lbrakk>\<not> zeroring R; {} \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; C = {}; ideal R {\<zero>}\<rbrakk> \<Longrightarrow> \<exists>U. ideal R U \<and> U \<subset> carrier R
 2. \<And>C. \<lbrakk>\<not> zeroring R; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>U\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>C. X \<subseteq> U
 3. \<lbrakk>\<not> zeroring R; \<exists>M\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>{I. ideal R I \<and> I \<subset> carrier R}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>I. maximal_ideal R I
[PROOF STEP]
apply (simp add:zeroring_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C. \<lbrakk>Ring R \<longrightarrow> carrier R \<noteq> {\<zero>}; {} \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; C = {}; ideal R {\<zero>}\<rbrakk> \<Longrightarrow> \<exists>U. ideal R U \<and> U \<subset> carrier R
 2. \<And>C. \<lbrakk>\<not> zeroring R; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>U\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>C. X \<subseteq> U
 3. \<lbrakk>\<not> zeroring R; \<exists>M\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>{I. ideal R I \<and> I \<subset> carrier R}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>I. maximal_ideal R I
[PROOF STEP]
apply (cut_tac Ring, simp,
           frule not_sym, thin_tac "carrier R \<noteq> {\<zero>}")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C. \<lbrakk>{} \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; C = {}; ideal R {\<zero>}; Ring R; {\<zero>} \<noteq> carrier R\<rbrakk> \<Longrightarrow> \<exists>U. ideal R U \<and> U \<subset> carrier R
 2. \<And>C. \<lbrakk>\<not> zeroring R; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>U\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>C. X \<subseteq> U
 3. \<lbrakk>\<not> zeroring R; \<exists>M\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>{I. ideal R I \<and> I \<subset> carrier R}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>I. maximal_ideal R I
[PROOF STEP]
apply (cut_tac ring_zero,
         frule singleton_sub[of "\<zero>" "carrier R"],
         thin_tac "\<zero> \<in> carrier R")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C. \<lbrakk>{} \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; C = {}; ideal R {\<zero>}; Ring R; {\<zero>} \<noteq> carrier R; {\<zero>} \<subseteq> carrier R\<rbrakk> \<Longrightarrow> \<exists>U. ideal R U \<and> U \<subset> carrier R
 2. \<And>C. \<lbrakk>\<not> zeroring R; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>U\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>C. X \<subseteq> U
 3. \<lbrakk>\<not> zeroring R; \<exists>M\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>{I. ideal R I \<and> I \<subset> carrier R}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>I. maximal_ideal R I
[PROOF STEP]
apply (subst psubset_eq)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C. \<lbrakk>{} \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; C = {}; ideal R {\<zero>}; Ring R; {\<zero>} \<noteq> carrier R; {\<zero>} \<subseteq> carrier R\<rbrakk> \<Longrightarrow> \<exists>U. ideal R U \<and> U \<subseteq> carrier R \<and> U \<noteq> carrier R
 2. \<And>C. \<lbrakk>\<not> zeroring R; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>U\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>C. X \<subseteq> U
 3. \<lbrakk>\<not> zeroring R; \<exists>M\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>{I. ideal R I \<and> I \<subset> carrier R}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>I. maximal_ideal R I
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C. \<lbrakk>\<not> zeroring R; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>U\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>C. X \<subseteq> U
 2. \<lbrakk>\<not> zeroring R; \<exists>M\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>{I. ideal R I \<and> I \<subset> carrier R}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>I. maximal_ideal R I
[PROOF STEP]
apply (subgoal_tac "\<Union>C \<in> {I. ideal R I \<and> I \<subset> carrier R}")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C. \<lbrakk>\<not> zeroring R; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; C \<noteq> {}; \<Union> C \<in> {I. ideal R I \<and> I \<subset> carrier R}\<rbrakk> \<Longrightarrow> \<exists>U\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>C. X \<subseteq> U
 2. \<And>C. \<lbrakk>\<not> zeroring R; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<Union> C \<in> {I. ideal R I \<and> I \<subset> carrier R}
 3. \<lbrakk>\<not> zeroring R; \<exists>M\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>{I. ideal R I \<and> I \<subset> carrier R}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>I. maximal_ideal R I
[PROOF STEP]
apply (subgoal_tac "\<forall>x\<in>C. x \<subseteq> (\<Union>C)", blast)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C. \<lbrakk>\<not> zeroring R; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; C \<noteq> {}; \<Union> C \<in> {I. ideal R I \<and> I \<subset> carrier R}\<rbrakk> \<Longrightarrow> \<forall>x\<in>C. x \<subseteq> \<Union> C
 2. \<And>C. \<lbrakk>\<not> zeroring R; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<Union> C \<in> {I. ideal R I \<and> I \<subset> carrier R}
 3. \<lbrakk>\<not> zeroring R; \<exists>M\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>{I. ideal R I \<and> I \<subset> carrier R}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>I. maximal_ideal R I
[PROOF STEP]
apply (rule ballI, rule Union_upper, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C. \<lbrakk>\<not> zeroring R; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<Union> C \<in> {I. ideal R I \<and> I \<subset> carrier R}
 2. \<lbrakk>\<not> zeroring R; \<exists>M\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>{I. ideal R I \<and> I \<subset> carrier R}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>I. maximal_ideal R I
[PROOF STEP]
apply (simp add:chains_un)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C. \<lbrakk>\<not> zeroring R; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; C \<noteq> {}\<rbrakk> \<Longrightarrow> \<Union> C \<subset> carrier R
 2. \<lbrakk>\<not> zeroring R; \<exists>M\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>{I. ideal R I \<and> I \<subset> carrier R}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>I. maximal_ideal R I
[PROOF STEP]
apply (cut_tac A = C in Union_least[of _ "carrier R"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>C X. \<lbrakk>\<not> zeroring R; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; C \<noteq> {}; X \<in> C\<rbrakk> \<Longrightarrow> X \<subseteq> carrier R
 2. \<And>C. \<lbrakk>\<not> zeroring R; C \<in> chains {I. ideal R I \<and> I \<subset> carrier R}; C \<noteq> {}; \<Union> C \<subseteq> carrier R\<rbrakk> \<Longrightarrow> \<Union> C \<subset> carrier R
 3. \<lbrakk>\<not> zeroring R; \<exists>M\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>{I. ideal R I \<and> I \<subset> carrier R}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>I. maximal_ideal R I
[PROOF STEP]
apply (simp add:chains_def, erule conjE,
        frule_tac c = X and A = C in
          subsetD[of _ "{I. ideal R I \<and> I \<subset> carrier R}"], assumption+,
          simp add:ideal_subset1, simp add:psubset_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C. \<lbrakk>\<not> zeroring R; C \<in> chains {I. ideal R I \<and> I \<subseteq> carrier R \<and> I \<noteq> carrier R}; C \<noteq> {}; \<Union> C \<subseteq> carrier R\<rbrakk> \<Longrightarrow> \<Union> C \<noteq> carrier R
 2. \<lbrakk>\<not> zeroring R; \<exists>M\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>{I. ideal R I \<and> I \<subset> carrier R}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>I. maximal_ideal R I
[PROOF STEP]
apply (rule contrapos_pp, simp+,
         cut_tac ring_one, frule sym, thin_tac "\<Union>C = carrier R")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C. \<lbrakk>\<not> zeroring R; C \<in> chains {I. ideal R I \<and> I \<subseteq> carrier R \<and> I \<noteq> carrier R}; C \<noteq> {}; 1\<^sub>r \<in> carrier R; carrier R = \<Union> C\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<not> zeroring R; \<exists>M\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>{I. ideal R I \<and> I \<subset> carrier R}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>I. maximal_ideal R I
[PROOF STEP]
apply (frule_tac B = "\<Union>C" in eq_set_inc[of "1\<^sub>r" "carrier R"], assumption,
         thin_tac "carrier R = \<Union>C")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C. \<lbrakk>\<not> zeroring R; C \<in> chains {I. ideal R I \<and> I \<subseteq> carrier R \<and> I \<noteq> carrier R}; C \<noteq> {}; 1\<^sub>r \<in> carrier R; 1\<^sub>r \<in> \<Union> C\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<not> zeroring R; \<exists>M\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>{I. ideal R I \<and> I \<subset> carrier R}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>I. maximal_ideal R I
[PROOF STEP]
apply (simp, erule bexE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C X. \<lbrakk>\<not> zeroring R; C \<in> chains {I. ideal R I \<and> I \<subseteq> carrier R \<and> I \<noteq> carrier R}; C \<noteq> {}; 1\<^sub>r \<in> carrier R; X \<in> C; 1\<^sub>r \<in> X\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<not> zeroring R; \<exists>M\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>{I. ideal R I \<and> I \<subset> carrier R}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>I. maximal_ideal R I
[PROOF STEP]
apply (simp add:chains_def, erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C X. \<lbrakk>\<not> zeroring R; C \<noteq> {}; 1\<^sub>r \<in> carrier R; X \<in> C; 1\<^sub>r \<in> X; C \<subseteq> {I. ideal R I \<and> I \<subseteq> carrier R \<and> I \<noteq> carrier R}; chain\<^sub>\<subseteq> C\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<not> zeroring R; \<exists>M\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>{I. ideal R I \<and> I \<subset> carrier R}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>I. maximal_ideal R I
[PROOF STEP]
apply (frule_tac c = X and A = C in
         subsetD[of _ "{I. ideal R I \<and> I \<subseteq> carrier R \<and> I \<noteq> carrier R}"],
         assumption+, simp, (erule conjE)+)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>C X. \<lbrakk>\<not> zeroring R; C \<noteq> {}; 1\<^sub>r \<in> carrier R; X \<in> C; 1\<^sub>r \<in> X; C \<subseteq> {I. ideal R I \<and> I \<subseteq> carrier R \<and> I \<noteq> carrier R}; chain\<^sub>\<subseteq> C; ideal R X; X \<subseteq> carrier R; X \<noteq> carrier R\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<not> zeroring R; \<exists>M\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>{I. ideal R I \<and> I \<subset> carrier R}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>I. maximal_ideal R I
[PROOF STEP]
apply (frule_tac I = X in ideal_inc_one, assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> zeroring R; \<exists>M\<in>{I. ideal R I \<and> I \<subset> carrier R}. \<forall>X\<in>{I. ideal R I \<and> I \<subset> carrier R}. M \<subseteq> X \<longrightarrow> X = M\<rbrakk> \<Longrightarrow> \<exists>I. maximal_ideal R I
[PROOF STEP]
apply (erule bexE, simp, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M. \<lbrakk>\<not> zeroring R; \<forall>X. ideal R X \<and> X \<subset> carrier R \<longrightarrow> M \<subseteq> X \<longrightarrow> X = M; ideal R M; M \<subset> carrier R\<rbrakk> \<Longrightarrow> \<exists>I. maximal_ideal R I
[PROOF STEP]
apply (subgoal_tac "maximal_ideal R M", blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M. \<lbrakk>\<not> zeroring R; \<forall>X. ideal R X \<and> X \<subset> carrier R \<longrightarrow> M \<subseteq> X \<longrightarrow> X = M; ideal R M; M \<subset> carrier R\<rbrakk> \<Longrightarrow> maximal_ideal R M
[PROOF STEP]
apply (simp add:maximal_ideal_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M. \<lbrakk>\<not> zeroring R; \<forall>X. ideal R X \<and> X \<subset> carrier R \<longrightarrow> M \<subseteq> X \<longrightarrow> X = M; ideal R M; M \<subset> carrier R\<rbrakk> \<Longrightarrow> 1\<^sub>r \<notin> M \<and> {J. ideal R J \<and> M \<subseteq> J} = {M, carrier R}
[PROOF STEP]
apply (rule conjI, rule contrapos_pp, simp+,
       frule_tac  I = M in ideal_inc_one, assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M. \<lbrakk>\<not> zeroring R; \<forall>X. ideal R X \<and> X \<subset> carrier R \<longrightarrow> M \<subseteq> X \<longrightarrow> X = M; ideal R M; M \<subset> carrier R\<rbrakk> \<Longrightarrow> {J. ideal R J \<and> M \<subseteq> J} = {M, carrier R}
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>M. \<lbrakk>\<not> zeroring R; \<forall>X. ideal R X \<and> X \<subset> carrier R \<longrightarrow> M \<subseteq> X \<longrightarrow> X = M; ideal R M; M \<subset> carrier R\<rbrakk> \<Longrightarrow> {J. ideal R J \<and> M \<subseteq> J} \<subseteq> {M, carrier R}
 2. \<And>M. \<lbrakk>\<not> zeroring R; \<forall>X. ideal R X \<and> X \<subset> carrier R \<longrightarrow> M \<subseteq> X \<longrightarrow> X = M; ideal R M; M \<subset> carrier R\<rbrakk> \<Longrightarrow> {M, carrier R} \<subseteq> {J. ideal R J \<and> M \<subseteq> J}
[PROOF STEP]
apply (rule subsetI, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>M x. \<lbrakk>\<not> zeroring R; \<forall>X. ideal R X \<and> X \<subset> carrier R \<longrightarrow> M \<subseteq> X \<longrightarrow> X = M; ideal R M; M \<subset> carrier R; ideal R x \<and> M \<subseteq> x\<rbrakk> \<Longrightarrow> x = M \<or> x = carrier R
 2. \<And>M. \<lbrakk>\<not> zeroring R; \<forall>X. ideal R X \<and> X \<subset> carrier R \<longrightarrow> M \<subseteq> X \<longrightarrow> X = M; ideal R M; M \<subset> carrier R\<rbrakk> \<Longrightarrow> {M, carrier R} \<subseteq> {J. ideal R J \<and> M \<subseteq> J}
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>M x. \<lbrakk>\<not> zeroring R; \<forall>X. ideal R X \<and> X \<subset> carrier R \<longrightarrow> M \<subseteq> X \<longrightarrow> X = M; ideal R M; M \<subset> carrier R; ideal R x; M \<subseteq> x\<rbrakk> \<Longrightarrow> x = M \<or> x = carrier R
 2. \<And>M. \<lbrakk>\<not> zeroring R; \<forall>X. ideal R X \<and> X \<subset> carrier R \<longrightarrow> M \<subseteq> X \<longrightarrow> X = M; ideal R M; M \<subset> carrier R\<rbrakk> \<Longrightarrow> {M, carrier R} \<subseteq> {J. ideal R J \<and> M \<subseteq> J}
[PROOF STEP]
apply (frule_tac x = x in spec,
        thin_tac "\<forall>x. ideal R x \<and> x \<subset> carrier R \<longrightarrow> M \<subseteq> x \<longrightarrow> x = M", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>M x. \<lbrakk>\<not> zeroring R; ideal R M; M \<subset> carrier R; ideal R x; M \<subseteq> x; x \<subset> carrier R \<longrightarrow> x = M\<rbrakk> \<Longrightarrow> x = M \<or> x = carrier R
 2. \<And>M. \<lbrakk>\<not> zeroring R; \<forall>X. ideal R X \<and> X \<subset> carrier R \<longrightarrow> M \<subseteq> X \<longrightarrow> X = M; ideal R M; M \<subset> carrier R\<rbrakk> \<Longrightarrow> {M, carrier R} \<subseteq> {J. ideal R J \<and> M \<subseteq> J}
[PROOF STEP]
apply (frule_tac I = x in ideal_subset1, simp add:psubset_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>M x. \<lbrakk>\<not> zeroring R; ideal R M; M \<subseteq> carrier R \<and> M \<noteq> carrier R; ideal R x; M \<subseteq> x; x \<noteq> carrier R \<longrightarrow> x = M; x \<subseteq> carrier R\<rbrakk> \<Longrightarrow> x = M \<or> x = carrier R
 2. \<And>M. \<lbrakk>\<not> zeroring R; \<forall>X. ideal R X \<and> X \<subset> carrier R \<longrightarrow> M \<subseteq> X \<longrightarrow> X = M; ideal R M; M \<subset> carrier R\<rbrakk> \<Longrightarrow> {M, carrier R} \<subseteq> {J. ideal R J \<and> M \<subseteq> J}
[PROOF STEP]
apply (case_tac "x = carrier R", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>M x. \<lbrakk>\<not> zeroring R; ideal R M; M \<subseteq> carrier R \<and> M \<noteq> carrier R; ideal R x; M \<subseteq> x; x \<noteq> carrier R \<longrightarrow> x = M; x \<subseteq> carrier R; x \<noteq> carrier R\<rbrakk> \<Longrightarrow> x = M \<or> x = carrier R
 2. \<And>M. \<lbrakk>\<not> zeroring R; \<forall>X. ideal R X \<and> X \<subset> carrier R \<longrightarrow> M \<subseteq> X \<longrightarrow> X = M; ideal R M; M \<subset> carrier R\<rbrakk> \<Longrightarrow> {M, carrier R} \<subseteq> {J. ideal R J \<and> M \<subseteq> J}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M. \<lbrakk>\<not> zeroring R; \<forall>X. ideal R X \<and> X \<subset> carrier R \<longrightarrow> M \<subseteq> X \<longrightarrow> X = M; ideal R M; M \<subset> carrier R\<rbrakk> \<Longrightarrow> {M, carrier R} \<subseteq> {J. ideal R J \<and> M \<subseteq> J}
[PROOF STEP]
apply (rule subsetI, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M x. \<lbrakk>\<not> zeroring R; \<forall>X. ideal R X \<and> X \<subset> carrier R \<longrightarrow> M \<subseteq> X \<longrightarrow> X = M; ideal R M; M \<subset> carrier R; x = M \<or> x = carrier R\<rbrakk> \<Longrightarrow> ideal R x \<and> M \<subseteq> x
[PROOF STEP]
apply (erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>M x. \<lbrakk>\<not> zeroring R; \<forall>X. ideal R X \<and> X \<subset> carrier R \<longrightarrow> M \<subseteq> X \<longrightarrow> X = M; ideal R M; M \<subset> carrier R; x = M\<rbrakk> \<Longrightarrow> ideal R x \<and> M \<subseteq> x
 2. \<And>M x. \<lbrakk>\<not> zeroring R; \<forall>X. ideal R X \<and> X \<subset> carrier R \<longrightarrow> M \<subseteq> X \<longrightarrow> X = M; ideal R M; M \<subset> carrier R; x = carrier R\<rbrakk> \<Longrightarrow> ideal R x \<and> M \<subseteq> x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M x. \<lbrakk>\<not> zeroring R; \<forall>X. ideal R X \<and> X \<subset> carrier R \<longrightarrow> M \<subseteq> X \<longrightarrow> X = M; ideal R M; M \<subset> carrier R; x = carrier R\<rbrakk> \<Longrightarrow> ideal R x \<and> M \<subseteq> x
[PROOF STEP]
apply (simp add:whole_ideal)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) ideal_Int_ideal:"\<lbrakk>S \<subseteq> {I. ideal R I}; S\<noteq>{}\<rbrakk> \<Longrightarrow>
                                                 ideal R (\<Inter> S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> ideal R (\<Inter> S)
[PROOF STEP]
apply (rule ideal_condition1)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<Inter> S \<subseteq> carrier R
 2. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<Inter> S \<noteq> {}
 3. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>\<Inter> S. \<forall>y\<in>\<Inter> S. x \<plusminus> y \<in> \<Inter> S
 4. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Inter> S. r \<cdot>\<^sub>r x \<in> \<Inter> S
[PROOF STEP]
apply (frule nonempty_ex[of "S"], erule exE)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}; x \<in> S\<rbrakk> \<Longrightarrow> \<Inter> S \<subseteq> carrier R
 2. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<Inter> S \<noteq> {}
 3. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>\<Inter> S. \<forall>y\<in>\<Inter> S. x \<plusminus> y \<in> \<Inter> S
 4. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Inter> S. r \<cdot>\<^sub>r x \<in> \<Inter> S
[PROOF STEP]
apply (frule_tac c = x in subsetD[of "S" "{I. ideal R I}"], assumption+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}; x \<in> S; x \<in> {I. ideal R I}\<rbrakk> \<Longrightarrow> \<Inter> S \<subseteq> carrier R
 2. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<Inter> S \<noteq> {}
 3. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>\<Inter> S. \<forall>y\<in>\<Inter> S. x \<plusminus> y \<in> \<Inter> S
 4. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Inter> S. r \<cdot>\<^sub>r x \<in> \<Inter> S
[PROOF STEP]
apply (simp, frule_tac I = x in ideal_subset1)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}; x \<in> S; ideal R x; x \<subseteq> carrier R\<rbrakk> \<Longrightarrow> \<Inter> S \<subseteq> carrier R
 2. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<Inter> S \<noteq> {}
 3. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>\<Inter> S. \<forall>y\<in>\<Inter> S. x \<plusminus> y \<in> \<Inter> S
 4. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Inter> S. r \<cdot>\<^sub>r x \<in> \<Inter> S
[PROOF STEP]
apply (frule_tac B = x and A = S in Inter_lower)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}; x \<in> S; ideal R x; x \<subseteq> carrier R; \<Inter> S \<subseteq> x\<rbrakk> \<Longrightarrow> \<Inter> S \<subseteq> carrier R
 2. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<Inter> S \<noteq> {}
 3. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>\<Inter> S. \<forall>y\<in>\<Inter> S. x \<plusminus> y \<in> \<Inter> S
 4. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Inter> S. r \<cdot>\<^sub>r x \<in> \<Inter> S
[PROOF STEP]
apply (rule_tac A = "\<Inter>S" and B = x and C = "carrier R" in subset_trans,
         assumption+)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<Inter> S \<noteq> {}
 2. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>\<Inter> S. \<forall>y\<in>\<Inter> S. x \<plusminus> y \<in> \<Inter> S
 3. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Inter> S. r \<cdot>\<^sub>r x \<in> \<Inter> S
[PROOF STEP]
apply (cut_tac ideal_zero_forall, blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>\<Inter> S. \<forall>y\<in>\<Inter> S. x \<plusminus> y \<in> \<Inter> S
 2. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Inter> S. r \<cdot>\<^sub>r x \<in> \<Inter> S
[PROOF STEP]
apply (simp, rule ballI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}; x \<in> \<Inter> S\<rbrakk> \<Longrightarrow> \<forall>y\<in>\<Inter> S. \<forall>X\<in>S. x \<plusminus> y \<in> X
 2. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Inter> S. r \<cdot>\<^sub>r x \<in> \<Inter> S
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y X. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}; x \<in> \<Inter> S; y \<in> \<Inter> S; X \<in> S\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> X
 2. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Inter> S. r \<cdot>\<^sub>r x \<in> \<Inter> S
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y X. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}; \<forall>X\<in>S. x \<in> X; \<forall>X\<in>S. y \<in> X; X \<in> S\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> X
 2. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Inter> S. r \<cdot>\<^sub>r x \<in> \<Inter> S
[PROOF STEP]
apply (frule_tac x = X in bspec, assumption,
        thin_tac "\<forall>X\<in>S. x \<in> X",
        frule_tac x = X in bspec, assumption,
        thin_tac "\<forall>X\<in>S. y \<in> X")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y X. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}; X \<in> S; x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> x \<plusminus> y \<in> X
 2. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Inter> S. r \<cdot>\<^sub>r x \<in> \<Inter> S
[PROOF STEP]
apply (frule_tac c = X in subsetD[of "S" "{I. ideal R I}"], assumption+,
       simp, rule_tac x = x and y = y in ideal_pOp_closed, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>r\<in>carrier R. \<forall>x\<in>\<Inter> S. r \<cdot>\<^sub>r x \<in> \<Inter> S
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}; r \<in> carrier R; x \<in> \<Inter> S\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r x \<in> \<Inter> S
[PROOF STEP]
apply (simp, rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x X. \<lbrakk>S \<subseteq> {I. ideal R I}; S \<noteq> {}; r \<in> carrier R; \<forall>X\<in>S. x \<in> X; X \<in> S\<rbrakk> \<Longrightarrow> r \<cdot>\<^sub>r x \<in> X
[PROOF STEP]
apply (frule_tac x = X in bspec, assumption,
        thin_tac "\<forall>X\<in>S. x \<in> X",
        frule_tac c = X in subsetD[of "S" "{I. ideal R I}"], assumption+,
        simp add:ideal_ring_multiple)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) sum_prideals_Int:"\<lbrakk>\<forall>l \<le> n. f l \<in> carrier R;
                S = {I. ideal R I \<and> f ` {i. i \<le> n} \<subseteq> I}\<rbrakk> \<Longrightarrow>
                                  (sum_pr_ideals R f n) = \<Inter> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>l\<le>n. f l \<in> carrier R; S = {I. ideal R I \<and> f ` {i. i \<le> n} \<subseteq> I}\<rbrakk> \<Longrightarrow> sum_pr_ideals R f n = \<Inter> S
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>l\<le>n. f l \<in> carrier R; S = {I. ideal R I \<and> f ` {i. i \<le> n} \<subseteq> I}\<rbrakk> \<Longrightarrow> sum_pr_ideals R f n \<subseteq> \<Inter> S
 2. \<lbrakk>\<forall>l\<le>n. f l \<in> carrier R; S = {I. ideal R I \<and> f ` {i. i \<le> n} \<subseteq> I}\<rbrakk> \<Longrightarrow> \<Inter> S \<subseteq> sum_pr_ideals R f n
[PROOF STEP]
apply (subgoal_tac "\<forall>X\<in>S. sum_pr_ideals R f n \<subseteq> X")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<forall>l\<le>n. f l \<in> carrier R; S = {I. ideal R I \<and> f ` {i. i \<le> n} \<subseteq> I}; \<forall>X\<in>S. sum_pr_ideals R f n \<subseteq> X\<rbrakk> \<Longrightarrow> sum_pr_ideals R f n \<subseteq> \<Inter> S
 2. \<lbrakk>\<forall>l\<le>n. f l \<in> carrier R; S = {I. ideal R I \<and> f ` {i. i \<le> n} \<subseteq> I}\<rbrakk> \<Longrightarrow> \<forall>X\<in>S. sum_pr_ideals R f n \<subseteq> X
 3. \<lbrakk>\<forall>l\<le>n. f l \<in> carrier R; S = {I. ideal R I \<and> f ` {i. i \<le> n} \<subseteq> I}\<rbrakk> \<Longrightarrow> \<Inter> S \<subseteq> sum_pr_ideals R f n
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>l\<le>n. f l \<in> carrier R; S = {I. ideal R I \<and> f ` {i. i \<le> n} \<subseteq> I}\<rbrakk> \<Longrightarrow> \<forall>X\<in>S. sum_pr_ideals R f n \<subseteq> X
 2. \<lbrakk>\<forall>l\<le>n. f l \<in> carrier R; S = {I. ideal R I \<and> f ` {i. i \<le> n} \<subseteq> I}\<rbrakk> \<Longrightarrow> \<Inter> S \<subseteq> sum_pr_ideals R f n
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>X. \<lbrakk>\<forall>l\<le>n. f l \<in> carrier R; S = {I. ideal R I \<and> f ` {i. i \<le> n} \<subseteq> I}; X \<in> S\<rbrakk> \<Longrightarrow> sum_pr_ideals R f n \<subseteq> X
 2. \<lbrakk>\<forall>l\<le>n. f l \<in> carrier R; S = {I. ideal R I \<and> f ` {i. i \<le> n} \<subseteq> I}\<rbrakk> \<Longrightarrow> \<Inter> S \<subseteq> sum_pr_ideals R f n
[PROOF STEP]
apply (simp, erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>X. \<lbrakk>\<forall>l\<le>n. f l \<in> carrier R; S = {I. ideal R I \<and> f ` {i. i \<le> n} \<subseteq> I}; ideal R X; f ` {i. i \<le> n} \<subseteq> X\<rbrakk> \<Longrightarrow> sum_pr_ideals R f n \<subseteq> X
 2. \<lbrakk>\<forall>l\<le>n. f l \<in> carrier R; S = {I. ideal R I \<and> f ` {i. i \<le> n} \<subseteq> I}\<rbrakk> \<Longrightarrow> \<Inter> S \<subseteq> sum_pr_ideals R f n
[PROOF STEP]
apply (rule_tac I = X and n = n and f = f in sum_of_prideals4, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>l\<le>n. f l \<in> carrier R; S = {I. ideal R I \<and> f ` {i. i \<le> n} \<subseteq> I}\<rbrakk> \<Longrightarrow> \<Inter> S \<subseteq> sum_pr_ideals R f n
[PROOF STEP]
apply (subgoal_tac "(sum_pr_ideals R f n) \<in> S")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>l\<le>n. f l \<in> carrier R; S = {I. ideal R I \<and> f ` {i. i \<le> n} \<subseteq> I}; sum_pr_ideals R f n \<in> S\<rbrakk> \<Longrightarrow> \<Inter> S \<subseteq> sum_pr_ideals R f n
 2. \<lbrakk>\<forall>l\<le>n. f l \<in> carrier R; S = {I. ideal R I \<and> f ` {i. i \<le> n} \<subseteq> I}\<rbrakk> \<Longrightarrow> sum_pr_ideals R f n \<in> S
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>l\<le>n. f l \<in> carrier R; S = {I. ideal R I \<and> f ` {i. i \<le> n} \<subseteq> I}\<rbrakk> \<Longrightarrow> sum_pr_ideals R f n \<in> S
[PROOF STEP]
apply (simp add:CollectI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>l\<le>n. f l \<in> carrier R; S = {I. ideal R I \<and> f ` {i. i \<le> n} \<subseteq> I}\<rbrakk> \<Longrightarrow> ideal R (sum_pr_ideals R f n) \<and> f ` {i. i \<le> n} \<subseteq> sum_pr_ideals R f n
[PROOF STEP]
apply (simp add: sum_of_prideals2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>l\<le>n. f l \<in> carrier R; S = {I. ideal R I \<and> f ` {i. i \<le> n} \<subseteq> I}\<rbrakk> \<Longrightarrow> ideal R (sum_pr_ideals R f n)
[PROOF STEP]
apply (simp add: sum_of_prideals)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Ring) prod_mem_prod_ideals:"\<lbrakk>ideal R I; ideal R J; i \<in> I; j \<in> J\<rbrakk> \<Longrightarrow>
                            i \<cdot>\<^sub>r j \<in> (I \<diamondsuit>\<^sub>r J)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; ideal R J; i \<in> I; j \<in> J\<rbrakk> \<Longrightarrow> i \<cdot>\<^sub>r j \<in> I \<diamondsuit>\<^sub>r J
[PROOF STEP]
apply (simp add:ideal_prod_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ideal R I; ideal R J; i \<in> I; j \<in> J\<rbrakk> \<Longrightarrow> \<forall>x. ideal R x \<and> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> x \<longrightarrow> i \<cdot>\<^sub>r j \<in> x
[PROOF STEP]
apply (rule allI, rule impI, erule conjE, rename_tac X)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>X. \<lbrakk>ideal R I; ideal R J; i \<in> I; j \<in> J; ideal R X; {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> X\<rbrakk> \<Longrightarrow> i \<cdot>\<^sub>r j \<in> X
[PROOF STEP]
apply (rule_tac A = "{x. \<exists>i\<in>I. \<exists>j\<in>J. x = Ring.tp R i j}" and B = X and c = "i \<cdot>\<^sub>r j" in  subsetD, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>X. \<lbrakk>ideal R I; ideal R J; i \<in> I; j \<in> J; ideal R X; {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> X\<rbrakk> \<Longrightarrow> i \<cdot>\<^sub>r j \<in> {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>X. \<lbrakk>ideal R I; ideal R J; i \<in> I; j \<in> J; ideal R X; {x. \<exists>i\<in>I. \<exists>j\<in>J. x = i \<cdot>\<^sub>r j} \<subseteq> X\<rbrakk> \<Longrightarrow> \<exists>ia\<in>I. \<exists>ja\<in>J. i \<cdot>\<^sub>r j = ia \<cdot>\<^sub>r ja
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done