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=\mathrm{SymGrp}\left(A\right)$$
	symgplusg.2	$$⊢B=A^A$$
	symgplusg.3	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	symgplusg	$$⊢\underset{\dot{}}{+}=\left(f\in B,g\in B⟼f\circ g\right)$$

Proof

Step	Hyp	Ref	Expression
1		symgplusg.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		symgplusg.2	$$⊢B=A^A$$
3		symgplusg.3	$$⊢\underset{\dot{}}{+}={+}_G$$
4		f1osetex	$$⊢\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}\in \mathrm{V}$$
5		eqid	$$⊢\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}=\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}$$
6		eqid	$$⊢{+}_{\mathrm{EndoFMnd}\left(A\right)}={+}_{\mathrm{EndoFMnd}\left(A\right)}$$
7	5 6	ressplusg	$$⊢\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}\in \mathrm{V}\to {+}_{\mathrm{EndoFMnd}\left(A\right)}={+}_{\left(\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}\right)}$$
8	4 7	ax-mp	$$⊢{+}_{\mathrm{EndoFMnd}\left(A\right)}={+}_{\left(\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}\right)}$$
9		eqid	$$⊢\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}=\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}$$
10	1 9	symgval	$$⊢G=\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}$$
11	10	eqcomi	$$⊢\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}=G$$
12	11	fveq2i	$$⊢{+}_{\left(\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}\right)}={+}_G$$
13	8 12	eqtri	$$⊢{+}_{\mathrm{EndoFMnd}\left(A\right)}={+}_G$$
14		eqid	$$⊢\mathrm{EndoFMnd}\left(A\right)=\mathrm{EndoFMnd}\left(A\right)$$
15		eqid	$$⊢{\mathrm{Base}}_{\mathrm{EndoFMnd}\left(A\right)}={\mathrm{Base}}_{\mathrm{EndoFMnd}\left(A\right)}$$
16	14 15	efmndbas	$$⊢{\mathrm{Base}}_{\mathrm{EndoFMnd}\left(A\right)}=A^A$$
17	2 16	eqtr4i	$$⊢B={\mathrm{Base}}_{\mathrm{EndoFMnd}\left(A\right)}$$
18	14 17 6	efmndplusg	$$⊢{+}_{\mathrm{EndoFMnd}\left(A\right)}=\left(f\in B,g\in B⟼f\circ g\right)$$
19	3 13 18	3eqtr2i	$$⊢\underset{\dot{}}{+}=\left(f\in B,g\in B⟼f\circ g\right)$$