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=\mathrm{SymGrp}\left(A\right)$$
	symgsubg.b	$$⊢B={\mathrm{Base}}_G$$
	symgsubg.m	$$⊢\underset{\dot{}}{-}={-}_G$$
Assertion	symgsubg	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{-}Y=X\circ Y^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		symgsubg.g	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		symgsubg.b	$$⊢B={\mathrm{Base}}_G$$
3		symgsubg.m	$$⊢\underset{\dot{}}{-}={-}_G$$
4		eqid	$$⊢{+}_G={+}_G$$
5		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
6	2 4 5 3	grpsubval	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{-}Y=X{+}_G{inv}_g\left(G\right)\left(Y\right)$$
7	1 2 5	symginv	$$⊢Y\in B\to {inv}_g\left(G\right)\left(Y\right)=Y^{-1}$$
8	7	adantl	$$⊢\left(X\in B\wedge Y\in B\right)\to {inv}_g\left(G\right)\left(Y\right)=Y^{-1}$$
9	8	oveq2d	$$⊢\left(X\in B\wedge Y\in B\right)\to X{+}_G{inv}_g\left(G\right)\left(Y\right)=X{+}_G{Y}^{-1}$$
10	1 2	elbasfv	$$⊢X\in B\to A\in \mathrm{V}$$
11	1	symggrp	$$⊢A\in \mathrm{V}\to G\in \mathrm{Grp}$$
12	10 11	syl	$$⊢X\in B\to G\in \mathrm{Grp}$$
13	2 5	grpinvcl	$$⊢\left(G\in \mathrm{Grp}\wedge Y\in B\right)\to {inv}_g\left(G\right)\left(Y\right)\in B$$
14	12 13	sylan	$$⊢\left(X\in B\wedge Y\in B\right)\to {inv}_g\left(G\right)\left(Y\right)\in B$$
15	8 14	eqeltrrd	$$⊢\left(X\in B\wedge Y\in B\right)\to Y^{-1}\in B$$
16	1 2 4	symgov	$$⊢\left(X\in B\wedge Y^{-1}\in B\right)\to X{+}_G{Y}^{-1}=X\circ Y^{-1}$$
17	15 16	syldan	$$⊢\left(X\in B\wedge Y\in B\right)\to X{+}_G{Y}^{-1}=X\circ Y^{-1}$$
18	6 9 17	3eqtrd	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{-}Y=X\circ Y^{-1}$$