Proof of Theorem issgrpd
| Step | Hyp | Ref
| Expression |
| 1 | | issgrpd.c |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) |
| 2 | 1 | 3expib 1123 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)) |
| 3 | | issgrpd.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) |
| 4 | 3 | eleq2d 2827 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (Base‘𝐺))) |
| 5 | 3 | eleq2d 2827 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ (Base‘𝐺))) |
| 6 | 4, 5 | anbi12d 632 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)))) |
| 7 | | issgrpd.p |
. . . . . . . 8
⊢ (𝜑 → + =
(+g‘𝐺)) |
| 8 | 7 | oveqd 7448 |
. . . . . . 7
⊢ (𝜑 → (𝑥 + 𝑦) = (𝑥(+g‘𝐺)𝑦)) |
| 9 | 8, 3 | eleq12d 2835 |
. . . . . 6
⊢ (𝜑 → ((𝑥 + 𝑦) ∈ 𝐵 ↔ (𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺))) |
| 10 | 2, 6, 9 | 3imtr3d 293 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺))) |
| 11 | 10 | imp 406 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → (𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
| 12 | | df-3an 1089 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵)) |
| 13 | | issgrpd.a |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
| 14 | 12, 13 | sylan2br 595 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
| 15 | 14 | ex 412 |
. . . . . . 7
⊢ (𝜑 → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))) |
| 16 | 3 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝜑 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ (Base‘𝐺))) |
| 17 | 6, 16 | anbi12d 632 |
. . . . . . 7
⊢ (𝜑 → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ↔ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑧 ∈ (Base‘𝐺)))) |
| 18 | | eqidd 2738 |
. . . . . . . . 9
⊢ (𝜑 → 𝑧 = 𝑧) |
| 19 | 7, 8, 18 | oveq123d 7452 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 + 𝑦) + 𝑧) = ((𝑥(+g‘𝐺)𝑦)(+g‘𝐺)𝑧)) |
| 20 | | eqidd 2738 |
. . . . . . . . 9
⊢ (𝜑 → 𝑥 = 𝑥) |
| 21 | 7 | oveqd 7448 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 + 𝑧) = (𝑦(+g‘𝐺)𝑧)) |
| 22 | 7, 20, 21 | oveq123d 7452 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 + (𝑦 + 𝑧)) = (𝑥(+g‘𝐺)(𝑦(+g‘𝐺)𝑧))) |
| 23 | 19, 22 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝜑 → (((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ↔ ((𝑥(+g‘𝐺)𝑦)(+g‘𝐺)𝑧) = (𝑥(+g‘𝐺)(𝑦(+g‘𝐺)𝑧)))) |
| 24 | 15, 17, 23 | 3imtr3d 293 |
. . . . . 6
⊢ (𝜑 → (((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ 𝑧 ∈ (Base‘𝐺)) → ((𝑥(+g‘𝐺)𝑦)(+g‘𝐺)𝑧) = (𝑥(+g‘𝐺)(𝑦(+g‘𝐺)𝑧)))) |
| 25 | 24 | impl 455 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) ∧ 𝑧 ∈ (Base‘𝐺)) → ((𝑥(+g‘𝐺)𝑦)(+g‘𝐺)𝑧) = (𝑥(+g‘𝐺)(𝑦(+g‘𝐺)𝑧))) |
| 26 | 25 | ralrimiva 3146 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → ∀𝑧 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦)(+g‘𝐺)𝑧) = (𝑥(+g‘𝐺)(𝑦(+g‘𝐺)𝑧))) |
| 27 | 11, 26 | jca 511 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺))) → ((𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺) ∧ ∀𝑧 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦)(+g‘𝐺)𝑧) = (𝑥(+g‘𝐺)(𝑦(+g‘𝐺)𝑧)))) |
| 28 | 27 | ralrimivva 3202 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺) ∧ ∀𝑧 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦)(+g‘𝐺)𝑧) = (𝑥(+g‘𝐺)(𝑦(+g‘𝐺)𝑧)))) |
| 29 | | issgrpd.v |
. . 3
⊢ (𝜑 → 𝐺 ∈ 𝑉) |
| 30 | | eqid 2737 |
. . . 4
⊢
(Base‘𝐺) =
(Base‘𝐺) |
| 31 | | eqid 2737 |
. . . 4
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 32 | 30, 31 | issgrpv 18734 |
. . 3
⊢ (𝐺 ∈ 𝑉 → (𝐺 ∈ Smgrp ↔ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺) ∧ ∀𝑧 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦)(+g‘𝐺)𝑧) = (𝑥(+g‘𝐺)(𝑦(+g‘𝐺)𝑧))))) |
| 33 | 29, 32 | syl 17 |
. 2
⊢ (𝜑 → (𝐺 ∈ Smgrp ↔ ∀𝑥 ∈ (Base‘𝐺)∀𝑦 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺) ∧ ∀𝑧 ∈ (Base‘𝐺)((𝑥(+g‘𝐺)𝑦)(+g‘𝐺)𝑧) = (𝑥(+g‘𝐺)(𝑦(+g‘𝐺)𝑧))))) |
| 34 | 28, 33 | mpbird 257 |
1
⊢ (𝜑 → 𝐺 ∈ Smgrp) |