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	|- G = ( SymGrp ` A )
	symgsubg.b	|- B = ( Base ` G )
	symgsubg.m	|- .- = ( -g ` G )
Assertion	symgsubg	|- ( ( X e. B /\ Y e. B ) -> ( X .- Y ) = ( X o. `' Y ) )

Proof

Step	Hyp	Ref	Expression
1		symgsubg.g	|- G = ( SymGrp ` A )
2		symgsubg.b	|- B = ( Base ` G )
3		symgsubg.m	|- .- = ( -g ` G )
4		eqid	|- ( +g ` G ) = ( +g ` G )
5		eqid	|- ( invg ` G ) = ( invg ` G )
6	2 4 5 3	grpsubval	|- ( ( X e. B /\ Y e. B ) -> ( X .- Y ) = ( X ( +g ` G ) ( ( invg ` G ) ` Y ) ) )
7	1 2 5	symginv	|- ( Y e. B -> ( ( invg ` G ) ` Y ) = `' Y )
8	7	adantl	|- ( ( X e. B /\ Y e. B ) -> ( ( invg ` G ) ` Y ) = `' Y )
9	8	oveq2d	|- ( ( X e. B /\ Y e. B ) -> ( X ( +g ` G ) ( ( invg ` G ) ` Y ) ) = ( X ( +g ` G ) `' Y ) )
10	1 2	elbasfv	|- ( X e. B -> A e. _V )
11	1	symggrp	|- ( A e. _V -> G e. Grp )
12	10 11	syl	|- ( X e. B -> G e. Grp )
13	2 5	grpinvcl	|- ( ( G e. Grp /\ Y e. B ) -> ( ( invg ` G ) ` Y ) e. B )
14	12 13	sylan	|- ( ( X e. B /\ Y e. B ) -> ( ( invg ` G ) ` Y ) e. B )
15	8 14	eqeltrrd	|- ( ( X e. B /\ Y e. B ) -> `' Y e. B )
16	1 2 4	symgov	|- ( ( X e. B /\ `' Y e. B ) -> ( X ( +g ` G ) `' Y ) = ( X o. `' Y ) )
17	15 16	syldan	|- ( ( X e. B /\ Y e. B ) -> ( X ( +g ` G ) `' Y ) = ( X o. `' Y ) )
18	6 9 17	3eqtrd	|- ( ( X e. B /\ Y e. B ) -> ( X .- Y ) = ( X o. `' Y ) )