| Step | Hyp | Ref
| Expression |
| 1 | | imasgrp.u |
. 2
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) |
| 2 | | imasgrp.v |
. 2
⊢ (𝜑 → 𝑉 = (Base‘𝑅)) |
| 3 | | imasgrp.p |
. 2
⊢ (𝜑 → + =
(+g‘𝑅)) |
| 4 | | imasgrp.f |
. 2
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) |
| 5 | | imasgrp.e |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) |
| 6 | | imasgrp.r |
. 2
⊢ (𝜑 → 𝑅 ∈ Grp) |
| 7 | 6 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → 𝑅 ∈ Grp) |
| 8 | | simp2 1138 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → 𝑥 ∈ 𝑉) |
| 9 | 2 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → 𝑉 = (Base‘𝑅)) |
| 10 | 8, 9 | eleqtrd 2843 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → 𝑥 ∈ (Base‘𝑅)) |
| 11 | | simp3 1139 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → 𝑦 ∈ 𝑉) |
| 12 | 11, 9 | eleqtrd 2843 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → 𝑦 ∈ (Base‘𝑅)) |
| 13 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 14 | | eqid 2737 |
. . . . 5
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 15 | 13, 14 | grpcl 18959 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(+g‘𝑅)𝑦) ∈ (Base‘𝑅)) |
| 16 | 7, 10, 12, 15 | syl3anc 1373 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥(+g‘𝑅)𝑦) ∈ (Base‘𝑅)) |
| 17 | 3 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → + =
(+g‘𝑅)) |
| 18 | 17 | oveqd 7448 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 + 𝑦) = (𝑥(+g‘𝑅)𝑦)) |
| 19 | 16, 18, 9 | 3eltr4d 2856 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 + 𝑦) ∈ 𝑉) |
| 20 | 6 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑅 ∈ Grp) |
| 21 | 10 | 3adant3r3 1185 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑥 ∈ (Base‘𝑅)) |
| 22 | 12 | 3adant3r3 1185 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑦 ∈ (Base‘𝑅)) |
| 23 | | simpr3 1197 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑧 ∈ 𝑉) |
| 24 | 2 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑉 = (Base‘𝑅)) |
| 25 | 23, 24 | eleqtrd 2843 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑧 ∈ (Base‘𝑅)) |
| 26 | 13, 14 | grpass 18960 |
. . . . 5
⊢ ((𝑅 ∈ Grp ∧ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅) ∧ 𝑧 ∈ (Base‘𝑅))) → ((𝑥(+g‘𝑅)𝑦)(+g‘𝑅)𝑧) = (𝑥(+g‘𝑅)(𝑦(+g‘𝑅)𝑧))) |
| 27 | 20, 21, 22, 25, 26 | syl13anc 1374 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑥(+g‘𝑅)𝑦)(+g‘𝑅)𝑧) = (𝑥(+g‘𝑅)(𝑦(+g‘𝑅)𝑧))) |
| 28 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → + =
(+g‘𝑅)) |
| 29 | 18 | 3adant3r3 1185 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 + 𝑦) = (𝑥(+g‘𝑅)𝑦)) |
| 30 | | eqidd 2738 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑧 = 𝑧) |
| 31 | 28, 29, 30 | oveq123d 7452 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 + 𝑦) + 𝑧) = ((𝑥(+g‘𝑅)𝑦)(+g‘𝑅)𝑧)) |
| 32 | | eqidd 2738 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑥 = 𝑥) |
| 33 | 28 | oveqd 7448 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦 + 𝑧) = (𝑦(+g‘𝑅)𝑧)) |
| 34 | 28, 32, 33 | oveq123d 7452 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 + (𝑦 + 𝑧)) = (𝑥(+g‘𝑅)(𝑦(+g‘𝑅)𝑧))) |
| 35 | 27, 31, 34 | 3eqtr4d 2787 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
| 36 | 35 | fveq2d 6910 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦) + 𝑧)) = (𝐹‘(𝑥 + (𝑦 + 𝑧)))) |
| 37 | | imasgrp.z |
. . . . 5
⊢ 0 =
(0g‘𝑅) |
| 38 | 13, 37 | grpidcl 18983 |
. . . 4
⊢ (𝑅 ∈ Grp → 0 ∈
(Base‘𝑅)) |
| 39 | 6, 38 | syl 17 |
. . 3
⊢ (𝜑 → 0 ∈ (Base‘𝑅)) |
| 40 | 39, 2 | eleqtrrd 2844 |
. 2
⊢ (𝜑 → 0 ∈ 𝑉) |
| 41 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → + =
(+g‘𝑅)) |
| 42 | 41 | oveqd 7448 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ( 0 + 𝑥) = ( 0 (+g‘𝑅)𝑥)) |
| 43 | 2 | eleq2d 2827 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝑉 ↔ 𝑥 ∈ (Base‘𝑅))) |
| 44 | 43 | biimpa 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ (Base‘𝑅)) |
| 45 | 13, 14, 37 | grplid 18985 |
. . . . 5
⊢ ((𝑅 ∈ Grp ∧ 𝑥 ∈ (Base‘𝑅)) → ( 0 (+g‘𝑅)𝑥) = 𝑥) |
| 46 | 6, 44, 45 | syl2an2r 685 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ( 0 (+g‘𝑅)𝑥) = 𝑥) |
| 47 | 42, 46 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ( 0 + 𝑥) = 𝑥) |
| 48 | 47 | fveq2d 6910 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘( 0 + 𝑥)) = (𝐹‘𝑥)) |
| 49 | | eqid 2737 |
. . . . 5
⊢
(invg‘𝑅) = (invg‘𝑅) |
| 50 | 13, 49 | grpinvcl 19005 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ 𝑥 ∈ (Base‘𝑅)) →
((invg‘𝑅)‘𝑥) ∈ (Base‘𝑅)) |
| 51 | 6, 44, 50 | syl2an2r 685 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((invg‘𝑅)‘𝑥) ∈ (Base‘𝑅)) |
| 52 | 2 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑉 = (Base‘𝑅)) |
| 53 | 51, 52 | eleqtrrd 2844 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((invg‘𝑅)‘𝑥) ∈ 𝑉) |
| 54 | 41 | oveqd 7448 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (((invg‘𝑅)‘𝑥) + 𝑥) = (((invg‘𝑅)‘𝑥)(+g‘𝑅)𝑥)) |
| 55 | 13, 14, 37, 49 | grplinv 19007 |
. . . . 5
⊢ ((𝑅 ∈ Grp ∧ 𝑥 ∈ (Base‘𝑅)) →
(((invg‘𝑅)‘𝑥)(+g‘𝑅)𝑥) = 0 ) |
| 56 | 6, 44, 55 | syl2an2r 685 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (((invg‘𝑅)‘𝑥)(+g‘𝑅)𝑥) = 0 ) |
| 57 | 54, 56 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (((invg‘𝑅)‘𝑥) + 𝑥) = 0 ) |
| 58 | 57 | fveq2d 6910 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘(((invg‘𝑅)‘𝑥) + 𝑥)) = (𝐹‘ 0 )) |
| 59 | 1, 2, 3, 4, 5, 6, 19, 36, 40, 48, 53, 58 | imasgrp2 19073 |
1
⊢ (𝜑 → (𝑈 ∈ Grp ∧ (𝐹‘ 0 ) =
(0g‘𝑈))) |