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	⊢ ( 𝑅 ∈ NzRing → ∃ 𝑚 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		nzrring	⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
2		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
3		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
4	2 3	lidl0	⊢ ( 𝑅 ∈ Ring → { ( 0g ‘ 𝑅 ) } ∈ ( LIdeal ‘ 𝑅 ) )
5	1 4	syl	⊢ ( 𝑅 ∈ NzRing → { ( 0g ‘ 𝑅 ) } ∈ ( LIdeal ‘ 𝑅 ) )
6		fvex	⊢ ( 0g ‘ 𝑅 ) ∈ V
7		hashsng	⊢ ( ( 0g ‘ 𝑅 ) ∈ V → ( ♯ ‘ { ( 0g ‘ 𝑅 ) } ) = 1 )
8	6 7	ax-mp	⊢ ( ♯ ‘ { ( 0g ‘ 𝑅 ) } ) = 1
9		simpr	⊢ ( ( 𝑅 ∈ NzRing ∧ { ( 0g ‘ 𝑅 ) } = ( Base ‘ 𝑅 ) ) → { ( 0g ‘ 𝑅 ) } = ( Base ‘ 𝑅 ) )
10	9	fveq2d	⊢ ( ( 𝑅 ∈ NzRing ∧ { ( 0g ‘ 𝑅 ) } = ( Base ‘ 𝑅 ) ) → ( ♯ ‘ { ( 0g ‘ 𝑅 ) } ) = ( ♯ ‘ ( Base ‘ 𝑅 ) ) )
11	8 10	eqtr3id	⊢ ( ( 𝑅 ∈ NzRing ∧ { ( 0g ‘ 𝑅 ) } = ( Base ‘ 𝑅 ) ) → 1 = ( ♯ ‘ ( Base ‘ 𝑅 ) ) )
12		1red	⊢ ( ( 𝑅 ∈ NzRing ∧ { ( 0g ‘ 𝑅 ) } = ( Base ‘ 𝑅 ) ) → 1 ∈ ℝ )
13		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
14	13	isnzr2hash	⊢ ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) ) )
15	14	simprbi	⊢ ( 𝑅 ∈ NzRing → 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) )
16	15	adantr	⊢ ( ( 𝑅 ∈ NzRing ∧ { ( 0g ‘ 𝑅 ) } = ( Base ‘ 𝑅 ) ) → 1 < ( ♯ ‘ ( Base ‘ 𝑅 ) ) )
17	12 16	ltned	⊢ ( ( 𝑅 ∈ NzRing ∧ { ( 0g ‘ 𝑅 ) } = ( Base ‘ 𝑅 ) ) → 1 ≠ ( ♯ ‘ ( Base ‘ 𝑅 ) ) )
18	17	neneqd	⊢ ( ( 𝑅 ∈ NzRing ∧ { ( 0g ‘ 𝑅 ) } = ( Base ‘ 𝑅 ) ) → ¬ 1 = ( ♯ ‘ ( Base ‘ 𝑅 ) ) )
19	11 18	pm2.65da	⊢ ( 𝑅 ∈ NzRing → ¬ { ( 0g ‘ 𝑅 ) } = ( Base ‘ 𝑅 ) )
20	19	neqned	⊢ ( 𝑅 ∈ NzRing → { ( 0g ‘ 𝑅 ) } ≠ ( Base ‘ 𝑅 ) )
21	13	ssmxidl	⊢ ( ( 𝑅 ∈ Ring ∧ { ( 0g ‘ 𝑅 ) } ∈ ( LIdeal ‘ 𝑅 ) ∧ { ( 0g ‘ 𝑅 ) } ≠ ( Base ‘ 𝑅 ) ) → ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) { ( 0g ‘ 𝑅 ) } ⊆ 𝑚 )
22	1 5 20 21	syl3anc	⊢ ( 𝑅 ∈ NzRing → ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) { ( 0g ‘ 𝑅 ) } ⊆ 𝑚 )
23		df-rex	⊢ ( ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) { ( 0g ‘ 𝑅 ) } ⊆ 𝑚 ↔ ∃ 𝑚 ( 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ∧ { ( 0g ‘ 𝑅 ) } ⊆ 𝑚 ) )
24		exsimpl	⊢ ( ∃ 𝑚 ( 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ∧ { ( 0g ‘ 𝑅 ) } ⊆ 𝑚 ) → ∃ 𝑚 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) )
25	23 24	sylbi	⊢ ( ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) { ( 0g ‘ 𝑅 ) } ⊆ 𝑚 → ∃ 𝑚 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) )
26	22 25	syl	⊢ ( 𝑅 ∈ NzRing → ∃ 𝑚 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) )