This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem drngnidl

Description: A division ring has only the two trivial ideals. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by Wolf Lammen, 6-Sep-2020)

Ref Expression
Hypotheses drngnidl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
drngnidl.z ⊢ 0 = ( 0g ‘ 𝑅 )
drngnidl.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
Assertion drngnidl ( 𝑅 ∈ DivRing → 𝑈 = { { 0 } , 𝐵 } )

Proof

Step Hyp Ref Expression
1 drngnidl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 drngnidl.z ⊢ 0 = ( 0g ‘ 𝑅 )
3 drngnidl.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
4 animorrl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑎 = { 0 } ) → ( 𝑎 = { 0 } ∨ 𝑎 = 𝐵 ) )
5 drngring ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
6 5 ad2antrr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑎 ≠ { 0 } ) → 𝑅 ∈ Ring )
7 simplr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑎 ≠ { 0 } ) → 𝑎 ∈ 𝑈 )
8 simpr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑎 ≠ { 0 } ) → 𝑎 ≠ { 0 } )
9 3 2 lidlnz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝑈 ∧ 𝑎 ≠ { 0 } ) → ∃ 𝑏 ∈ 𝑎 𝑏 ≠ 0 )
10 6 7 8 9 syl3anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑎 ≠ { 0 } ) → ∃ 𝑏 ∈ 𝑎 𝑏 ≠ 0 )
11 simpll ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ ( 𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 ) ) → 𝑅 ∈ DivRing )
12 1 3 lidlss ⊢ ( 𝑎 ∈ 𝑈 → 𝑎 ⊆ 𝐵 )
13 12 adantl ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) → 𝑎 ⊆ 𝐵 )
14 13 sselda ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝑎 ) → 𝑏 ∈ 𝐵 )
15 14 adantrr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ ( 𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 ) ) → 𝑏 ∈ 𝐵 )
16 simprr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ ( 𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 ) ) → 𝑏 ≠ 0 )
17 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
18 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
19 eqid ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
20 1 2 17 18 19 drnginvrl ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑏 ∈ 𝐵 ∧ 𝑏 ≠ 0 ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑏 ) ( .r ‘ 𝑅 ) 𝑏 ) = ( 1r ‘ 𝑅 ) )
21 11 15 16 20 syl3anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ ( 𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑏 ) ( .r ‘ 𝑅 ) 𝑏 ) = ( 1r ‘ 𝑅 ) )
22 5 ad2antrr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ ( 𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 ) ) → 𝑅 ∈ Ring )
23 simplr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ ( 𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 ) ) → 𝑎 ∈ 𝑈 )
24 1 2 19 drnginvrcl ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑏 ∈ 𝐵 ∧ 𝑏 ≠ 0 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑏 ) ∈ 𝐵 )
25 11 15 16 24 syl3anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ ( 𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝑏 ) ∈ 𝐵 )
26 simprl ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ ( 𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 ) ) → 𝑏 ∈ 𝑎 )
27 3 1 17 lidlmcl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝑈 ) ∧ ( ( ( invr ‘ 𝑅 ) ‘ 𝑏 ) ∈ 𝐵 ∧ 𝑏 ∈ 𝑎 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑏 ) ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑎 )
28 22 23 25 26 27 syl22anc ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ ( 𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝑏 ) ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑎 )
29 21 28 eqeltrrd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ ( 𝑏 ∈ 𝑎 ∧ 𝑏 ≠ 0 ) ) → ( 1r ‘ 𝑅 ) ∈ 𝑎 )
30 29 rexlimdvaa ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) → ( ∃ 𝑏 ∈ 𝑎 𝑏 ≠ 0 → ( 1r ‘ 𝑅 ) ∈ 𝑎 ) )
31 30 imp ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ ∃ 𝑏 ∈ 𝑎 𝑏 ≠ 0 ) → ( 1r ‘ 𝑅 ) ∈ 𝑎 )
32 10 31 syldan ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑎 ≠ { 0 } ) → ( 1r ‘ 𝑅 ) ∈ 𝑎 )
33 3 1 18 lidl1el ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝑈 ) → ( ( 1r ‘ 𝑅 ) ∈ 𝑎 ↔ 𝑎 = 𝐵 ) )
34 5 33 sylan ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) → ( ( 1r ‘ 𝑅 ) ∈ 𝑎 ↔ 𝑎 = 𝐵 ) )
35 34 adantr ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑎 ≠ { 0 } ) → ( ( 1r ‘ 𝑅 ) ∈ 𝑎 ↔ 𝑎 = 𝐵 ) )
36 32 35 mpbid ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑎 ≠ { 0 } ) → 𝑎 = 𝐵 )
37 36 olcd ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑎 ≠ { 0 } ) → ( 𝑎 = { 0 } ∨ 𝑎 = 𝐵 ) )
38 4 37 pm2.61dane ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) → ( 𝑎 = { 0 } ∨ 𝑎 = 𝐵 ) )
39 vex ⊢ 𝑎 ∈ V
40 39 elpr ⊢ ( 𝑎 ∈ { { 0 } , 𝐵 } ↔ ( 𝑎 = { 0 } ∨ 𝑎 = 𝐵 ) )
41 38 40 sylibr ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑎 ∈ 𝑈 ) → 𝑎 ∈ { { 0 } , 𝐵 } )
42 41 ex ⊢ ( 𝑅 ∈ DivRing → ( 𝑎 ∈ 𝑈 → 𝑎 ∈ { { 0 } , 𝐵 } ) )
43 42 ssrdv ⊢ ( 𝑅 ∈ DivRing → 𝑈 ⊆ { { 0 } , 𝐵 } )
44 3 2 lidl0 ⊢ ( 𝑅 ∈ Ring → { 0 } ∈ 𝑈 )
45 3 1 lidl1 ⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ 𝑈 )
46 44 45 prssd ⊢ ( 𝑅 ∈ Ring → { { 0 } , 𝐵 } ⊆ 𝑈 )
47 5 46 syl ⊢ ( 𝑅 ∈ DivRing → { { 0 } , 𝐵 } ⊆ 𝑈 )
48 43 47 eqssd ⊢ ( 𝑅 ∈ DivRing → 𝑈 = { { 0 } , 𝐵 } )