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	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
	symgplusg.2	⊢ 𝐵 = ( 𝐴 ↑m 𝐴 )
	symgplusg.3	⊢ + = ( +g ‘ 𝐺 )
Assertion	symgplusg	⊢ + = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) )

Proof

Step	Hyp	Ref	Expression
1		symgplusg.1	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2		symgplusg.2	⊢ 𝐵 = ( 𝐴 ↑m 𝐴 )
3		symgplusg.3	⊢ + = ( +g ‘ 𝐺 )
4		f1osetex	⊢ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ∈ V
5		eqid	⊢ ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ) = ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } )
6		eqid	⊢ ( +g ‘ ( EndoFMnd ‘ 𝐴 ) ) = ( +g ‘ ( EndoFMnd ‘ 𝐴 ) )
7	5 6	ressplusg	⊢ ( { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ∈ V → ( +g ‘ ( EndoFMnd ‘ 𝐴 ) ) = ( +g ‘ ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ) ) )
8	4 7	ax-mp	⊢ ( +g ‘ ( EndoFMnd ‘ 𝐴 ) ) = ( +g ‘ ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ) )
9		eqid	⊢ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } = { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 }
10	1 9	symgval	⊢ 𝐺 = ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } )
11	10	eqcomi	⊢ ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ) = 𝐺
12	11	fveq2i	⊢ ( +g ‘ ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ) ) = ( +g ‘ 𝐺 )
13	8 12	eqtri	⊢ ( +g ‘ ( EndoFMnd ‘ 𝐴 ) ) = ( +g ‘ 𝐺 )
14		eqid	⊢ ( EndoFMnd ‘ 𝐴 ) = ( EndoFMnd ‘ 𝐴 )
15		eqid	⊢ ( Base ‘ ( EndoFMnd ‘ 𝐴 ) ) = ( Base ‘ ( EndoFMnd ‘ 𝐴 ) )
16	14 15	efmndbas	⊢ ( Base ‘ ( EndoFMnd ‘ 𝐴 ) ) = ( 𝐴 ↑m 𝐴 )
17	2 16	eqtr4i	⊢ 𝐵 = ( Base ‘ ( EndoFMnd ‘ 𝐴 ) )
18	14 17 6	efmndplusg	⊢ ( +g ‘ ( EndoFMnd ‘ 𝐴 ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) )
19	3 13 18	3eqtr2i	⊢ + = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑓 ∘ 𝑔 ) )