This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grplinv

Description: The left 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	grplinv	$⊢ (G \in Grp \land X \in B) \to N (X) \underset{˙}{+} X = \underset{˙}{0}$

Proof

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 3 4	grpinvval	$⊢ X \in B \to N (X) = (ι y \in B \| y \underset{˙}{+} X = \underset{˙}{0})$
6	5	adantl	$⊢ (G \in Grp \land X \in B) \to N (X) = (ι y \in B \| y \underset{˙}{+} X = \underset{˙}{0})$
7	1 2 3	grpinveu	$⊢ (G \in Grp \land X \in B) \to \exists! y \in B y \underset{˙}{+} X = \underset{˙}{0}$
8		riotacl2	$⊢ \exists! y \in B y \underset{˙}{+} X = \underset{˙}{0} \to (ι y \in B \| y \underset{˙}{+} X = \underset{˙}{0}) \in \{y \in B \| y \underset{˙}{+} X = \underset{˙}{0}\}$
9	7 8	syl	$⊢ (G \in Grp \land X \in B) \to (ι y \in B \| y \underset{˙}{+} X = \underset{˙}{0}) \in \{y \in B \| y \underset{˙}{+} X = \underset{˙}{0}\}$
10	6 9	eqeltrd	$⊢ (G \in Grp \land X \in B) \to N (X) \in \{y \in B \| y \underset{˙}{+} X = \underset{˙}{0}\}$
11		oveq1	$⊢ y = N (X) \to y \underset{˙}{+} X = N (X) \underset{˙}{+} X$
12	11	eqeq1d	$⊢ y = N (X) \to (y \underset{˙}{+} X = \underset{˙}{0} \leftrightarrow N (X) \underset{˙}{+} X = \underset{˙}{0})$
13	12	elrab	$⊢ N (X) \in \{y \in B \| y \underset{˙}{+} X = \underset{˙}{0}\} \leftrightarrow (N (X) \in B \land N (X) \underset{˙}{+} X = \underset{˙}{0})$
14	13	simprbi	$⊢ N (X) \in \{y \in B \| y \underset{˙}{+} X = \underset{˙}{0}\} \to N (X) \underset{˙}{+} X = \underset{˙}{0}$
15	10 14	syl	$⊢ (G \in Grp \land X \in B) \to N (X) \underset{˙}{+} X = \underset{˙}{0}$