grprida

Description: Deduce right identity from left inverse and left identity in an associative structure (such as a group). (Contributed by NM, 10-Aug-2013) (Proof shortened by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Hypotheses	grpinva.c	$⊢ (φ \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
	grpinva.o	$⊢ φ \to O \in B$
	grpinva.i	$⊢ (φ \land x \in B) \to O \underset{˙}{+} x = x$
	grpinva.a	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
	grpinva.r	$⊢ (φ \land x \in B) \to \exists y \in B y \underset{˙}{+} x = O$
Assertion	grprida	$⊢ (φ \land x \in B) \to x \underset{˙}{+} O = x$

Proof

Step	Hyp	Ref	Expression
1		grpinva.c	$⊢ (φ \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
2		grpinva.o	$⊢ φ \to O \in B$
3		grpinva.i	$⊢ (φ \land x \in B) \to O \underset{˙}{+} x = x$
4		grpinva.a	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
5		grpinva.r	$⊢ (φ \land x \in B) \to \exists y \in B y \underset{˙}{+} x = O$
6		oveq1	$⊢ y = n \to y \underset{˙}{+} x = n \underset{˙}{+} x$
7	6	eqeq1d	$⊢ y = n \to (y \underset{˙}{+} x = O \leftrightarrow n \underset{˙}{+} x = O)$
8	7	cbvrexvw	$⊢ \exists y \in B y \underset{˙}{+} x = O \leftrightarrow \exists n \in B n \underset{˙}{+} x = O$
9	5 8	sylib	$⊢ (φ \land x \in B) \to \exists n \in B n \underset{˙}{+} x = O$
10	4	caovassg	$⊢ (φ \land (u \in B \land v \in B \land w \in B)) \to (u \underset{˙}{+} v) \underset{˙}{+} w = u \underset{˙}{+} (v \underset{˙}{+} w)$
11	10	adantlr	$⊢ ((φ \land (x \in B \land (n \in B \land n \underset{˙}{+} x = O))) \land (u \in B \land v \in B \land w \in B)) \to (u \underset{˙}{+} v) \underset{˙}{+} w = u \underset{˙}{+} (v \underset{˙}{+} w)$
12		simprl	$⊢ (φ \land (x \in B \land (n \in B \land n \underset{˙}{+} x = O))) \to x \in B$
13		simprrl	$⊢ (φ \land (x \in B \land (n \in B \land n \underset{˙}{+} x = O))) \to n \in B$
14	11 12 13 12	caovassd	$⊢ (φ \land (x \in B \land (n \in B \land n \underset{˙}{+} x = O))) \to (x \underset{˙}{+} n) \underset{˙}{+} x = x \underset{˙}{+} (n \underset{˙}{+} x)$
15		simprrr	$⊢ (φ \land (x \in B \land (n \in B \land n \underset{˙}{+} x = O))) \to n \underset{˙}{+} x = O$
16	1 2 3 4 5 12 13 15	grpinva	$⊢ (φ \land (x \in B \land (n \in B \land n \underset{˙}{+} x = O))) \to x \underset{˙}{+} n = O$
17	16	oveq1d	$⊢ (φ \land (x \in B \land (n \in B \land n \underset{˙}{+} x = O))) \to (x \underset{˙}{+} n) \underset{˙}{+} x = O \underset{˙}{+} x$
18	15	oveq2d	$⊢ (φ \land (x \in B \land (n \in B \land n \underset{˙}{+} x = O))) \to x \underset{˙}{+} (n \underset{˙}{+} x) = x \underset{˙}{+} O$
19	14 17 18	3eqtr3d	$⊢ (φ \land (x \in B \land (n \in B \land n \underset{˙}{+} x = O))) \to O \underset{˙}{+} x = x \underset{˙}{+} O$
20	19	anassrs	$⊢ ((φ \land x \in B) \land (n \in B \land n \underset{˙}{+} x = O)) \to O \underset{˙}{+} x = x \underset{˙}{+} O$
21	9 20	rexlimddv	$⊢ (φ \land x \in B) \to O \underset{˙}{+} x = x \underset{˙}{+} O$
22	21 3	eqtr3d	$⊢ (φ \land x \in B) \to x \underset{˙}{+} O = x$

Metamath Proof Explorer

Theorem grprida

Proof