Theorem 5oalem7 9605

Description: Lemma for orthoarguesian law 5OA.

Hypotheses

Ref	Expression
5oalem5.1	|- A e. SH
5oalem5.2	|- B e. SH
5oalem5.3	|- C e. SH
5oalem5.4	|- D e. SH
5oalem5.5	|- F e. SH
5oalem5.6	|- G e. SH
5oalem5.7	|- R e. SH
5oalem5.8	|- S e. SH

Assertion

Ref	Expression
5oalem7	|- (((A +H B) i^i (C +H D)) i^i ((F +H G) i^i (R +H S))) (_ (B +H (A i^i (C +H ((((A +H C) i^i (B +H D)) i^i (((A +H R) i^i (B +H S)) +H ((C +H R) i^i (D +H S)))) i^i ((((A +H F) i^i (B +H G)) i^i (((A +H R) i^i (B +H S)) +H ((F +H R) i^i (G +H S)))) +H (((C +H F) i^i (D +H G)) i^i (((C +H R) i^i (D +H S)) +H ((F +H R) i^i (G +H S)))))))))

Proof of Theorem 5oalem7

Step	Hyp	Ref	Expression
1		ee4anv 1325	. . . 4 |- (E.xE.yE.fE.g(E.zE.w(((x e. A /\ y e. B) /\ h = (x +h y)) /\ ((z e. C /\ w e. D) /\ h = (z +h w))) /\ E.vE.u(((f e. F /\ g e. G) /\ h = (f +h g)) /\ ((v e. R /\ u e. S) /\ h = (v +h u)))) <-> (E.xE.yE.zE.w(((x e. A /\ y e. B) /\ h = (x +h y)) /\ ((z e. C /\ w e. D) /\ h = (z +h w))) /\ E.fE.gE.vE.u(((f e. F /\ g e. G) /\ h = (f +h g)) /\ ((v e. R /\ u e. S) /\ h = (v +h u)))))
2		exrot4 1100	. . . . . 6 |- (E.zE.wE.fE.gE.vE.u((((x e. A /\ y e. B) /\ h = (x +h y)) /\ ((z e. C /\ w e. D) /\ h = (z +h w))) /\ (((f e. F /\ g e. G) /\ h = (f +h g)) /\ ((v e. R /\ u e. S) /\ h = (v +h u)))) <-> E.fE.gE.zE.wE.vE.u((((x e. A /\ y e. B) /\ h = (x +h y)) /\ ((z e. C /\ w e. D) /\ h = (z +h w))) /\ (((f e. F /\ g e. G) /\ h = (f +h g)) /\ ((v e. R /\ u e. S) /\ h = (v +h u)))))
3		ee4anv 1325	. . . . . . 7 |- (E.zE.wE.vE.u((((x e. A /\ y e. B) /\ h = (x +h y)) /\ ((z e. C /\ w e. D) /\ h = (z +h w))) /\ (((f e. F /\ g e. G) /\ h = (f +h g)) /\ ((v e. R /\ u e. S) /\ h = (v +h u)))) <-> (E.zE.w(((x e. A /\ y e. B) /\ h = (x +h y)) /\ ((z e. C /\ w e. D) /\ h = (z +h w))) /\ E.vE.u(((f e. F /\ g e. G) /\ h = (f +h g)) /\ ((v e. R /\ u e. S) /\ h = (v +h u)))))
4	3	2exbii 1052	. . . . . 6 |- (E.fE.gE.zE.wE.vE.u((((x e. A /\ y e. B) /\ h = (x +h y)) /\ ((z e. C /\ w e. D) /\ h = (z +h w))) /\ (((f e. F /\ g e. G) /\ h = (f +h g)) /\ ((v e. R /\ u e. S) /\ h = (v +h u)))) <-> E.fE.g(E.zE.w(((x e. A /\ y e. B) /\ h = (x +h y)) /\ ((z e. C /\ w e. D) /\ h = (z +h w))) /\ E.vE.u(((f e. F /\ g e. G) /\ h = (f +h g)) /\ ((v e. R /\ u e. S) /\ h = (v +h u)))))
5	2, 4	bitr 173	. . . . 5 |- (E.zE.wE.fE.gE.vE.u((((x e. A /\ y e. B) /\ h = (x +h y)) /\ ((z e. C /\ w e. D) /\ h = (z +h w))) /\ (((f e. F /\ g e. G) /\ h = (f +h g)) /\ ((v e. R /\ u e. S) /\ h = (v +h u)))) <-> E.fE.g(E.zE.w(((x e. A /\ y e. B) /\ h = (x +h y)) /\ ((z e. C /\ w e. D) /\ h = (z +h w))) /\ E.vE.u(((f e. F /\ g e. G) /\ h = (f +h g)) /\ ((v e. R /\ u e. S) /\ h = (v +h u)))))
6	5	2exbii 1052	. . . 4 |- (E.xE.yE.zE.wE.fE.gE.vE.u((((x e. A /\ y e. B) /\ h = (x +h y)) /\ ((z e. C /\ w e. D) /\ h = (z +h w))) /\ (((f e. F /\ g e. G) /\ h = (f +h g)) /\ ((v e. R /\ u e. S) /\ h = (v +h u)))) <-> E.xE.yE.fE.g(E.zE.w(((x e. A /\ y e. B) /\ h = (x +h y)) /\ ((z e. C /\ w e. D) /\ h = (z +h w))) /\ E.vE.u(((f e. F /\ g e. G) /\ h = (f +h g)) /\ ((v e. R /\ u e. S) /\ h = (v +h u)))))
7		elin 2207	. . . . 5 |- (h e. (((A +H B) i^i (C +H D)) i^i ((F +H G) i^i (R +H S))) <-> (h e. ((A +H B) i^i (C +H D)) /\ h e. ((F +H G) i^i (R +H S))))
8		5oalem5.1	. . . . . . . . . 10 |- A e. SH
9		5oalem5.2	. . . . . . . . . 10 |- B e. SH
10	8, 9	shsel 9280	. . . . . . . . 9 |- (h e. (A +H B) <-> E.x e. A E.y e. B h = (x +h y))
11		r2ex 1691	. . . . . . . . 9 |- (E.x e. A E.y e. B h = (x +h y) <-> E.xE.y((x e. A /\ y e. B) /\ h = (x +h y)))
12	10, 11	bitr 173	. . . . . . . 8 |- (h e. (A +H B) <-> E.xE.y((x e. A /\ y e. B) /\ h = (x +h y)))
13		5oalem5.3	. . . . . . . . . 10 |- C e. SH
14		5oalem5.4	. . . . . . . . . 10 |- D e. SH
15	13, 14	shsel 9280	. . . . . . . . 9 |- (h e. (C +H D) <-> E.z e. C E.w e. D h = (z +h w))
16		r2ex 1691	. . . . . . . . 9 |- (E.z e. C E.w e. D h = (z +h w) <-> E.zE.w((z e. C /\ w e. D) /\ h = (z +h w)))
17	15, 16	bitr 173	. . . . . . . 8 |- (h e. (C +H D) <-> E.zE.w((z e. C /\ w e. D) /\ h = (z +h w)))
18	12, 17	anbi12i 482	. . . . . . 7 |- ((h e. (A +H B) /\ h e. (C +H D)) <-> (E.xE.y((x e. A /\ y e. B) /\ h = (x +h y)) /\ E.zE.w((z e. C /\ w e. D) /\ h = (z +h w))))
19		elin 2207	. . . . . . 7 |- (h e. ((A +H B) i^i (C +H D)) <-> (h e. (A +H B) /\ h e. (C +H D)))
20		ee4anv 1325	. . . . . . 7 |- (E.xE.yE.zE.w(((x e. A /\ y e. B) /\ h = (x +h y)) /\ ((z e. C /\ w e. D) /\ h = (z +h w))) <-> (E.xE.y((x e. A /\ y e. B) /\ h = (x +h y)) /\ E.zE.w((z e. C /\ w e. D) /\ h = (z +h w))))
21	18, 19, 20	3bitr4r 184	. . . . . 6 |- (E.xE.yE.zE.w(((x e. A /\ y e. B) /\ h = (x +h y)) /\ ((z e. C /\ w e. D) /\ h = (z +h w))) <-> h e. ((A +H B) i^i (C +H D)))
22		5oalem5.5	. . . . . . . . . 10 |- F e. SH
23		5oalem5.6	. . . . . . . . . 10 |- G e. SH
24	22, 23	shsel 9280	. . . . . . . . 9 |- (h e. (F +H G) <-> E.f e. F E.g e. G h = (f +h g))
25		r2ex 1691	. . . . . . . . 9 |- (E.f e. F E.g e. G h = (f +h g) <-> E.fE.g((f e. F /\ g e. G) /\ h = (f +h g)))
26	24, 25	bitr 173	. . . . . . . 8 |- (h e. (F +H G) <-> E.fE.g((f e. F /\ g e. G) /\ h = (f +h g)))
27		5oalem5.7	. . . . . . . . . 10 |- R e. SH
28		5oalem5.8	. . . . . . . . . 10 |- S e. SH
29	27, 28	shsel 9280	. . . . . . . . 9 |- (h e. (R +H S) <-> E.v e. R E.u e. S h = (v +h u))
30		r2ex 1691	. . . . . . . . 9 |- (E.v e. R E.u e. S h = (v +h u) <-> E.vE.u((v e. R /\ u e. S) /\ h = (v +h u))