Metamath Proof Explorer

Theorem galactghm

Description: The currying of a group action is a group homomorphism between the group G and the symmetric group ( SymGrpY ) . (Contributed by FL, 17-May-2010) (Proof shortened by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses galactghm.x ⊢X=BaseG
galactghm.h ⊢H=SymGrp⁡Y
galactghm.f ⊢F=x∈X⟼y∈Y⟼x⊕˙y
Assertion galactghm ⊢⊕˙∈GGrpActY→F∈GGrpHomH

Proof

Step Hyp Ref Expression
1 galactghm.x ⊢X=BaseG
2 galactghm.h ⊢H=SymGrp⁡Y
3 galactghm.f ⊢F=x∈X⟼y∈Y⟼x⊕˙y
4 eqid ⊢BaseH=BaseH
5 eqid ⊢+G=+G
6 eqid ⊢+H=+H
7 gagrp ⊢⊕˙∈GGrpActY→G∈Grp
8 gaset ⊢⊕˙∈GGrpActY→Y∈V
9 2 symggrp ⊢Y∈V→H∈Grp
10 8 9 syl ⊢⊕˙∈GGrpActY→H∈Grp
11 eqid ⊢y∈Y⟼x⊕˙y=y∈Y⟼x⊕˙y
12 1 11 gapm ⊢⊕˙∈GGrpActY∧x∈X→y∈Y⟼x⊕˙y:Y⟶1-1 ontoY
13 8 adantr ⊢⊕˙∈GGrpActY∧x∈X→Y∈V
14 2 4 elsymgbas ⊢Y∈V→y∈Y⟼x⊕˙y∈BaseH↔y∈Y⟼x⊕˙y:Y⟶1-1 ontoY
15 13 14 syl ⊢⊕˙∈GGrpActY∧x∈X→y∈Y⟼x⊕˙y∈BaseH↔y∈Y⟼x⊕˙y:Y⟶1-1 ontoY
16 12 15 mpbird ⊢⊕˙∈GGrpActY∧x∈X→y∈Y⟼x⊕˙y∈BaseH
17 16 3 fmptd ⊢⊕˙∈GGrpActY→F:X⟶BaseH
18 df-3an ⊢z∈X∧w∈X∧y∈Y↔z∈X∧w∈X∧y∈Y
19 1 5 gaass ⊢⊕˙∈GGrpActY∧z∈X∧w∈X∧y∈Y→z+Gw⊕˙y=z⊕˙w⊕˙y
20 18 19 sylan2br ⊢⊕˙∈GGrpActY∧z∈X∧w∈X∧y∈Y→z+Gw⊕˙y=z⊕˙w⊕˙y
21 20 anassrs ⊢⊕˙∈GGrpActY∧z∈X∧w∈X∧y∈Y→z+Gw⊕˙y=z⊕˙w⊕˙y
22 21 mpteq2dva ⊢⊕˙∈GGrpActY∧z∈X∧w∈X→y∈Y⟼z+Gw⊕˙y=y∈Y⟼z⊕˙w⊕˙y
23 oveq1 ⊢x=z+Gw→x⊕˙y=z+Gw⊕˙y
24 23 mpteq2dv ⊢x=z+Gw→y∈Y⟼x⊕˙y=y∈Y⟼z+Gw⊕˙y
25 7 adantr ⊢⊕˙∈GGrpActY∧z∈X∧w∈X→G∈Grp
26 simprl ⊢⊕˙∈GGrpActY∧z∈X∧w∈X→z∈X
27 simprr ⊢⊕˙∈GGrpActY∧z∈X∧w∈X→w∈X
28 1 5 grpcl ⊢G∈Grp∧z∈X∧w∈X→z+Gw∈X
29 25 26 27 28 syl3anc ⊢⊕˙∈GGrpActY∧z∈X∧w∈X→z+Gw∈X
30 8 adantr ⊢⊕˙∈GGrpActY∧z∈X∧w∈X→Y∈V
31 30 mptexd ⊢⊕˙∈GGrpActY∧z∈X∧w∈X→y∈Y⟼z+Gw⊕˙y∈V
32 3 24 29 31 fvmptd3 ⊢⊕˙∈GGrpActY∧z∈X∧w∈X→F⁡z+Gw=y∈Y⟼z+Gw⊕˙y
33 17 adantr ⊢⊕˙∈GGrpActY∧z∈X∧w∈X→F:X⟶BaseH
34 33 26 ffvelcdmd ⊢⊕˙∈GGrpActY∧z∈X∧w∈X→F⁡z∈BaseH
35 33 27 ffvelcdmd ⊢⊕˙∈GGrpActY∧z∈X∧w∈X→F⁡w∈BaseH
36 2 4 6 symgov ⊢F⁡z∈BaseH∧F⁡w∈BaseH→F⁡z+HF⁡w=F⁡z∘F⁡w
37 34 35 36 syl2anc ⊢⊕˙∈GGrpActY∧z∈X∧w∈X→F⁡z+HF⁡w=F⁡z∘F⁡w
38 1 gaf ⊢⊕˙∈GGrpActY→⊕˙:X×Y⟶Y
39 38 ad2antrr ⊢⊕˙∈GGrpActY∧z∈X∧w∈X∧y∈Y→⊕˙:X×Y⟶Y
40 27 adantr ⊢⊕˙∈GGrpActY∧z∈X∧w∈X∧y∈Y→w∈X
41 simpr ⊢⊕˙∈GGrpActY∧z∈X∧w∈X∧y∈Y→y∈Y
42 39 40 41 fovcdmd ⊢⊕˙∈GGrpActY∧z∈X∧w∈X∧y∈Y→w⊕˙y∈Y
43 oveq1 ⊢x=w→x⊕˙y=w⊕˙y
44 43 mpteq2dv ⊢x=w→y∈Y⟼x⊕˙y=y∈Y⟼w⊕˙y
45 30 mptexd ⊢⊕˙∈GGrpActY∧z∈X∧w∈X→y∈Y⟼w⊕˙y∈V
46 3 44 27 45 fvmptd3 ⊢⊕˙∈GGrpActY∧z∈X∧w∈X→F⁡w=y∈Y⟼w⊕˙y
47 oveq1 ⊢x=z→x⊕˙y=z⊕˙y
48 47 mpteq2dv ⊢x=z→y∈Y⟼x⊕˙y=y∈Y⟼z⊕˙y
49 30 mptexd ⊢⊕˙∈GGrpActY∧z∈X∧w∈X→y∈Y⟼z⊕˙y∈V
50 3 48 26 49 fvmptd3 ⊢⊕˙∈GGrpActY∧z∈X∧w∈X→F⁡z=y∈Y⟼z⊕˙y
51 oveq2 ⊢y=x→z⊕˙y=z⊕˙x
52 51 cbvmptv ⊢y∈Y⟼z⊕˙y=x∈Y⟼z⊕˙x
53 50 52 eqtrdi ⊢⊕˙∈GGrpActY∧z∈X∧w∈X→F⁡z=x∈Y⟼z⊕˙x
54 oveq2 ⊢x=w⊕˙y→z⊕˙x=z⊕˙w⊕˙y
55 42 46 53 54 fmptco ⊢⊕˙∈GGrpActY∧z∈X∧w∈X→F⁡z∘F⁡w=y∈Y⟼z⊕˙w⊕˙y
56 37 55 eqtrd ⊢⊕˙∈GGrpActY∧z∈X∧w∈X→F⁡z+HF⁡w=y∈Y⟼z⊕˙w⊕˙y
57 22 32 56 3eqtr4d ⊢⊕˙∈GGrpActY∧z∈X∧w∈X→F⁡z+Gw=F⁡z+HF⁡w
58 1 4 5 6 7 10 17 57 isghmd ⊢⊕˙∈GGrpActY→F∈GGrpHomH