Step | Hyp | Ref
| Expression |
1 | | isdrngd.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ Ring) |
2 | | difss 4131 |
. . . . . 6
⊢ (𝐵 ∖ { 0 }) ⊆ 𝐵 |
3 | | isdrngd.b |
. . . . . 6
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) |
4 | 2, 3 | sseqtrid 4032 |
. . . . 5
⊢ (𝜑 → (𝐵 ∖ { 0 }) ⊆
(Base‘𝑅)) |
5 | | eqid 2726 |
. . . . . 6
⊢
((mulGrp‘𝑅)
↾s (𝐵
∖ { 0 })) = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) |
6 | | eqid 2726 |
. . . . . . 7
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
7 | | eqid 2726 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) |
8 | 6, 7 | mgpbas 20123 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
9 | 5, 8 | ressbas2 17251 |
. . . . 5
⊢ ((𝐵 ∖ { 0 }) ⊆
(Base‘𝑅) →
(𝐵 ∖ { 0 }) =
(Base‘((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })))) |
10 | 4, 9 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐵 ∖ { 0 }) =
(Base‘((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })))) |
11 | | isdrngd.t |
. . . . 5
⊢ (𝜑 → · =
(.r‘𝑅)) |
12 | | fvex 6914 |
. . . . . . 7
⊢
(Base‘𝑅)
∈ V |
13 | 3, 12 | eqeltrdi 2834 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ V) |
14 | | difexg 5334 |
. . . . . 6
⊢ (𝐵 ∈ V → (𝐵 ∖ { 0 }) ∈
V) |
15 | | eqid 2726 |
. . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) |
16 | 6, 15 | mgpplusg 20121 |
. . . . . . 7
⊢
(.r‘𝑅) = (+g‘(mulGrp‘𝑅)) |
17 | 5, 16 | ressplusg 17304 |
. . . . . 6
⊢ ((𝐵 ∖ { 0 }) ∈ V →
(.r‘𝑅) =
(+g‘((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })))) |
18 | 13, 14, 17 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (.r‘𝑅) =
(+g‘((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })))) |
19 | 11, 18 | eqtrd 2766 |
. . . 4
⊢ (𝜑 → · =
(+g‘((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })))) |
20 | | eldifsn 4795 |
. . . . 5
⊢ (𝑥 ∈ (𝐵 ∖ { 0 }) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) |
21 | | eldifsn 4795 |
. . . . . 6
⊢ (𝑦 ∈ (𝐵 ∖ { 0 }) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) |
22 | 7, 15 | ringcl 20233 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)𝑦) ∈ (Base‘𝑅)) |
23 | 1, 22 | syl3an1 1160 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)𝑦) ∈ (Base‘𝑅)) |
24 | 23 | 3expib 1119 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)𝑦) ∈ (Base‘𝑅))) |
25 | 3 | eleq2d 2812 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (Base‘𝑅))) |
26 | 3 | eleq2d 2812 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ (Base‘𝑅))) |
27 | 25, 26 | anbi12d 630 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)))) |
28 | 11 | oveqd 7441 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 · 𝑦) = (𝑥(.r‘𝑅)𝑦)) |
29 | 28, 3 | eleq12d 2820 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 · 𝑦) ∈ 𝐵 ↔ (𝑥(.r‘𝑅)𝑦) ∈ (Base‘𝑅))) |
30 | 24, 27, 29 | 3imtr4d 293 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵)) |
31 | 30 | 3impib 1113 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵) |
32 | 31 | 3adant2r 1176 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵) |
33 | 32 | 3adant3r 1178 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝑥 · 𝑦) ∈ 𝐵) |
34 | | isdrngd.n |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝑥 · 𝑦) ≠ 0 ) |
35 | | eldifsn 4795 |
. . . . . . 7
⊢ ((𝑥 · 𝑦) ∈ (𝐵 ∖ { 0 }) ↔ ((𝑥 · 𝑦) ∈ 𝐵 ∧ (𝑥 · 𝑦) ≠ 0 )) |
36 | 33, 34, 35 | sylanbrc 581 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝑥 · 𝑦) ∈ (𝐵 ∖ { 0 })) |
37 | 21, 36 | syl3an3b 1402 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → (𝑥 · 𝑦) ∈ (𝐵 ∖ { 0 })) |
38 | 20, 37 | syl3an2b 1401 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → (𝑥 · 𝑦) ∈ (𝐵 ∖ { 0 })) |
39 | 7, 15 | ringass 20236 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) → ((𝑥(.r‘𝑅)𝑦)(.r‘𝑅)𝑧) = (𝑥(.r‘𝑅)(𝑦(.r‘𝑅)𝑧))) |
40 | 39 | ex 411 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → ((𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅)) → ((𝑥(.r‘𝑅)𝑦)(.r‘𝑅)𝑧) = (𝑥(.r‘𝑅)(𝑦(.r‘𝑅)𝑧)))) |
41 | 1, 40 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅)) → ((𝑥(.r‘𝑅)𝑦)(.r‘𝑅)𝑧) = (𝑥(.r‘𝑅)(𝑦(.r‘𝑅)𝑧)))) |
42 | 3 | eleq2d 2812 |
. . . . . . 7
⊢ (𝜑 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ (Base‘𝑅))) |
43 | 25, 26, 42 | 3anbi123d 1433 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ↔ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅)))) |
44 | | eqidd 2727 |
. . . . . . . 8
⊢ (𝜑 → 𝑧 = 𝑧) |
45 | 11, 28, 44 | oveq123d 7445 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 · 𝑦) · 𝑧) = ((𝑥(.r‘𝑅)𝑦)(.r‘𝑅)𝑧)) |
46 | | eqidd 2727 |
. . . . . . . 8
⊢ (𝜑 → 𝑥 = 𝑥) |
47 | 11 | oveqd 7441 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 · 𝑧) = (𝑦(.r‘𝑅)𝑧)) |
48 | 11, 46, 47 | oveq123d 7445 |
. . . . . . 7
⊢ (𝜑 → (𝑥 · (𝑦 · 𝑧)) = (𝑥(.r‘𝑅)(𝑦(.r‘𝑅)𝑧))) |
49 | 45, 48 | eqeq12d 2742 |
. . . . . 6
⊢ (𝜑 → (((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)) ↔ ((𝑥(.r‘𝑅)𝑦)(.r‘𝑅)𝑧) = (𝑥(.r‘𝑅)(𝑦(.r‘𝑅)𝑧)))) |
50 | 41, 43, 49 | 3imtr4d 293 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))) |
51 | | eldifi 4126 |
. . . . . 6
⊢ (𝑥 ∈ (𝐵 ∖ { 0 }) → 𝑥 ∈ 𝐵) |
52 | | eldifi 4126 |
. . . . . 6
⊢ (𝑦 ∈ (𝐵 ∖ { 0 }) → 𝑦 ∈ 𝐵) |
53 | | eldifi 4126 |
. . . . . 6
⊢ (𝑧 ∈ (𝐵 ∖ { 0 }) → 𝑧 ∈ 𝐵) |
54 | 51, 52, 53 | 3anim123i 1148 |
. . . . 5
⊢ ((𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 }) ∧ 𝑧 ∈ (𝐵 ∖ { 0 })) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) |
55 | 50, 54 | impel 504 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 }) ∧ 𝑧 ∈ (𝐵 ∖ { 0 }))) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) |
56 | | eqid 2726 |
. . . . . . . 8
⊢
(1r‘𝑅) = (1r‘𝑅) |
57 | 7, 56 | ringidcl 20245 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) |
58 | 1, 57 | syl 17 |
. . . . . 6
⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅)) |
59 | | isdrngd.u |
. . . . . 6
⊢ (𝜑 → 1 =
(1r‘𝑅)) |
60 | 58, 59, 3 | 3eltr4d 2841 |
. . . . 5
⊢ (𝜑 → 1 ∈ 𝐵) |
61 | | isdrngd.o |
. . . . 5
⊢ (𝜑 → 1 ≠ 0 ) |
62 | | eldifsn 4795 |
. . . . 5
⊢ ( 1 ∈ (𝐵 ∖ { 0 }) ↔ ( 1 ∈ 𝐵 ∧ 1 ≠ 0 )) |
63 | 60, 61, 62 | sylanbrc 581 |
. . . 4
⊢ (𝜑 → 1 ∈ (𝐵 ∖ { 0 })) |
64 | 7, 15, 56 | ringlidm 20248 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑅)) →
((1r‘𝑅)(.r‘𝑅)𝑥) = 𝑥) |
65 | 64 | ex 411 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → (𝑥 ∈ (Base‘𝑅) →
((1r‘𝑅)(.r‘𝑅)𝑥) = 𝑥)) |
66 | 1, 65 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑅) → ((1r‘𝑅)(.r‘𝑅)𝑥) = 𝑥)) |
67 | 11, 59, 46 | oveq123d 7445 |
. . . . . . . . 9
⊢ (𝜑 → ( 1 · 𝑥) = ((1r‘𝑅)(.r‘𝑅)𝑥)) |
68 | 67 | eqeq1d 2728 |
. . . . . . . 8
⊢ (𝜑 → (( 1 · 𝑥) = 𝑥 ↔ ((1r‘𝑅)(.r‘𝑅)𝑥) = 𝑥)) |
69 | 66, 25, 68 | 3imtr4d 293 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐵 → ( 1 · 𝑥) = 𝑥)) |
70 | 69 | imp 405 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 1 · 𝑥) = 𝑥) |
71 | 70 | adantrr 715 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → ( 1 · 𝑥) = 𝑥) |
72 | 20, 71 | sylan2b 592 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → ( 1 · 𝑥) = 𝑥) |
73 | | isdrngd.i |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ∈ 𝐵) |
74 | 61 | adantr 479 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 1 ≠ 0
) |
75 | | simpr 483 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) ∧ 𝐼 = 0 ) → 𝐼 = 0 ) |
76 | 75 | oveq1d 7439 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) ∧ 𝐼 = 0 ) → (𝐼 · 𝑥) = ( 0 · 𝑥)) |
77 | | isdrngd.k |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → (𝐼 · 𝑥) = 1 ) |
78 | 77 | adantr 479 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) ∧ 𝐼 = 0 ) → (𝐼 · 𝑥) = 1 ) |
79 | 25 | biimpa 475 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ (Base‘𝑅)) |
80 | 79 | adantrr 715 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝑥 ∈ (Base‘𝑅)) |
81 | | eqid 2726 |
. . . . . . . . . . . 12
⊢
(0g‘𝑅) = (0g‘𝑅) |
82 | 7, 15, 81 | ringlz 20272 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑅)) →
((0g‘𝑅)(.r‘𝑅)𝑥) = (0g‘𝑅)) |
83 | 1, 80, 82 | syl2an2r 683 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) →
((0g‘𝑅)(.r‘𝑅)𝑥) = (0g‘𝑅)) |
84 | | isdrngd.z |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 =
(0g‘𝑅)) |
85 | 11, 84, 46 | oveq123d 7445 |
. . . . . . . . . . 11
⊢ (𝜑 → ( 0 · 𝑥) = ((0g‘𝑅)(.r‘𝑅)𝑥)) |
86 | 85 | adantr 479 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → ( 0 · 𝑥) = ((0g‘𝑅)(.r‘𝑅)𝑥)) |
87 | 84 | adantr 479 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 0 =
(0g‘𝑅)) |
88 | 83, 86, 87 | 3eqtr4d 2776 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → ( 0 · 𝑥) = 0 ) |
89 | 88 | adantr 479 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) ∧ 𝐼 = 0 ) → ( 0 · 𝑥) = 0 ) |
90 | 76, 78, 89 | 3eqtr3d 2774 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) ∧ 𝐼 = 0 ) → 1 = 0
) |
91 | 74, 90 | mteqand 3023 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ≠ 0 ) |
92 | | eldifsn 4795 |
. . . . . 6
⊢ (𝐼 ∈ (𝐵 ∖ { 0 }) ↔ (𝐼 ∈ 𝐵 ∧ 𝐼 ≠ 0 )) |
93 | 73, 91, 92 | sylanbrc 581 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ∈ (𝐵 ∖ { 0 })) |
94 | 20, 93 | sylan2b 592 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → 𝐼 ∈ (𝐵 ∖ { 0 })) |
95 | 20, 77 | sylan2b 592 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → (𝐼 · 𝑥) = 1 ) |
96 | 10, 19, 38, 55, 63, 72, 94, 95 | isgrpd 18953 |
. . 3
⊢ (𝜑 → ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) ∈
Grp) |
97 | 84 | sneqd 4645 |
. . . . . . 7
⊢ (𝜑 → { 0 } =
{(0g‘𝑅)}) |
98 | 3, 97 | difeq12d 4122 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∖ { 0 }) = ((Base‘𝑅) ∖
{(0g‘𝑅)})) |
99 | 98 | oveq2d 7440 |
. . . . 5
⊢ (𝜑 → ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) = ((mulGrp‘𝑅) ↾s
((Base‘𝑅) ∖
{(0g‘𝑅)}))) |
100 | 99 | eleq1d 2811 |
. . . 4
⊢ (𝜑 → (((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) ∈ Grp ↔
((mulGrp‘𝑅)
↾s ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∈
Grp)) |
101 | 100 | anbi2d 628 |
. . 3
⊢ (𝜑 → ((𝑅 ∈ Ring ∧ ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) ∈ Grp) ↔
(𝑅 ∈ Ring ∧
((mulGrp‘𝑅)
↾s ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∈
Grp))) |
102 | 1, 96, 101 | mpbi2and 710 |
. 2
⊢ (𝜑 → (𝑅 ∈ Ring ∧ ((mulGrp‘𝑅) ↾s
((Base‘𝑅) ∖
{(0g‘𝑅)}))
∈ Grp)) |
103 | | eqid 2726 |
. . 3
⊢
((mulGrp‘𝑅)
↾s ((Base‘𝑅) ∖ {(0g‘𝑅)})) = ((mulGrp‘𝑅) ↾s
((Base‘𝑅) ∖
{(0g‘𝑅)})) |
104 | 7, 81, 103 | isdrng2 20721 |
. 2
⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧
((mulGrp‘𝑅)
↾s ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∈
Grp)) |
105 | 102, 104 | sylibr 233 |
1
⊢ (𝜑 → 𝑅 ∈ DivRing) |