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

Metamath Proof Explorer

Theorem symgga

Description: The symmetric group induces a group action on its base set. (Contributed by Mario Carneiro, 24-Jan-2015)

Ref Expression
Hypotheses symgga.g 
|- G = ( SymGrp ` X )
symgga.b 
|- B = ( Base ` G )
symgga.f 
|- F = ( f e. B , x e. X |-> ( f ` x ) )
Assertion symgga 
|- ( X e. V -> F e. ( G GrpAct X ) )

Proof

Step Hyp Ref Expression
1 symgga.g 
 |-  G = ( SymGrp ` X )
2 symgga.b 
 |-  B = ( Base ` G )
3 symgga.f 
 |-  F = ( f e. B , x e. X |-> ( f ` x ) )
4 1 symggrp 
 |-  ( X e. V -> G e. Grp )
5 2 idghm 
 |-  ( G e. Grp -> ( _I |` B ) e. ( G GrpHom G ) )
6 fvresi 
 |-  ( f e. B -> ( ( _I |` B ) ` f ) = f )
7 6 adantr 
 |-  ( ( f e. B /\ x e. X ) -> ( ( _I |` B ) ` f ) = f )
8 7 fveq1d 
 |-  ( ( f e. B /\ x e. X ) -> ( ( ( _I |` B ) ` f ) ` x ) = ( f ` x ) )
9 8 mpoeq3ia 
 |-  ( f e. B , x e. X |-> ( ( ( _I |` B ) ` f ) ` x ) ) = ( f e. B , x e. X |-> ( f ` x ) )
10 3 9 eqtr4i 
 |-  F = ( f e. B , x e. X |-> ( ( ( _I |` B ) ` f ) ` x ) )
11 2 1 10 lactghmga 
 |-  ( ( _I |` B ) e. ( G GrpHom G ) -> F e. ( G GrpAct X ) )
12 4 5 11 3syl 
 |-  ( X e. V -> F e. ( G GrpAct X ) )