This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
		symgov.2	⊢ 𝐵 = ( Base ‘ 𝐺 )
		symgov.3	⊢ + = ( +_g ‘ 𝐺 )
	Assertion	symgov	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) = ( 𝑋 ∘ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		symgov.1	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2		symgov.2	⊢ 𝐵 = ( Base ‘ 𝐺 )
3		symgov.3	⊢ + = ( +_g ‘ 𝐺 )
4		eqid	⊢ ( 𝐴 ↑_m 𝐴 ) = ( 𝐴 ↑_m 𝐴 )
5	1 4 3	symgplusg	⊢ + = ( 𝑓 ∈ ( 𝐴 ↑_m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑_m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) )
6	5	a1i	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → + = ( 𝑓 ∈ ( 𝐴 ↑_m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑_m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) )
7		simpl	⊢ ( ( 𝑓 = 𝑋 ∧ 𝑔 = 𝑌 ) → 𝑓 = 𝑋 )
8		simpr	⊢ ( ( 𝑓 = 𝑋 ∧ 𝑔 = 𝑌 ) → 𝑔 = 𝑌 )
9	7 8	coeq12d	⊢ ( ( 𝑓 = 𝑋 ∧ 𝑔 = 𝑌 ) → ( 𝑓 ∘ 𝑔 ) = ( 𝑋 ∘ 𝑌 ) )
10	9	adantl	⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑓 = 𝑋 ∧ 𝑔 = 𝑌 ) ) → ( 𝑓 ∘ 𝑔 ) = ( 𝑋 ∘ 𝑌 ) )
11	1 2	symgbasmap	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( 𝐴 ↑_m 𝐴 ) )
12	11	adantr	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ ( 𝐴 ↑_m 𝐴 ) )
13	1 2	symgbasmap	⊢ ( 𝑌 ∈ 𝐵 → 𝑌 ∈ ( 𝐴 ↑_m 𝐴 ) )
14	13	adantl	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ ( 𝐴 ↑_m 𝐴 ) )
15		coexg	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∘ 𝑌 ) ∈ V )
16	6 10 12 14 15	ovmpod	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) = ( 𝑋 ∘ 𝑌 ) )