grpsubid

Description: Subtraction of a group element from itself. (Contributed by NM, 31-Mar-2014)

	Ref	Expression
Hypotheses	grpsubid.b	$⊢ B = {Base}_{G}$
	grpsubid.o	$⊢ \underset{˙}{0} = 0_{G}$
	grpsubid.m	$⊢ \underset{˙}{-} = -_{G}$
Assertion	grpsubid	$⊢ (G \in Grp \land X \in B) \to X \underset{˙}{-} X = \underset{˙}{0}$

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

Metamath Proof Explorer