Theorem grprinvd

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	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y\in B$$
	grprinvlem.o	$$⊢\phi \to O\in B$$
	grprinvlem.i	$$⊢\left(\phi \wedge x\in B\right)\to O\underset{\dot{}}{+}x=x$$
	grprinvlem.a	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)$$
	grprinvlem.n	$$⊢\left(\phi \wedge x\in B\right)\to \exists y\in By\underset{\dot{}}{+}x=O$$
	grprinvd.x	$$⊢\left(\phi \wedge \psi \right)\to X\in B$$
	grprinvd.n	$$⊢\left(\phi \wedge \psi \right)\to N\in B$$
	grprinvd.e	$$⊢\left(\phi \wedge \psi \right)\to N\underset{\dot{}}{+}X=O$$
Assertion	grprinvd	$$⊢\left(\phi \wedge \psi \right)\to X\underset{\dot{}}{+}N=O$$

Proof

Step	Hyp	Ref	Expression
1		grprinvlem.c	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y\in B$$
2		grprinvlem.o	$$⊢\phi \to O\in B$$
3		grprinvlem.i	$$⊢\left(\phi \wedge x\in B\right)\to O\underset{\dot{}}{+}x=x$$
4		grprinvlem.a	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)$$
5		grprinvlem.n	$$⊢\left(\phi \wedge x\in B\right)\to \exists y\in By\underset{\dot{}}{+}x=O$$
6		grprinvd.x	$$⊢\left(\phi \wedge \psi \right)\to X\in B$$
7		grprinvd.n	$$⊢\left(\phi \wedge \psi \right)\to N\in B$$
8		grprinvd.e	$$⊢\left(\phi \wedge \psi \right)\to N\underset{\dot{}}{+}X=O$$
9	1	3expb	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x\underset{\dot{}}{+}y\in B$$
10	9	caovclg	$$⊢\left(\phi \wedge \left(u\in B\wedge v\in B\right)\right)\to u\underset{\dot{}}{+}v\in B$$
11	10	adantlr	$$⊢\left(\left(\phi \wedge \psi \right)\wedge \left(u\in B\wedge v\in B\right)\right)\to u\underset{\dot{}}{+}v\in B$$
12	11 6 7	caovcld	$$⊢\left(\phi \wedge \psi \right)\to X\underset{\dot{}}{+}N\in B$$
13	4	caovassg	$$⊢\left(\phi \wedge \left(u\in B\wedge v\in B\wedge w\in B\right)\right)\to \left(u\underset{\dot{}}{+}v\right)\underset{\dot{}}{+}w=u\underset{\dot{}}{+}\left(v\underset{\dot{}}{+}w\right)$$
14	13	adantlr	$$⊢\left(\left(\phi \wedge \psi \right)\wedge \left(u\in B\wedge v\in B\wedge w\in B\right)\right)\to \left(u\underset{\dot{}}{+}v\right)\underset{\dot{}}{+}w=u\underset{\dot{}}{+}\left(v\underset{\dot{}}{+}w\right)$$
15	14 6 7 12	caovassd	$$⊢\left(\phi \wedge \psi \right)\to \left(X\underset{\dot{}}{+}N\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}N\right)=X\underset{\dot{}}{+}\left(N\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}N\right)\right)$$
16	8	oveq1d	$$⊢\left(\phi \wedge \psi \right)\to \left(N\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}N=O\underset{\dot{}}{+}N$$
17	14 7 6 7	caovassd	$$⊢\left(\phi \wedge \psi \right)\to \left(N\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}N=N\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}N\right)$$
18		oveq2	$$⊢y=N\to O\underset{\dot{}}{+}y=O\underset{\dot{}}{+}N$$
19		id	$$⊢y=N\to y=N$$
20	18 19	eqeq12d	$$⊢y=N\to \left(O\underset{\dot{}}{+}y=y\leftrightarrow O\underset{\dot{}}{+}N=N\right)$$
21	3	ralrimiva	$$⊢\phi \to \forall x\in BO\underset{\dot{}}{+}x=x$$
22		oveq2	$$⊢x=y\to O\underset{\dot{}}{+}x=O\underset{\dot{}}{+}y$$
23		id	$$⊢x=y\to x=y$$
24	22 23	eqeq12d	$$⊢x=y\to \left(O\underset{\dot{}}{+}x=x\leftrightarrow O\underset{\dot{}}{+}y=y\right)$$
25	24	cbvralvw	$$⊢\forall x\in BO\underset{\dot{}}{+}x=x\leftrightarrow \forall y\in BO\underset{\dot{}}{+}y=y$$
26	21 25	sylib	$$⊢\phi \to \forall y\in BO\underset{\dot{}}{+}y=y$$
27	26	adantr	$$⊢\left(\phi \wedge \psi \right)\to \forall y\in BO\underset{\dot{}}{+}y=y$$
28	20 27 7	rspcdva	$$⊢\left(\phi \wedge \psi \right)\to O\underset{\dot{}}{+}N=N$$
29	16 17 28	3eqtr3d	$$⊢\left(\phi \wedge \psi \right)\to N\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}N\right)=N$$
30	29	oveq2d	$$⊢\left(\phi \wedge \psi \right)\to X\underset{\dot{}}{+}\left(N\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}N\right)\right)=X\underset{\dot{}}{+}N$$
31	15 30	eqtrd	$$⊢\left(\phi \wedge \psi \right)\to \left(X\underset{\dot{}}{+}N\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}N\right)=X\underset{\dot{}}{+}N$$
32	1 2 3 4 5 12 31	grprinvlem	$$⊢\left(\phi \wedge \psi \right)\to X\underset{\dot{}}{+}N=O$$