grpinvex

Description: Every member of a group has a left inverse. (Contributed by NM, 16-Aug-2011) (Revised by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Hypotheses	grpcl.b	$⊢ B = {Base}_{G}$
	grpcl.p	$⊢ \underset{˙}{+} = +_{G}$
	grpinvex.p	$⊢ \underset{˙}{0} = 0_{G}$
Assertion	grpinvex	$⊢ (G \in Grp \land X \in B) \to \exists y \in B y \underset{˙}{+} X = \underset{˙}{0}$

Step	Hyp	Ref	Expression
1		grpcl.b	$⊢ B = {Base}_{G}$
2		grpcl.p	$⊢ \underset{˙}{+} = +_{G}$
3		grpinvex.p	$⊢ \underset{˙}{0} = 0_{G}$
4	1 2 3	isgrp	$⊢ G \in Grp \leftrightarrow (G \in Mnd \land \forall x \in B \exists y \in B y \underset{˙}{+} x = \underset{˙}{0})$
5	4	simprbi	$⊢ G \in Grp \to \forall x \in B \exists y \in B y \underset{˙}{+} x = \underset{˙}{0}$
6		oveq2	$⊢ x = X \to y \underset{˙}{+} x = y \underset{˙}{+} X$
7	6	eqeq1d	$⊢ x = X \to (y \underset{˙}{+} x = \underset{˙}{0} \leftrightarrow y \underset{˙}{+} X = \underset{˙}{0})$
8	7	rexbidv	$⊢ x = X \to (\exists y \in B y \underset{˙}{+} x = \underset{˙}{0} \leftrightarrow \exists y \in B y \underset{˙}{+} X = \underset{˙}{0})$
9	8	rspccva	$⊢ (\forall x \in B \exists y \in B y \underset{˙}{+} x = \underset{˙}{0} \land X \in B) \to \exists y \in B y \underset{˙}{+} X = \underset{˙}{0}$
10	5 9	sylan	$⊢ (G \in Grp \land X \in B) \to \exists y \in B y \underset{˙}{+} X = \underset{˙}{0}$

Metamath Proof Explorer