Theorem 5oalem6 9604

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

5oalem6

|- (((((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)))) -> h e. (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 5oalem6

Step	Hyp	Ref	Expression
1		eqeq1 1481	. . . . . . . . . . . 12 |- (h = (x +h y) -> (h = (v +h u) <-> (x +h y) = (v +h u)))
2	1	biimpcd 155	. . . . . . . . . . 11 |- (h = (v +h u) -> (h = (x +h y) -> (x +h y) = (v +h u)))
3		eqeq1 1481	. . . . . . . . . . . 12 |- (h = (z +h w) -> (h = (v +h u) <-> (z +h w) = (v +h u)))
4	3	biimpcd 155	. . . . . . . . . . 11 |- (h = (v +h u) -> (h = (z +h w) -> (z +h w) = (v +h u)))
5	2, 4	anim12d 558	. . . . . . . . . 10 |- (h = (v +h u) -> ((h = (x +h y) /\ h = (z +h w)) -> ((x +h y) = (v +h u) /\ (z +h w) = (v +h u))))
6		eqeq1 1481	. . . . . . . . . . 11 |- (h = (f +h g) -> (h = (v +h u) <-> (f +h g) = (v +h u)))
7	6	biimpcd 155	. . . . . . . . . 10 |- (h = (v +h u) -> (h = (f +h g) -> (f +h g) = (v +h u)))
8	5, 7	anim12d 558	. . . . . . . . 9 |- (h = (v +h u) -> (((h = (x +h y) /\ h = (z +h w)) /\ h = (f +h g)) -> (((x +h y) = (v +h u) /\ (z +h w) = (v +h u)) /\ (f +h g) = (v +h u))))
9	8	exp3a 375	. . . . . . . 8 |- (h = (v +h u) -> ((h = (x +h y) /\ h = (z +h w)) -> (h = (f +h g) -> (((x +h y) = (v +h u) /\ (z +h w) = (v +h u)) /\ (f +h g) = (v +h u)))))
10	9	com3l 34	. . . . . . 7 |- ((h = (x +h y) /\ h = (z +h w)) -> (h = (f +h g) -> (h = (v +h u) -> (((x +h y) = (v +h u) /\ (z +h w) = (v +h u)) /\ (f +h g) = (v +h u)))))
11	10	imp32 363	. . . . . 6 |- (((h = (x +h y) /\ h = (z +h w)) /\ (h = (f +h g) /\ h = (v +h u))) -> (((x +h y) = (v +h u) /\ (z +h w) = (v +h u)) /\ (f +h g) = (v +h u)))
12	11	anim2i 335	. . . . 5 |- (((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ ((f e. F /\ g e. G) /\ (v e. R /\ u e. S))) /\ ((h = (x +h y) /\ h = (z +h w)) /\ (h = (f +h g) /\ h = (v +h u)))) -> ((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ ((f e. F /\ g e. G) /\ (v e. R /\ u e. S))) /\ (((x +h y) = (v +h u) /\ (z +h w) = (v +h u)) /\ (f +h g) = (v +h u))))
13	12	an4s 508	. . . 4 |- (((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (h = (x +h y) /\ h = (z +h w))) /\ (((f e. F /\ g e. G) /\ (v e. R /\ u e. S)) /\ (h = (f +h g) /\ h = (v +h u)))) -> ((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ ((f e. F /\ g e. G) /\ (v e. R /\ u e. S))) /\ (((x +h y) = (v +h u) /\ (z +h w) = (v +h u)) /\ (f +h g) = (v +h u))))
14		an4 506	. . . 4 |- ((((x e. A /\ y e. B) /\ h = (x +h y)) /\ ((z e. C /\ w e. D) /\ h = (z +h w))) <-> (((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (h = (x +h y) /\ h = (z +h w))))
15		an4 506	. . . 4 |- ((((f e. F /\ g e. G) /\ h = (f +h g)) /\ ((v e. R /\ u e. S) /\ h = (v +h u))) <-> (((f e. F /\ g e. G) /\ (v e. R /\ u e. S)) /\ (h = (f +h g) /\ h = (v +h u))))
16	13, 14, 15	syl2anb 455	. . 3 |- (((((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)))) -> ((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ ((f e. F /\ g e. G) /\ (v e. R /\ u e. S))) /\ (((x +h y) = (v +h u) /\ (z +h w) = (v +h u)) /\ (f +h g) = (v +h u))))
17		5oalem5.1	. . . 4 |- A e. SH
18		5oalem5.2	. . . 4 |- B e. SH
19		5oalem5.3	. . . 4 |- C e. SH
20		5oalem5.4	. . . 4 |- D e. SH
21		5oalem5.5	. . . 4 |- F e. SH
22		5oalem5.6	. . . 4 |- G e. SH
23		5oalem5.7	. . . 4 |- R e. SH
24		5oalem5.8	. . . 4 |- S e. SH
25	17, 18, 19, 20, 21, 22, 23, 24	5oalem5 9603	. . 3 |- (((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ ((f e. F /\ g e. G) /\ (v e. R /\ u e. S))) /\ (((x +h y) = (v +h u) /\ (z +h w) = (v +h u)) /\ (f +h g) = (v +h u))) -> (x -h z) e. ((((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)))))))
26	16, 25	syl 10	. 2 |- (((((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)))) -> (x -h z) e. ((((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)))))))
27	17, 19	shscl 9281	. . . . . . . . . . 11 |- (A +H C) e. SH
28	18, 20	shscl 9281	. . . . . . . . . . 11 |- (B +H D) e. SH
29	27, 28	shincl 9331	. . . . . . . . . 10 |- ((A +H C) i^i (B +H D)) e. SH
30	17, 23	shscl 9281	. . . . . . . . . . . 12 |- (A +H R) e. SH
31	18, 24	shscl 9281	. . . . . . . . . . . 12 |- (B +H S) e. SH
32	30, 31	shincl 9331	. . . . . . . . . . 11 |- ((A +H R) i^i (B +H S)) e. SH
33	19, 23	shscl 9281	. . . . . . . . . . . 12 |- (C +H R) e. SH
34	20, 24	shscl 9281	. . . . . . . . . . . 12 |- (D +H S) e. SH
35	33, 34	shincl 9331	. . . . . . . . . . 11 |- ((C +H R) i^i (D +H S)) e. SH
36	32, 35	shscl 9281	. . . . . . . . . 10 |- (((A