Metamath Proof Explorer

Theorem drngidl

Description: A nonzero ring is a division ring if and only if its only left ideals are the zero ideal and the unit ideal. (Proposed by Gerard Lang, 13-Mar-2025.) (Contributed by Thierry Arnoux, 13-Mar-2025)

Ref Expression
Hypotheses drngidl.b 
|- B = ( Base ` R )
drngidl.z 
|- .0. = ( 0g ` R )
drngidl.u 
|- U = ( LIdeal ` R )
Assertion drngidl 
|- ( R e. NzRing -> ( R e. DivRing <-> U = { { .0. } , B } ) )

Proof

Step Hyp Ref Expression
1 drngidl.b 
 |-  B = ( Base ` R )
2 drngidl.z 
 |-  .0. = ( 0g ` R )
3 drngidl.u 
 |-  U = ( LIdeal ` R )
4 1 2 3 drngnidl 
 |-  ( R e. DivRing -> U = { { .0. } , B } )
5 4 adantl 
 |-  ( ( R e. NzRing /\ R e. DivRing ) -> U = { { .0. } , B } )
6 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
7 6 2 nzrnz 
 |-  ( R e. NzRing -> ( 1r ` R ) =/= .0. )
8 7 adantr 
 |-  ( ( R e. NzRing /\ U = { { .0. } , B } ) -> ( 1r ` R ) =/= .0. )
9 eqid 
 |-  ( .r ` R ) = ( .r ` R )
10 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
11 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
12 11 adantr 
 |-  ( ( R e. NzRing /\ U = { { .0. } , B } ) -> R e. Ring )
13 12 adantr 
 |-  ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) -> R e. Ring )
14 13 ad4antr 
 |-  ( ( ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) /\ z e. B ) /\ ( 1r ` R ) = ( z ( .r ` R ) y ) ) -> R e. Ring )
15 simp-4r 
 |-  ( ( ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) /\ z e. B ) /\ ( 1r ` R ) = ( z ( .r ` R ) y ) ) -> y e. B )
16 simplr 
 |-  ( ( ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) /\ z e. B ) /\ ( 1r ` R ) = ( z ( .r ` R ) y ) ) -> z e. B )
17 simpr 
 |-  ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) -> x e. ( B \ { .0. } ) )
18 17 eldifad 
 |-  ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) -> x e. B )
19 18 ad2antrr 
 |-  ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) -> x e. B )
20 19 ad2antrr 
 |-  ( ( ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) /\ z e. B ) /\ ( 1r ` R ) = ( z ( .r ` R ) y ) ) -> x e. B )
21 simpr 
 |-  ( ( ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) /\ z e. B ) /\ ( 1r ` R ) = ( z ( .r ` R ) y ) ) -> ( 1r ` R ) = ( z ( .r ` R ) y ) )
22 21 eqcomd 
 |-  ( ( ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) /\ z e. B ) /\ ( 1r ` R ) = ( z ( .r ` R ) y ) ) -> ( z ( .r ` R ) y ) = ( 1r ` R ) )
23 simpr 
 |-  ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) -> ( 1r ` R ) = ( y ( .r ` R ) x ) )
24 23 eqcomd 
 |-  ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) -> ( y ( .r ` R ) x ) = ( 1r ` R ) )
25 24 ad2antrr 
 |-  ( ( ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) /\ z e. B ) /\ ( 1r ` R ) = ( z ( .r ` R ) y ) ) -> ( y ( .r ` R ) x ) = ( 1r ` R ) )
26 1 2 6 9 10 14 15 16 20 22 25 ringinveu 
 |-  ( ( ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) /\ z e. B ) /\ ( 1r ` R ) = ( z ( .r ` R ) y ) ) -> x = z )
27 26 oveq1d 
 |-  ( ( ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) /\ z e. B ) /\ ( 1r ` R ) = ( z ( .r ` R ) y ) ) -> ( x ( .r ` R ) y ) = ( z ( .r ` R ) y ) )
28 27 22 eqtrd 
 |-  ( ( ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) /\ z e. B ) /\ ( 1r ` R ) = ( z ( .r ` R ) y ) ) -> ( x ( .r ` R ) y ) = ( 1r ` R ) )
29 13 ad2antrr 
 |-  ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) -> R e. Ring )
30 simplr 
 |-  ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) -> y e. B )
31 1 6 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. B )
32 13 31 syl 
 |-  ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) -> ( 1r ` R ) e. B )
33 32 ad2antrr 
 |-  ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) -> ( 1r ` R ) e. B )
34 30 snssd 
 |-  ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) -> { y } C_ B )
35 eqid 
 |-  ( RSpan ` R ) = ( RSpan ` R )
36 35 1 3 rspcl 
 |-  ( ( R e. Ring /\ { y } C_ B ) -> ( ( RSpan ` R ) ` { y } ) e. U )
37 29 34 36 syl2anc 
 |-  ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) -> ( ( RSpan ` R ) ` { y } ) e. U )
38 simp-4r 
 |-  ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) -> U = { { .0. } , B } )
39 37 38 eleqtrd 
 |-  ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) -> ( ( RSpan ` R ) ` { y } ) e. { { .0. } , B } )
40 elpri 
 |-  ( ( ( RSpan ` R ) ` { y } ) e. { { .0. } , B } -> ( ( ( RSpan ` R ) ` { y } ) = { .0. } \/ ( ( RSpan ` R ) ` { y } ) = B ) )
41 39 40 syl 
 |-  ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) -> ( ( ( RSpan ` R ) ` { y } ) = { .0. } \/ ( ( RSpan ` R ) ` { y } ) = B ) )
42 simplr 
 |-  ( ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) /\ y = .0. ) -> ( 1r ` R ) = ( y ( .r ` R ) x ) )
43 simpr 
 |-  ( ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) /\ y = .0. ) -> y = .0. )
44 43 oveq1d 
 |-  ( ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) /\ y = .0. ) -> ( y ( .r ` R ) x ) = ( .0. ( .r ` R ) x ) )
45 1 9 2 ringlz 
 |-  ( ( R e. Ring /\ x e. B ) -> ( .0. ( .r ` R ) x ) = .0. )
46 13 18 45 syl2anc 
 |-  ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) -> ( .0. ( .r ` R ) x ) = .0. )
47 46 ad3antrrr 
 |-  ( ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) /\ y = .0. ) -> ( .0. ( .r ` R ) x ) = .0. )
48 42 44 47 3eqtrd 
 |-  ( ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) /\ y = .0. ) -> ( 1r ` R ) = .0. )
49 8 ad4antr 
 |-  ( ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) /\ y = .0. ) -> ( 1r ` R ) =/= .0. )
50 49 neneqd 
 |-  ( ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) /\ y = .0. ) -> -. ( 1r ` R ) = .0. )
51 48 50 pm2.65da 
 |-  ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) -> -. y = .0. )
52 51 neqned 
 |-  ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) -> y =/= .0. )
53 1 2 35 pidlnz 
 |-  ( ( R e. Ring /\ y e. B /\ y =/= .0. ) -> ( ( RSpan ` R ) ` { y } ) =/= { .0. } )
54 29 30 52 53 syl3anc 
 |-  ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) -> ( ( RSpan ` R ) ` { y } ) =/= { .0. } )
55 54 neneqd 
 |-  ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) -> -. ( ( RSpan ` R ) ` { y } ) = { .0. } )
56 41 55 orcnd 
 |-  ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) -> ( ( RSpan ` R ) ` { y } ) = B )
57 33 56 eleqtrrd 
 |-  ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) -> ( 1r ` R ) e. ( ( RSpan ` R ) ` { y } ) )
58 1 9 35 elrspsn 
 |-  ( ( R e. Ring /\ y e. B ) -> ( ( 1r ` R ) e. ( ( RSpan ` R ) ` { y } ) <-> E. z e. B ( 1r ` R ) = ( z ( .r ` R ) y ) ) )
59 58 biimpa 
 |-  ( ( ( R e. Ring /\ y e. B ) /\ ( 1r ` R ) e. ( ( RSpan ` R ) ` { y } ) ) -> E. z e. B ( 1r ` R ) = ( z ( .r ` R ) y ) )
60 29 30 57 59 syl21anc 
 |-  ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) -> E. z e. B ( 1r ` R ) = ( z ( .r ` R ) y ) )
61 28 60 r19.29a 
 |-  ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) -> ( x ( .r ` R ) y ) = ( 1r ` R ) )
62 61 24 jca 
 |-  ( ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ y e. B ) /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) -> ( ( x ( .r ` R ) y ) = ( 1r ` R ) /\ ( y ( .r ` R ) x ) = ( 1r ` R ) ) )
63 62 anasss 
 |-  ( ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) /\ ( y e. B /\ ( 1r ` R ) = ( y ( .r ` R ) x ) ) ) -> ( ( x ( .r ` R ) y ) = ( 1r ` R ) /\ ( y ( .r ` R ) x ) = ( 1r ` R ) ) )
64 18 snssd 
 |-  ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) -> { x } C_ B )
65 35 1 3 rspcl 
 |-  ( ( R e. Ring /\ { x } C_ B ) -> ( ( RSpan ` R ) ` { x } ) e. U )
66 13 64 65 syl2anc 
 |-  ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) -> ( ( RSpan ` R ) ` { x } ) e. U )
67 simplr 
 |-  ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) -> U = { { .0. } , B } )
68 66 67 eleqtrd 
 |-  ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) -> ( ( RSpan ` R ) ` { x } ) e. { { .0. } , B } )
69 elpri 
 |-  ( ( ( RSpan ` R ) ` { x } ) e. { { .0. } , B } -> ( ( ( RSpan ` R ) ` { x } ) = { .0. } \/ ( ( RSpan ` R ) ` { x } ) = B ) )
70 68 69 syl 
 |-  ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) -> ( ( ( RSpan ` R ) ` { x } ) = { .0. } \/ ( ( RSpan ` R ) ` { x } ) = B ) )
71 eldifsni 
 |-  ( x e. ( B \ { .0. } ) -> x =/= .0. )
72 71 adantl 
 |-  ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) -> x =/= .0. )
73 1 2 35 pidlnz 
 |-  ( ( R e. Ring /\ x e. B /\ x =/= .0. ) -> ( ( RSpan ` R ) ` { x } ) =/= { .0. } )
74 13 18 72 73 syl3anc 
 |-  ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) -> ( ( RSpan ` R ) ` { x } ) =/= { .0. } )
75 74 neneqd 
 |-  ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) -> -. ( ( RSpan ` R ) ` { x } ) = { .0. } )
76 70 75 orcnd 
 |-  ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) -> ( ( RSpan ` R ) ` { x } ) = B )
77 32 76 eleqtrrd 
 |-  ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) -> ( 1r ` R ) e. ( ( RSpan ` R ) ` { x } ) )
78 1 9 35 elrspsn 
 |-  ( ( R e. Ring /\ x e. B ) -> ( ( 1r ` R ) e. ( ( RSpan ` R ) ` { x } ) <-> E. y e. B ( 1r ` R ) = ( y ( .r ` R ) x ) ) )
79 78 biimpa 
 |-  ( ( ( R e. Ring /\ x e. B ) /\ ( 1r ` R ) e. ( ( RSpan ` R ) ` { x } ) ) -> E. y e. B ( 1r ` R ) = ( y ( .r ` R ) x ) )
80 13 18 77 79 syl21anc 
 |-  ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) -> E. y e. B ( 1r ` R ) = ( y ( .r ` R ) x ) )
81 63 80 reximddv 
 |-  ( ( ( R e. NzRing /\ U = { { .0. } , B } ) /\ x e. ( B \ { .0. } ) ) -> E. y e. B ( ( x ( .r ` R ) y ) = ( 1r ` R ) /\ ( y ( .r ` R ) x ) = ( 1r ` R ) ) )
82 81 ralrimiva 
 |-  ( ( R e. NzRing /\ U = { { .0. } , B } ) -> A. x e. ( B \ { .0. } ) E. y e. B ( ( x ( .r ` R ) y ) = ( 1r ` R ) /\ ( y ( .r ` R ) x ) = ( 1r ` R ) ) )
83 1 2 6 9 10 12 isdrng4 
 |-  ( ( R e. NzRing /\ U = { { .0. } , B } ) -> ( R e. DivRing <-> ( ( 1r ` R ) =/= .0. /\ A. x e. ( B \ { .0. } ) E. y e. B ( ( x ( .r ` R ) y ) = ( 1r ` R ) /\ ( y ( .r ` R ) x ) = ( 1r ` R ) ) ) ) )
84 8 82 83 mpbir2and 
 |-  ( ( R e. NzRing /\ U = { { .0. } , B } ) -> R e. DivRing )
85 5 84 impbida 
 |-  ( R e. NzRing -> ( R e. DivRing <-> U = { { .0. } , B } ) )