Metamath Proof Explorer

Theorem isdrng2

Description: A division ring can equivalently be defined as a ring such that the nonzero elements form a group under multiplication (from which it follows that this is the same group as the group of units). (Contributed by Mario Carneiro, 2-Dec-2014) (Proof shortened by AV, 12-Sep-2026)

Ref Expression
Hypotheses isdrng2.b 
|- B = ( Base ` R )
isdrng2.z 
|- .0. = ( 0g ` R )
isdrng2.g 
|- G = ( ( mulGrp ` R ) |`s ( B \ { .0. } ) )
Assertion isdrng2 
|- ( R e. DivRing <-> ( R e. Ring /\ G e. Grp ) )

Proof

Step Hyp Ref Expression
1 isdrng2.b 
 |-  B = ( Base ` R )
2 isdrng2.z 
 |-  .0. = ( 0g ` R )
3 isdrng2.g 
 |-  G = ( ( mulGrp ` R ) |`s ( B \ { .0. } ) )
4 1 2 3 drngprops 
 |-  ( R e. DivRing -> ( R e. Ring /\ G e. Grp ) )
5 simpl 
 |-  ( ( R e. Ring /\ G e. Grp ) -> R e. Ring )
6 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
7 1 6 unitcl 
 |-  ( x e. ( Unit ` R ) -> x e. B )
8 7 adantl 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( Unit ` R ) ) -> x e. B )
9 difss 
 |-  ( B \ { .0. } ) C_ B
10 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
11 10 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
12 3 11 ressbas2 
 |-  ( ( B \ { .0. } ) C_ B -> ( B \ { .0. } ) = ( Base ` G ) )
13 9 12 ax-mp 
 |-  ( B \ { .0. } ) = ( Base ` G )
14 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
15 13 14 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. ( B \ { .0. } ) )
16 15 ad2antlr 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( Unit ` R ) ) -> ( 0g ` G ) e. ( B \ { .0. } ) )
17 16 eldifsnbd 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( Unit ` R ) ) -> ( 0g ` G ) =/= .0. )
18 simpll 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( Unit ` R ) ) -> R e. Ring )
19 16 eldifad 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( Unit ` R ) ) -> ( 0g ` G ) e. B )
20 simpr 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( Unit ` R ) ) -> x e. ( Unit ` R ) )
21 eqid 
 |-  ( /r ` R ) = ( /r ` R )
22 eqid 
 |-  ( .r ` R ) = ( .r ` R )
23 1 6 21 22 dvrcan1 
 |-  ( ( R e. Ring /\ ( 0g ` G ) e. B /\ x e. ( Unit ` R ) ) -> ( ( ( 0g ` G ) ( /r ` R ) x ) ( .r ` R ) x ) = ( 0g ` G ) )
24 18 19 20 23 syl3anc 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( Unit ` R ) ) -> ( ( ( 0g ` G ) ( /r ` R ) x ) ( .r ` R ) x ) = ( 0g ` G ) )
25 1 6 21 dvrcl 
 |-  ( ( R e. Ring /\ ( 0g ` G ) e. B /\ x e. ( Unit ` R ) ) -> ( ( 0g ` G ) ( /r ` R ) x ) e. B )
26 18 19 20 25 syl3anc 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( Unit ` R ) ) -> ( ( 0g ` G ) ( /r ` R ) x ) e. B )
27 1 22 2 18 26 ringrzd 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( Unit ` R ) ) -> ( ( ( 0g ` G ) ( /r ` R ) x ) ( .r ` R ) .0. ) = .0. )
28 17 24 27 3netr4d 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( Unit ` R ) ) -> ( ( ( 0g ` G ) ( /r ` R ) x ) ( .r ` R ) x ) =/= ( ( ( 0g ` G ) ( /r ` R ) x ) ( .r ` R ) .0. ) )
29 oveq2 
 |-  ( x = .0. -> ( ( ( 0g ` G ) ( /r ` R ) x ) ( .r ` R ) x ) = ( ( ( 0g ` G ) ( /r ` R ) x ) ( .r ` R ) .0. ) )
30 29 necon3i 
 |-  ( ( ( ( 0g ` G ) ( /r ` R ) x ) ( .r ` R ) x ) =/= ( ( ( 0g ` G ) ( /r ` R ) x ) ( .r ` R ) .0. ) -> x =/= .0. )
31 28 30 syl 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( Unit ` R ) ) -> x =/= .0. )
32 8 31 eldifsnd 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( Unit ` R ) ) -> x e. ( B \ { .0. } ) )
33 32 ex 
 |-  ( ( R e. Ring /\ G e. Grp ) -> ( x e. ( Unit ` R ) -> x e. ( B \ { .0. } ) ) )
34 33 ssrdv 
 |-  ( ( R e. Ring /\ G e. Grp ) -> ( Unit ` R ) C_ ( B \ { .0. } ) )
35 eldifi 
 |-  ( x e. ( B \ { .0. } ) -> x e. B )
36 35 adantl 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( B \ { .0. } ) ) -> x e. B )
37 eqid 
 |-  ( invg ` G ) = ( invg ` G )
38 13 37 grpinvcl 
 |-  ( ( G e. Grp /\ x e. ( B \ { .0. } ) ) -> ( ( invg ` G ) ` x ) e. ( B \ { .0. } ) )
39 38 adantll 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( B \ { .0. } ) ) -> ( ( invg ` G ) ` x ) e. ( B \ { .0. } ) )
40 39 eldifad 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( B \ { .0. } ) ) -> ( ( invg ` G ) ` x ) e. B )
41 eqid 
 |-  ( ||r ` R ) = ( ||r ` R )
42 1 41 22 dvdsrmul 
 |-  ( ( x e. B /\ ( ( invg ` G ) ` x ) e. B ) -> x ( ||r ` R ) ( ( ( invg ` G ) ` x ) ( .r ` R ) x ) )
43 36 40 42 syl2anc 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( B \ { .0. } ) ) -> x ( ||r ` R ) ( ( ( invg ` G ) ` x ) ( .r ` R ) x ) )
44 1 fvexi 
 |-  B e. _V
45 difexg 
 |-  ( B e. _V -> ( B \ { .0. } ) e. _V )
46 10 22 mgpplusg 
 |-  ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
47 3 46 ressplusg 
 |-  ( ( B \ { .0. } ) e. _V -> ( .r ` R ) = ( +g ` G ) )
48 44 45 47 mp2b 
 |-  ( .r ` R ) = ( +g ` G )
49 13 48 14 37 grplinv 
 |-  ( ( G e. Grp /\ x e. ( B \ { .0. } ) ) -> ( ( ( invg ` G ) ` x ) ( .r ` R ) x ) = ( 0g ` G ) )
50 49 adantll 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( B \ { .0. } ) ) -> ( ( ( invg ` G ) ` x ) ( .r ` R ) x ) = ( 0g ` G ) )
51 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
52 1 51 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. B )
53 1 22 51 ringlidm 
 |-  ( ( R e. Ring /\ ( 1r ` R ) e. B ) -> ( ( 1r ` R ) ( .r ` R ) ( 1r ` R ) ) = ( 1r ` R ) )
54 52 53 mpdan 
 |-  ( R e. Ring -> ( ( 1r ` R ) ( .r ` R ) ( 1r ` R ) ) = ( 1r ` R ) )
55 54 adantr 
 |-  ( ( R e. Ring /\ G e. Grp ) -> ( ( 1r ` R ) ( .r ` R ) ( 1r ` R ) ) = ( 1r ` R ) )
56 simpr 
 |-  ( ( R e. Ring /\ G e. Grp ) -> G e. Grp )
57 6 51 1unit 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Unit ` R ) )
58 57 adantr 
 |-  ( ( R e. Ring /\ G e. Grp ) -> ( 1r ` R ) e. ( Unit ` R ) )
59 34 58 sseldd 
 |-  ( ( R e. Ring /\ G e. Grp ) -> ( 1r ` R ) e. ( B \ { .0. } ) )
60 13 48 14 grpid 
 |-  ( ( G e. Grp /\ ( 1r ` R ) e. ( B \ { .0. } ) ) -> ( ( ( 1r ` R ) ( .r ` R ) ( 1r ` R ) ) = ( 1r ` R ) <-> ( 0g ` G ) = ( 1r ` R ) ) )
61 56 59 60 syl2anc 
 |-  ( ( R e. Ring /\ G e. Grp ) -> ( ( ( 1r ` R ) ( .r ` R ) ( 1r ` R ) ) = ( 1r ` R ) <-> ( 0g ` G ) = ( 1r ` R ) ) )
62 55 61 mpbid 
 |-  ( ( R e. Ring /\ G e. Grp ) -> ( 0g ` G ) = ( 1r ` R ) )
63 62 adantr 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( B \ { .0. } ) ) -> ( 0g ` G ) = ( 1r ` R ) )
64 50 63 eqtrd 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( B \ { .0. } ) ) -> ( ( ( invg ` G ) ` x ) ( .r ` R ) x ) = ( 1r ` R ) )
65 43 64 breqtrd 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( B \ { .0. } ) ) -> x ( ||r ` R ) ( 1r ` R ) )
66 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
67 66 1 opprbas 
 |-  B = ( Base ` ( oppR ` R ) )
68 eqid 
 |-  ( ||r ` ( oppR ` R ) ) = ( ||r ` ( oppR ` R ) )
69 eqid 
 |-  ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
70 67 68 69 dvdsrmul 
 |-  ( ( x e. B /\ ( ( invg ` G ) ` x ) e. B ) -> x ( ||r ` ( oppR ` R ) ) ( ( ( invg ` G ) ` x ) ( .r ` ( oppR ` R ) ) x ) )
71 36 40 70 syl2anc 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( B \ { .0. } ) ) -> x ( ||r ` ( oppR ` R ) ) ( ( ( invg ` G ) ` x ) ( .r ` ( oppR ` R ) ) x ) )
72 1 22 66 69 opprmul 
 |-  ( ( ( invg ` G ) ` x ) ( .r ` ( oppR ` R ) ) x ) = ( x ( .r ` R ) ( ( invg ` G ) ` x ) )
73 13 48 14 37 grprinv 
 |-  ( ( G e. Grp /\ x e. ( B \ { .0. } ) ) -> ( x ( .r ` R ) ( ( invg ` G ) ` x ) ) = ( 0g ` G ) )
74 73 adantll 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( B \ { .0. } ) ) -> ( x ( .r ` R ) ( ( invg ` G ) ` x ) ) = ( 0g ` G ) )
75 74 63 eqtrd 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( B \ { .0. } ) ) -> ( x ( .r ` R ) ( ( invg ` G ) ` x ) ) = ( 1r ` R ) )
76 72 75 eqtrid 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( B \ { .0. } ) ) -> ( ( ( invg ` G ) ` x ) ( .r ` ( oppR ` R ) ) x ) = ( 1r ` R ) )
77 71 76 breqtrd 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( B \ { .0. } ) ) -> x ( ||r ` ( oppR ` R ) ) ( 1r ` R ) )
78 6 51 41 66 68 isunit 
 |-  ( x e. ( Unit ` R ) <-> ( x ( ||r ` R ) ( 1r ` R ) /\ x ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) )
79 65 77 78 sylanbrc 
 |-  ( ( ( R e. Ring /\ G e. Grp ) /\ x e. ( B \ { .0. } ) ) -> x e. ( Unit ` R ) )
80 34 79 eqelssd 
 |-  ( ( R e. Ring /\ G e. Grp ) -> ( Unit ` R ) = ( B \ { .0. } ) )
81 1 6 2 isdrng 
 |-  ( R e. DivRing <-> ( R e. Ring /\ ( Unit ` R ) = ( B \ { .0. } ) ) )
82 5 80 81 sylanbrc 
 |-  ( ( R e. Ring /\ G e. Grp ) -> R e. DivRing )
83 4 82 impbii 
 |-  ( R e. DivRing <-> ( R e. Ring /\ G e. Grp ) )