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 = {Base}_{G}$
	grpsubid.o	$⊢ \underset{˙}{0} = 0_{G}$
	grpsubid.m	$⊢ \underset{˙}{-} = -_{G}$
	grpsubadd0sub.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	grpsubadd0sub	$⊢ (G \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{-} Y = X \underset{˙}{+} (\underset{˙}{0} \underset{˙}{-} Y)$

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

Metamath Proof Explorer