grpinva

Description: Deduce right inverse 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	grprinvlem.c	$⊢ (φ \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
	grprinvlem.o	$⊢ φ \to O \in B$
	grprinvlem.i	$⊢ (φ \land x \in B) \to O \underset{˙}{+} x = x$
	grprinvlem.a	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
	grprinvlem.n	$⊢ (φ \land x \in B) \to \exists y \in B y \underset{˙}{+} x = O$
	grpinva.x	$⊢ (φ \land ψ) \to X \in B$
	grpinva.n	$⊢ (φ \land ψ) \to N \in B$
	grpinva.e	$⊢ (φ \land ψ) \to N \underset{˙}{+} X = O$
Assertion	grpinva	$⊢ (φ \land ψ) \to X \underset{˙}{+} N = O$

Proof

Step	Hyp	Ref	Expression
1		grprinvlem.c	$⊢ (φ \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
2		grprinvlem.o	$⊢ φ \to O \in B$
3		grprinvlem.i	$⊢ (φ \land x \in B) \to O \underset{˙}{+} x = x$
4		grprinvlem.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		grprinvlem.n	$⊢ (φ \land x \in B) \to \exists y \in B y \underset{˙}{+} x = O$
6		grpinva.x	$⊢ (φ \land ψ) \to X \in B$
7		grpinva.n	$⊢ (φ \land ψ) \to N \in B$
8		grpinva.e	$⊢ (φ \land ψ) \to N \underset{˙}{+} X = O$
9	1	3expb	$⊢ (φ \land (x \in B \land y \in B)) \to x \underset{˙}{+} y \in B$
10	9	caovclg	$⊢ (φ \land (u \in B \land v \in B)) \to u \underset{˙}{+} v \in B$
11	10	adantlr	$⊢ ((φ \land ψ) \land (u \in B \land v \in B)) \to u \underset{˙}{+} v \in B$
12	11 6 7	caovcld	$⊢ (φ \land ψ) \to X \underset{˙}{+} N \in B$
13	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)$
14	13	adantlr	$⊢ ((φ \land ψ) \land (u \in B \land v \in B \land w \in B)) \to (u \underset{˙}{+} v) \underset{˙}{+} w = u \underset{˙}{+} (v \underset{˙}{+} w)$
15	14 6 7 12	caovassd	$⊢ (φ \land ψ) \to (X \underset{˙}{+} N) \underset{˙}{+} (X \underset{˙}{+} N) = X \underset{˙}{+} (N \underset{˙}{+} (X \underset{˙}{+} N))$
16	8	oveq1d	$⊢ (φ \land ψ) \to (N \underset{˙}{+} X) \underset{˙}{+} N = O \underset{˙}{+} N$
17	14 7 6 7	caovassd	$⊢ (φ \land ψ) \to (N \underset{˙}{+} X) \underset{˙}{+} N = N \underset{˙}{+} (X \underset{˙}{+} N)$
18		oveq2	$⊢ y = N \to O \underset{˙}{+} y = O \underset{˙}{+} N$
19		id	$⊢ y = N \to y = N$
20	18 19	eqeq12d	$⊢ y = N \to (O \underset{˙}{+} y = y \leftrightarrow O \underset{˙}{+} N = N)$
21	3	ralrimiva	$⊢ φ \to \forall x \in B O \underset{˙}{+} x = x$
22		oveq2	$⊢ x = y \to O \underset{˙}{+} x = O \underset{˙}{+} y$
23		id	$⊢ x = y \to x = y$
24	22 23	eqeq12d	$⊢ x = y \to (O \underset{˙}{+} x = x \leftrightarrow O \underset{˙}{+} y = y)$
25	24	cbvralvw	$⊢ \forall x \in B O \underset{˙}{+} x = x \leftrightarrow \forall y \in B O \underset{˙}{+} y = y$
26	21 25	sylib	$⊢ φ \to \forall y \in B O \underset{˙}{+} y = y$
27	26	adantr	$⊢ (φ \land ψ) \to \forall y \in B O \underset{˙}{+} y = y$
28	20 27 7	rspcdva	$⊢ (φ \land ψ) \to O \underset{˙}{+} N = N$
29	16 17 28	3eqtr3d	$⊢ (φ \land ψ) \to N \underset{˙}{+} (X \underset{˙}{+} N) = N$
30	29	oveq2d	$⊢ (φ \land ψ) \to X \underset{˙}{+} (N \underset{˙}{+} (X \underset{˙}{+} N)) = X \underset{˙}{+} N$
31	15 30	eqtrd	$⊢ (φ \land ψ) \to (X \underset{˙}{+} N) \underset{˙}{+} (X \underset{˙}{+} N) = X \underset{˙}{+} N$
32	1 2 3 4 5 12 31	grprinvlem	$⊢ (φ \land ψ) \to X \underset{˙}{+} N = O$

Metamath Proof Explorer

Theorem grpinva

Proof