Theorem drngmxidlr

Description: If a ring's only maximal ideal is the zero ideal, it is a division ring. See also drngmxidl . (Contributed by Thierry Arnoux, 3-Jun-2025)

	Ref	Expression
Hypotheses	drngmxidlr.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	drngmxidlr.z	⊢ 0 = ( 0g ‘ 𝑅 )
	drngmxidlr.u	⊢ 𝑀 = ( MaxIdeal ‘ 𝑅 )
	drngmxidlr.r	⊢ ( 𝜑 → 𝑅 ∈ NzRing )
	drngmxidlr.2	⊢ ( 𝜑 → 𝑀 = { { 0 } } )
Assertion	drngmxidlr	⊢ ( 𝜑 → 𝑅 ∈ DivRing )

Proof

Step	Hyp	Ref	Expression
1		drngmxidlr.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		drngmxidlr.z	⊢ 0 = ( 0g ‘ 𝑅 )
3		drngmxidlr.u	⊢ 𝑀 = ( MaxIdeal ‘ 𝑅 )
4		drngmxidlr.r	⊢ ( 𝜑 → 𝑅 ∈ NzRing )
5		drngmxidlr.2	⊢ ( 𝜑 → 𝑀 = { { 0 } } )
6		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑖 ≠ 𝐵 ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑖 ⊆ 𝑚 ) → 𝑖 ⊆ 𝑚 )
7		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑖 ≠ 𝐵 ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑖 ⊆ 𝑚 ) → 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) )
8	7 3	eleqtrrdi	⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑖 ≠ 𝐵 ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑖 ⊆ 𝑚 ) → 𝑚 ∈ 𝑀 )
9	5	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑖 ≠ 𝐵 ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑖 ⊆ 𝑚 ) → 𝑀 = { { 0 } } )
10	8 9	eleqtrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑖 ≠ 𝐵 ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑖 ⊆ 𝑚 ) → 𝑚 ∈ { { 0 } } )
11		elsni	⊢ ( 𝑚 ∈ { { 0 } } → 𝑚 = { 0 } )
12	10 11	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑖 ≠ 𝐵 ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑖 ⊆ 𝑚 ) → 𝑚 = { 0 } )
13	6 12	sseqtrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑖 ≠ 𝐵 ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑖 ⊆ 𝑚 ) → 𝑖 ⊆ { 0 } )
14		nzrring	⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
15	4 14	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
16		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
17	16 2	lidl0cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) → 0 ∈ 𝑖 )
18	15 17	sylan	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) → 0 ∈ 𝑖 )
19	18	snssd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) → { 0 } ⊆ 𝑖 )
20	19	ad3antrrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑖 ≠ 𝐵 ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑖 ⊆ 𝑚 ) → { 0 } ⊆ 𝑖 )
21	13 20	eqssd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑖 ≠ 𝐵 ) ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ∧ 𝑖 ⊆ 𝑚 ) → 𝑖 = { 0 } )
22	15	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑖 ≠ 𝐵 ) → 𝑅 ∈ Ring )
23		simplr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑖 ≠ 𝐵 ) → 𝑖 ∈ ( LIdeal ‘ 𝑅 ) )
24		simpr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑖 ≠ 𝐵 ) → 𝑖 ≠ 𝐵 )
25	1	ssmxidl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑖 ≠ 𝐵 ) → ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) 𝑖 ⊆ 𝑚 )
26	22 23 24 25	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑖 ≠ 𝐵 ) → ∃ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) 𝑖 ⊆ 𝑚 )
27	21 26	r19.29a	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑖 ≠ 𝐵 ) → 𝑖 = { 0 } )
28		simpr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑖 = 𝐵 ) → 𝑖 = 𝐵 )
29		exmidne	⊢ ( 𝑖 = 𝐵 ∨ 𝑖 ≠ 𝐵 )
30	29	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 𝑖 = 𝐵 ∨ 𝑖 ≠ 𝐵 ) )
31	30	orcomd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 𝑖 ≠ 𝐵 ∨ 𝑖 = 𝐵 ) )
32	27 28 31	orim12da	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 𝑖 = { 0 } ∨ 𝑖 = 𝐵 ) )
33		vex	⊢ 𝑖 ∈ V
34	33	elpr	⊢ ( 𝑖 ∈ { { 0 } , 𝐵 } ↔ ( 𝑖 = { 0 } ∨ 𝑖 = 𝐵 ) )
35	32 34	sylibr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑖 ∈ { { 0 } , 𝐵 } )
36	35	ex	⊢ ( 𝜑 → ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) → 𝑖 ∈ { { 0 } , 𝐵 } ) )
37	36	ssrdv	⊢ ( 𝜑 → ( LIdeal ‘ 𝑅 ) ⊆ { { 0 } , 𝐵 } )
38	16 2	lidl0	⊢ ( 𝑅 ∈ Ring → { 0 } ∈ ( LIdeal ‘ 𝑅 ) )
39	15 38	syl	⊢ ( 𝜑 → { 0 } ∈ ( LIdeal ‘ 𝑅 ) )
40	16 1	lidl1	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ ( LIdeal ‘ 𝑅 ) )
41	15 40	syl	⊢ ( 𝜑 → 𝐵 ∈ ( LIdeal ‘ 𝑅 ) )
42	39 41	prssd	⊢ ( 𝜑 → { { 0 } , 𝐵 } ⊆ ( LIdeal ‘ 𝑅 ) )
43	37 42	eqssd	⊢ ( 𝜑 → ( LIdeal ‘ 𝑅 ) = { { 0 } , 𝐵 } )
44	1 2 16	drngidl	⊢ ( 𝑅 ∈ NzRing → ( 𝑅 ∈ DivRing ↔ ( LIdeal ‘ 𝑅 ) = { { 0 } , 𝐵 } ) )
45	4 44	syl	⊢ ( 𝜑 → ( 𝑅 ∈ DivRing ↔ ( LIdeal ‘ 𝑅 ) = { { 0 } , 𝐵 } ) )
46	43 45	mpbird	⊢ ( 𝜑 → 𝑅 ∈ DivRing )