Theorem krull

Description: Krull's theorem: Any nonzero ring has at least one maximal ideal. (Contributed by Thierry Arnoux, 10-Apr-2024)

	Ref	Expression
Assertion	krull	Could not format assertion : No typesetting found for |- ( R e. NzRing -> E. m m e. ( MaxIdeal ` R ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		nzrring	$$⊢R\in \mathrm{NzRing}\to R\in \mathrm{Ring}$$
2		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
3		eqid	$$⊢0_R=0_R$$
4	2 3	lidl0	$$⊢R\in \mathrm{Ring}\to \left\{0_R\right\}\in \mathrm{LIdeal}\left(R\right)$$
5	1 4	syl	$$⊢R\in \mathrm{NzRing}\to \left\{0_R\right\}\in \mathrm{LIdeal}\left(R\right)$$
6		fvex	$$⊢0_R\in \mathrm{V}$$
7		hashsng	$$⊢0_R\in \mathrm{V}\to \left|\left\{0_R\right\}\right|=1$$
8	6 7	ax-mp	$$⊢\left|\left\{0_R\right\}\right|=1$$
9		simpr	$$⊢\left(R\in \mathrm{NzRing}\wedge \left\{0_R\right\}={\mathrm{Base}}_R\right)\to \left\{0_R\right\}={\mathrm{Base}}_R$$
10	9	fveq2d	$$⊢\left(R\in \mathrm{NzRing}\wedge \left\{0_R\right\}={\mathrm{Base}}_R\right)\to \left|\left\{0_R\right\}\right|=\left|{\mathrm{Base}}_R\right|$$
11	8 10	syl5eqr	$$⊢\left(R\in \mathrm{NzRing}\wedge \left\{0_R\right\}={\mathrm{Base}}_R\right)\to 1=\left|{\mathrm{Base}}_R\right|$$
12		1red	$$⊢\left(R\in \mathrm{NzRing}\wedge \left\{0_R\right\}={\mathrm{Base}}_R\right)\to 1\in ℝ$$
13		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
14	13	isnzr2hash	$$⊢R\in \mathrm{NzRing}\leftrightarrow \left(R\in \mathrm{Ring}\wedge 1<\left|{\mathrm{Base}}_R\right|\right)$$
15	14	simprbi	$$⊢R\in \mathrm{NzRing}\to 1<\left|{\mathrm{Base}}_R\right|$$
16	15	adantr	$$⊢\left(R\in \mathrm{NzRing}\wedge \left\{0_R\right\}={\mathrm{Base}}_R\right)\to 1<\left|{\mathrm{Base}}_R\right|$$
17	12 16	ltned	$$⊢\left(R\in \mathrm{NzRing}\wedge \left\{0_R\right\}={\mathrm{Base}}_R\right)\to 1\ne \left|{\mathrm{Base}}_R\right|$$
18	17	neneqd	$$⊢\left(R\in \mathrm{NzRing}\wedge \left\{0_R\right\}={\mathrm{Base}}_R\right)\to \neg 1=\left|{\mathrm{Base}}_R\right|$$
19	11 18	pm2.65da	$$⊢R\in \mathrm{NzRing}\to \neg \left\{0_R\right\}={\mathrm{Base}}_R$$
20	19	neqned	$$⊢R\in \mathrm{NzRing}\to \left\{0_R\right\}\ne {\mathrm{Base}}_R$$
21	13	ssmxidl	Could not format ( ( R e. Ring /\ { ( 0g ` R ) } e. ( LIdeal ` R ) /\ { ( 0g ` R ) } =/= ( Base ` R ) ) -> E. m e. ( MaxIdeal ` R ) { ( 0g ` R ) } C_ m ) : No typesetting found for |- ( ( R e. Ring /\ { ( 0g ` R ) } e. ( LIdeal ` R ) /\ { ( 0g ` R ) } =/= ( Base ` R ) ) -> E. m e. ( MaxIdeal ` R ) { ( 0g ` R ) } C_ m ) with typecode |-
22	1 5 20 21	syl3anc	Could not format ( R e. NzRing -> E. m e. ( MaxIdeal ` R ) { ( 0g ` R ) } C_ m ) : No typesetting found for |- ( R e. NzRing -> E. m e. ( MaxIdeal ` R ) { ( 0g ` R ) } C_ m ) with typecode |-
23		df-rex	Could not format ( E. m e. ( MaxIdeal ` R ) { ( 0g ` R ) } C_ m <-> E. m ( m e. ( MaxIdeal ` R ) /\ { ( 0g ` R ) } C_ m ) ) : No typesetting found for |- ( E. m e. ( MaxIdeal ` R ) { ( 0g ` R ) } C_ m <-> E. m ( m e. ( MaxIdeal ` R ) /\ { ( 0g ` R ) } C_ m ) ) with typecode |-
24		exsimpl	Could not format ( E. m ( m e. ( MaxIdeal ` R ) /\ { ( 0g ` R ) } C_ m ) -> E. m m e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( E. m ( m e. ( MaxIdeal ` R ) /\ { ( 0g ` R ) } C_ m ) -> E. m m e. ( MaxIdeal ` R ) ) with typecode |-
25	23 24	sylbi	Could not format ( E. m e. ( MaxIdeal ` R ) { ( 0g ` R ) } C_ m -> E. m m e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( E. m e. ( MaxIdeal ` R ) { ( 0g ` R ) } C_ m -> E. m m e. ( MaxIdeal ` R ) ) with typecode |-
26	22 25	syl	Could not format ( R e. NzRing -> E. m m e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( R e. NzRing -> E. m m e. ( MaxIdeal ` R ) ) with typecode |-