Theorem symgsubg

Description: The value of the group subtraction operation of the symmetric group. (Contributed by Thierry Arnoux, 15-Oct-2023)

	Ref	Expression
Hypotheses	symgsubg.g	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
	symgsubg.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	symgsubg.m	⊢ − = ( -g ‘ 𝐺 )
Assertion	symgsubg	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 − 𝑌 ) = ( 𝑋 ∘ ◡ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		symgsubg.g	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2		symgsubg.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
3		symgsubg.m	⊢ − = ( -g ‘ 𝐺 )
4		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
5		eqid	⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
6	2 4 5 3	grpsubval	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 − 𝑌 ) = ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) )
7	1 2 5	symginv	⊢ ( 𝑌 ∈ 𝐵 → ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) = ◡ 𝑌 )
8	7	adantl	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) = ◡ 𝑌 )
9	8	oveq2d	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) = ( 𝑋 ( +g ‘ 𝐺 ) ◡ 𝑌 ) )
10	1 2	elbasfv	⊢ ( 𝑋 ∈ 𝐵 → 𝐴 ∈ V )
11	1	symggrp	⊢ ( 𝐴 ∈ V → 𝐺 ∈ Grp )
12	10 11	syl	⊢ ( 𝑋 ∈ 𝐵 → 𝐺 ∈ Grp )
13	2 5	grpinvcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ∈ 𝐵 )
14	12 13	sylan	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ∈ 𝐵 )
15	8 14	eqeltrrd	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ◡ 𝑌 ∈ 𝐵 )
16	1 2 4	symgov	⊢ ( ( 𝑋 ∈ 𝐵 ∧ ◡ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( +g ‘ 𝐺 ) ◡ 𝑌 ) = ( 𝑋 ∘ ◡ 𝑌 ) )
17	15 16	syldan	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( +g ‘ 𝐺 ) ◡ 𝑌 ) = ( 𝑋 ∘ ◡ 𝑌 ) )
18	6 9 17	3eqtrd	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 − 𝑌 ) = ( 𝑋 ∘ ◡ 𝑌 ) )