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

Metamath Proof Explorer

Theorem grplrinv

Description: In a group, every member has a left and right inverse. (Contributed by AV, 1-Sep-2021)

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

Proof

Step	Hyp	Ref	Expression
1		grplrinv.b	$⊢ B = {Base}_{G}$
2		grplrinv.p	$⊢ \underset{˙}{+} = +_{G}$
3		grplrinv.i	$⊢ \underset{˙}{0} = 0_{G}$
4		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
5	1 4	grpinvcl	$⊢ (G \in Grp \land x \in B) \to {inv}_{g} (G) (x) \in B$
6		oveq1	$⊢ y = {inv}_{g} (G) (x) \to y \underset{˙}{+} x = {inv}_{g} (G) (x) \underset{˙}{+} x$
7	6	eqeq1d	$⊢ y = {inv}_{g} (G) (x) \to (y \underset{˙}{+} x = \underset{˙}{0} \leftrightarrow {inv}_{g} (G) (x) \underset{˙}{+} x = \underset{˙}{0})$
8		oveq2	$⊢ y = {inv}_{g} (G) (x) \to x \underset{˙}{+} y = x \underset{˙}{+} {inv}_{g} (G) (x)$
9	8	eqeq1d	$⊢ y = {inv}_{g} (G) (x) \to (x \underset{˙}{+} y = \underset{˙}{0} \leftrightarrow x \underset{˙}{+} {inv}_{g} (G) (x) = \underset{˙}{0})$
10	7 9	anbi12d	$⊢ y = {inv}_{g} (G) (x) \to ((y \underset{˙}{+} x = \underset{˙}{0} \land x \underset{˙}{+} y = \underset{˙}{0}) \leftrightarrow ({inv}_{g} (G) (x) \underset{˙}{+} x = \underset{˙}{0} \land x \underset{˙}{+} {inv}_{g} (G) (x) = \underset{˙}{0}))$
11	10	adantl	$⊢ ((G \in Grp \land x \in B) \land y = {inv}_{g} (G) (x)) \to ((y \underset{˙}{+} x = \underset{˙}{0} \land x \underset{˙}{+} y = \underset{˙}{0}) \leftrightarrow ({inv}_{g} (G) (x) \underset{˙}{+} x = \underset{˙}{0} \land x \underset{˙}{+} {inv}_{g} (G) (x) = \underset{˙}{0}))$
12	1 2 3 4	grplinv	$⊢ (G \in Grp \land x \in B) \to {inv}_{g} (G) (x) \underset{˙}{+} x = \underset{˙}{0}$
13	1 2 3 4	grprinv	$⊢ (G \in Grp \land x \in B) \to x \underset{˙}{+} {inv}_{g} (G) (x) = \underset{˙}{0}$
14	12 13	jca	$⊢ (G \in Grp \land x \in B) \to ({inv}_{g} (G) (x) \underset{˙}{+} x = \underset{˙}{0} \land x \underset{˙}{+} {inv}_{g} (G) (x) = \underset{˙}{0})$
15	5 11 14	rspcedvd	$⊢ (G \in Grp \land x \in B) \to \exists y \in B (y \underset{˙}{+} x = \underset{˙}{0} \land x \underset{˙}{+} y = \underset{˙}{0})$
16	15	ralrimiva	$⊢ G \in Grp \to \forall x \in B \exists y \in B (y \underset{˙}{+} x = \underset{˙}{0} \land x \underset{˙}{+} y = \underset{˙}{0})$