grprinv

Description: The right inverse of a group element. (Contributed by NM, 24-Aug-2011) (Revised by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Hypotheses	grpinv.b	$⊢ B = {Base}_{G}$
	grpinv.p	$⊢ \underset{˙}{+} = +_{G}$
	grpinv.u	$⊢ \underset{˙}{0} = 0_{G}$
	grpinv.n	$⊢ N = {inv}_{g} (G)$
Assertion	grprinv	$⊢ (G \in Grp \land X \in B) \to X \underset{˙}{+} N (X) = \underset{˙}{0}$

Step	Hyp	Ref	Expression
1		grpinv.b	$⊢ B = {Base}_{G}$
2		grpinv.p	$⊢ \underset{˙}{+} = +_{G}$
3		grpinv.u	$⊢ \underset{˙}{0} = 0_{G}$
4		grpinv.n	$⊢ N = {inv}_{g} (G)$
5	1 2	grpcl	$⊢ (G \in Grp \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
6	1 3	grpidcl	$⊢ G \in Grp \to \underset{˙}{0} \in B$
7	1 2 3	grplid	$⊢ (G \in Grp \land x \in B) \to \underset{˙}{0} \underset{˙}{+} x = x$
8	1 2	grpass	$⊢ (G \in Grp \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
9	1 2 3	grpinvex	$⊢ (G \in Grp \land x \in B) \to \exists y \in B y \underset{˙}{+} x = \underset{˙}{0}$
10		simpr	$⊢ (G \in Grp \land X \in B) \to X \in B$
11	1 4	grpinvcl	$⊢ (G \in Grp \land X \in B) \to N (X) \in B$
12	1 2 3 4	grplinv	$⊢ (G \in Grp \land X \in B) \to N (X) \underset{˙}{+} X = \underset{˙}{0}$
13	5 6 7 8 9 10 11 12	grpinva	$⊢ (G \in Grp \land X \in B) \to X \underset{˙}{+} N (X) = \underset{˙}{0}$

Metamath Proof Explorer