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 = Base G
galactghm.h ⊢ H = SymGrp ⁡ Y
galactghm.f ⊢ F = x ∈ X ⟼ y ∈ Y ⟼ x ⊕ ˙ y
Assertion galactghm ⊢ ⊕ ˙ ∈ G GrpAct Y → F ∈ G GrpHom H

Proof

Step Hyp Ref Expression
1 galactghm.x ⊢ X = Base G
2 galactghm.h ⊢ H = SymGrp ⁡ Y
3 galactghm.f ⊢ F = x ∈ X ⟼ y ∈ Y ⟼ x ⊕ ˙ y
4 eqid ⊢ Base H = Base H
5 eqid ⊢ + G = + G
6 eqid ⊢ + H = + H
7 gagrp ⊢ ⊕ ˙ ∈ G GrpAct Y → G ∈ Grp
8 gaset ⊢ ⊕ ˙ ∈ G GrpAct Y → Y ∈ V
9 2 symggrp ⊢ Y ∈ V → H ∈ Grp
10 8 9 syl ⊢ ⊕ ˙ ∈ G GrpAct Y → H ∈ Grp
11 eqid ⊢ y ∈ Y ⟼ x ⊕ ˙ y = y ∈ Y ⟼ x ⊕ ˙ y
12 1 11 gapm ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ x ∈ X → y ∈ Y ⟼ x ⊕ ˙ y : Y ⟶ 1-1 onto Y
13 8 adantr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ x ∈ X → Y ∈ V
14 2 4 elsymgbas ⊢ Y ∈ V → y ∈ Y ⟼ x ⊕ ˙ y ∈ Base H ↔ y ∈ Y ⟼ x ⊕ ˙ y : Y ⟶ 1-1 onto Y
15 13 14 syl ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ x ∈ X → y ∈ Y ⟼ x ⊕ ˙ y ∈ Base H ↔ y ∈ Y ⟼ x ⊕ ˙ y : Y ⟶ 1-1 onto Y
16 12 15 mpbird ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ x ∈ X → y ∈ Y ⟼ x ⊕ ˙ y ∈ Base H
17 16 3 fmptd ⊢ ⊕ ˙ ∈ G GrpAct Y → F : X ⟶ Base H
18 df-3an ⊢ z ∈ X ∧ w ∈ X ∧ y ∈ Y ↔ z ∈ X ∧ w ∈ X ∧ y ∈ Y
19 1 5 gaass ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ z ∈ X ∧ w ∈ X ∧ y ∈ Y → z + G w ⊕ ˙ y = z ⊕ ˙ w ⊕ ˙ y
20 18 19 sylan2br ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ z ∈ X ∧ w ∈ X ∧ y ∈ Y → z + G w ⊕ ˙ y = z ⊕ ˙ w ⊕ ˙ y
21 20 anassrs ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ z ∈ X ∧ w ∈ X ∧ y ∈ Y → z + G w ⊕ ˙ y = z ⊕ ˙ w ⊕ ˙ y
22 21 mpteq2dva ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ z ∈ X ∧ w ∈ X → y ∈ Y ⟼ z + G w ⊕ ˙ y = y ∈ Y ⟼ z ⊕ ˙ w ⊕ ˙ y
23 oveq1 ⊢ x = z + G w → x ⊕ ˙ y = z + G w ⊕ ˙ y
24 23 mpteq2dv ⊢ x = z + G w → y ∈ Y ⟼ x ⊕ ˙ y = y ∈ Y ⟼ z + G w ⊕ ˙ y
25 7 adantr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ z ∈ X ∧ w ∈ X → G ∈ Grp
26 simprl ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ z ∈ X ∧ w ∈ X → z ∈ X
27 simprr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ z ∈ X ∧ w ∈ X → w ∈ X
28 1 5 grpcl ⊢ G ∈ Grp ∧ z ∈ X ∧ w ∈ X → z + G w ∈ X
29 25 26 27 28 syl3anc ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ z ∈ X ∧ w ∈ X → z + G w ∈ X
30 8 adantr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ z ∈ X ∧ w ∈ X → Y ∈ V
31 30 mptexd ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ z ∈ X ∧ w ∈ X → y ∈ Y ⟼ z + G w ⊕ ˙ y ∈ V
32 3 24 29 31 fvmptd3 ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ z ∈ X ∧ w ∈ X → F ⁡ z + G w = y ∈ Y ⟼ z + G w ⊕ ˙ y
33 17 adantr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ z ∈ X ∧ w ∈ X → F : X ⟶ Base H
34 33 26 ffvelrnd ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ z ∈ X ∧ w ∈ X → F ⁡ z ∈ Base H
35 33 27 ffvelrnd ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ z ∈ X ∧ w ∈ X → F ⁡ w ∈ Base H
36 2 4 6 symgov ⊢ F ⁡ z ∈ Base H ∧ F ⁡ w ∈ Base H → F ⁡ z + H F ⁡ w = F ⁡ z ∘ F ⁡ w
37 34 35 36 syl2anc ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ z ∈ X ∧ w ∈ X → F ⁡ z + H F ⁡ w = F ⁡ z ∘ F ⁡ w
38 1 gaf ⊢ ⊕ ˙ ∈ G GrpAct Y → ⊕ ˙ : X × Y ⟶ Y
39 38 ad2antrr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ z ∈ X ∧ w ∈ X ∧ y ∈ Y → ⊕ ˙ : X × Y ⟶ Y
40 27 adantr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ z ∈ X ∧ w ∈ X ∧ y ∈ Y → w ∈ X
41 simpr ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ z ∈ X ∧ w ∈ X ∧ y ∈ Y → y ∈ Y
42 39 40 41 fovrnd ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ 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 ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ z ∈ X ∧ w ∈ X → y ∈ Y ⟼ w ⊕ ˙ y ∈ V
46 3 44 27 45 fvmptd3 ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ 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 ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ z ∈ X ∧ w ∈ X → y ∈ Y ⟼ z ⊕ ˙ y ∈ V
50 3 48 26 49 fvmptd3 ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ 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 ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ 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 ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ z ∈ X ∧ w ∈ X → F ⁡ z ∘ F ⁡ w = y ∈ Y ⟼ z ⊕ ˙ w ⊕ ˙ y
56 37 55 eqtrd ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ z ∈ X ∧ w ∈ X → F ⁡ z + H F ⁡ w = y ∈ Y ⟼ z ⊕ ˙ w ⊕ ˙ y
57 22 32 56 3eqtr4d ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ z ∈ X ∧ w ∈ X → F ⁡ z + G w = F ⁡ z + H F ⁡ w
58 1 4 5 6 7 10 17 57 isghmd ⊢ ⊕ ˙ ∈ G GrpAct Y → F ∈ G GrpHom H