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)

Ref Expression
Hypotheses symgplusg.1 G = SymGrp A
symgplusg.2 B = A A
symgplusg.3 + ˙ = + G
Assertion symgplusg + ˙ = f B , g B f g

Proof

Step Hyp Ref Expression
1 symgplusg.1 G = SymGrp A
2 symgplusg.2 B = A A
3 symgplusg.3 + ˙ = + G
4 permsetex A V f | f : A 1-1 onto A V
5 eqid Could not format ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) = ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) : No typesetting found for |- ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) = ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) with typecode |-
6 eqid Could not format ( +g ` ( EndoFMnd ` A ) ) = ( +g ` ( EndoFMnd ` A ) ) : No typesetting found for |- ( +g ` ( EndoFMnd ` A ) ) = ( +g ` ( EndoFMnd ` A ) ) with typecode |-
7 5 6 ressplusg Could not format ( { f | f : A -1-1-onto-> A } e. _V -> ( +g ` ( EndoFMnd ` A ) ) = ( +g ` ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) ) ) : No typesetting found for |- ( { f | f : A -1-1-onto-> A } e. _V -> ( +g ` ( EndoFMnd ` A ) ) = ( +g ` ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) ) ) with typecode |-
8 4 7 syl Could not format ( A e. _V -> ( +g ` ( EndoFMnd ` A ) ) = ( +g ` ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) ) ) : No typesetting found for |- ( A e. _V -> ( +g ` ( EndoFMnd ` A ) ) = ( +g ` ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) ) ) with typecode |-
9 eqid f | f : A 1-1 onto A = f | f : A 1-1 onto A
10 1 9 symgval Could not format G = ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) : No typesetting found for |- G = ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) with typecode |-
11 10 eqcomi Could not format ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) = G : No typesetting found for |- ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) = G with typecode |-
12 11 fveq2i Could not format ( +g ` ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) ) = ( +g ` G ) : No typesetting found for |- ( +g ` ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) ) = ( +g ` G ) with typecode |-
13 8 12 eqtrdi Could not format ( A e. _V -> ( +g ` ( EndoFMnd ` A ) ) = ( +g ` G ) ) : No typesetting found for |- ( A e. _V -> ( +g ` ( EndoFMnd ` A ) ) = ( +g ` G ) ) with typecode |-
14 fvprc Could not format ( -. A e. _V -> ( EndoFMnd ` A ) = (/) ) : No typesetting found for |- ( -. A e. _V -> ( EndoFMnd ` A ) = (/) ) with typecode |-
15 fvprc ¬ A V SymGrp A =
16 1 15 syl5req ¬ A V = G
17 14 16 eqtrd Could not format ( -. A e. _V -> ( EndoFMnd ` A ) = G ) : No typesetting found for |- ( -. A e. _V -> ( EndoFMnd ` A ) = G ) with typecode |-
18 17 fveq2d Could not format ( -. A e. _V -> ( +g ` ( EndoFMnd ` A ) ) = ( +g ` G ) ) : No typesetting found for |- ( -. A e. _V -> ( +g ` ( EndoFMnd ` A ) ) = ( +g ` G ) ) with typecode |-
19 13 18 pm2.61i Could not format ( +g ` ( EndoFMnd ` A ) ) = ( +g ` G ) : No typesetting found for |- ( +g ` ( EndoFMnd ` A ) ) = ( +g ` G ) with typecode |-
20 eqid Could not format ( EndoFMnd ` A ) = ( EndoFMnd ` A ) : No typesetting found for |- ( EndoFMnd ` A ) = ( EndoFMnd ` A ) with typecode |-
21 eqid Could not format ( Base ` ( EndoFMnd ` A ) ) = ( Base ` ( EndoFMnd ` A ) ) : No typesetting found for |- ( Base ` ( EndoFMnd ` A ) ) = ( Base ` ( EndoFMnd ` A ) ) with typecode |-
22 20 21 efmndbas Could not format ( Base ` ( EndoFMnd ` A ) ) = ( A ^m A ) : No typesetting found for |- ( Base ` ( EndoFMnd ` A ) ) = ( A ^m A ) with typecode |-
23 2 22 eqtr4i Could not format B = ( Base ` ( EndoFMnd ` A ) ) : No typesetting found for |- B = ( Base ` ( EndoFMnd ` A ) ) with typecode |-
24 20 23 6 efmndplusg Could not format ( +g ` ( EndoFMnd ` A ) ) = ( f e. B , g e. B |-> ( f o. g ) ) : No typesetting found for |- ( +g ` ( EndoFMnd ` A ) ) = ( f e. B , g e. B |-> ( f o. g ) ) with typecode |-
25 3 19 24 3eqtr2i + ˙ = f B , g B f g