grpsubid1

Description: Subtraction of the identity from a group element. (Contributed by Mario Carneiro, 14-Jan-2015)

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

Step	Hyp	Ref	Expression
1		grpsubid.b	$⊢ B = {Base}_{G}$
2		grpsubid.o	$⊢ \underset{˙}{0} = 0_{G}$
3		grpsubid.m	$⊢ \underset{˙}{-} = -_{G}$
4		id	$⊢ X \in B \to X \in B$
5	1 2	grpidcl	$⊢ G \in Grp \to \underset{˙}{0} \in B$
6		eqid	$⊢ +_{G} = +_{G}$
7		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
8	1 6 7 3	grpsubval	$⊢ (X \in B \land \underset{˙}{0} \in B) \to X \underset{˙}{-} \underset{˙}{0} = X +_{G} {inv}_{g} (G) (\underset{˙}{0})$
9	4 5 8	syl2anr	$⊢ (G \in Grp \land X \in B) \to X \underset{˙}{-} \underset{˙}{0} = X +_{G} {inv}_{g} (G) (\underset{˙}{0})$
10	2 7	grpinvid	$⊢ G \in Grp \to {inv}_{g} (G) (\underset{˙}{0}) = \underset{˙}{0}$
11	10	adantr	$⊢ (G \in Grp \land X \in B) \to {inv}_{g} (G) (\underset{˙}{0}) = \underset{˙}{0}$
12	11	oveq2d	$⊢ (G \in Grp \land X \in B) \to X +_{G} {inv}_{g} (G) (\underset{˙}{0}) = X +_{G} \underset{˙}{0}$
13	1 6 2	grprid	$⊢ (G \in Grp \land X \in B) \to X +_{G} \underset{˙}{0} = X$
14	9 12 13	3eqtrd	$⊢ (G \in Grp \land X \in B) \to X \underset{˙}{-} \underset{˙}{0} = X$

Metamath Proof Explorer