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 syl5eq ⊢ ( ( ( 𝑅 ∈ 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 ) )