Step | Hyp | Ref
| Expression |
1 | | ghmgrp1 18751 |
. 2
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝐺 ∈ Grp) |
2 | | ghmgrp2 18752 |
. . 3
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝐻 ∈ Grp) |
3 | | grpn0 18526 |
. . 3
⊢ (𝐻 ∈ Grp → 𝐻 ≠ ∅) |
4 | | lactghmga.h |
. . . . 5
⊢ 𝐻 = (SymGrp‘𝑌) |
5 | | fvprc 6748 |
. . . . 5
⊢ (¬
𝑌 ∈ V →
(SymGrp‘𝑌) =
∅) |
6 | 4, 5 | eqtrid 2790 |
. . . 4
⊢ (¬
𝑌 ∈ V → 𝐻 = ∅) |
7 | 6 | necon1ai 2970 |
. . 3
⊢ (𝐻 ≠ ∅ → 𝑌 ∈ V) |
8 | 2, 3, 7 | 3syl 18 |
. 2
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝑌 ∈ V) |
9 | | lactghmga.x |
. . . . . . . . . . 11
⊢ 𝑋 = (Base‘𝐺) |
10 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(Base‘𝐻) =
(Base‘𝐻) |
11 | 9, 10 | ghmf 18753 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝐹:𝑋⟶(Base‘𝐻)) |
12 | 11 | ffvelrnda 6943 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ (Base‘𝐻)) |
13 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑋) → 𝑌 ∈ V) |
14 | 4, 10 | elsymgbas 18896 |
. . . . . . . . . 10
⊢ (𝑌 ∈ V → ((𝐹‘𝑥) ∈ (Base‘𝐻) ↔ (𝐹‘𝑥):𝑌–1-1-onto→𝑌)) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑋) → ((𝐹‘𝑥) ∈ (Base‘𝐻) ↔ (𝐹‘𝑥):𝑌–1-1-onto→𝑌)) |
16 | 12, 15 | mpbid 231 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥):𝑌–1-1-onto→𝑌) |
17 | | f1of 6700 |
. . . . . . . 8
⊢ ((𝐹‘𝑥):𝑌–1-1-onto→𝑌 → (𝐹‘𝑥):𝑌⟶𝑌) |
18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥):𝑌⟶𝑌) |
19 | 18 | ffvelrnda 6943 |
. . . . . 6
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → ((𝐹‘𝑥)‘𝑦) ∈ 𝑌) |
20 | 19 | ralrimiva 3107 |
. . . . 5
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 ((𝐹‘𝑥)‘𝑦) ∈ 𝑌) |
21 | 20 | ralrimiva 3107 |
. . . 4
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝐹‘𝑥)‘𝑦) ∈ 𝑌) |
22 | | lactghmga.f |
. . . . 5
⊢ ⊕ =
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝐹‘𝑥)‘𝑦)) |
23 | 22 | fmpo 7881 |
. . . 4
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 ((𝐹‘𝑥)‘𝑦) ∈ 𝑌 ↔ ⊕ :(𝑋 × 𝑌)⟶𝑌) |
24 | 21, 23 | sylib 217 |
. . 3
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → ⊕ :(𝑋 × 𝑌)⟶𝑌) |
25 | | eqid 2738 |
. . . . . . . . 9
⊢
(0g‘𝐺) = (0g‘𝐺) |
26 | 9, 25 | grpidcl 18522 |
. . . . . . . 8
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝑋) |
27 | 1, 26 | syl 17 |
. . . . . . 7
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → (0g‘𝐺) ∈ 𝑋) |
28 | | fveq2 6756 |
. . . . . . . . 9
⊢ (𝑥 = (0g‘𝐺) → (𝐹‘𝑥) = (𝐹‘(0g‘𝐺))) |
29 | 28 | fveq1d 6758 |
. . . . . . . 8
⊢ (𝑥 = (0g‘𝐺) → ((𝐹‘𝑥)‘𝑦) = ((𝐹‘(0g‘𝐺))‘𝑦)) |
30 | | fveq2 6756 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → ((𝐹‘(0g‘𝐺))‘𝑦) = ((𝐹‘(0g‘𝐺))‘𝑧)) |
31 | | fvex 6769 |
. . . . . . . 8
⊢ ((𝐹‘(0g‘𝐺))‘𝑧) ∈ V |
32 | 29, 30, 22, 31 | ovmpo 7411 |
. . . . . . 7
⊢
(((0g‘𝐺) ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) → ((0g‘𝐺) ⊕ 𝑧) = ((𝐹‘(0g‘𝐺))‘𝑧)) |
33 | 27, 32 | sylan 579 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → ((0g‘𝐺) ⊕ 𝑧) = ((𝐹‘(0g‘𝐺))‘𝑧)) |
34 | | eqid 2738 |
. . . . . . . . . 10
⊢
(0g‘𝐻) = (0g‘𝐻) |
35 | 25, 34 | ghmid 18755 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → (𝐹‘(0g‘𝐺)) = (0g‘𝐻)) |
36 | 35 | adantr 480 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → (𝐹‘(0g‘𝐺)) = (0g‘𝐻)) |
37 | 8 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → 𝑌 ∈ V) |
38 | 4 | symgid 18924 |
. . . . . . . . 9
⊢ (𝑌 ∈ V → ( I ↾
𝑌) =
(0g‘𝐻)) |
39 | 37, 38 | syl 17 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → ( I ↾ 𝑌) = (0g‘𝐻)) |
40 | 36, 39 | eqtr4d 2781 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → (𝐹‘(0g‘𝐺)) = ( I ↾ 𝑌)) |
41 | 40 | fveq1d 6758 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → ((𝐹‘(0g‘𝐺))‘𝑧) = (( I ↾ 𝑌)‘𝑧)) |
42 | | fvresi 7027 |
. . . . . . 7
⊢ (𝑧 ∈ 𝑌 → (( I ↾ 𝑌)‘𝑧) = 𝑧) |
43 | 42 | adantl 481 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → (( I ↾ 𝑌)‘𝑧) = 𝑧) |
44 | 33, 41, 43 | 3eqtrd 2782 |
. . . . 5
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → ((0g‘𝐺) ⊕ 𝑧) = 𝑧) |
45 | 11 | ad2antrr 722 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝐹:𝑋⟶(Base‘𝐻)) |
46 | | simprr 769 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝑣 ∈ 𝑋) |
47 | 45, 46 | ffvelrnd 6944 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝐹‘𝑣) ∈ (Base‘𝐻)) |
48 | 8 | ad2antrr 722 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝑌 ∈ V) |
49 | 4, 10 | elsymgbas 18896 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ V → ((𝐹‘𝑣) ∈ (Base‘𝐻) ↔ (𝐹‘𝑣):𝑌–1-1-onto→𝑌)) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝐹‘𝑣) ∈ (Base‘𝐻) ↔ (𝐹‘𝑣):𝑌–1-1-onto→𝑌)) |
51 | 47, 50 | mpbid 231 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝐹‘𝑣):𝑌–1-1-onto→𝑌) |
52 | | f1of 6700 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑣):𝑌–1-1-onto→𝑌 → (𝐹‘𝑣):𝑌⟶𝑌) |
53 | 51, 52 | syl 17 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝐹‘𝑣):𝑌⟶𝑌) |
54 | | simplr 765 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝑧 ∈ 𝑌) |
55 | | fvco3 6849 |
. . . . . . . . 9
⊢ (((𝐹‘𝑣):𝑌⟶𝑌 ∧ 𝑧 ∈ 𝑌) → (((𝐹‘𝑢) ∘ (𝐹‘𝑣))‘𝑧) = ((𝐹‘𝑢)‘((𝐹‘𝑣)‘𝑧))) |
56 | 53, 54, 55 | syl2anc 583 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (((𝐹‘𝑢) ∘ (𝐹‘𝑣))‘𝑧) = ((𝐹‘𝑢)‘((𝐹‘𝑣)‘𝑧))) |
57 | | simpll 763 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝐹 ∈ (𝐺 GrpHom 𝐻)) |
58 | | simprl 767 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝑢 ∈ 𝑋) |
59 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(+g‘𝐺) = (+g‘𝐺) |
60 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(+g‘𝐻) = (+g‘𝐻) |
61 | 9, 59, 60 | ghmlin 18754 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → (𝐹‘(𝑢(+g‘𝐺)𝑣)) = ((𝐹‘𝑢)(+g‘𝐻)(𝐹‘𝑣))) |
62 | 57, 58, 46, 61 | syl3anc 1369 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝐹‘(𝑢(+g‘𝐺)𝑣)) = ((𝐹‘𝑢)(+g‘𝐻)(𝐹‘𝑣))) |
63 | 45, 58 | ffvelrnd 6944 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝐹‘𝑢) ∈ (Base‘𝐻)) |
64 | 4, 10, 60 | symgov 18906 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑢) ∈ (Base‘𝐻) ∧ (𝐹‘𝑣) ∈ (Base‘𝐻)) → ((𝐹‘𝑢)(+g‘𝐻)(𝐹‘𝑣)) = ((𝐹‘𝑢) ∘ (𝐹‘𝑣))) |
65 | 63, 47, 64 | syl2anc 583 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝐹‘𝑢)(+g‘𝐻)(𝐹‘𝑣)) = ((𝐹‘𝑢) ∘ (𝐹‘𝑣))) |
66 | 62, 65 | eqtrd 2778 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝐹‘(𝑢(+g‘𝐺)𝑣)) = ((𝐹‘𝑢) ∘ (𝐹‘𝑣))) |
67 | 66 | fveq1d 6758 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝐹‘(𝑢(+g‘𝐺)𝑣))‘𝑧) = (((𝐹‘𝑢) ∘ (𝐹‘𝑣))‘𝑧)) |
68 | 53, 54 | ffvelrnd 6944 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝐹‘𝑣)‘𝑧) ∈ 𝑌) |
69 | | fveq2 6756 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑢 → (𝐹‘𝑥) = (𝐹‘𝑢)) |
70 | 69 | fveq1d 6758 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑢 → ((𝐹‘𝑥)‘𝑦) = ((𝐹‘𝑢)‘𝑦)) |
71 | | fveq2 6756 |
. . . . . . . . . 10
⊢ (𝑦 = ((𝐹‘𝑣)‘𝑧) → ((𝐹‘𝑢)‘𝑦) = ((𝐹‘𝑢)‘((𝐹‘𝑣)‘𝑧))) |
72 | | fvex 6769 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑢)‘((𝐹‘𝑣)‘𝑧)) ∈ V |
73 | 70, 71, 22, 72 | ovmpo 7411 |
. . . . . . . . 9
⊢ ((𝑢 ∈ 𝑋 ∧ ((𝐹‘𝑣)‘𝑧) ∈ 𝑌) → (𝑢 ⊕ ((𝐹‘𝑣)‘𝑧)) = ((𝐹‘𝑢)‘((𝐹‘𝑣)‘𝑧))) |
74 | 58, 68, 73 | syl2anc 583 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑢 ⊕ ((𝐹‘𝑣)‘𝑧)) = ((𝐹‘𝑢)‘((𝐹‘𝑣)‘𝑧))) |
75 | 56, 67, 74 | 3eqtr4d 2788 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝐹‘(𝑢(+g‘𝐺)𝑣))‘𝑧) = (𝑢 ⊕ ((𝐹‘𝑣)‘𝑧))) |
76 | 1 | ad2antrr 722 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝐺 ∈ Grp) |
77 | 9, 59 | grpcl 18500 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → (𝑢(+g‘𝐺)𝑣) ∈ 𝑋) |
78 | 76, 58, 46, 77 | syl3anc 1369 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑢(+g‘𝐺)𝑣) ∈ 𝑋) |
79 | | fveq2 6756 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑢(+g‘𝐺)𝑣) → (𝐹‘𝑥) = (𝐹‘(𝑢(+g‘𝐺)𝑣))) |
80 | 79 | fveq1d 6758 |
. . . . . . . . 9
⊢ (𝑥 = (𝑢(+g‘𝐺)𝑣) → ((𝐹‘𝑥)‘𝑦) = ((𝐹‘(𝑢(+g‘𝐺)𝑣))‘𝑦)) |
81 | | fveq2 6756 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → ((𝐹‘(𝑢(+g‘𝐺)𝑣))‘𝑦) = ((𝐹‘(𝑢(+g‘𝐺)𝑣))‘𝑧)) |
82 | | fvex 6769 |
. . . . . . . . 9
⊢ ((𝐹‘(𝑢(+g‘𝐺)𝑣))‘𝑧) ∈ V |
83 | 80, 81, 22, 82 | ovmpo 7411 |
. . . . . . . 8
⊢ (((𝑢(+g‘𝐺)𝑣) ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) → ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = ((𝐹‘(𝑢(+g‘𝐺)𝑣))‘𝑧)) |
84 | 78, 54, 83 | syl2anc 583 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = ((𝐹‘(𝑢(+g‘𝐺)𝑣))‘𝑧)) |
85 | | fveq2 6756 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑣 → (𝐹‘𝑥) = (𝐹‘𝑣)) |
86 | 85 | fveq1d 6758 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑣 → ((𝐹‘𝑥)‘𝑦) = ((𝐹‘𝑣)‘𝑦)) |
87 | | fveq2 6756 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → ((𝐹‘𝑣)‘𝑦) = ((𝐹‘𝑣)‘𝑧)) |
88 | | fvex 6769 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑣)‘𝑧) ∈ V |
89 | 86, 87, 22, 88 | ovmpo 7411 |
. . . . . . . . 9
⊢ ((𝑣 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) → (𝑣 ⊕ 𝑧) = ((𝐹‘𝑣)‘𝑧)) |
90 | 46, 54, 89 | syl2anc 583 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑣 ⊕ 𝑧) = ((𝐹‘𝑣)‘𝑧)) |
91 | 90 | oveq2d 7271 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑢 ⊕ (𝑣 ⊕ 𝑧)) = (𝑢 ⊕ ((𝐹‘𝑣)‘𝑧))) |
92 | 75, 84, 91 | 3eqtr4d 2788 |
. . . . . 6
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = (𝑢 ⊕ (𝑣 ⊕ 𝑧))) |
93 | 92 | ralrimivva 3114 |
. . . . 5
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = (𝑢 ⊕ (𝑣 ⊕ 𝑧))) |
94 | 44, 93 | jca 511 |
. . . 4
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → (((0g‘𝐺) ⊕ 𝑧) = 𝑧 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = (𝑢 ⊕ (𝑣 ⊕ 𝑧)))) |
95 | 94 | ralrimiva 3107 |
. . 3
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → ∀𝑧 ∈ 𝑌 (((0g‘𝐺) ⊕ 𝑧) = 𝑧 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = (𝑢 ⊕ (𝑣 ⊕ 𝑧)))) |
96 | 24, 95 | jca 511 |
. 2
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → ( ⊕ :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑧 ∈ 𝑌 (((0g‘𝐺) ⊕ 𝑧) = 𝑧 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = (𝑢 ⊕ (𝑣 ⊕ 𝑧))))) |
97 | 9, 59, 25 | isga 18812 |
. 2
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) ↔ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) ∧ ( ⊕ :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑧 ∈ 𝑌 (((0g‘𝐺) ⊕ 𝑧) = 𝑧 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = (𝑢 ⊕ (𝑣 ⊕ 𝑧)))))) |
98 | 1, 8, 96, 97 | syl21anbrc 1342 |
1
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → ⊕ ∈ (𝐺 GrpAct 𝑌)) |