Theorem 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	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y\in B$$
	grpinva.o	$$⊢\phi \to O\in B$$
	grpinva.i	$$⊢\left(\phi \wedge x\in B\right)\to O\underset{\dot{}}{+}x=x$$
	grpinva.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)$$
	grpinva.r	$$⊢\left(\phi \wedge x\in B\right)\to \exists y\in By\underset{\dot{}}{+}x=O$$
Assertion	grprida	$$⊢\left(\phi \wedge x\in B\right)\to x\underset{\dot{}}{+}O=x$$

Proof

Step	Hyp	Ref	Expression
1		grpinva.c	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y\in B$$
2		grpinva.o	$$⊢\phi \to O\in B$$
3		grpinva.i	$$⊢\left(\phi \wedge x\in B\right)\to O\underset{\dot{}}{+}x=x$$
4		grpinva.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		grpinva.r	$$⊢\left(\phi \wedge x\in B\right)\to \exists y\in By\underset{\dot{}}{+}x=O$$
6		oveq1	$$⊢y=n\to y\underset{\dot{}}{+}x=n\underset{\dot{}}{+}x$$
7	6	eqeq1d	$$⊢y=n\to \left(y\underset{\dot{}}{+}x=O\leftrightarrow n\underset{\dot{}}{+}x=O\right)$$
8	7	cbvrexvw	$$⊢\exists y\in By\underset{\dot{}}{+}x=O\leftrightarrow \exists n\in Bn\underset{\dot{}}{+}x=O$$
9	5 8	sylib	$$⊢\left(\phi \wedge x\in B\right)\to \exists n\in Bn\underset{\dot{}}{+}x=O$$
10	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)$$
11	10	adantlr	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge \left(n\in B\wedge n\underset{\dot{}}{+}x=O\right)\right)\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)$$
12		simprl	$$⊢\left(\phi \wedge \left(x\in B\wedge \left(n\in B\wedge n\underset{\dot{}}{+}x=O\right)\right)\right)\to x\in B$$
13		simprrl	$$⊢\left(\phi \wedge \left(x\in B\wedge \left(n\in B\wedge n\underset{\dot{}}{+}x=O\right)\right)\right)\to n\in B$$
14	11 12 13 12	caovassd	$$⊢\left(\phi \wedge \left(x\in B\wedge \left(n\in B\wedge n\underset{\dot{}}{+}x=O\right)\right)\right)\to \left(x\underset{\dot{}}{+}n\right)\underset{\dot{}}{+}x=x\underset{\dot{}}{+}\left(n\underset{\dot{}}{+}x\right)$$
15		simprrr	$$⊢\left(\phi \wedge \left(x\in B\wedge \left(n\in B\wedge n\underset{\dot{}}{+}x=O\right)\right)\right)\to n\underset{\dot{}}{+}x=O$$
16	1 2 3 4 5 12 13 15	grpinva	$$⊢\left(\phi \wedge \left(x\in B\wedge \left(n\in B\wedge n\underset{\dot{}}{+}x=O\right)\right)\right)\to x\underset{\dot{}}{+}n=O$$
17	16	oveq1d	$$⊢\left(\phi \wedge \left(x\in B\wedge \left(n\in B\wedge n\underset{\dot{}}{+}x=O\right)\right)\right)\to \left(x\underset{\dot{}}{+}n\right)\underset{\dot{}}{+}x=O\underset{\dot{}}{+}x$$
18	15	oveq2d	$$⊢\left(\phi \wedge \left(x\in B\wedge \left(n\in B\wedge n\underset{\dot{}}{+}x=O\right)\right)\right)\to x\underset{\dot{}}{+}\left(n\underset{\dot{}}{+}x\right)=x\underset{\dot{}}{+}O$$
19	14 17 18	3eqtr3d	$$⊢\left(\phi \wedge \left(x\in B\wedge \left(n\in B\wedge n\underset{\dot{}}{+}x=O\right)\right)\right)\to O\underset{\dot{}}{+}x=x\underset{\dot{}}{+}O$$
20	19	anassrs	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge \left(n\in B\wedge n\underset{\dot{}}{+}x=O\right)\right)\to O\underset{\dot{}}{+}x=x\underset{\dot{}}{+}O$$
21	9 20	rexlimddv	$$⊢\left(\phi \wedge x\in B\right)\to O\underset{\dot{}}{+}x=x\underset{\dot{}}{+}O$$
22	21 3	eqtr3d	$$⊢\left(\phi \wedge x\in B\right)\to x\underset{\dot{}}{+}O=x$$