Theorem 5oalem7 5550

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 982	. . . 4 |- (E.xE.yE.fE.g(E.zE.w(((x e. A /\ y e. B) /\ h = (x +v y)) /\ ((z e. C /\ w e. D) /\ h = (z +v w))) /\ E.vE.u(((f e. F /\ g e. G) /\ h = (f +v g)) /\ ((v e. R /\ u e. S) /\ h = (v +v u)))) <-> (E.xE.yE.zE.w(((x e. A /\ y e. B) /\ h = (x +v y)) /\ ((z e. C /\ w e. D) /\ h = (z +v w))) /\ E.fE.gE.vE.u(((f e. F /\ g e. G) /\ h = (f +v g)) /\ ((v e. R /\ u e. S) /\ h = (v +v u)))))
2		exrot4 778	. . . . . 6 |- (E.zE.wE.fE.gE.vE.u((((x e. A /\ y e. B) /\ h = (x +v y)) /\ ((z e. C /\ w e. D) /\ h = (z +v w))) /\ (((f e. F /\ g e. G) /\ h = (f +v g)) /\ ((v e. R /\ u e. S) /\ h = (v +v u)))) <-> E.fE.gE.zE.wE.vE.u((((x e. A /\ y e. B) /\ h = (x +v y)) /\ ((z e. C /\ w e. D) /\ h = (z +v w))) /\ (((f e. F /\ g e. G) /\ h = (f +v g)) /\ ((v e. R /\ u e. S) /\ h = (v +v u)))))
3		ee4anv 982	. . . . . . 7 |- (E.zE.wE.vE.u((((x e. A /\ y e. B) /\ h = (x +v y)) /\ ((z e. C /\ w e. D) /\ h = (z +v w))) /\ (((f e. F /\ g e. G) /\ h = (f +v g)) /\ ((v e. R /\ u e. S) /\ h = (v +v u)))) <-> (E.zE.w(((x e. A /\ y e. B) /\ h = (x +v y)) /\ ((z e. C /\ w e. D) /\ h = (z +v w))) /\ E.vE.u(((f e. F /\ g e. G) /\ h = (f +v g)) /\ ((v e. R /\ u e. S) /\ h = (v +v u)))))
4	3	bi2ex 734	. . . . . 6 |- (E.fE.gE.zE.wE.vE.u((((x e. A /\ y e. B) /\ h = (x +v y)) /\ ((z e. C /\ w e. D) /\ h = (z +v w))) /\ (((f e. F /\ g e. G) /\ h = (f +v g)) /\ ((v e. R /\ u e. S) /\ h = (v +v u)))) <-> E.fE.g(E.zE.w(((x e. A /\ y e. B) /\ h = (x +v y)) /\ ((z e. C /\ w e. D) /\ h = (z +v w))) /\ E.vE.u(((f e. F /\ g e. G) /\ h = (f +v g)) /\ ((v e. R /\ u e. S) /\ h = (v +v u)))))
5	2, 4	bitr 151	. . . . 5 |- (E.zE.wE.fE.gE.vE.u((((x e. A /\ y e. B) /\ h = (x +v y)) /\ ((z e. C /\ w e. D) /\ h = (z +v w))) /\ (((f e. F /\ g e. G) /\ h = (f +v g)) /\ ((v e. R /\ u e. S) /\ h = (v +v u)))) <-> E.fE.g(E.zE.w(((x e. A /\ y e. B) /\ h = (x +v y)) /\ ((z e. C /\ w e. D) /\ h = (z +v w))) /\ E.vE.u(((f e. F /\ g e. G) /\ h = (f +v g)) /\ ((v e. R /\ u e. S) /\ h = (v +v u)))))
6	5	bi2ex 734	. . . 4 |- (E.xE.yE.zE.wE.fE.gE.vE.u((((x e. A /\ y e. B) /\ h = (x +v y)) /\ ((z e. C /\ w e. D) /\ h = (z +v w))) /\ (((f e. F /\ g e. G) /\ h = (f +v g)) /\ ((v e. R /\ u e. S) /\ h = (v +v u)))) <-> E.xE.yE.fE.g(E.zE.w(((x e. A /\ y e. B) /\ h = (x +v y)) /\ ((z e. C /\ w e. D) /\ h = (z +v w))) /\ E.vE.u(((f e. F /\ g e. G) /\ h = (f +v g)) /\ ((v e. R /\ u e. S) /\ h = (v +v u)))))
7		elin 1635	. . . . 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 5281	. . . . . . . . 9 |- (h e. (A +H B) <-> E.x e. A E.y e. B h = (x +v y))
11		r2ex 1241	. . . . . . . . 9 |- (E.x e. A E.y e. B h = (x +v y) <-> E.xE.y((x e. A /\ y e. B) /\ h = (x +v y)))
12	10, 11	bitr 151	. . . . . . . 8 |- (h e. (A +H B) <-> E.xE.y((x e. A /\ y e. B) /\ h = (x +v y)))
13		5oalem5.3	. . . . . . . . . 10 |- C e. SH
14		5oalem5.4	. . . . . . . . . 10 |- D e. SH
15	13, 14	shsel 5281	. . . . . . . . 9 |- (h e. (C +H D) <-> E.z e. C E.w e. D h = (z +v w))
16		r2ex 1241	. . . . . . . . 9 |- (E.z e. C E.w e. D h = (z +v w) <-> E.zE.w((z e. C /\ w e. D) /\ h = (z +v w)))
17	15, 16	bitr 151	. . . . . . . 8 |- (h e. (C +H D) <-> E.zE.w((z e. C /\ w e. D) /\ h = (z +v w)))
18	12, 17	anbi12i 369	. . . . . . 7 |- ((h e. (A +H B) /\ h e. (C +H D)) <-> (E.xE.y((x e. A /\ y e. B) /\ h = (x +v y)) /\ E.zE.w((z e. C /\ w e. D) /\ h = (z +v w))))
19		elin 1635	. . . . . . 7 |- (h e. ((A +H B) i^i (C +H D)) <-> (h e. (A +H B) /\ h e. (C +H D)))
20		ee4anv 982	. . . . . . 7 |- (E.xE.yE.zE.w(((x e. A /\ y e. B) /\ h = (x +v y)) /\ ((z e. C /\ w e. D) /\ h = (z +v w))) <-> (E.xE.y((x e. A /\ y e. B) /\ h = (x +v y)) /\ E.zE.w((z e. C /\ w e. D) /\ h = (z +v w))))
21	18, 19, 20	3bitr4r 159	. . . . . 6 |- (E.xE.yE.zE.w(((x e. A /\ y e. B) /\ h = (x +v y)) /\ ((z e. C /\ w e. D) /\ h = (z +v 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 5281	. . . . . . . . 9 |- (h e. (F +H G) <-> E.f e. F E.g e. G h = (f +v g))
25		r2ex 1241	. . . . . . . . 9 |- (E.f e. F E.g e. G h = (f +v g) <-> E.fE.g((f e. F /\ g e. G) /\ h = (f +v g)))
26	24, 25	bitr 151	. . . . . . . 8 |- (h e. (F +H G) <-> E.fE.g((f e. F /\ g e. G) /\ h = (f +v g)))
27		5oalem5.7	. . . . . . . . . 10 |- R e. SH
28		5oalem5.8	. . . . . . . . . 10 |- S e. SH
29	27, 28	shsel 5281	. . . . . . . . 9 |- (h e. (R +H S) <-> E.v e. R E.u e. S h = (v +v u))
30		r2ex 1241	. . . . . . . . 9 |- (E.v e. R E.u e. S h = (v +v u) <-> E.vE.u((v e. R /\ u e. S) /\ h = (v +v u)))
31	29, 30	bitr 151	. . . . . . . 8 |- (h e. (R +H S) <-> E.vE.u((v e. R /\