Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  curgrpact Unicode version

Theorem curgrpact 25475
 Description: The currying of a group action is a group homomorphism between the group and the symmetry group . (Contributed by FL, 17-May-2010.) (Proof shortened by Mario Carneiro, 13-Jan-2015.)
Assertion
Ref Expression
curgrpact

Proof of Theorem curgrpact
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvex 5555 . . . . . 6
21a1i 10 . . . . 5
3 gaset 14763 . . . . . 6
43adantr 451 . . . . 5
5 simpr 447 . . . . 5
6 eqid 2296 . . . . . . . 8
76gaf 14765 . . . . . . 7
87adantr 451 . . . . . 6
9 ffn 5405 . . . . . 6
108, 9syl 15 . . . . 5
11 domrancur1c 25305 . . . . 5
122, 4, 5, 10, 11syl22anc 1183 . . . 4
1312feqmptd 5591 . . 3
14 valcurfn2 25308 . . . . . . 7
15143expia 1153 . . . . . 6
162, 4, 5, 10, 15syl22anc 1183 . . . . 5
1716imp 418 . . . 4
1817mpteq2dva 4122 . . 3
1913, 18eqtrd 2328 . 2
20 eqid 2296 . . . 4
21 eqid 2296 . . . 4
226, 20, 21galactghm 14799 . . 3