Metamath Proof Explorer

Theorem drngidlhash

Description: A ring is a division ring if and only if it admits exactly two ideals. (Proposed by Gerard Lang, 13-Mar-2025.) (Contributed by Thierry Arnoux, 13-Mar-2025)

Ref Expression
Hypothesis drngidlhash.u 
|- U = ( LIdeal ` R )
Assertion drngidlhash 
|- ( R e. Ring -> ( R e. DivRing <-> ( # ` U ) = 2 ) )

Proof

Step Hyp Ref Expression
1 drngidlhash.u 
 |-  U = ( LIdeal ` R )
2 eqid 
 |-  ( Base ` R ) = ( Base ` R )
3 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
4 2 3 1 drngnidl 
 |-  ( R e. DivRing -> U = { { ( 0g ` R ) } , ( Base ` R ) } )
5 4 fveq2d 
 |-  ( R e. DivRing -> ( # ` U ) = ( # ` { { ( 0g ` R ) } , ( Base ` R ) } ) )
6 drngnzr 
 |-  ( R e. DivRing -> R e. NzRing )
7 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
8 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
9 2 8 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
10 7 9 syl 
 |-  ( R e. NzRing -> ( 1r ` R ) e. ( Base ` R ) )
11 8 3 nzrnz 
 |-  ( R e. NzRing -> ( 1r ` R ) =/= ( 0g ` R ) )
12 nelsn 
 |-  ( ( 1r ` R ) =/= ( 0g ` R ) -> -. ( 1r ` R ) e. { ( 0g ` R ) } )
13 11 12 syl 
 |-  ( R e. NzRing -> -. ( 1r ` R ) e. { ( 0g ` R ) } )
14 nelne1 
 |-  ( ( ( 1r ` R ) e. ( Base ` R ) /\ -. ( 1r ` R ) e. { ( 0g ` R ) } ) -> ( Base ` R ) =/= { ( 0g ` R ) } )
15 10 13 14 syl2anc 
 |-  ( R e. NzRing -> ( Base ` R ) =/= { ( 0g ` R ) } )
16 15 necomd 
 |-  ( R e. NzRing -> { ( 0g ` R ) } =/= ( Base ` R ) )
17 6 16 syl 
 |-  ( R e. DivRing -> { ( 0g ` R ) } =/= ( Base ` R ) )
18 snex 
 |-  { ( 0g ` R ) } e. _V
19 fvex 
 |-  ( Base ` R ) e. _V
20 hashprg 
 |-  ( ( { ( 0g ` R ) } e. _V /\ ( Base ` R ) e. _V ) -> ( { ( 0g ` R ) } =/= ( Base ` R ) <-> ( # ` { { ( 0g ` R ) } , ( Base ` R ) } ) = 2 ) )
21 18 19 20 mp2an 
 |-  ( { ( 0g ` R ) } =/= ( Base ` R ) <-> ( # ` { { ( 0g ` R ) } , ( Base ` R ) } ) = 2 )
22 17 21 sylib 
 |-  ( R e. DivRing -> ( # ` { { ( 0g ` R ) } , ( Base ` R ) } ) = 2 )
23 5 22 eqtrd 
 |-  ( R e. DivRing -> ( # ` U ) = 2 )
24 23 adantl 
 |-  ( ( R e. Ring /\ R e. DivRing ) -> ( # ` U ) = 2 )
25 simpl 
 |-  ( ( R e. Ring /\ ( # ` U ) = 2 ) -> R e. Ring )
26 simplr 
 |-  ( ( ( R e. Ring /\ ( # ` U ) = 2 ) /\ { ( 0g ` R ) } = ( Base ` R ) ) -> ( # ` U ) = 2 )
27 2re 
 |-  2 e. RR
28 26 27 eqeltrdi 
 |-  ( ( ( R e. Ring /\ ( # ` U ) = 2 ) /\ { ( 0g ` R ) } = ( Base ` R ) ) -> ( # ` U ) e. RR )
29 simpl 
 |-  ( ( R e. Ring /\ { ( 0g ` R ) } = ( Base ` R ) ) -> R e. Ring )
30 simpr 
 |-  ( ( R e. Ring /\ { ( 0g ` R ) } = ( Base ` R ) ) -> { ( 0g ` R ) } = ( Base ` R ) )
31 30 fveq2d 
 |-  ( ( R e. Ring /\ { ( 0g ` R ) } = ( Base ` R ) ) -> ( # ` { ( 0g ` R ) } ) = ( # ` ( Base ` R ) ) )
32 fvex 
 |-  ( 0g ` R ) e. _V
33 hashsng 
 |-  ( ( 0g ` R ) e. _V -> ( # ` { ( 0g ` R ) } ) = 1 )
34 32 33 ax-mp 
 |-  ( # ` { ( 0g ` R ) } ) = 1
35 31 34 eqtr3di 
 |-  ( ( R e. Ring /\ { ( 0g ` R ) } = ( Base ` R ) ) -> ( # ` ( Base ` R ) ) = 1 )
36 2 3 0ringidl 
 |-  ( ( R e. Ring /\ ( # ` ( Base ` R ) ) = 1 ) -> ( LIdeal ` R ) = { { ( 0g ` R ) } } )
37 29 35 36 syl2anc 
 |-  ( ( R e. Ring /\ { ( 0g ` R ) } = ( Base ` R ) ) -> ( LIdeal ` R ) = { { ( 0g ` R ) } } )
38 1 37 eqtrid 
 |-  ( ( R e. Ring /\ { ( 0g ` R ) } = ( Base ` R ) ) -> U = { { ( 0g ` R ) } } )
39 38 fveq2d 
 |-  ( ( R e. Ring /\ { ( 0g ` R ) } = ( Base ` R ) ) -> ( # ` U ) = ( # ` { { ( 0g ` R ) } } ) )
40 hashsng 
 |-  ( { ( 0g ` R ) } e. _V -> ( # ` { { ( 0g ` R ) } } ) = 1 )
41 18 40 ax-mp 
 |-  ( # ` { { ( 0g ` R ) } } ) = 1
42 39 41 eqtrdi 
 |-  ( ( R e. Ring /\ { ( 0g ` R ) } = ( Base ` R ) ) -> ( # ` U ) = 1 )
43 42 adantlr 
 |-  ( ( ( R e. Ring /\ ( # ` U ) = 2 ) /\ { ( 0g ` R ) } = ( Base ` R ) ) -> ( # ` U ) = 1 )
44 1lt2 
 |-  1 < 2
45 43 44 eqbrtrdi 
 |-  ( ( ( R e. Ring /\ ( # ` U ) = 2 ) /\ { ( 0g ` R ) } = ( Base ` R ) ) -> ( # ` U ) < 2 )
46 28 45 ltned 
 |-  ( ( ( R e. Ring /\ ( # ` U ) = 2 ) /\ { ( 0g ` R ) } = ( Base ` R ) ) -> ( # ` U ) =/= 2 )
47 46 neneqd 
 |-  ( ( ( R e. Ring /\ ( # ` U ) = 2 ) /\ { ( 0g ` R ) } = ( Base ` R ) ) -> -. ( # ` U ) = 2 )
48 26 47 pm2.65da 
 |-  ( ( R e. Ring /\ ( # ` U ) = 2 ) -> -. { ( 0g ` R ) } = ( Base ` R ) )
49 48 neqned 
 |-  ( ( R e. Ring /\ ( # ` U ) = 2 ) -> { ( 0g ` R ) } =/= ( Base ` R ) )
50 2 3 8 01eq0ring 
 |-  ( ( R e. Ring /\ ( 0g ` R ) = ( 1r ` R ) ) -> ( Base ` R ) = { ( 0g ` R ) } )
51 50 eqcomd 
 |-  ( ( R e. Ring /\ ( 0g ` R ) = ( 1r ` R ) ) -> { ( 0g ` R ) } = ( Base ` R ) )
52 51 ex 
 |-  ( R e. Ring -> ( ( 0g ` R ) = ( 1r ` R ) -> { ( 0g ` R ) } = ( Base ` R ) ) )
53 52 necon3d 
 |-  ( R e. Ring -> ( { ( 0g ` R ) } =/= ( Base ` R ) -> ( 0g ` R ) =/= ( 1r ` R ) ) )
54 25 49 53 sylc 
 |-  ( ( R e. Ring /\ ( # ` U ) = 2 ) -> ( 0g ` R ) =/= ( 1r ` R ) )
55 54 necomd 
 |-  ( ( R e. Ring /\ ( # ` U ) = 2 ) -> ( 1r ` R ) =/= ( 0g ` R ) )
56 8 3 isnzr 
 |-  ( R e. NzRing <-> ( R e. Ring /\ ( 1r ` R ) =/= ( 0g ` R ) ) )
57 25 55 56 sylanbrc 
 |-  ( ( R e. Ring /\ ( # ` U ) = 2 ) -> R e. NzRing )
58 1 fvexi 
 |-  U e. _V
59 58 a1i 
 |-  ( ( R e. Ring /\ ( # ` U ) = 2 ) -> U e. _V )
60 simpr 
 |-  ( ( R e. Ring /\ ( # ` U ) = 2 ) -> ( # ` U ) = 2 )
61 1 3 lidl0 
 |-  ( R e. Ring -> { ( 0g ` R ) } e. U )
62 25 61 syl 
 |-  ( ( R e. Ring /\ ( # ` U ) = 2 ) -> { ( 0g ` R ) } e. U )
63 1 2 lidl1 
 |-  ( R e. Ring -> ( Base ` R ) e. U )
64 25 63 syl 
 |-  ( ( R e. Ring /\ ( # ` U ) = 2 ) -> ( Base ` R ) e. U )
65 hash2prd 
 |-  ( ( U e. _V /\ ( # ` U ) = 2 ) -> ( ( { ( 0g ` R ) } e. U /\ ( Base ` R ) e. U /\ { ( 0g ` R ) } =/= ( Base ` R ) ) -> U = { { ( 0g ` R ) } , ( Base ` R ) } ) )
66 65 imp 
 |-  ( ( ( U e. _V /\ ( # ` U ) = 2 ) /\ ( { ( 0g ` R ) } e. U /\ ( Base ` R ) e. U /\ { ( 0g ` R ) } =/= ( Base ` R ) ) ) -> U = { { ( 0g ` R ) } , ( Base ` R ) } )
67 59 60 62 64 49 66 syl23anc 
 |-  ( ( R e. Ring /\ ( # ` U ) = 2 ) -> U = { { ( 0g ` R ) } , ( Base ` R ) } )
68 2 3 1 drngidl 
 |-  ( R e. NzRing -> ( R e. DivRing <-> U = { { ( 0g ` R ) } , ( Base ` R ) } ) )
69 68 biimpar 
 |-  ( ( R e. NzRing /\ U = { { ( 0g ` R ) } , ( Base ` R ) } ) -> R e. DivRing )
70 57 67 69 syl2anc 
 |-  ( ( R e. Ring /\ ( # ` U ) = 2 ) -> R e. DivRing )
71 24 70 impbida 
 |-  ( R e. Ring -> ( R e. DivRing <-> ( # ` U ) = 2 ) )