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	ffvelrnd	\|- ( ( .(+) e. ( G GrpAct Y ) /\ ( z e. X /\ w e. X ) ) -> ( F ` z ) e. ( Base ` H ) )
35	33 27	ffvelrnd	\|- ( ( .(+) 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	fovrnd	\|- ( ( ( .(+) 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 ) )

Metamath Proof Explorer

Theorem galactghm

Proof