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)

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