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 ) )