This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. X |-> ( y e. Y |-> ( x .(+) y ) ) )
Assertion galactghm 
|- ( .(+) e. ( G GrpAct Y ) -> F e. ( 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 e. X |-> ( y e. Y |-> ( x .(+) y ) ) )
4 eqid 
 |-  ( Base ` H ) = ( Base ` H )
5 eqid 
 |-  ( +g ` G ) = ( +g ` G )
6 eqid 
 |-  ( +g ` H ) = ( +g ` H )
7 gagrp 
 |-  ( .(+) e. ( G GrpAct Y ) -> G e. Grp )
8 gaset 
 |-  ( .(+) e. ( G GrpAct Y ) -> Y e. _V )
9 2 symggrp 
 |-  ( Y e. _V -> H e. Grp )
10 8 9 syl 
 |-  ( .(+) e. ( G GrpAct Y ) -> H e. Grp )
11 eqid 
 |-  ( y e. Y |-> ( x .(+) y ) ) = ( y e. Y |-> ( x .(+) y ) )
12 1 11 gapm 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ x e. X ) -> ( y e. Y |-> ( x .(+) y ) ) : Y -1-1-onto-> Y )
13 8 adantr 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ x e. X ) -> Y e. _V )
14 2 4 elsymgbas 
 |-  ( Y e. _V -> ( ( y e. Y |-> ( x .(+) y ) ) e. ( Base ` H ) <-> ( y e. Y |-> ( x .(+) y ) ) : Y -1-1-onto-> Y ) )
15 13 14 syl 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ x e. X ) -> ( ( y e. Y |-> ( x .(+) y ) ) e. ( Base ` H ) <-> ( y e. Y |-> ( x .(+) y ) ) : Y -1-1-onto-> Y ) )
16 12 15 mpbird 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ x e. X ) -> ( y e. Y |-> ( x .(+) y ) ) e. ( Base ` H ) )
17 16 3 fmptd 
 |-  ( .(+) e. ( G GrpAct Y ) -> F : X --> ( Base ` H ) )
18 df-3an 
 |-  ( ( z e. X /\ w e. X /\ y e. Y ) <-> ( ( z e. X /\ w e. X ) /\ y e. Y ) )
19 1 5 gaass 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X /\ y e. Y ) ) -> ( ( z ( +g ` G ) w ) .(+) y ) = ( z .(+) ( w .(+) y ) ) )
20 18 19 sylan2br 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( ( z e. X /\ w e. X ) /\ y e. Y ) ) -> ( ( z ( +g ` G ) w ) .(+) y ) = ( z .(+) ( w .(+) y ) ) )
21 20 anassrs 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) /\ y e. Y ) -> ( ( z ( +g ` G ) w ) .(+) y ) = ( z .(+) ( w .(+) y ) ) )
22 21 mpteq2dva 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) -> ( y e. Y |-> ( ( z ( +g ` G ) w ) .(+) y ) ) = ( y e. Y |-> ( z .(+) ( w .(+) y ) ) ) )
23 oveq1 
 |-  ( x = ( z ( +g ` G ) w ) -> ( x .(+) y ) = ( ( z ( +g ` G ) w ) .(+) y ) )
24 23 mpteq2dv 
 |-  ( x = ( z ( +g ` G ) w ) -> ( y e. Y |-> ( x .(+) y ) ) = ( y e. Y |-> ( ( z ( +g ` G ) w ) .(+) y ) ) )
25 7 adantr 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) -> G e. Grp )
26 simprl 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) -> z e. X )
27 simprr 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) -> w e. X )
28 1 5 grpcl 
 |-  ( ( G e. Grp /\ z e. X /\ w e. X ) -> ( z ( +g ` G ) w ) e. X )
29 25 26 27 28 syl3anc 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) -> ( z ( +g ` G ) w ) e. X )
30 8 adantr 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) -> Y e. _V )
31 30 mptexd 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) -> ( y e. Y |-> ( ( z ( +g ` G ) w ) .(+) y ) ) e. _V )
32 3 24 29 31 fvmptd3 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) -> ( F ` ( z ( +g ` G ) w ) ) = ( y e. Y |-> ( ( z ( +g ` G ) w ) .(+) y ) ) )
33 17 adantr 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) -> F : X --> ( Base ` H ) )
34 33 26 ffvelcdmd 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) -> ( F ` z ) e. ( Base ` H ) )
35 33 27 ffvelcdmd 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) -> ( F ` w ) e. ( Base ` H ) )
36 2 4 6 symgov 
 |-  ( ( ( F ` z ) e. ( Base ` H ) /\ ( F ` w ) e. ( Base ` H ) ) -> ( ( F ` z ) ( +g ` H ) ( F ` w ) ) = ( ( F ` z ) o. ( F ` w ) ) )
37 34 35 36 syl2anc 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) -> ( ( F ` z ) ( +g ` H ) ( F ` w ) ) = ( ( F ` z ) o. ( F ` w ) ) )
38 1 gaf 
 |-  ( .(+) e. ( G GrpAct Y ) -> .(+) : ( X X. Y ) --> Y )
39 38 ad2antrr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) /\ y e. Y ) -> .(+) : ( X X. Y ) --> Y )
40 27 adantr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) /\ y e. Y ) -> w e. X )
41 simpr 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) /\ y e. Y ) -> y e. Y )
42 39 40 41 fovcdmd 
 |-  ( ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) /\ y e. Y ) -> ( w .(+) y ) e. Y )
43 oveq1 
 |-  ( x = w -> ( x .(+) y ) = ( w .(+) y ) )
44 43 mpteq2dv 
 |-  ( x = w -> ( y e. Y |-> ( x .(+) y ) ) = ( y e. Y |-> ( w .(+) y ) ) )
45 30 mptexd 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) -> ( y e. Y |-> ( w .(+) y ) ) e. _V )
46 3 44 27 45 fvmptd3 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) -> ( F ` w ) = ( y e. Y |-> ( w .(+) y ) ) )
47 oveq1 
 |-  ( x = z -> ( x .(+) y ) = ( z .(+) y ) )
48 47 mpteq2dv 
 |-  ( x = z -> ( y e. Y |-> ( x .(+) y ) ) = ( y e. Y |-> ( z .(+) y ) ) )
49 30 mptexd 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) -> ( y e. Y |-> ( z .(+) y ) ) e. _V )
50 3 48 26 49 fvmptd3 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) -> ( F ` z ) = ( y e. Y |-> ( z .(+) y ) ) )
51 oveq2 
 |-  ( y = x -> ( z .(+) y ) = ( z .(+) x ) )
52 51 cbvmptv 
 |-  ( y e. Y |-> ( z .(+) y ) ) = ( x e. Y |-> ( z .(+) x ) )
53 50 52 eqtrdi 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) -> ( F ` z ) = ( x e. Y |-> ( z .(+) x ) ) )
54 oveq2 
 |-  ( x = ( w .(+) y ) -> ( z .(+) x ) = ( z .(+) ( w .(+) y ) ) )
55 42 46 53 54 fmptco 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) -> ( ( F ` z ) o. ( F ` w ) ) = ( y e. Y |-> ( z .(+) ( w .(+) y ) ) ) )
56 37 55 eqtrd 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) -> ( ( F ` z ) ( +g ` H ) ( F ` w ) ) = ( y e. Y |-> ( z .(+) ( w .(+) y ) ) ) )
57 22 32 56 3eqtr4d 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) -> ( F ` ( z ( +g ` G ) w ) ) = ( ( F ` z ) ( +g ` H ) ( F ` w ) ) )
58 1 4 5 6 7 10 17 57 isghmd 
 |-  ( .(+) e. ( G GrpAct Y ) -> F e. ( G GrpHom H ) )