Theorem grprinvlem

Description: Lemma for grpinva . (Contributed by NM, 9-Aug-2013)

	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$$
	grprinvlem.x	$$⊢\left(\phi \wedge \psi \right)\to X\in B$$
	grprinvlem.e	$$⊢\left(\phi \wedge \psi \right)\to X\underset{\dot{}}{+}X=X$$
Assertion	grprinvlem	$$⊢\left(\phi \wedge \psi \right)\to X=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		grprinvlem.x	$$⊢\left(\phi \wedge \psi \right)\to X\in B$$
7		grprinvlem.e	$$⊢\left(\phi \wedge \psi \right)\to X\underset{\dot{}}{+}X=X$$
8	5	ralrimiva	$$⊢\phi \to \forall x\in B\exists y\in By\underset{\dot{}}{+}x=O$$
9		oveq2	$$⊢x=z\to y\underset{\dot{}}{+}x=y\underset{\dot{}}{+}z$$
10	9	eqeq1d	$$⊢x=z\to \left(y\underset{\dot{}}{+}x=O\leftrightarrow y\underset{\dot{}}{+}z=O\right)$$
11	10	rexbidv	$$⊢x=z\to \left(\exists y\in By\underset{\dot{}}{+}x=O\leftrightarrow \exists y\in By\underset{\dot{}}{+}z=O\right)$$
12	11	cbvralvw	$$⊢\forall x\in B\exists y\in By\underset{\dot{}}{+}x=O\leftrightarrow \forall z\in B\exists y\in By\underset{\dot{}}{+}z=O$$
13	8 12	sylib	$$⊢\phi \to \forall z\in B\exists y\in By\underset{\dot{}}{+}z=O$$
14		oveq2	$$⊢z=X\to y\underset{\dot{}}{+}z=y\underset{\dot{}}{+}X$$
15	14	eqeq1d	$$⊢z=X\to \left(y\underset{\dot{}}{+}z=O\leftrightarrow y\underset{\dot{}}{+}X=O\right)$$
16	15	rexbidv	$$⊢z=X\to \left(\exists y\in By\underset{\dot{}}{+}z=O\leftrightarrow \exists y\in By\underset{\dot{}}{+}X=O\right)$$
17	16	rspccva	$$⊢\left(\forall z\in B\exists y\in By\underset{\dot{}}{+}z=O\wedge X\in B\right)\to \exists y\in By\underset{\dot{}}{+}X=O$$
18	13 6 17	syl2an2r	$$⊢\left(\phi \wedge \psi \right)\to \exists y\in By\underset{\dot{}}{+}X=O$$
19	7	oveq2d	$$⊢\left(\phi \wedge \psi \right)\to y\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}X\right)=y\underset{\dot{}}{+}X$$
20	19	adantr	$$⊢\left(\left(\phi \wedge \psi \right)\wedge \left(y\in B\wedge y\underset{\dot{}}{+}X=O\right)\right)\to y\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}X\right)=y\underset{\dot{}}{+}X$$
21		simprr	$$⊢\left(\left(\phi \wedge \psi \right)\wedge \left(y\in B\wedge y\underset{\dot{}}{+}X=O\right)\right)\to y\underset{\dot{}}{+}X=O$$
22	21	oveq1d	$$⊢\left(\left(\phi \wedge \psi \right)\wedge \left(y\in B\wedge y\underset{\dot{}}{+}X=O\right)\right)\to \left(y\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}X=O\underset{\dot{}}{+}X$$
23	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)$$
24	23	ad4ant14	$$⊢\left(\left(\left(\phi \wedge \psi \right)\wedge \left(y\in B\wedge y\underset{\dot{}}{+}X=O\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)$$
25		simprl	$$⊢\left(\left(\phi \wedge \psi \right)\wedge \left(y\in B\wedge y\underset{\dot{}}{+}X=O\right)\right)\to y\in B$$
26	6	adantr	$$⊢\left(\left(\phi \wedge \psi \right)\wedge \left(y\in B\wedge y\underset{\dot{}}{+}X=O\right)\right)\to X\in B$$
27	24 25 26 26	caovassd	$$⊢\left(\left(\phi \wedge \psi \right)\wedge \left(y\in B\wedge y\underset{\dot{}}{+}X=O\right)\right)\to \left(y\underset{\dot{}}{+}X\right)\underset{\dot{}}{+}X=y\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}X\right)$$
28		oveq2	$$⊢y=X\to O\underset{\dot{}}{+}y=O\underset{\dot{}}{+}X$$
29		id	$$⊢y=X\to y=X$$
30	28 29	eqeq12d	$$⊢y=X\to \left(O\underset{\dot{}}{+}y=y\leftrightarrow O\underset{\dot{}}{+}X=X\right)$$
31	3	ralrimiva	$$⊢\phi \to \forall x\in BO\underset{\dot{}}{+}x=x$$
32		oveq2	$$⊢x=y\to O\underset{\dot{}}{+}x=O\underset{\dot{}}{+}y$$
33		id	$$⊢x=y\to x=y$$
34	32 33	eqeq12d	$$⊢x=y\to \left(O\underset{\dot{}}{+}x=x\leftrightarrow O\underset{\dot{}}{+}y=y\right)$$
35	34	cbvralvw	$$⊢\forall x\in BO\underset{\dot{}}{+}x=x\leftrightarrow \forall y\in BO\underset{\dot{}}{+}y=y$$
36	31 35	sylib	$$⊢\phi \to \forall y\in BO\underset{\dot{}}{+}y=y$$
37	36	adantr	$$⊢\left(\phi \wedge \psi \right)\to \forall y\in BO\underset{\dot{}}{+}y=y$$
38	30 37 6	rspcdva	$$⊢\left(\phi \wedge \psi \right)\to O\underset{\dot{}}{+}X=X$$
39	38	adantr	$$⊢\left(\left(\phi \wedge \psi \right)\wedge \left(y\in B\wedge y\underset{\dot{}}{+}X=O\right)\right)\to O\underset{\dot{}}{+}X=X$$
40	22 27 39	3eqtr3d	$$⊢\left(\left(\phi \wedge \psi \right)\wedge \left(y\in B\wedge y\underset{\dot{}}{+}X=O\right)\right)\to y\underset{\dot{}}{+}\left(X\underset{\dot{}}{+}X\right)=X$$
41	20 40 21	3eqtr3d	$$⊢\left(\left(\phi \wedge \psi \right)\wedge \left(y\in B\wedge y\underset{\dot{}}{+}X=O\right)\right)\to X=O$$
42	18 41	rexlimddv	$$⊢\left(\phi \wedge \psi \right)\to X=O$$