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

Metamath Proof Explorer

Theorem symgplusg

Description: The group operation of a symmetric group is the function composition. (Contributed by Paul Chapman, 25-Feb-2008) (Revised by Mario Carneiro, 28-Jan-2015) (Proof shortened by AV, 19-Feb-2024) (Revised by AV, 29-Mar-2024) (Proof shortened by AV, 14-Aug-2024)

Ref Expression
Hypotheses symgplusg.1 
|- G = ( SymGrp ` A )
symgplusg.2 
|- B = ( A ^m A )
symgplusg.3 
|- .+ = ( +g ` G )
Assertion symgplusg 
|- .+ = ( f e. B , g e. B |-> ( f o. g ) )

Proof

Step Hyp Ref Expression
1 symgplusg.1 
 |-  G = ( SymGrp ` A )
2 symgplusg.2 
 |-  B = ( A ^m A )
3 symgplusg.3 
 |-  .+ = ( +g ` G )
4 f1osetex 
 |-  { f | f : A -1-1-onto-> A } e. _V
5 eqid 
 |-  ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) = ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } )
6 eqid 
 |-  ( +g ` ( EndoFMnd ` A ) ) = ( +g ` ( EndoFMnd ` A ) )
7 5 6 ressplusg 
 |-  ( { f | f : A -1-1-onto-> A } e. _V -> ( +g ` ( EndoFMnd ` A ) ) = ( +g ` ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) ) )
8 4 7 ax-mp 
 |-  ( +g ` ( EndoFMnd ` A ) ) = ( +g ` ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) )
9 eqid 
 |-  { f | f : A -1-1-onto-> A } = { f | f : A -1-1-onto-> A }
10 1 9 symgval 
 |-  G = ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } )
11 10 eqcomi 
 |-  ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) = G
12 11 fveq2i 
 |-  ( +g ` ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) ) = ( +g ` G )
13 8 12 eqtri 
 |-  ( +g ` ( EndoFMnd ` A ) ) = ( +g ` G )
14 eqid 
 |-  ( EndoFMnd ` A ) = ( EndoFMnd ` A )
15 eqid 
 |-  ( Base ` ( EndoFMnd ` A ) ) = ( Base ` ( EndoFMnd ` A ) )
16 14 15 efmndbas 
 |-  ( Base ` ( EndoFMnd ` A ) ) = ( A ^m A )
17 2 16 eqtr4i 
 |-  B = ( Base ` ( EndoFMnd ` A ) )
18 14 17 6 efmndplusg 
 |-  ( +g ` ( EndoFMnd ` A ) ) = ( f e. B , g e. B |-> ( f o. g ) )
19 3 13 18 3eqtr2i 
 |-  .+ = ( f e. B , g e. B |-> ( f o. g ) )