Step | Hyp | Ref
| Expression |
1 | | ghmgrp1 17485 |
. . 3
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝐺 ∈ Grp) |
2 | | ghmgrp2 17486 |
. . . 4
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝐻 ∈ Grp) |
3 | | grpn0 17277 |
. . . 4
⊢ (𝐻 ∈ Grp → 𝐻 ≠ ∅) |
4 | | lactghmga.h |
. . . . . 6
⊢ 𝐻 = (SymGrp‘𝑌) |
5 | | fvprc 6097 |
. . . . . 6
⊢ (¬
𝑌 ∈ V →
(SymGrp‘𝑌) =
∅) |
6 | 4, 5 | syl5eq 2656 |
. . . . 5
⊢ (¬
𝑌 ∈ V → 𝐻 = ∅) |
7 | 6 | necon1ai 2809 |
. . . 4
⊢ (𝐻 ≠ ∅ → 𝑌 ∈ V) |
8 | 2, 3, 7 | 3syl 18 |
. . 3
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝑌 ∈ V) |
9 | 1, 8 | jca 553 |
. 2
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → (𝐺 ∈ Grp ∧ 𝑌 ∈ V)) |
10 | | lactghmga.x |
. . . . . . . . . . 11
⊢ 𝑋 = (Base‘𝐺) |
11 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘𝐻) =
(Base‘𝐻) |
12 | 10, 11 | ghmf 17487 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → 𝐹:𝑋⟶(Base‘𝐻)) |
13 | 12 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ (Base‘𝐻)) |
14 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑋) → 𝑌 ∈ V) |
15 | 4, 11 | elsymgbas 17625 |
. . . . . . . . . 10
⊢ (𝑌 ∈ V → ((𝐹‘𝑥) ∈ (Base‘𝐻) ↔ (𝐹‘𝑥):𝑌–1-1-onto→𝑌)) |
16 | 14, 15 | syl 17 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑋) → ((𝐹‘𝑥) ∈ (Base‘𝐻) ↔ (𝐹‘𝑥):𝑌–1-1-onto→𝑌)) |
17 | 13, 16 | mpbid 221 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥):𝑌–1-1-onto→𝑌) |
18 | | f1of 6050 |
. . . . . . . 8
⊢ ((𝐹‘𝑥):𝑌–1-1-onto→𝑌 → (𝐹‘𝑥):𝑌⟶𝑌) |
19 | 17, 18 | syl 17 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥):𝑌⟶𝑌) |
20 | 19 | ffvelrnda 6267 |
. . . . . 6
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → ((𝐹‘𝑥)‘𝑦) ∈ 𝑌) |
21 | 20 | ralrimiva 2949 |
. . . . 5
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 ((𝐹‘𝑥)‘𝑦) ∈ 𝑌) |
22 | 21 | ralrimiva 2949 |
. . . 4
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝐹‘𝑥)‘𝑦) ∈ 𝑌) |
23 | | lactghmga.f |
. . . . 5
⊢ ⊕ =
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝐹‘𝑥)‘𝑦)) |
24 | 23 | fmpt2 7126 |
. . . 4
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑌 ((𝐹‘𝑥)‘𝑦) ∈ 𝑌 ↔ ⊕ :(𝑋 × 𝑌)⟶𝑌) |
25 | 22, 24 | sylib 207 |
. . 3
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → ⊕ :(𝑋 × 𝑌)⟶𝑌) |
26 | | eqid 2610 |
. . . . . . . . 9
⊢
(0g‘𝐺) = (0g‘𝐺) |
27 | 10, 26 | grpidcl 17273 |
. . . . . . . 8
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝑋) |
28 | 1, 27 | syl 17 |
. . . . . . 7
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → (0g‘𝐺) ∈ 𝑋) |
29 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑥 = (0g‘𝐺) → (𝐹‘𝑥) = (𝐹‘(0g‘𝐺))) |
30 | 29 | fveq1d 6105 |
. . . . . . . 8
⊢ (𝑥 = (0g‘𝐺) → ((𝐹‘𝑥)‘𝑦) = ((𝐹‘(0g‘𝐺))‘𝑦)) |
31 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → ((𝐹‘(0g‘𝐺))‘𝑦) = ((𝐹‘(0g‘𝐺))‘𝑧)) |
32 | | fvex 6113 |
. . . . . . . 8
⊢ ((𝐹‘(0g‘𝐺))‘𝑧) ∈ V |
33 | 30, 31, 23, 32 | ovmpt2 6694 |
. . . . . . 7
⊢
(((0g‘𝐺) ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) → ((0g‘𝐺) ⊕ 𝑧) = ((𝐹‘(0g‘𝐺))‘𝑧)) |
34 | 28, 33 | sylan 487 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → ((0g‘𝐺) ⊕ 𝑧) = ((𝐹‘(0g‘𝐺))‘𝑧)) |
35 | | eqid 2610 |
. . . . . . . . . 10
⊢
(0g‘𝐻) = (0g‘𝐻) |
36 | 26, 35 | ghmid 17489 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → (𝐹‘(0g‘𝐺)) = (0g‘𝐻)) |
37 | 36 | adantr 480 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → (𝐹‘(0g‘𝐺)) = (0g‘𝐻)) |
38 | 8 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → 𝑌 ∈ V) |
39 | 4 | symgid 17644 |
. . . . . . . . 9
⊢ (𝑌 ∈ V → ( I ↾
𝑌) =
(0g‘𝐻)) |
40 | 38, 39 | syl 17 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → ( I ↾ 𝑌) = (0g‘𝐻)) |
41 | 37, 40 | eqtr4d 2647 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → (𝐹‘(0g‘𝐺)) = ( I ↾ 𝑌)) |
42 | 41 | fveq1d 6105 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → ((𝐹‘(0g‘𝐺))‘𝑧) = (( I ↾ 𝑌)‘𝑧)) |
43 | | fvresi 6344 |
. . . . . . 7
⊢ (𝑧 ∈ 𝑌 → (( I ↾ 𝑌)‘𝑧) = 𝑧) |
44 | 43 | adantl 481 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → (( I ↾ 𝑌)‘𝑧) = 𝑧) |
45 | 34, 42, 44 | 3eqtrd 2648 |
. . . . 5
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → ((0g‘𝐺) ⊕ 𝑧) = 𝑧) |
46 | 12 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝐹:𝑋⟶(Base‘𝐻)) |
47 | | simprr 792 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝑣 ∈ 𝑋) |
48 | 46, 47 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝐹‘𝑣) ∈ (Base‘𝐻)) |
49 | 8 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝑌 ∈ V) |
50 | 4, 11 | elsymgbas 17625 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ V → ((𝐹‘𝑣) ∈ (Base‘𝐻) ↔ (𝐹‘𝑣):𝑌–1-1-onto→𝑌)) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝐹‘𝑣) ∈ (Base‘𝐻) ↔ (𝐹‘𝑣):𝑌–1-1-onto→𝑌)) |
52 | 48, 51 | mpbid 221 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝐹‘𝑣):𝑌–1-1-onto→𝑌) |
53 | | f1of 6050 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑣):𝑌–1-1-onto→𝑌 → (𝐹‘𝑣):𝑌⟶𝑌) |
54 | 52, 53 | syl 17 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝐹‘𝑣):𝑌⟶𝑌) |
55 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝑧 ∈ 𝑌) |
56 | | fvco3 6185 |
. . . . . . . . 9
⊢ (((𝐹‘𝑣):𝑌⟶𝑌 ∧ 𝑧 ∈ 𝑌) → (((𝐹‘𝑢) ∘ (𝐹‘𝑣))‘𝑧) = ((𝐹‘𝑢)‘((𝐹‘𝑣)‘𝑧))) |
57 | 54, 55, 56 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (((𝐹‘𝑢) ∘ (𝐹‘𝑣))‘𝑧) = ((𝐹‘𝑢)‘((𝐹‘𝑣)‘𝑧))) |
58 | | simpll 786 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝐹 ∈ (𝐺 GrpHom 𝐻)) |
59 | | simprl 790 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝑢 ∈ 𝑋) |
60 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(+g‘𝐺) = (+g‘𝐺) |
61 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(+g‘𝐻) = (+g‘𝐻) |
62 | 10, 60, 61 | ghmlin 17488 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → (𝐹‘(𝑢(+g‘𝐺)𝑣)) = ((𝐹‘𝑢)(+g‘𝐻)(𝐹‘𝑣))) |
63 | 58, 59, 47, 62 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝐹‘(𝑢(+g‘𝐺)𝑣)) = ((𝐹‘𝑢)(+g‘𝐻)(𝐹‘𝑣))) |
64 | 46, 59 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝐹‘𝑢) ∈ (Base‘𝐻)) |
65 | 4, 11, 61 | symgov 17633 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑢) ∈ (Base‘𝐻) ∧ (𝐹‘𝑣) ∈ (Base‘𝐻)) → ((𝐹‘𝑢)(+g‘𝐻)(𝐹‘𝑣)) = ((𝐹‘𝑢) ∘ (𝐹‘𝑣))) |
66 | 64, 48, 65 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝐹‘𝑢)(+g‘𝐻)(𝐹‘𝑣)) = ((𝐹‘𝑢) ∘ (𝐹‘𝑣))) |
67 | 63, 66 | eqtrd 2644 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝐹‘(𝑢(+g‘𝐺)𝑣)) = ((𝐹‘𝑢) ∘ (𝐹‘𝑣))) |
68 | 67 | fveq1d 6105 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝐹‘(𝑢(+g‘𝐺)𝑣))‘𝑧) = (((𝐹‘𝑢) ∘ (𝐹‘𝑣))‘𝑧)) |
69 | 54, 55 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝐹‘𝑣)‘𝑧) ∈ 𝑌) |
70 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑢 → (𝐹‘𝑥) = (𝐹‘𝑢)) |
71 | 70 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑢 → ((𝐹‘𝑥)‘𝑦) = ((𝐹‘𝑢)‘𝑦)) |
72 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑦 = ((𝐹‘𝑣)‘𝑧) → ((𝐹‘𝑢)‘𝑦) = ((𝐹‘𝑢)‘((𝐹‘𝑣)‘𝑧))) |
73 | | fvex 6113 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑢)‘((𝐹‘𝑣)‘𝑧)) ∈ V |
74 | 71, 72, 23, 73 | ovmpt2 6694 |
. . . . . . . . 9
⊢ ((𝑢 ∈ 𝑋 ∧ ((𝐹‘𝑣)‘𝑧) ∈ 𝑌) → (𝑢 ⊕ ((𝐹‘𝑣)‘𝑧)) = ((𝐹‘𝑢)‘((𝐹‘𝑣)‘𝑧))) |
75 | 59, 69, 74 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑢 ⊕ ((𝐹‘𝑣)‘𝑧)) = ((𝐹‘𝑢)‘((𝐹‘𝑣)‘𝑧))) |
76 | 57, 68, 75 | 3eqtr4d 2654 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝐹‘(𝑢(+g‘𝐺)𝑣))‘𝑧) = (𝑢 ⊕ ((𝐹‘𝑣)‘𝑧))) |
77 | 1 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝐺 ∈ Grp) |
78 | 10, 60 | grpcl 17253 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → (𝑢(+g‘𝐺)𝑣) ∈ 𝑋) |
79 | 77, 59, 47, 78 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑢(+g‘𝐺)𝑣) ∈ 𝑋) |
80 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑢(+g‘𝐺)𝑣) → (𝐹‘𝑥) = (𝐹‘(𝑢(+g‘𝐺)𝑣))) |
81 | 80 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝑥 = (𝑢(+g‘𝐺)𝑣) → ((𝐹‘𝑥)‘𝑦) = ((𝐹‘(𝑢(+g‘𝐺)𝑣))‘𝑦)) |
82 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → ((𝐹‘(𝑢(+g‘𝐺)𝑣))‘𝑦) = ((𝐹‘(𝑢(+g‘𝐺)𝑣))‘𝑧)) |
83 | | fvex 6113 |
. . . . . . . . 9
⊢ ((𝐹‘(𝑢(+g‘𝐺)𝑣))‘𝑧) ∈ V |
84 | 81, 82, 23, 83 | ovmpt2 6694 |
. . . . . . . 8
⊢ (((𝑢(+g‘𝐺)𝑣) ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) → ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = ((𝐹‘(𝑢(+g‘𝐺)𝑣))‘𝑧)) |
85 | 79, 55, 84 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = ((𝐹‘(𝑢(+g‘𝐺)𝑣))‘𝑧)) |
86 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑣 → (𝐹‘𝑥) = (𝐹‘𝑣)) |
87 | 86 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑣 → ((𝐹‘𝑥)‘𝑦) = ((𝐹‘𝑣)‘𝑦)) |
88 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → ((𝐹‘𝑣)‘𝑦) = ((𝐹‘𝑣)‘𝑧)) |
89 | | fvex 6113 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑣)‘𝑧) ∈ V |
90 | 87, 88, 23, 89 | ovmpt2 6694 |
. . . . . . . . 9
⊢ ((𝑣 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) → (𝑣 ⊕ 𝑧) = ((𝐹‘𝑣)‘𝑧)) |
91 | 47, 55, 90 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑣 ⊕ 𝑧) = ((𝐹‘𝑣)‘𝑧)) |
92 | 91 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑢 ⊕ (𝑣 ⊕ 𝑧)) = (𝑢 ⊕ ((𝐹‘𝑣)‘𝑧))) |
93 | 76, 85, 92 | 3eqtr4d 2654 |
. . . . . 6
⊢ (((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = (𝑢 ⊕ (𝑣 ⊕ 𝑧))) |
94 | 93 | ralrimivva 2954 |
. . . . 5
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = (𝑢 ⊕ (𝑣 ⊕ 𝑧))) |
95 | 45, 94 | jca 553 |
. . . 4
⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑧 ∈ 𝑌) → (((0g‘𝐺) ⊕ 𝑧) = 𝑧 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = (𝑢 ⊕ (𝑣 ⊕ 𝑧)))) |
96 | 95 | ralrimiva 2949 |
. . 3
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → ∀𝑧 ∈ 𝑌 (((0g‘𝐺) ⊕ 𝑧) = 𝑧 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = (𝑢 ⊕ (𝑣 ⊕ 𝑧)))) |
97 | 25, 96 | jca 553 |
. 2
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → ( ⊕ :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑧 ∈ 𝑌 (((0g‘𝐺) ⊕ 𝑧) = 𝑧 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = (𝑢 ⊕ (𝑣 ⊕ 𝑧))))) |
98 | 10, 60, 26 | isga 17547 |
. 2
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) ↔ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) ∧ ( ⊕ :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑧 ∈ 𝑌 (((0g‘𝐺) ⊕ 𝑧) = 𝑧 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = (𝑢 ⊕ (𝑣 ⊕ 𝑧)))))) |
99 | 9, 97, 98 | sylanbrc 695 |
1
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → ⊕ ∈ (𝐺 GrpAct 𝑌)) |