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=\mathrm{SymGrp}\left(A\right)$$
	symgov.2	$$⊢B={\mathrm{Base}}_G$$
	symgov.3	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	symgov	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y=X\circ Y$$

Proof

Step	Hyp	Ref	Expression
1		symgov.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		symgov.2	$$⊢B={\mathrm{Base}}_G$$
3		symgov.3	$$⊢\underset{\dot{}}{+}={+}_G$$
4		eqid	$$⊢A^A=A^A$$
5	1 4 3	symgplusg	$$⊢\underset{\dot{}}{+}=\left(f\in \left(A^A\right),g\in \left(A^A\right)⟼f\circ g\right)$$
6	5	a1i	$$⊢\left(X\in B\wedge Y\in B\right)\to \underset{\dot{}}{+}=\left(f\in \left(A^A\right),g\in \left(A^A\right)⟼f\circ g\right)$$
7		simpl	$$⊢\left(f=X\wedge g=Y\right)\to f=X$$
8		simpr	$$⊢\left(f=X\wedge g=Y\right)\to g=Y$$
9	7 8	coeq12d	$$⊢\left(f=X\wedge g=Y\right)\to f\circ g=X\circ Y$$
10	9	adantl	$$⊢\left(\left(X\in B\wedge Y\in B\right)\wedge \left(f=X\wedge g=Y\right)\right)\to f\circ g=X\circ Y$$
11	1 2	symgbasmap	$$⊢X\in B\to X\in \left(A^A\right)$$
12	11	adantr	$$⊢\left(X\in B\wedge Y\in B\right)\to X\in \left(A^A\right)$$
13	1 2	symgbasmap	$$⊢Y\in B\to Y\in \left(A^A\right)$$
14	13	adantl	$$⊢\left(X\in B\wedge Y\in B\right)\to Y\in \left(A^A\right)$$
15		coexg	$$⊢\left(X\in B\wedge Y\in B\right)\to X\circ Y\in \mathrm{V}$$
16	6 10 12 14 15	ovmpod	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y=X\circ Y$$