Metamath Proof Explorer

Theorem isdrngd

Description: Properties that characterize a division ring among rings: it should be nonzero, have no nonzero zero-divisors, and every nonzero element x should have a left-inverse I ( x ) . See isdrngrd for the characterization using right-inverses. (Contributed by NM, 2-Aug-2013) Remove hypothesis. (Revised by SN, 19-Feb-2025)

Ref Expression
Hypotheses isdrngd.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
isdrngd.t ⊢ ( 𝜑 → · = ( .r ‘ 𝑅 ) )
isdrngd.z ⊢ ( 𝜑 → 0 = ( 0g ‘ 𝑅 ) )
isdrngd.u ⊢ ( 𝜑 → 1 = ( 1r ‘ 𝑅 ) )
isdrngd.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
isdrngd.n ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ≠ 0 )
isdrngd.o ⊢ ( 𝜑 → 1 ≠ 0 )
isdrngd.i ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → 𝐼 ∈ 𝐵 )
isdrngd.k ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝐼 · 𝑥 ) = 1 )
Assertion isdrngd ( 𝜑 → 𝑅 ∈ DivRing )

Proof

Step Hyp Ref Expression
1 isdrngd.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
2 isdrngd.t ⊢ ( 𝜑 → · = ( .r ‘ 𝑅 ) )
3 isdrngd.z ⊢ ( 𝜑 → 0 = ( 0g ‘ 𝑅 ) )
4 isdrngd.u ⊢ ( 𝜑 → 1 = ( 1r ‘ 𝑅 ) )
5 isdrngd.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 isdrngd.n ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ≠ 0 )
7 isdrngd.o ⊢ ( 𝜑 → 1 ≠ 0 )
8 isdrngd.i ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → 𝐼 ∈ 𝐵 )
9 isdrngd.k ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝐼 · 𝑥 ) = 1 )
10 difss ⊢ ( 𝐵 ∖ { 0 } ) ⊆ 𝐵
11 10 1 sseqtrid ⊢ ( 𝜑 → ( 𝐵 ∖ { 0 } ) ⊆ ( Base ‘ 𝑅 ) )
12 eqid ⊢ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) )
13 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
14 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
15 13 14 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
16 12 15 ressbas2 ⊢ ( ( 𝐵 ∖ { 0 } ) ⊆ ( Base ‘ 𝑅 ) → ( 𝐵 ∖ { 0 } ) = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
17 11 16 syl ⊢ ( 𝜑 → ( 𝐵 ∖ { 0 } ) = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
18 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
19 1 18 eqeltrdi ⊢ ( 𝜑 → 𝐵 ∈ V )
20 difexg ⊢ ( 𝐵 ∈ V → ( 𝐵 ∖ { 0 } ) ∈ V )
21 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
22 13 21 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
23 12 22 ressplusg ⊢ ( ( 𝐵 ∖ { 0 } ) ∈ V → ( .r ‘ 𝑅 ) = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
24 19 20 23 3syl ⊢ ( 𝜑 → ( .r ‘ 𝑅 ) = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
25 2 24 eqtrd ⊢ ( 𝜑 → · = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
26 eldifsn ⊢ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) )
27 eldifsn ⊢ ( 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) )
28 14 21 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
29 5 28 syl3an1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
30 29 3expib ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) )
31 1 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ( Base ‘ 𝑅 ) ) )
32 1 eleq2d ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ( Base ‘ 𝑅 ) ) )
33 31 32 anbi12d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) )
34 2 oveqd ⊢ ( 𝜑 → ( 𝑥 · 𝑦 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) )
35 34 1 eleq12d ⊢ ( 𝜑 → ( ( 𝑥 · 𝑦 ) ∈ 𝐵 ↔ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) )
36 30 33 35 3imtr4d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 · 𝑦 ) ∈ 𝐵 ) )
37 36 3impib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 · 𝑦 ) ∈ 𝐵 )
38 37 3adant2r ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 · 𝑦 ) ∈ 𝐵 )
39 38 3adant3r ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝐵 )
40 eldifsn ⊢ ( ( 𝑥 · 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ↔ ( ( 𝑥 · 𝑦 ) ∈ 𝐵 ∧ ( 𝑥 · 𝑦 ) ≠ 0 ) )
41 39 6 40 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) )
42 27 41 syl3an3b ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) )
43 26 42 syl3an2b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) )
44 14 21 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) )
45 44 ex ⊢ ( 𝑅 ∈ Ring → ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) ) )
46 5 45 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) ) )
47 1 eleq2d ⊢ ( 𝜑 → ( 𝑧 ∈ 𝐵 ↔ 𝑧 ∈ ( Base ‘ 𝑅 ) ) )
48 31 32 47 3anbi123d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) )
49 eqidd ⊢ ( 𝜑 → 𝑧 = 𝑧 )
50 2 34 49 oveq123d ⊢ ( 𝜑 → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) )
51 eqidd ⊢ ( 𝜑 → 𝑥 = 𝑥 )
52 2 oveqd ⊢ ( 𝜑 → ( 𝑦 · 𝑧 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) )
53 2 51 52 oveq123d ⊢ ( 𝜑 → ( 𝑥 · ( 𝑦 · 𝑧 ) ) = ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) )
54 50 53 eqeq12d ⊢ ( 𝜑 → ( ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) ↔ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) ) )
55 46 48 54 3imtr4d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) ) )
56 eldifi ⊢ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) → 𝑥 ∈ 𝐵 )
57 eldifi ⊢ ( 𝑦 ∈ ( 𝐵 ∖ { 0 } ) → 𝑦 ∈ 𝐵 )
58 eldifi ⊢ ( 𝑧 ∈ ( 𝐵 ∖ { 0 } ) → 𝑧 ∈ 𝐵 )
59 56 57 58 3anim123i ⊢ ( ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑧 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) )
60 55 59 impel ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑧 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
61 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
62 14 61 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
63 5 62 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
64 63 4 1 3eltr4d ⊢ ( 𝜑 → 1 ∈ 𝐵 )
65 eldifsn ⊢ ( 1 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 1 ∈ 𝐵 ∧ 1 ≠ 0 ) )
66 64 7 65 sylanbrc ⊢ ( 𝜑 → 1 ∈ ( 𝐵 ∖ { 0 } ) )
67 14 21 61 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 )
68 67 ex ⊢ ( 𝑅 ∈ Ring → ( 𝑥 ∈ ( Base ‘ 𝑅 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ) )
69 5 68 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑅 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ) )
70 2 4 51 oveq123d ⊢ ( 𝜑 → ( 1 · 𝑥 ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) )
71 70 eqeq1d ⊢ ( 𝜑 → ( ( 1 · 𝑥 ) = 𝑥 ↔ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ) )
72 69 31 71 3imtr4d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → ( 1 · 𝑥 ) = 𝑥 ) )
73 72 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 1 · 𝑥 ) = 𝑥 )
74 73 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 1 · 𝑥 ) = 𝑥 )
75 26 74 sylan2b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 1 · 𝑥 ) = 𝑥 )
76 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → 1 ≠ 0 )
77 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) ∧ 𝐼 = 0 ) → 𝐼 = 0 )
78 77 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) ∧ 𝐼 = 0 ) → ( 𝐼 · 𝑥 ) = ( 0 · 𝑥 ) )
79 9 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) ∧ 𝐼 = 0 ) → ( 𝐼 · 𝑥 ) = 1 )
80 31 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
81 80 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
82 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
83 14 21 82 ringlz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) )
84 5 81 83 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) )
85 2 3 51 oveq123d ⊢ ( 𝜑 → ( 0 · 𝑥 ) = ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) )
86 85 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 0 · 𝑥 ) = ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) )
87 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → 0 = ( 0g ‘ 𝑅 ) )
88 84 86 87 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 0 · 𝑥 ) = 0 )
89 88 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) ∧ 𝐼 = 0 ) → ( 0 · 𝑥 ) = 0 )
90 78 79 89 3eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) ∧ 𝐼 = 0 ) → 1 = 0 )
91 76 90 mteqand ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → 𝐼 ≠ 0 )
92 eldifsn ⊢ ( 𝐼 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 𝐼 ∈ 𝐵 ∧ 𝐼 ≠ 0 ) )
93 8 91 92 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → 𝐼 ∈ ( 𝐵 ∖ { 0 } ) )
94 26 93 sylan2b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝐼 ∈ ( 𝐵 ∖ { 0 } ) )
95 26 9 sylan2b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝐼 · 𝑥 ) = 1 )
96 17 25 43 60 66 75 94 95 isgrpd ⊢ ( 𝜑 → ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp )
97 3 sneqd ⊢ ( 𝜑 → { 0 } = { ( 0g ‘ 𝑅 ) } )
98 1 97 difeq12d ⊢ ( 𝜑 → ( 𝐵 ∖ { 0 } ) = ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) )
99 98 oveq2d ⊢ ( 𝜑 → ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ) )
100 99 eleq1d ⊢ ( 𝜑 → ( ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ↔ ( ( mulGrp ‘ 𝑅 ) ↾s ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ) ∈ Grp ) )
101 100 anbi2d ⊢ ( 𝜑 → ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) ↔ ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ) ∈ Grp ) ) )
102 5 96 101 mpbi2and ⊢ ( 𝜑 → ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ) ∈ Grp ) )
103 eqid ⊢ ( ( mulGrp ‘ 𝑅 ) ↾s ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) )
104 14 82 103 isdrng2 ⊢ ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ) ∈ Grp ) )
105 102 104 sylibr ⊢ ( 𝜑 → 𝑅 ∈ DivRing )