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 𝐵 = ( Base ‘ 𝑅 )
isdrng2.z 0 = ( 0g𝑅 )
isdrng2.g 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) )
Assertion isdrng2 ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) )

Proof

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