Theorem grpsubadd0sub

Description: Subtraction expressed as addition of the difference of the identity element and the subtrahend. (Contributed by AV, 9-Nov-2019)

	Ref	Expression
Hypotheses	grpsubid.b	$$⊢B={\mathrm{Base}}_G$$
	grpsubid.o	$$⊢\underset{\dot{}}{0}=0_G$$
	grpsubid.m	$$⊢\underset{\dot{}}{-}={-}_G$$
	grpsubadd0sub.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	grpsubadd0sub	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{-}Y=X\underset{\dot{}}{+}\left(\underset{\dot{}}{0}\underset{\dot{}}{-}Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		grpsubid.b	$$⊢B={\mathrm{Base}}_G$$
2		grpsubid.o	$$⊢\underset{\dot{}}{0}=0_G$$
3		grpsubid.m	$$⊢\underset{\dot{}}{-}={-}_G$$
4		grpsubadd0sub.p	$$⊢\underset{\dot{}}{+}={+}_G$$
5		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
6	1 4 5 3	grpsubval	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{-}Y=X\underset{\dot{}}{+}{inv}_g\left(G\right)\left(Y\right)$$
7	6	3adant1	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{-}Y=X\underset{\dot{}}{+}{inv}_g\left(G\right)\left(Y\right)$$
8	1 3 5 2	grpinvval2	$$⊢\left(G\in \mathrm{Grp}\wedge Y\in B\right)\to {inv}_g\left(G\right)\left(Y\right)=\underset{\dot{}}{0}\underset{\dot{}}{-}Y$$
9	8	3adant2	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\wedge Y\in B\right)\to {inv}_g\left(G\right)\left(Y\right)=\underset{\dot{}}{0}\underset{\dot{}}{-}Y$$
10	9	oveq2d	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}{inv}_g\left(G\right)\left(Y\right)=X\underset{\dot{}}{+}\left(\underset{\dot{}}{0}\underset{\dot{}}{-}Y\right)$$
11	7 10	eqtrd	$$⊢\left(G\in \mathrm{Grp}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{-}Y=X\underset{\dot{}}{+}\left(\underset{\dot{}}{0}\underset{\dot{}}{-}Y\right)$$