Theorem 5oalem5 9603

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

5oalem5

|- (((((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)))))))

Proof of Theorem 5oalem5

Step	Hyp	Ref	Expression
1		5oalem5.1	. . . . 5 |- A e. SH
2		5oalem5.2	. . . . 5 |- B e. SH
3		5oalem5.3	. . . . 5 |- C e. SH
4		5oalem5.4	. . . . 5 |- D e. SH
5		5oalem5.7	. . . . 5 |- R e. SH
6		5oalem5.8	. . . . 5 |- S e. SH
7	1, 2, 3, 4, 5, 6	5oalem4 9602	. . . 4 |- (((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (v e. R /\ u e. S)) /\ ((x +h y) = (v +h u) /\ (z +h w) = (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)))))
8		pm3.27 323	. . . . 5 |- (((f e. F /\ g e. G) /\ (v e. R /\ u e. S)) -> (v e. R /\ u e. S))
9	8	anim2i 335	. . . 4 |- ((((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 e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (v e. R /\ u e. S)))
10		pm3.26 319	. . . 4 |- ((((x +h y) = (v +h u) /\ (z +h w) = (v +h u)) /\ (f +h g) = (v +h u)) -> ((x +h y) = (v +h u) /\ (z +h w) = (v +h u)))
11	7, 9, 10	syl2an 454	. . 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)))))
12		hvsubsub4t 8927	. . . . . . . . 9 |- (((x e. H~ /\ f e. H~) /\ (z e. H~ /\ f e. H~)) -> ((x -h f) -h (z -h f)) = ((x -h z) -h (f -h f)))
13	12	anandirs 513	. . . . . . . 8 |- (((x e. H~ /\ z e. H~) /\ f e. H~) -> ((x -h f) -h (z -h f)) = ((x -h z) -h (f -h f)))
14		hvsubidt 8895	. . . . . . . . . 10 |- (f e. H~ -> (f -h f) = 0h)
15	14	opreq2d 3976	. . . . . . . . 9 |- (f e. H~ -> ((x -h z) -h (f -h f)) = ((x -h z) -h 0h))
16	15	adantl 388	. . . . . . . 8 |- (((x e. H~ /\ z e. H~) /\ f e. H~) -> ((x -h z) -h (f -h f)) = ((x -h z) -h 0h))
17		hvsubclt 8887	. . . . . . . . . 10 |- ((x e. H~ /\ z e. H~) -> (x -h z) e. H~)
18		hvsub0t 8943	. . . . . . . . . 10 |- ((x -h z) e. H~ -> ((x -h z) -h 0h) = (x -h z))
19	17, 18	syl 10	. . . . . . . . 9 |- ((x e. H~ /\ z e. H~) -> ((x -h z) -h 0h) = (x -h z))
20	19	adantr 389	. . . . . . . 8 |- (((x e. H~ /\ z e. H~) /\ f e. H~) -> ((x -h z) -h 0h) = (x -h z))
21	13, 16, 20	3eqtrd 1511	. . . . . . 7 |- (((x e. H~ /\ z e. H~) /\ f e. H~) -> ((x -h f) -h (z -h f)) = (x -h z))
22	1	shel 9082	. . . . . . . . 9 |- (x e. A -> x e. H~)
23	22	adantr 389	. . . . . . . 8 |- ((x e. A /\ y e. B) -> x e. H~)
24	3	shel 9082	. . . . . . . . 9 |- (z e. C -> z e. H~)
25	24	adantr 389	. . . . . . . 8 |- ((z e. C /\ w e. D) -> z e. H~)
26	23, 25	anim12i 333	. . . . . . 7 |- (((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) -> (x e. H~ /\ z e. H~))
27		5oalem5.5	. . . . . . . . 9 |- F e. SH
28	27	shel 9082	. . . . . . . 8 |- (f e. F -> f e. H~)
29	28	adantr 389	. . . . . . 7 |- ((f e. F /\ g e. G) -> f e. H~)
30	21, 26, 29	syl2an 454	. . . . . 6 |- ((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (f e. F /\ g e. G)) -> ((x -h f) -h (z -h f)) = (x -h z))
31	30	adantrr 395	. . . . 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))) -> ((x -h f) -h (z -h f)) = (x -h z))
32	31	adantr 389	. . . 4 |- (((((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 f) -h (z -h f)) = (x -h z))
33		pm3.26 319	. . . . . . . . 9 |- (((f e. F /\ g e. G) /\ (v e. R /\ u e. S)) -> (f e. F /\ g e. G))
34	33	anim2i 335	. . . . . . . 8 |- ((((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 e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (f e. F /\ g e. G)))
35		anandir 511	. . . . . . . 8 |- ((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (f e. F /\ g e. G)) <-> (((x e. A /\ y e. B) /\ (f e. F /\ g e. G)) /\ ((z e. C /\ w e. D) /\ (f e. F /\ g e. G))))
36	34, 35	sylib 198	. . . . . . 7 |- ((((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 e. A /\ y e. B) /\ (f e. F /\ g e. G)) /\ ((z e. C /\ w e. D) /\ (f e. F /\ g e. G))))
37		simprr 415	. . . . . . 7 |- ((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ ((f e. F /\ g e. G) /\ (v e. R /\ u e. S))) -> (v e. R /\ u e. S))
38	36, 37	jca 288	. . . . . 6 |- ((((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 e. A /\ y e. B) /\ (f e. F /\ g e. G)) /\ ((z e. C /\ w e. D) /\ (f e. F /\ g e. G))) /\ (v e. R /\ u e. S)))
39		pm3.26 319	. . . . . . . 8 |- (((x +h y) = (v +h u) /\ (z +h w) = (v +h u)) -> (x +h y) = (v +h u))
40	39	anim1i 334	. . . . . . 7 |- ((((x +h y) = (v +h u) /\ (z +h w) = (v +h u)) /\ (f +h g) = (v +h u)) -> ((x +h y) = (v +h u) /\ (f +h g) = (v +h u)))
41		pm3.27 323	. . . . . . . 8 |- (((x +h y) = (v +h u) /\ (z +h w) = (v +h u)) -> (z +h w) = (v +h u))
42	41	anim1i 334	. . . . . . 7 |- ((((x +h y) = (v +h u) /\ (z +h w) = (v +h u)) /\ (f +h g) = (v +h u)) -> ((z +h w) = (v +h u) /\ (f +h g) = (v +h u)))
43	40, 42	jca 288	. . . . . 6 |- ((((x +h y) = (v +h u) /\ (z +h w