Step | Hyp | Ref
| Expression |
1 | | galactghm.x |
. 2
⊢ 𝑋 = (Base‘𝐺) |
2 | | eqid 2610 |
. 2
⊢
(Base‘𝐻) =
(Base‘𝐻) |
3 | | eqid 2610 |
. 2
⊢
(+g‘𝐺) = (+g‘𝐺) |
4 | | eqid 2610 |
. 2
⊢
(+g‘𝐻) = (+g‘𝐻) |
5 | | gagrp 17548 |
. 2
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) → 𝐺 ∈ Grp) |
6 | | gaset 17549 |
. . 3
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) → 𝑌 ∈ V) |
7 | | galactghm.h |
. . . 4
⊢ 𝐻 = (SymGrp‘𝑌) |
8 | 7 | symggrp 17643 |
. . 3
⊢ (𝑌 ∈ V → 𝐻 ∈ Grp) |
9 | 6, 8 | syl 17 |
. 2
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) → 𝐻 ∈ Grp) |
10 | | eqid 2610 |
. . . . 5
⊢ (𝑦 ∈ 𝑌 ↦ (𝑥 ⊕ 𝑦)) = (𝑦 ∈ 𝑌 ↦ (𝑥 ⊕ 𝑦)) |
11 | 1, 10 | gapm 17562 |
. . . 4
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ (𝑥 ⊕ 𝑦)):𝑌–1-1-onto→𝑌) |
12 | 6 | adantr 480 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑥 ∈ 𝑋) → 𝑌 ∈ V) |
13 | 7, 2 | elsymgbas 17625 |
. . . . 5
⊢ (𝑌 ∈ V → ((𝑦 ∈ 𝑌 ↦ (𝑥 ⊕ 𝑦)) ∈ (Base‘𝐻) ↔ (𝑦 ∈ 𝑌 ↦ (𝑥 ⊕ 𝑦)):𝑌–1-1-onto→𝑌)) |
14 | 12, 13 | syl 17 |
. . . 4
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑥 ∈ 𝑋) → ((𝑦 ∈ 𝑌 ↦ (𝑥 ⊕ 𝑦)) ∈ (Base‘𝐻) ↔ (𝑦 ∈ 𝑌 ↦ (𝑥 ⊕ 𝑦)):𝑌–1-1-onto→𝑌)) |
15 | 11, 14 | mpbird 246 |
. . 3
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ (𝑥 ⊕ 𝑦)) ∈ (Base‘𝐻)) |
16 | | galactghm.f |
. . 3
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥 ⊕ 𝑦))) |
17 | 15, 16 | fmptd 6292 |
. 2
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) → 𝐹:𝑋⟶(Base‘𝐻)) |
18 | | df-3an 1033 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) ↔ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌)) |
19 | 1, 3 | gaass 17553 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → ((𝑧(+g‘𝐺)𝑤) ⊕ 𝑦) = (𝑧 ⊕ (𝑤 ⊕ 𝑦))) |
20 | 18, 19 | sylan2br 492 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ ((𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌)) → ((𝑧(+g‘𝐺)𝑤) ⊕ 𝑦) = (𝑧 ⊕ (𝑤 ⊕ 𝑦))) |
21 | 20 | anassrs 678 |
. . . 4
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) ∧ 𝑦 ∈ 𝑌) → ((𝑧(+g‘𝐺)𝑤) ⊕ 𝑦) = (𝑧 ⊕ (𝑤 ⊕ 𝑦))) |
22 | 21 | mpteq2dva 4672 |
. . 3
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝑦 ∈ 𝑌 ↦ ((𝑧(+g‘𝐺)𝑤) ⊕ 𝑦)) = (𝑦 ∈ 𝑌 ↦ (𝑧 ⊕ (𝑤 ⊕ 𝑦)))) |
23 | 5 | adantr 480 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → 𝐺 ∈ Grp) |
24 | | simprl 790 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → 𝑧 ∈ 𝑋) |
25 | | simprr 792 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → 𝑤 ∈ 𝑋) |
26 | 1, 3 | grpcl 17253 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑧(+g‘𝐺)𝑤) ∈ 𝑋) |
27 | 23, 24, 25, 26 | syl3anc 1318 |
. . . 4
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝑧(+g‘𝐺)𝑤) ∈ 𝑋) |
28 | 6 | adantr 480 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → 𝑌 ∈ V) |
29 | | mptexg 6389 |
. . . . 5
⊢ (𝑌 ∈ V → (𝑦 ∈ 𝑌 ↦ ((𝑧(+g‘𝐺)𝑤) ⊕ 𝑦)) ∈ V) |
30 | 28, 29 | syl 17 |
. . . 4
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝑦 ∈ 𝑌 ↦ ((𝑧(+g‘𝐺)𝑤) ⊕ 𝑦)) ∈ V) |
31 | | oveq1 6556 |
. . . . . 6
⊢ (𝑥 = (𝑧(+g‘𝐺)𝑤) → (𝑥 ⊕ 𝑦) = ((𝑧(+g‘𝐺)𝑤) ⊕ 𝑦)) |
32 | 31 | mpteq2dv 4673 |
. . . . 5
⊢ (𝑥 = (𝑧(+g‘𝐺)𝑤) → (𝑦 ∈ 𝑌 ↦ (𝑥 ⊕ 𝑦)) = (𝑦 ∈ 𝑌 ↦ ((𝑧(+g‘𝐺)𝑤) ⊕ 𝑦))) |
33 | 32, 16 | fvmptg 6189 |
. . . 4
⊢ (((𝑧(+g‘𝐺)𝑤) ∈ 𝑋 ∧ (𝑦 ∈ 𝑌 ↦ ((𝑧(+g‘𝐺)𝑤) ⊕ 𝑦)) ∈ V) → (𝐹‘(𝑧(+g‘𝐺)𝑤)) = (𝑦 ∈ 𝑌 ↦ ((𝑧(+g‘𝐺)𝑤) ⊕ 𝑦))) |
34 | 27, 30, 33 | syl2anc 691 |
. . 3
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝐹‘(𝑧(+g‘𝐺)𝑤)) = (𝑦 ∈ 𝑌 ↦ ((𝑧(+g‘𝐺)𝑤) ⊕ 𝑦))) |
35 | 17 | adantr 480 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → 𝐹:𝑋⟶(Base‘𝐻)) |
36 | 35, 24 | ffvelrnd 6268 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝐹‘𝑧) ∈ (Base‘𝐻)) |
37 | 35, 25 | ffvelrnd 6268 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝐹‘𝑤) ∈ (Base‘𝐻)) |
38 | 7, 2, 4 | symgov 17633 |
. . . . 5
⊢ (((𝐹‘𝑧) ∈ (Base‘𝐻) ∧ (𝐹‘𝑤) ∈ (Base‘𝐻)) → ((𝐹‘𝑧)(+g‘𝐻)(𝐹‘𝑤)) = ((𝐹‘𝑧) ∘ (𝐹‘𝑤))) |
39 | 36, 37, 38 | syl2anc 691 |
. . . 4
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ((𝐹‘𝑧)(+g‘𝐻)(𝐹‘𝑤)) = ((𝐹‘𝑧) ∘ (𝐹‘𝑤))) |
40 | 1 | gaf 17551 |
. . . . . . 7
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) → ⊕ :(𝑋 × 𝑌)⟶𝑌) |
41 | 40 | ad2antrr 758 |
. . . . . 6
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) ∧ 𝑦 ∈ 𝑌) → ⊕ :(𝑋 × 𝑌)⟶𝑌) |
42 | 25 | adantr 480 |
. . . . . 6
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) ∧ 𝑦 ∈ 𝑌) → 𝑤 ∈ 𝑋) |
43 | | simpr 476 |
. . . . . 6
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌) |
44 | 41, 42, 43 | fovrnd 6704 |
. . . . 5
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) ∧ 𝑦 ∈ 𝑌) → (𝑤 ⊕ 𝑦) ∈ 𝑌) |
45 | | mptexg 6389 |
. . . . . . 7
⊢ (𝑌 ∈ V → (𝑦 ∈ 𝑌 ↦ (𝑤 ⊕ 𝑦)) ∈ V) |
46 | 28, 45 | syl 17 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝑦 ∈ 𝑌 ↦ (𝑤 ⊕ 𝑦)) ∈ V) |
47 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑥 = 𝑤 → (𝑥 ⊕ 𝑦) = (𝑤 ⊕ 𝑦)) |
48 | 47 | mpteq2dv 4673 |
. . . . . . 7
⊢ (𝑥 = 𝑤 → (𝑦 ∈ 𝑌 ↦ (𝑥 ⊕ 𝑦)) = (𝑦 ∈ 𝑌 ↦ (𝑤 ⊕ 𝑦))) |
49 | 48, 16 | fvmptg 6189 |
. . . . . 6
⊢ ((𝑤 ∈ 𝑋 ∧ (𝑦 ∈ 𝑌 ↦ (𝑤 ⊕ 𝑦)) ∈ V) → (𝐹‘𝑤) = (𝑦 ∈ 𝑌 ↦ (𝑤 ⊕ 𝑦))) |
50 | 25, 46, 49 | syl2anc 691 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝐹‘𝑤) = (𝑦 ∈ 𝑌 ↦ (𝑤 ⊕ 𝑦))) |
51 | | mptexg 6389 |
. . . . . . . 8
⊢ (𝑌 ∈ V → (𝑦 ∈ 𝑌 ↦ (𝑧 ⊕ 𝑦)) ∈ V) |
52 | 28, 51 | syl 17 |
. . . . . . 7
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝑦 ∈ 𝑌 ↦ (𝑧 ⊕ 𝑦)) ∈ V) |
53 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝑥 ⊕ 𝑦) = (𝑧 ⊕ 𝑦)) |
54 | 53 | mpteq2dv 4673 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑦 ∈ 𝑌 ↦ (𝑥 ⊕ 𝑦)) = (𝑦 ∈ 𝑌 ↦ (𝑧 ⊕ 𝑦))) |
55 | 54, 16 | fvmptg 6189 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ∧ (𝑦 ∈ 𝑌 ↦ (𝑧 ⊕ 𝑦)) ∈ V) → (𝐹‘𝑧) = (𝑦 ∈ 𝑌 ↦ (𝑧 ⊕ 𝑦))) |
56 | 24, 52, 55 | syl2anc 691 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝐹‘𝑧) = (𝑦 ∈ 𝑌 ↦ (𝑧 ⊕ 𝑦))) |
57 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (𝑧 ⊕ 𝑦) = (𝑧 ⊕ 𝑥)) |
58 | 57 | cbvmptv 4678 |
. . . . . 6
⊢ (𝑦 ∈ 𝑌 ↦ (𝑧 ⊕ 𝑦)) = (𝑥 ∈ 𝑌 ↦ (𝑧 ⊕ 𝑥)) |
59 | 56, 58 | syl6eq 2660 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝐹‘𝑧) = (𝑥 ∈ 𝑌 ↦ (𝑧 ⊕ 𝑥))) |
60 | | oveq2 6557 |
. . . . 5
⊢ (𝑥 = (𝑤 ⊕ 𝑦) → (𝑧 ⊕ 𝑥) = (𝑧 ⊕ (𝑤 ⊕ 𝑦))) |
61 | 44, 50, 59, 60 | fmptco 6303 |
. . . 4
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ((𝐹‘𝑧) ∘ (𝐹‘𝑤)) = (𝑦 ∈ 𝑌 ↦ (𝑧 ⊕ (𝑤 ⊕ 𝑦)))) |
62 | 39, 61 | eqtrd 2644 |
. . 3
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ((𝐹‘𝑧)(+g‘𝐻)(𝐹‘𝑤)) = (𝑦 ∈ 𝑌 ↦ (𝑧 ⊕ (𝑤 ⊕ 𝑦)))) |
63 | 22, 34, 62 | 3eqtr4d 2654 |
. 2
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → (𝐹‘(𝑧(+g‘𝐺)𝑤)) = ((𝐹‘𝑧)(+g‘𝐻)(𝐹‘𝑤))) |
64 | 1, 2, 3, 4, 5, 9, 17, 63 | isghmd 17492 |
1
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) → 𝐹 ∈ (𝐺 GrpHom 𝐻)) |