Metamath Proof Explorer

Theorem drng0mxidl

Description: In a division ring, the zero ideal is a maximal ideal. (Contributed by Thierry Arnoux, 16-Mar-2025)

Ref Expression
Hypothesis drngmxidl.1 ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion drng0mxidl ( 𝑅 ∈ DivRing → { 0 } ∈ ( MaxIdeal ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 drngmxidl.1 ⊢ 0 = ( 0g ‘ 𝑅 )
2 drngring ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
3 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
4 3 1 lidl0 ⊢ ( 𝑅 ∈ Ring → { 0 } ∈ ( LIdeal ‘ 𝑅 ) )
5 2 4 syl ⊢ ( 𝑅 ∈ DivRing → { 0 } ∈ ( LIdeal ‘ 𝑅 ) )
6 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
8 6 7 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
9 2 8 syl ⊢ ( 𝑅 ∈ DivRing → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
10 drngnzr ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ NzRing )
11 7 1 nzrnz ⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ 0 )
12 nelsn ⊢ ( ( 1r ‘ 𝑅 ) ≠ 0 → ¬ ( 1r ‘ 𝑅 ) ∈ { 0 } )
13 10 11 12 3syl ⊢ ( 𝑅 ∈ DivRing → ¬ ( 1r ‘ 𝑅 ) ∈ { 0 } )
14 nelne1 ⊢ ( ( ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ ¬ ( 1r ‘ 𝑅 ) ∈ { 0 } ) → ( Base ‘ 𝑅 ) ≠ { 0 } )
15 9 13 14 syl2anc ⊢ ( 𝑅 ∈ DivRing → ( Base ‘ 𝑅 ) ≠ { 0 } )
16 15 necomd ⊢ ( 𝑅 ∈ DivRing → { 0 } ≠ ( Base ‘ 𝑅 ) )
17 6 1 3 drngnidl ⊢ ( 𝑅 ∈ DivRing → ( LIdeal ‘ 𝑅 ) = { { 0 } , ( Base ‘ 𝑅 ) } )
18 17 eleq2d ⊢ ( 𝑅 ∈ DivRing → ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ↔ 𝑗 ∈ { { 0 } , ( Base ‘ 𝑅 ) } ) )
19 18 biimpa ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑗 ∈ { { 0 } , ( Base ‘ 𝑅 ) } )
20 elpri ⊢ ( 𝑗 ∈ { { 0 } , ( Base ‘ 𝑅 ) } → ( 𝑗 = { 0 } ∨ 𝑗 = ( Base ‘ 𝑅 ) ) )
21 19 20 syl ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 𝑗 = { 0 } ∨ 𝑗 = ( Base ‘ 𝑅 ) ) )
22 21 a1d ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ) → ( { 0 } ⊆ 𝑗 → ( 𝑗 = { 0 } ∨ 𝑗 = ( Base ‘ 𝑅 ) ) ) )
23 22 ralrimiva ⊢ ( 𝑅 ∈ DivRing → ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( { 0 } ⊆ 𝑗 → ( 𝑗 = { 0 } ∨ 𝑗 = ( Base ‘ 𝑅 ) ) ) )
24 6 ismxidl ⊢ ( 𝑅 ∈ Ring → ( { 0 } ∈ ( MaxIdeal ‘ 𝑅 ) ↔ ( { 0 } ∈ ( LIdeal ‘ 𝑅 ) ∧ { 0 } ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( { 0 } ⊆ 𝑗 → ( 𝑗 = { 0 } ∨ 𝑗 = ( Base ‘ 𝑅 ) ) ) ) ) )
25 24 biimpar ⊢ ( ( 𝑅 ∈ Ring ∧ ( { 0 } ∈ ( LIdeal ‘ 𝑅 ) ∧ { 0 } ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( { 0 } ⊆ 𝑗 → ( 𝑗 = { 0 } ∨ 𝑗 = ( Base ‘ 𝑅 ) ) ) ) ) → { 0 } ∈ ( MaxIdeal ‘ 𝑅 ) )
26 2 5 16 23 25 syl13anc ⊢ ( 𝑅 ∈ DivRing → { 0 } ∈ ( MaxIdeal ‘ 𝑅 ) )