Theorem symgov

Description: The value of the group operation of the symmetric group on A . (Contributed by Paul Chapman, 25-Feb-2008) (Revised by Mario Carneiro, 28-Jan-2015) (Revised by AV, 30-Mar-2024)

	Ref	Expression
Hypotheses	symgov.1	|- G = ( SymGrp ` A )
	symgov.2	|- B = ( Base ` G )
	symgov.3	|- .+ = ( +g ` G )
Assertion	symgov	|- ( ( X e. B /\ Y e. B ) -> ( X .+ Y ) = ( X o. Y ) )

Proof

Step	Hyp	Ref	Expression
1		symgov.1	|- G = ( SymGrp ` A )
2		symgov.2	|- B = ( Base ` G )
3		symgov.3	|- .+ = ( +g ` G )
4		eqid	|- ( A ^m A ) = ( A ^m A )
5	1 4 3	symgplusg	|- .+ = ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) )
6	5	a1i	|- ( ( X e. B /\ Y e. B ) -> .+ = ( f e. ( A ^m A ) , g e. ( A ^m A ) |-> ( f o. g ) ) )
7		simpl	|- ( ( f = X /\ g = Y ) -> f = X )
8		simpr	|- ( ( f = X /\ g = Y ) -> g = Y )
9	7 8	coeq12d	|- ( ( f = X /\ g = Y ) -> ( f o. g ) = ( X o. Y ) )
10	9	adantl	|- ( ( ( X e. B /\ Y e. B ) /\ ( f = X /\ g = Y ) ) -> ( f o. g ) = ( X o. Y ) )
11	1 2	symgbasmap	|- ( X e. B -> X e. ( A ^m A ) )
12	11	adantr	|- ( ( X e. B /\ Y e. B ) -> X e. ( A ^m A ) )
13	1 2	symgbasmap	|- ( Y e. B -> Y e. ( A ^m A ) )
14	13	adantl	|- ( ( X e. B /\ Y e. B ) -> Y e. ( A ^m A ) )
15		coexg	|- ( ( X e. B /\ Y e. B ) -> ( X o. Y ) e. _V )
16	6 10 12 14 15	ovmpod	|- ( ( X e. B /\ Y e. B ) -> ( X .+ Y ) = ( X o. Y ) )