grpsubinv

Step	Hyp	Ref	Expression
1		grpsubinv.b	$⊢ B = {Base}_{G}$
2		grpsubinv.p	$⊢ \underset{˙}{+} = +_{G}$
3		grpsubinv.m	$⊢ \underset{˙}{-} = -_{G}$
4		grpsubinv.n	$⊢ N = {inv}_{g} (G)$
5		grpsubinv.g	$⊢ φ \to G \in Grp$
6		grpsubinv.x	$⊢ φ \to X \in B$
7		grpsubinv.y	$⊢ φ \to Y \in B$
8	1 4	grpinvcl	$⊢ (G \in Grp \land Y \in B) \to N (Y) \in B$
9	5 7 8	syl2anc	$⊢ φ \to N (Y) \in B$
10	1 2 4 3	grpsubval	$⊢ (X \in B \land N (Y) \in B) \to X \underset{˙}{-} N (Y) = X \underset{˙}{+} N (N (Y))$
11	6 9 10	syl2anc	$⊢ φ \to X \underset{˙}{-} N (Y) = X \underset{˙}{+} N (N (Y))$
12	1 4	grpinvinv	$⊢ (G \in Grp \land Y \in B) \to N (N (Y)) = Y$
13	5 7 12	syl2anc	$⊢ φ \to N (N (Y)) = Y$
14	13	oveq2d	$⊢ φ \to X \underset{˙}{+} N (N (Y)) = X \underset{˙}{+} Y$
15	11 14	eqtrd	$⊢ φ \to X \underset{˙}{-} N (Y) = X \underset{˙}{+} Y$

Metamath Proof Explorer