Proof of Theorem isringd
| Step | Hyp | Ref
| Expression |
| 1 | | isringd.g |
. 2
⊢ (𝜑 → 𝑅 ∈ Grp) |
| 2 | | isringd.b |
. . . 4
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) |
| 3 | | eqid 2737 |
. . . . 5
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
| 4 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 5 | 3, 4 | mgpbas 20142 |
. . . 4
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
| 6 | 2, 5 | eqtrdi 2793 |
. . 3
⊢ (𝜑 → 𝐵 = (Base‘(mulGrp‘𝑅))) |
| 7 | | isringd.t |
. . . 4
⊢ (𝜑 → · =
(.r‘𝑅)) |
| 8 | | eqid 2737 |
. . . . 5
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 9 | 3, 8 | mgpplusg 20141 |
. . . 4
⊢
(.r‘𝑅) = (+g‘(mulGrp‘𝑅)) |
| 10 | 7, 9 | eqtrdi 2793 |
. . 3
⊢ (𝜑 → · =
(+g‘(mulGrp‘𝑅))) |
| 11 | | isringd.c |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵) |
| 12 | | isringd.a |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) |
| 13 | | isringd.u |
. . 3
⊢ (𝜑 → 1 ∈ 𝐵) |
| 14 | | isringd.i |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 1 · 𝑥) = 𝑥) |
| 15 | | isringd.h |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 · 1 ) = 𝑥) |
| 16 | 6, 10, 11, 12, 13, 14, 15 | ismndd 18769 |
. 2
⊢ (𝜑 → (mulGrp‘𝑅) ∈ Mnd) |
| 17 | 2 | eleq2d 2827 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (Base‘𝑅))) |
| 18 | 2 | eleq2d 2827 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ (Base‘𝑅))) |
| 19 | 2 | eleq2d 2827 |
. . . . . 6
⊢ (𝜑 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ (Base‘𝑅))) |
| 20 | 17, 18, 19 | 3anbi123d 1438 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ↔ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅)))) |
| 21 | 20 | biimpar 477 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) |
| 22 | | isringd.d |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧))) |
| 23 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → · =
(.r‘𝑅)) |
| 24 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑥 = 𝑥) |
| 25 | | isringd.p |
. . . . . . . 8
⊢ (𝜑 → + =
(+g‘𝑅)) |
| 26 | 25 | oveqdr 7459 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦 + 𝑧) = (𝑦(+g‘𝑅)𝑧)) |
| 27 | 23, 24, 26 | oveq123d 7452 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑥 · (𝑦 + 𝑧)) = (𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧))) |
| 28 | 25 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → + =
(+g‘𝑅)) |
| 29 | 7 | oveqdr 7459 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑥 · 𝑦) = (𝑥(.r‘𝑅)𝑦)) |
| 30 | 7 | oveqdr 7459 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑥 · 𝑧) = (𝑥(.r‘𝑅)𝑧)) |
| 31 | 28, 29, 30 | oveq123d 7452 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 · 𝑦) + (𝑥 · 𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧))) |
| 32 | 22, 27, 31 | 3eqtr3d 2785 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧))) |
| 33 | | isringd.e |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) |
| 34 | 25 | oveqdr 7459 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑥 + 𝑦) = (𝑥(+g‘𝑅)𝑦)) |
| 35 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑧 = 𝑧) |
| 36 | 23, 34, 35 | oveq123d 7452 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧)) |
| 37 | 7 | oveqdr 7459 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦 · 𝑧) = (𝑦(.r‘𝑅)𝑧)) |
| 38 | 28, 30, 37 | oveq123d 7452 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 · 𝑧) + (𝑦 · 𝑧)) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧))) |
| 39 | 33, 36, 38 | 3eqtr3d 2785 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧))) |
| 40 | 32, 39 | jca 511 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧)))) |
| 41 | 21, 40 | syldan 591 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) → ((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧)))) |
| 42 | 41 | ralrimivvva 3205 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧)))) |
| 43 | | eqid 2737 |
. . 3
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 44 | 4, 3, 43, 8 | isring 20234 |
. 2
⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧
(mulGrp‘𝑅) ∈ Mnd
∧ ∀𝑥 ∈
(Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧))))) |
| 45 | 1, 16, 42, 44 | syl3anbrc 1344 |
1
⊢ (𝜑 → 𝑅 ∈ Ring) |