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 
|- B = ( Base ` R )
drngnidl.z 
|- .0. = ( 0g ` R )
drngnidl.u 
|- U = ( LIdeal ` R )
Assertion drngnidl 
|- ( R e. DivRing -> U = { { .0. } , B } )

Proof

Step Hyp Ref Expression
1 drngnidl.b 
 |-  B = ( Base ` R )
2 drngnidl.z 
 |-  .0. = ( 0g ` R )
3 drngnidl.u 
 |-  U = ( LIdeal ` R )
4 animorrl 
 |-  ( ( ( R e. DivRing /\ a e. U ) /\ a = { .0. } ) -> ( a = { .0. } \/ a = B ) )
5 drngring 
 |-  ( R e. DivRing -> R e. Ring )
6 5 ad2antrr 
 |-  ( ( ( R e. DivRing /\ a e. U ) /\ a =/= { .0. } ) -> R e. Ring )
7 simplr 
 |-  ( ( ( R e. DivRing /\ a e. U ) /\ a =/= { .0. } ) -> a e. U )
8 simpr 
 |-  ( ( ( R e. DivRing /\ a e. U ) /\ a =/= { .0. } ) -> a =/= { .0. } )
9 3 2 lidlnz 
 |-  ( ( R e. Ring /\ a e. U /\ a =/= { .0. } ) -> E. b e. a b =/= .0. )
10 6 7 8 9 syl3anc 
 |-  ( ( ( R e. DivRing /\ a e. U ) /\ a =/= { .0. } ) -> E. b e. a b =/= .0. )
11 simpll 
 |-  ( ( ( R e. DivRing /\ a e. U ) /\ ( b e. a /\ b =/= .0. ) ) -> R e. DivRing )
12 1 3 lidlss 
 |-  ( a e. U -> a C_ B )
13 12 adantl 
 |-  ( ( R e. DivRing /\ a e. U ) -> a C_ B )
14 13 sselda 
 |-  ( ( ( R e. DivRing /\ a e. U ) /\ b e. a ) -> b e. B )
15 14 adantrr 
 |-  ( ( ( R e. DivRing /\ a e. U ) /\ ( b e. a /\ b =/= .0. ) ) -> b e. B )
16 simprr 
 |-  ( ( ( R e. DivRing /\ a e. U ) /\ ( b e. a /\ b =/= .0. ) ) -> b =/= .0. )
17 eqid 
 |-  ( .r ` R ) = ( .r ` R )
18 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
19 eqid 
 |-  ( invr ` R ) = ( invr ` R )
20 1 2 17 18 19 drnginvrl 
 |-  ( ( R e. DivRing /\ b e. B /\ b =/= .0. ) -> ( ( ( invr ` R ) ` b ) ( .r ` R ) b ) = ( 1r ` R ) )
21 11 15 16 20 syl3anc 
 |-  ( ( ( R e. DivRing /\ a e. U ) /\ ( b e. a /\ b =/= .0. ) ) -> ( ( ( invr ` R ) ` b ) ( .r ` R ) b ) = ( 1r ` R ) )
22 5 ad2antrr 
 |-  ( ( ( R e. DivRing /\ a e. U ) /\ ( b e. a /\ b =/= .0. ) ) -> R e. Ring )
23 simplr 
 |-  ( ( ( R e. DivRing /\ a e. U ) /\ ( b e. a /\ b =/= .0. ) ) -> a e. U )
24 1 2 19 drnginvrcl 
 |-  ( ( R e. DivRing /\ b e. B /\ b =/= .0. ) -> ( ( invr ` R ) ` b ) e. B )
25 11 15 16 24 syl3anc 
 |-  ( ( ( R e. DivRing /\ a e. U ) /\ ( b e. a /\ b =/= .0. ) ) -> ( ( invr ` R ) ` b ) e. B )
26 simprl 
 |-  ( ( ( R e. DivRing /\ a e. U ) /\ ( b e. a /\ b =/= .0. ) ) -> b e. a )
27 3 1 17 lidlmcl 
 |-  ( ( ( R e. Ring /\ a e. U ) /\ ( ( ( invr ` R ) ` b ) e. B /\ b e. a ) ) -> ( ( ( invr ` R ) ` b ) ( .r ` R ) b ) e. a )
28 22 23 25 26 27 syl22anc 
 |-  ( ( ( R e. DivRing /\ a e. U ) /\ ( b e. a /\ b =/= .0. ) ) -> ( ( ( invr ` R ) ` b ) ( .r ` R ) b ) e. a )
29 21 28 eqeltrrd 
 |-  ( ( ( R e. DivRing /\ a e. U ) /\ ( b e. a /\ b =/= .0. ) ) -> ( 1r ` R ) e. a )
30 29 rexlimdvaa 
 |-  ( ( R e. DivRing /\ a e. U ) -> ( E. b e. a b =/= .0. -> ( 1r ` R ) e. a ) )
31 30 imp 
 |-  ( ( ( R e. DivRing /\ a e. U ) /\ E. b e. a b =/= .0. ) -> ( 1r ` R ) e. a )
32 10 31 syldan 
 |-  ( ( ( R e. DivRing /\ a e. U ) /\ a =/= { .0. } ) -> ( 1r ` R ) e. a )
33 3 1 18 lidl1el 
 |-  ( ( R e. Ring /\ a e. U ) -> ( ( 1r ` R ) e. a <-> a = B ) )
34 5 33 sylan 
 |-  ( ( R e. DivRing /\ a e. U ) -> ( ( 1r ` R ) e. a <-> a = B ) )
35 34 adantr 
 |-  ( ( ( R e. DivRing /\ a e. U ) /\ a =/= { .0. } ) -> ( ( 1r ` R ) e. a <-> a = B ) )
36 32 35 mpbid 
 |-  ( ( ( R e. DivRing /\ a e. U ) /\ a =/= { .0. } ) -> a = B )
37 36 olcd 
 |-  ( ( ( R e. DivRing /\ a e. U ) /\ a =/= { .0. } ) -> ( a = { .0. } \/ a = B ) )
38 4 37 pm2.61dane 
 |-  ( ( R e. DivRing /\ a e. U ) -> ( a = { .0. } \/ a = B ) )
39 vex 
 |-  a e. _V
40 39 elpr 
 |-  ( a e. { { .0. } , B } <-> ( a = { .0. } \/ a = B ) )
41 38 40 sylibr 
 |-  ( ( R e. DivRing /\ a e. U ) -> a e. { { .0. } , B } )
42 41 ex 
 |-  ( R e. DivRing -> ( a e. U -> a e. { { .0. } , B } ) )
43 42 ssrdv 
 |-  ( R e. DivRing -> U C_ { { .0. } , B } )
44 3 2 lidl0 
 |-  ( R e. Ring -> { .0. } e. U )
45 3 1 lidl1 
 |-  ( R e. Ring -> B e. U )
46 44 45 prssd 
 |-  ( R e. Ring -> { { .0. } , B } C_ U )
47 5 46 syl 
 |-  ( R e. DivRing -> { { .0. } , B } C_ U )
48 43 47 eqssd 
 |-  ( R e. DivRing -> U = { { .0. } , B } )