| Step | Hyp | Ref
| Expression |
| 1 | | isdrng2.b |
. . 3
⊢ 𝐵 = (Base‘𝑅) |
| 2 | | eqid 2737 |
. . 3
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
| 3 | | isdrng2.z |
. . 3
⊢ 0 =
(0g‘𝑅) |
| 4 | 1, 2, 3 | isdrng 20733 |
. 2
⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧
(Unit‘𝑅) = (𝐵 ∖ { 0 }))) |
| 5 | | oveq2 7439 |
. . . . . . 7
⊢
((Unit‘𝑅) =
(𝐵 ∖ { 0 }) →
((mulGrp‘𝑅)
↾s (Unit‘𝑅)) = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 }))) |
| 6 | 5 | adantl 481 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧
(Unit‘𝑅) = (𝐵 ∖ { 0 })) →
((mulGrp‘𝑅)
↾s (Unit‘𝑅)) = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 }))) |
| 7 | | isdrng2.g |
. . . . . 6
⊢ 𝐺 = ((mulGrp‘𝑅) ↾s (𝐵 ∖ { 0 })) |
| 8 | 6, 7 | eqtr4di 2795 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧
(Unit‘𝑅) = (𝐵 ∖ { 0 })) →
((mulGrp‘𝑅)
↾s (Unit‘𝑅)) = 𝐺) |
| 9 | | eqid 2737 |
. . . . . . 7
⊢
((mulGrp‘𝑅)
↾s (Unit‘𝑅)) = ((mulGrp‘𝑅) ↾s (Unit‘𝑅)) |
| 10 | 2, 9 | unitgrp 20383 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
((mulGrp‘𝑅)
↾s (Unit‘𝑅)) ∈ Grp) |
| 11 | 10 | adantr 480 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧
(Unit‘𝑅) = (𝐵 ∖ { 0 })) →
((mulGrp‘𝑅)
↾s (Unit‘𝑅)) ∈ Grp) |
| 12 | 8, 11 | eqeltrrd 2842 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧
(Unit‘𝑅) = (𝐵 ∖ { 0 })) → 𝐺 ∈ Grp) |
| 13 | 1, 2 | unitcl 20375 |
. . . . . . . . 9
⊢ (𝑥 ∈ (Unit‘𝑅) → 𝑥 ∈ 𝐵) |
| 14 | 13 | adantl 481 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) → 𝑥 ∈ 𝐵) |
| 15 | | difss 4136 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∖ { 0 }) ⊆ 𝐵 |
| 16 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
| 17 | 16, 1 | mgpbas 20142 |
. . . . . . . . . . . . . . . 16
⊢ 𝐵 =
(Base‘(mulGrp‘𝑅)) |
| 18 | 7, 17 | ressbas2 17283 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∖ { 0 }) ⊆ 𝐵 → (𝐵 ∖ { 0 }) = (Base‘𝐺)) |
| 19 | 15, 18 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∖ { 0 }) = (Base‘𝐺) |
| 20 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 21 | 19, 20 | grpidcl 18983 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ (𝐵 ∖ { 0
})) |
| 22 | 21 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) →
(0g‘𝐺)
∈ (𝐵 ∖ { 0
})) |
| 23 | | eldifsn 4786 |
. . . . . . . . . . . 12
⊢
((0g‘𝐺) ∈ (𝐵 ∖ { 0 }) ↔
((0g‘𝐺)
∈ 𝐵 ∧
(0g‘𝐺)
≠ 0
)) |
| 24 | 22, 23 | sylib 218 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) →
((0g‘𝐺)
∈ 𝐵 ∧
(0g‘𝐺)
≠ 0
)) |
| 25 | 24 | simprd 495 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) →
(0g‘𝐺)
≠ 0
) |
| 26 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) → 𝑅 ∈ Ring) |
| 27 | 22 | eldifad 3963 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) →
(0g‘𝐺)
∈ 𝐵) |
| 28 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) → 𝑥 ∈ (Unit‘𝑅)) |
| 29 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(/r‘𝑅) = (/r‘𝑅) |
| 30 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 31 | 1, 2, 29, 30 | dvrcan1 20409 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧
(0g‘𝐺)
∈ 𝐵 ∧ 𝑥 ∈ (Unit‘𝑅)) →
(((0g‘𝐺)(/r‘𝑅)𝑥)(.r‘𝑅)𝑥) = (0g‘𝐺)) |
| 32 | 26, 27, 28, 31 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) →
(((0g‘𝐺)(/r‘𝑅)𝑥)(.r‘𝑅)𝑥) = (0g‘𝐺)) |
| 33 | 1, 2, 29 | dvrcl 20404 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧
(0g‘𝐺)
∈ 𝐵 ∧ 𝑥 ∈ (Unit‘𝑅)) →
((0g‘𝐺)(/r‘𝑅)𝑥) ∈ 𝐵) |
| 34 | 26, 27, 28, 33 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) →
((0g‘𝐺)(/r‘𝑅)𝑥) ∈ 𝐵) |
| 35 | 1, 30, 3 | ringrz 20291 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧
((0g‘𝐺)(/r‘𝑅)𝑥) ∈ 𝐵) → (((0g‘𝐺)(/r‘𝑅)𝑥)(.r‘𝑅) 0 ) = 0 ) |
| 36 | 26, 34, 35 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) →
(((0g‘𝐺)(/r‘𝑅)𝑥)(.r‘𝑅) 0 ) = 0 ) |
| 37 | 25, 32, 36 | 3netr4d 3018 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) →
(((0g‘𝐺)(/r‘𝑅)𝑥)(.r‘𝑅)𝑥) ≠ (((0g‘𝐺)(/r‘𝑅)𝑥)(.r‘𝑅) 0 )) |
| 38 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑥 = 0 →
(((0g‘𝐺)(/r‘𝑅)𝑥)(.r‘𝑅)𝑥) = (((0g‘𝐺)(/r‘𝑅)𝑥)(.r‘𝑅) 0 )) |
| 39 | 38 | necon3i 2973 |
. . . . . . . . 9
⊢
((((0g‘𝐺)(/r‘𝑅)𝑥)(.r‘𝑅)𝑥) ≠ (((0g‘𝐺)(/r‘𝑅)𝑥)(.r‘𝑅) 0 ) → 𝑥 ≠ 0 ) |
| 40 | 37, 39 | syl 17 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) → 𝑥 ≠ 0 ) |
| 41 | | eldifsn 4786 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐵 ∖ { 0 }) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) |
| 42 | 14, 40, 41 | sylanbrc 583 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (Unit‘𝑅)) → 𝑥 ∈ (𝐵 ∖ { 0 })) |
| 43 | 42 | ex 412 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) → (𝑥 ∈ (Unit‘𝑅) → 𝑥 ∈ (𝐵 ∖ { 0 }))) |
| 44 | 43 | ssrdv 3989 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) →
(Unit‘𝑅) ⊆
(𝐵 ∖ { 0
})) |
| 45 | | eldifi 4131 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐵 ∖ { 0 }) → 𝑥 ∈ 𝐵) |
| 46 | 45 | adantl 481 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → 𝑥 ∈ 𝐵) |
| 47 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(invg‘𝐺) = (invg‘𝐺) |
| 48 | 19, 47 | grpinvcl 19005 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) →
((invg‘𝐺)‘𝑥) ∈ (𝐵 ∖ { 0 })) |
| 49 | 48 | adantll 714 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) →
((invg‘𝐺)‘𝑥) ∈ (𝐵 ∖ { 0 })) |
| 50 | 49 | eldifad 3963 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) →
((invg‘𝐺)‘𝑥) ∈ 𝐵) |
| 51 | | eqid 2737 |
. . . . . . . . 9
⊢
(∥r‘𝑅) = (∥r‘𝑅) |
| 52 | 1, 51, 30 | dvdsrmul 20364 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐵 ∧ ((invg‘𝐺)‘𝑥) ∈ 𝐵) → 𝑥(∥r‘𝑅)(((invg‘𝐺)‘𝑥)(.r‘𝑅)𝑥)) |
| 53 | 46, 50, 52 | syl2anc 584 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → 𝑥(∥r‘𝑅)(((invg‘𝐺)‘𝑥)(.r‘𝑅)𝑥)) |
| 54 | 1 | fvexi 6920 |
. . . . . . . . . . 11
⊢ 𝐵 ∈ V |
| 55 | | difexg 5329 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ V → (𝐵 ∖ { 0 }) ∈
V) |
| 56 | 16, 30 | mgpplusg 20141 |
. . . . . . . . . . . 12
⊢
(.r‘𝑅) = (+g‘(mulGrp‘𝑅)) |
| 57 | 7, 56 | ressplusg 17334 |
. . . . . . . . . . 11
⊢ ((𝐵 ∖ { 0 }) ∈ V →
(.r‘𝑅) =
(+g‘𝐺)) |
| 58 | 54, 55, 57 | mp2b 10 |
. . . . . . . . . 10
⊢
(.r‘𝑅) = (+g‘𝐺) |
| 59 | 19, 58, 20, 47 | grplinv 19007 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) →
(((invg‘𝐺)‘𝑥)(.r‘𝑅)𝑥) = (0g‘𝐺)) |
| 60 | 59 | adantll 714 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) →
(((invg‘𝐺)‘𝑥)(.r‘𝑅)𝑥) = (0g‘𝐺)) |
| 61 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(1r‘𝑅) = (1r‘𝑅) |
| 62 | 1, 61 | ringidcl 20262 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝐵) |
| 63 | 1, 30, 61 | ringlidm 20266 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧
(1r‘𝑅)
∈ 𝐵) →
((1r‘𝑅)(.r‘𝑅)(1r‘𝑅)) = (1r‘𝑅)) |
| 64 | 62, 63 | mpdan 687 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring →
((1r‘𝑅)(.r‘𝑅)(1r‘𝑅)) = (1r‘𝑅)) |
| 65 | 64 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) →
((1r‘𝑅)(.r‘𝑅)(1r‘𝑅)) = (1r‘𝑅)) |
| 66 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) → 𝐺 ∈ Grp) |
| 67 | 2, 61 | 1unit 20374 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Unit‘𝑅)) |
| 68 | 67 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) →
(1r‘𝑅)
∈ (Unit‘𝑅)) |
| 69 | 44, 68 | sseldd 3984 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) →
(1r‘𝑅)
∈ (𝐵 ∖ { 0
})) |
| 70 | 19, 58, 20 | grpid 18993 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧
(1r‘𝑅)
∈ (𝐵 ∖ { 0 })) →
(((1r‘𝑅)(.r‘𝑅)(1r‘𝑅)) = (1r‘𝑅) ↔ (0g‘𝐺) = (1r‘𝑅))) |
| 71 | 66, 69, 70 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) →
(((1r‘𝑅)(.r‘𝑅)(1r‘𝑅)) = (1r‘𝑅) ↔ (0g‘𝐺) = (1r‘𝑅))) |
| 72 | 65, 71 | mpbid 232 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) →
(0g‘𝐺) =
(1r‘𝑅)) |
| 73 | 72 | adantr 480 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) →
(0g‘𝐺) =
(1r‘𝑅)) |
| 74 | 60, 73 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) →
(((invg‘𝐺)‘𝑥)(.r‘𝑅)𝑥) = (1r‘𝑅)) |
| 75 | 53, 74 | breqtrd 5169 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → 𝑥(∥r‘𝑅)(1r‘𝑅)) |
| 76 | | eqid 2737 |
. . . . . . . . . 10
⊢
(oppr‘𝑅) = (oppr‘𝑅) |
| 77 | 76, 1 | opprbas 20341 |
. . . . . . . . 9
⊢ 𝐵 =
(Base‘(oppr‘𝑅)) |
| 78 | | eqid 2737 |
. . . . . . . . 9
⊢
(∥r‘(oppr‘𝑅)) =
(∥r‘(oppr‘𝑅)) |
| 79 | | eqid 2737 |
. . . . . . . . 9
⊢
(.r‘(oppr‘𝑅)) =
(.r‘(oppr‘𝑅)) |
| 80 | 77, 78, 79 | dvdsrmul 20364 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐵 ∧ ((invg‘𝐺)‘𝑥) ∈ 𝐵) → 𝑥(∥r‘(oppr‘𝑅))(((invg‘𝐺)‘𝑥)(.r‘(oppr‘𝑅))𝑥)) |
| 81 | 46, 50, 80 | syl2anc 584 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → 𝑥(∥r‘(oppr‘𝑅))(((invg‘𝐺)‘𝑥)(.r‘(oppr‘𝑅))𝑥)) |
| 82 | 1, 30, 76, 79 | opprmul 20337 |
. . . . . . . 8
⊢
(((invg‘𝐺)‘𝑥)(.r‘(oppr‘𝑅))𝑥) = (𝑥(.r‘𝑅)((invg‘𝐺)‘𝑥)) |
| 83 | 19, 58, 20, 47 | grprinv 19008 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → (𝑥(.r‘𝑅)((invg‘𝐺)‘𝑥)) = (0g‘𝐺)) |
| 84 | 83 | adantll 714 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → (𝑥(.r‘𝑅)((invg‘𝐺)‘𝑥)) = (0g‘𝐺)) |
| 85 | 84, 73 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → (𝑥(.r‘𝑅)((invg‘𝐺)‘𝑥)) = (1r‘𝑅)) |
| 86 | 82, 85 | eqtrid 2789 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) →
(((invg‘𝐺)‘𝑥)(.r‘(oppr‘𝑅))𝑥) = (1r‘𝑅)) |
| 87 | 81, 86 | breqtrd 5169 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → 𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅)) |
| 88 | 2, 61, 51, 76, 78 | isunit 20373 |
. . . . . 6
⊢ (𝑥 ∈ (Unit‘𝑅) ↔ (𝑥(∥r‘𝑅)(1r‘𝑅) ∧ 𝑥(∥r‘(oppr‘𝑅))(1r‘𝑅))) |
| 89 | 75, 87, 88 | sylanbrc 583 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) ∧ 𝑥 ∈ (𝐵 ∖ { 0 })) → 𝑥 ∈ (Unit‘𝑅)) |
| 90 | 44, 89 | eqelssd 4005 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ Grp) →
(Unit‘𝑅) = (𝐵 ∖ { 0 })) |
| 91 | 12, 90 | impbida 801 |
. . 3
⊢ (𝑅 ∈ Ring →
((Unit‘𝑅) = (𝐵 ∖ { 0 }) ↔ 𝐺 ∈ Grp)) |
| 92 | 91 | pm5.32i 574 |
. 2
⊢ ((𝑅 ∈ Ring ∧
(Unit‘𝑅) = (𝐵 ∖ { 0 })) ↔ (𝑅 ∈ Ring ∧ 𝐺 ∈ Grp)) |
| 93 | 4, 92 | bitri 275 |
1
⊢ (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ 𝐺 ∈ Grp)) |