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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
galactghm.h ⊢ 𝐻 = ( SymGrp ‘ 𝑌 )
galactghm.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 ⊕ 𝑦 ) ) )
Assertion galactghm ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )

Proof

Step Hyp Ref Expression
1 galactghm.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 galactghm.h ⊢ 𝐻 = ( SymGrp ‘ 𝑌 )
3 galactghm.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 ⊕ 𝑦 ) ) )
4 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
5 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
6 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
7 gagrp ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → 𝐺 ∈ Grp )
8 gaset ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → 𝑌 ∈ V )
9 2 symggrp ⊢ ( 𝑌 ∈ V → 𝐻 ∈ Grp )
10 8 9 syl ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → 𝐻 ∈ Grp )
11 eqid ⊢ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 ⊕ 𝑦 ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 ⊕ 𝑦 ) )
12 1 11 gapm ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 ⊕ 𝑦 ) ) : 𝑌 –1-1-onto→ 𝑌 )
13 8 adantr ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑌 ∈ V )
14 2 4 elsymgbas ⊢ ( 𝑌 ∈ V → ( ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 ⊕ 𝑦 ) ) ∈ ( Base ‘ 𝐻 ) ↔ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 ⊕ 𝑦 ) ) : 𝑌 –1-1-onto→ 𝑌 ) )
15 13 14 syl ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 ⊕ 𝑦 ) ) ∈ ( Base ‘ 𝐻 ) ↔ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 ⊕ 𝑦 ) ) : 𝑌 –1-1-onto→ 𝑌 ) )
16 12 15 mpbird ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 ⊕ 𝑦 ) ) ∈ ( Base ‘ 𝐻 ) )
17 16 3 fmptd ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → 𝐹 : 𝑋 ⟶ ( Base ‘ 𝐻 ) )
18 df-3an ⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ↔ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) )
19 1 5 gaass ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → ( ( 𝑧 ( +g ‘ 𝐺 ) 𝑤 ) ⊕ 𝑦 ) = ( 𝑧 ⊕ ( 𝑤 ⊕ 𝑦 ) ) )
20 18 19 sylan2br ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) ) → ( ( 𝑧 ( +g ‘ 𝐺 ) 𝑤 ) ⊕ 𝑦 ) = ( 𝑧 ⊕ ( 𝑤 ⊕ 𝑦 ) ) )
21 20 anassrs ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝑧 ( +g ‘ 𝐺 ) 𝑤 ) ⊕ 𝑦 ) = ( 𝑧 ⊕ ( 𝑤 ⊕ 𝑦 ) ) )
22 21 mpteq2dva ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝑦 ∈ 𝑌 ↦ ( ( 𝑧 ( +g ‘ 𝐺 ) 𝑤 ) ⊕ 𝑦 ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑧 ⊕ ( 𝑤 ⊕ 𝑦 ) ) ) )
23 oveq1 ⊢ ( 𝑥 = ( 𝑧 ( +g ‘ 𝐺 ) 𝑤 ) → ( 𝑥 ⊕ 𝑦 ) = ( ( 𝑧 ( +g ‘ 𝐺 ) 𝑤 ) ⊕ 𝑦 ) )
24 23 mpteq2dv ⊢ ( 𝑥 = ( 𝑧 ( +g ‘ 𝐺 ) 𝑤 ) → ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 ⊕ 𝑦 ) ) = ( 𝑦 ∈ 𝑌 ↦ ( ( 𝑧 ( +g ‘ 𝐺 ) 𝑤 ) ⊕ 𝑦 ) ) )
25 7 adantr ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → 𝐺 ∈ Grp )
26 simprl ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → 𝑧 ∈ 𝑋 )
27 simprr ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → 𝑤 ∈ 𝑋 )
28 1 5 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( 𝑧 ( +g ‘ 𝐺 ) 𝑤 ) ∈ 𝑋 )
29 25 26 27 28 syl3anc ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝑧 ( +g ‘ 𝐺 ) 𝑤 ) ∈ 𝑋 )
30 8 adantr ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → 𝑌 ∈ V )
31 30 mptexd ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝑦 ∈ 𝑌 ↦ ( ( 𝑧 ( +g ‘ 𝐺 ) 𝑤 ) ⊕ 𝑦 ) ) ∈ V )
32 3 24 29 31 fvmptd3 ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑧 ( +g ‘ 𝐺 ) 𝑤 ) ) = ( 𝑦 ∈ 𝑌 ↦ ( ( 𝑧 ( +g ‘ 𝐺 ) 𝑤 ) ⊕ 𝑦 ) ) )
33 17 adantr ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → 𝐹 : 𝑋 ⟶ ( Base ‘ 𝐻 ) )
34 33 26 ffvelcdmd ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ( Base ‘ 𝐻 ) )
35 33 27 ffvelcdmd ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ ( Base ‘ 𝐻 ) )
36 2 4 6 symgov ⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ ( Base ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑤 ) ∈ ( Base ‘ 𝐻 ) ) → ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑤 ) ) = ( ( 𝐹 ‘ 𝑧 ) ∘ ( 𝐹 ‘ 𝑤 ) ) )
37 34 35 36 syl2anc ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑤 ) ) = ( ( 𝐹 ‘ 𝑧 ) ∘ ( 𝐹 ‘ 𝑤 ) ) )
38 1 gaf ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → ⊕ : ( 𝑋 × 𝑌 ) ⟶ 𝑌 )
39 38 ad2antrr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ 𝑦 ∈ 𝑌 ) → ⊕ : ( 𝑋 × 𝑌 ) ⟶ 𝑌 )
40 27 adantr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ 𝑦 ∈ 𝑌 ) → 𝑤 ∈ 𝑋 )
41 simpr ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝑌 )
42 39 40 41 fovcdmd ⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝑤 ⊕ 𝑦 ) ∈ 𝑌 )
43 oveq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 ⊕ 𝑦 ) = ( 𝑤 ⊕ 𝑦 ) )
44 43 mpteq2dv ⊢ ( 𝑥 = 𝑤 → ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 ⊕ 𝑦 ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑤 ⊕ 𝑦 ) ) )
45 30 mptexd ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝑦 ∈ 𝑌 ↦ ( 𝑤 ⊕ 𝑦 ) ) ∈ V )
46 3 44 27 45 fvmptd3 ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑤 ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑤 ⊕ 𝑦 ) ) )
47 oveq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ⊕ 𝑦 ) = ( 𝑧 ⊕ 𝑦 ) )
48 47 mpteq2dv ⊢ ( 𝑥 = 𝑧 → ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 ⊕ 𝑦 ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑧 ⊕ 𝑦 ) ) )
49 30 mptexd ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝑦 ∈ 𝑌 ↦ ( 𝑧 ⊕ 𝑦 ) ) ∈ V )
50 3 48 26 49 fvmptd3 ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑧 ⊕ 𝑦 ) ) )
51 oveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑧 ⊕ 𝑦 ) = ( 𝑧 ⊕ 𝑥 ) )
52 51 cbvmptv ⊢ ( 𝑦 ∈ 𝑌 ↦ ( 𝑧 ⊕ 𝑦 ) ) = ( 𝑥 ∈ 𝑌 ↦ ( 𝑧 ⊕ 𝑥 ) )
53 50 52 eqtrdi ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝑥 ∈ 𝑌 ↦ ( 𝑧 ⊕ 𝑥 ) ) )
54 oveq2 ⊢ ( 𝑥 = ( 𝑤 ⊕ 𝑦 ) → ( 𝑧 ⊕ 𝑥 ) = ( 𝑧 ⊕ ( 𝑤 ⊕ 𝑦 ) ) )
55 42 46 53 54 fmptco ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑧 ) ∘ ( 𝐹 ‘ 𝑤 ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑧 ⊕ ( 𝑤 ⊕ 𝑦 ) ) ) )
56 37 55 eqtrd ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑤 ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑧 ⊕ ( 𝑤 ⊕ 𝑦 ) ) ) )
57 22 32 56 3eqtr4d ⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑧 ( +g ‘ 𝐺 ) 𝑤 ) ) = ( ( 𝐹 ‘ 𝑧 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑤 ) ) )
58 1 4 5 6 7 10 17 57 isghmd ⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )