grpinvsub

Description: Inverse of a group subtraction. (Contributed by NM, 9-Sep-2014)

	Ref	Expression
Hypotheses	grpsubcl.b	$⊢ B = {Base}_{G}$
	grpsubcl.m	$⊢ \underset{˙}{-} = -_{G}$
	grpinvsub.n	$⊢ N = {inv}_{g} (G)$
Assertion	grpinvsub	$⊢ (G \in Grp \land X \in B \land Y \in B) \to N (X \underset{˙}{-} Y) = Y \underset{˙}{-} X$

Step	Hyp	Ref	Expression
1		grpsubcl.b	$⊢ B = {Base}_{G}$
2		grpsubcl.m	$⊢ \underset{˙}{-} = -_{G}$
3		grpinvsub.n	$⊢ N = {inv}_{g} (G)$
4	1 3	grpinvcl	$⊢ (G \in Grp \land Y \in B) \to N (Y) \in B$
5	4	3adant2	$⊢ (G \in Grp \land X \in B \land Y \in B) \to N (Y) \in B$
6		eqid	$⊢ +_{G} = +_{G}$
7	1 6 3	grpinvadd	$⊢ (G \in Grp \land X \in B \land N (Y) \in B) \to N (X +_{G} N (Y)) = N (N (Y)) +_{G} N (X)$
8	5 7	syld3an3	$⊢ (G \in Grp \land X \in B \land Y \in B) \to N (X +_{G} N (Y)) = N (N (Y)) +_{G} N (X)$
9	1 3	grpinvinv	$⊢ (G \in Grp \land Y \in B) \to N (N (Y)) = Y$
10	9	3adant2	$⊢ (G \in Grp \land X \in B \land Y \in B) \to N (N (Y)) = Y$
11	10	oveq1d	$⊢ (G \in Grp \land X \in B \land Y \in B) \to N (N (Y)) +_{G} N (X) = Y +_{G} N (X)$
12	8 11	eqtrd	$⊢ (G \in Grp \land X \in B \land Y \in B) \to N (X +_{G} N (Y)) = Y +_{G} N (X)$
13	1 6 3 2	grpsubval	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{-} Y = X +_{G} N (Y)$
14	13	3adant1	$⊢ (G \in Grp \land X \in B \land Y \in B) \to X \underset{˙}{-} Y = X +_{G} N (Y)$
15	14	fveq2d	$⊢ (G \in Grp \land X \in B \land Y \in B) \to N (X \underset{˙}{-} Y) = N (X +_{G} N (Y))$
16	1 6 3 2	grpsubval	$⊢ (Y \in B \land X \in B) \to Y \underset{˙}{-} X = Y +_{G} N (X)$
17	16	ancoms	$⊢ (X \in B \land Y \in B) \to Y \underset{˙}{-} X = Y +_{G} N (X)$
18	17	3adant1	$⊢ (G \in Grp \land X \in B \land Y \in B) \to Y \underset{˙}{-} X = Y +_{G} N (X)$
19	12 15 18	3eqtr4d	$⊢ (G \in Grp \land X \in B \land Y \in B) \to N (X \underset{˙}{-} Y) = Y \underset{˙}{-} X$

Metamath Proof Explorer