| Step | Hyp | Ref
| Expression |
| 1 | | isdrngd.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 2 | | difss 4136 |
. . . . . 6
⊢ (𝐵 ∖ { 0 }) ⊆ 𝐵 |
| 3 | | isdrngd.b |
. . . . . 6
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) |
| 4 | 2, 3 | sseqtrid 4026 |
. . . . 5
⊢ (𝜑 → (𝐵 ∖ { 0 }) ⊆
(Base‘𝑅)) |
| 5 | | eqid 2737 |
. . . . . 6
⊢
((mulGrp‘𝑅)
↾s (𝐵
∖ { 0 })) = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) |
| 6 | | eqid 2737 |
. . . . . . 7
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
| 7 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 8 | 6, 7 | mgpbas 20142 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
| 9 | 5, 8 | ressbas2 17283 |
. . . . 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 6919 |
. . . . . . 7
⊢
(Base‘𝑅)
∈ V |
| 13 | 3, 12 | eqeltrdi 2849 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ V) |
| 14 | | difexg 5329 |
. . . . . 6
⊢ (𝐵 ∈ V → (𝐵 ∖ { 0 }) ∈
V) |
| 15 | | eqid 2737 |
. . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 16 | 6, 15 | mgpplusg 20141 |
. . . . . . 7
⊢
(.r‘𝑅) = (+g‘(mulGrp‘𝑅)) |
| 17 | 5, 16 | ressplusg 17334 |
. . . . . 6
⊢ ((𝐵 ∖ { 0 }) ∈ V →
(.r‘𝑅) =
(+g‘((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })))) |
| 18 | 13, 14, 17 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (.r‘𝑅) =
(+g‘((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })))) |
| 19 | 11, 18 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → · =
(+g‘((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })))) |
| 20 | | eldifsn 4786 |
. . . . 5
⊢ (𝑥 ∈ (𝐵 ∖ { 0 }) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) |
| 21 | | eldifsn 4786 |
. . . . . 6
⊢ (𝑦 ∈ (𝐵 ∖ { 0 }) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) |
| 22 | 7, 15 | ringcl 20247 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)𝑦) ∈ (Base‘𝑅)) |
| 23 | 1, 22 | syl3an1 1164 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)𝑦) ∈ (Base‘𝑅)) |
| 24 | 23 | 3expib 1123 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)𝑦) ∈ (Base‘𝑅))) |
| 25 | 3 | eleq2d 2827 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (Base‘𝑅))) |
| 26 | 3 | eleq2d 2827 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ (Base‘𝑅))) |
| 27 | 25, 26 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)))) |
| 28 | 11 | oveqd 7448 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 · 𝑦) = (𝑥(.r‘𝑅)𝑦)) |
| 29 | 28, 3 | eleq12d 2835 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 · 𝑦) ∈ 𝐵 ↔ (𝑥(.r‘𝑅)𝑦) ∈ (Base‘𝑅))) |
| 30 | 24, 27, 29 | 3imtr4d 294 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵)) |
| 31 | 30 | 3impib 1117 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵) |
| 32 | 31 | 3adant2r 1180 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵) |
| 33 | 32 | 3adant3r 1182 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝑥 · 𝑦) ∈ 𝐵) |
| 34 | | isdrngd.n |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝑥 · 𝑦) ≠ 0 ) |
| 35 | | eldifsn 4786 |
. . . . . . 7
⊢ ((𝑥 · 𝑦) ∈ (𝐵 ∖ { 0 }) ↔ ((𝑥 · 𝑦) ∈ 𝐵 ∧ (𝑥 · 𝑦) ≠ 0 )) |
| 36 | 33, 34, 35 | sylanbrc 583 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝑥 · 𝑦) ∈ (𝐵 ∖ { 0 })) |
| 37 | 21, 36 | syl3an3b 1407 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → (𝑥 · 𝑦) ∈ (𝐵 ∖ { 0 })) |
| 38 | 20, 37 | syl3an2b 1406 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → (𝑥 · 𝑦) ∈ (𝐵 ∖ { 0 })) |
| 39 | 7, 15 | ringass 20250 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) → ((𝑥(.r‘𝑅)𝑦)(.r‘𝑅)𝑧) = (𝑥(.r‘𝑅)(𝑦(.r‘𝑅)𝑧))) |
| 40 | 39 | ex 412 |
. . . . . . 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 2827 |
. . . . . . 7
⊢ (𝜑 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ (Base‘𝑅))) |
| 43 | 25, 26, 42 | 3anbi123d 1438 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ↔ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅)))) |
| 44 | | eqidd 2738 |
. . . . . . . 8
⊢ (𝜑 → 𝑧 = 𝑧) |
| 45 | 11, 28, 44 | oveq123d 7452 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 · 𝑦) · 𝑧) = ((𝑥(.r‘𝑅)𝑦)(.r‘𝑅)𝑧)) |
| 46 | | eqidd 2738 |
. . . . . . . 8
⊢ (𝜑 → 𝑥 = 𝑥) |
| 47 | 11 | oveqd 7448 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 · 𝑧) = (𝑦(.r‘𝑅)𝑧)) |
| 48 | 11, 46, 47 | oveq123d 7452 |
. . . . . . 7
⊢ (𝜑 → (𝑥 · (𝑦 · 𝑧)) = (𝑥(.r‘𝑅)(𝑦(.r‘𝑅)𝑧))) |
| 49 | 45, 48 | eqeq12d 2753 |
. . . . . 6
⊢ (𝜑 → (((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)) ↔ ((𝑥(.r‘𝑅)𝑦)(.r‘𝑅)𝑧) = (𝑥(.r‘𝑅)(𝑦(.r‘𝑅)𝑧)))) |
| 50 | 41, 43, 49 | 3imtr4d 294 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧)))) |
| 51 | | eldifi 4131 |
. . . . . 6
⊢ (𝑥 ∈ (𝐵 ∖ { 0 }) → 𝑥 ∈ 𝐵) |
| 52 | | eldifi 4131 |
. . . . . 6
⊢ (𝑦 ∈ (𝐵 ∖ { 0 }) → 𝑦 ∈ 𝐵) |
| 53 | | eldifi 4131 |
. . . . . 6
⊢ (𝑧 ∈ (𝐵 ∖ { 0 }) → 𝑧 ∈ 𝐵) |
| 54 | 51, 52, 53 | 3anim123i 1152 |
. . . . 5
⊢ ((𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 }) ∧ 𝑧 ∈ (𝐵 ∖ { 0 })) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) |
| 55 | 50, 54 | impel 505 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 }) ∧ 𝑧 ∈ (𝐵 ∖ { 0 }))) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) |
| 56 | | eqid 2737 |
. . . . . . . 8
⊢
(1r‘𝑅) = (1r‘𝑅) |
| 57 | 7, 56 | ringidcl 20262 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) |
| 58 | 1, 57 | syl 17 |
. . . . . 6
⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅)) |
| 59 | | isdrngd.u |
. . . . . 6
⊢ (𝜑 → 1 =
(1r‘𝑅)) |
| 60 | 58, 59, 3 | 3eltr4d 2856 |
. . . . 5
⊢ (𝜑 → 1 ∈ 𝐵) |
| 61 | | isdrngd.o |
. . . . 5
⊢ (𝜑 → 1 ≠ 0 ) |
| 62 | | eldifsn 4786 |
. . . . 5
⊢ ( 1 ∈ (𝐵 ∖ { 0 }) ↔ ( 1 ∈ 𝐵 ∧ 1 ≠ 0 )) |
| 63 | 60, 61, 62 | sylanbrc 583 |
. . . 4
⊢ (𝜑 → 1 ∈ (𝐵 ∖ { 0 })) |
| 64 | 7, 15, 56 | ringlidm 20266 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑅)) →
((1r‘𝑅)(.r‘𝑅)𝑥) = 𝑥) |
| 65 | 64 | ex 412 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → (𝑥 ∈ (Base‘𝑅) →
((1r‘𝑅)(.r‘𝑅)𝑥) = 𝑥)) |
| 66 | 1, 65 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑅) → ((1r‘𝑅)(.r‘𝑅)𝑥) = 𝑥)) |
| 67 | 11, 59, 46 | oveq123d 7452 |
. . . . . . . . 9
⊢ (𝜑 → ( 1 · 𝑥) = ((1r‘𝑅)(.r‘𝑅)𝑥)) |
| 68 | 67 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝜑 → (( 1 · 𝑥) = 𝑥 ↔ ((1r‘𝑅)(.r‘𝑅)𝑥) = 𝑥)) |
| 69 | 66, 25, 68 | 3imtr4d 294 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐵 → ( 1 · 𝑥) = 𝑥)) |
| 70 | 69 | imp 406 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 1 · 𝑥) = 𝑥) |
| 71 | 70 | adantrr 717 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → ( 1 · 𝑥) = 𝑥) |
| 72 | 20, 71 | sylan2b 594 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → ( 1 · 𝑥) = 𝑥) |
| 73 | | isdrngd.i |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ∈ 𝐵) |
| 74 | 61 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 1 ≠ 0
) |
| 75 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) ∧ 𝐼 = 0 ) → 𝐼 = 0 ) |
| 76 | 75 | oveq1d 7446 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) ∧ 𝐼 = 0 ) → (𝐼 · 𝑥) = ( 0 · 𝑥)) |
| 77 | | isdrngd.k |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → (𝐼 · 𝑥) = 1 ) |
| 78 | 77 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) ∧ 𝐼 = 0 ) → (𝐼 · 𝑥) = 1 ) |
| 79 | 25 | biimpa 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ (Base‘𝑅)) |
| 80 | 79 | adantrr 717 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝑥 ∈ (Base‘𝑅)) |
| 81 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 82 | 7, 15, 81 | ringlz 20290 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑅)) →
((0g‘𝑅)(.r‘𝑅)𝑥) = (0g‘𝑅)) |
| 83 | 1, 80, 82 | syl2an2r 685 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) →
((0g‘𝑅)(.r‘𝑅)𝑥) = (0g‘𝑅)) |
| 84 | | isdrngd.z |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 =
(0g‘𝑅)) |
| 85 | 11, 84, 46 | oveq123d 7452 |
. . . . . . . . . . 11
⊢ (𝜑 → ( 0 · 𝑥) = ((0g‘𝑅)(.r‘𝑅)𝑥)) |
| 86 | 85 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → ( 0 · 𝑥) = ((0g‘𝑅)(.r‘𝑅)𝑥)) |
| 87 | 84 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 0 =
(0g‘𝑅)) |
| 88 | 83, 86, 87 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → ( 0 · 𝑥) = 0 ) |
| 89 | 88 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) ∧ 𝐼 = 0 ) → ( 0 · 𝑥) = 0 ) |
| 90 | 76, 78, 89 | 3eqtr3d 2785 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) ∧ 𝐼 = 0 ) → 1 = 0
) |
| 91 | 74, 90 | mteqand 3033 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ≠ 0 ) |
| 92 | | eldifsn 4786 |
. . . . . 6
⊢ (𝐼 ∈ (𝐵 ∖ { 0 }) ↔ (𝐼 ∈ 𝐵 ∧ 𝐼 ≠ 0 )) |
| 93 | 73, 91, 92 | sylanbrc 583 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) → 𝐼 ∈ (𝐵 ∖ { 0 })) |
| 94 | 20, 93 | sylan2b 594 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → 𝐼 ∈ (𝐵 ∖ { 0 })) |
| 95 | 20, 77 | sylan2b 594 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → (𝐼 · 𝑥) = 1 ) |
| 96 | 10, 19, 38, 55, 63, 72, 94, 95 | isgrpd 18976 |
. . 3
⊢ (𝜑 → ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) ∈
Grp) |
| 97 | 84 | sneqd 4638 |
. . . . . . 7
⊢ (𝜑 → { 0 } =
{(0g‘𝑅)}) |
| 98 | 3, 97 | difeq12d 4127 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∖ { 0 }) = ((Base‘𝑅) ∖
{(0g‘𝑅)})) |
| 99 | 98 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) = ((mulGrp‘𝑅) ↾s
((Base‘𝑅) ∖
{(0g‘𝑅)}))) |
| 100 | 99 | eleq1d 2826 |
. . . 4
⊢ (𝜑 → (((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) ∈ Grp ↔
((mulGrp‘𝑅)
↾s ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∈
Grp)) |
| 101 | 100 | anbi2d 630 |
. . 3
⊢ (𝜑 → ((𝑅 ∈ Ring ∧ ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) ∈ Grp) ↔
(𝑅 ∈ Ring ∧
((mulGrp‘𝑅)
↾s ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∈
Grp))) |
| 102 | 1, 96, 101 | mpbi2and 712 |
. 2
⊢ (𝜑 → (𝑅 ∈ Ring ∧ ((mulGrp‘𝑅) ↾s
((Base‘𝑅) ∖
{(0g‘𝑅)}))
∈ Grp)) |
| 103 | | eqid 2737 |
. . 3
⊢
((mulGrp‘𝑅)
↾s ((Base‘𝑅) ∖ {(0g‘𝑅)})) = ((mulGrp‘𝑅) ↾s
((Base‘𝑅) ∖
{(0g‘𝑅)})) |
| 104 | 7, 81, 103 | isdrng2 20743 |
. 2
⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧
((mulGrp‘𝑅)
↾s ((Base‘𝑅) ∖ {(0g‘𝑅)})) ∈
Grp)) |
| 105 | 102, 104 | sylibr 234 |
1
⊢ (𝜑 → 𝑅 ∈ DivRing) |