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 eqtrid
 |-  ( ( ( 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 ) )