Theorem 5oalem5 5548

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 +v y) = (v +v u) /\ (z +v w) = (v +v u)) /\ (f +v g) = (v +v u))) -> (x -v 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 5547	. . . 4 |- (((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (v e. R /\ u e. S)) /\ ((x +v y) = (v +v u) /\ (z +v w) = (v +v u))) -> (x -v 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 260	. . . . 5 |- (((f e. F /\ g e. G) /\ (v e. R /\ u e. S)) -> (v e. R /\ u e. S))
9	8	anim2i 270	. . . 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 256	. . . 4 |- ((((x +v y) = (v +v u) /\ (z +v w) = (v +v u)) /\ (f +v g) = (v +v u)) -> ((x +v y) = (v +v u) /\ (z +v w) = (v +v u)))
11	7, 9, 10	syl2an 349	. . 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 +v y) = (v +v u) /\ (z +v w) = (v +v u)) /\ (f +v g) = (v +v u))) -> (x -v 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 5032	. . . . . . . . 9 |- (((x e. H~ /\ f e. H~) /\ (z e. H~ /\ f e. H~)) -> ((x -v f) -v (z -v f)) = ((x -v z) -v (f -v f)))
13	12	anandirs 395	. . . . . . . 8 |- (((x e. H~ /\ z e. H~) /\ f e. H~) -> ((x -v f) -v (z -v f)) = ((x -v z) -v (f -v f)))
14		hvsubidt 5005	. . . . . . . . . 10 |- (f e. H~ -> (f -v f) = 0v)
15	14	opreq2d 3013	. . . . . . . . 9 |- (f e. H~ -> ((x -v z) -v (f -v f)) = ((x -v z) -v 0v))
16	15	adantl 305	. . . . . . . 8 |- (((x e. H~ /\ z e. H~) /\ f e. H~) -> ((x -v z) -v (f -v f)) = ((x -v z) -v 0v))
17		hvsubclt 4998	. . . . . . . . . 10 |- ((x e. H~ /\ z e. H~) -> (x -v z) e. H~)
18		hvsub0t 5041	. . . . . . . . . 10 |- ((x -v z) e. H~ -> ((x -v z) -v 0v) = (x -v z))
19	17, 18	syl 12	. . . . . . . . 9 |- ((x e. H~ /\ z e. H~) -> ((x -v z) -v 0v) = (x -v z))
20	19	adantr 306	. . . . . . . 8 |- (((x e. H~ /\ z e. H~) /\ f e. H~) -> ((x -v z) -v 0v) = (x -v z))
21	13, 16, 20	3eqtrd 1132	. . . . . . 7 |- (((x e. H~ /\ z e. H~) /\ f e. H~) -> ((x -v f) -v (z -v f)) = (x -v z))
22	1	shel 5120	. . . . . . . . 9 |- (x e. A -> x e. H~)
23	22	adantr 306	. . . . . . . 8 |- ((x e. A /\ y e. B) -> x e. H~)
24	3	shel 5120	. . . . . . . . 9 |- (z e. C -> z e. H~)
25	24	adantr 306	. . . . . . . 8 |- ((z e. C /\ w e. D) -> z e. H~)
26	23, 25	anim12i 268	. . . . . . 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 5120	. . . . . . . 8 |- (f e. F -> f e. H~)
29	28	adantr 306	. . . . . . 7 |- ((f e. F /\ g e. G) -> f e. H~)
30	21, 26, 29	syl2an 349	. . . . . 6 |- ((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (f e. F /\ g e. G)) -> ((x -v f) -v (z -v f)) = (x -v z))
31	30	adantrr 312	. . . . 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 -v f) -v (z -v f)) = (x -v z))
32	31	adantr 306	. . . 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 +v y) = (v +v u) /\ (z +v w) = (v +v u)) /\ (f +v g) = (v +v u))) -> ((x -v f) -v (z -v f)) = (x -v z))
33		pm3.26 256	. . . . . . . . 9 |- (((f e. F /\ g e. G) /\ (v e. R /\ u e. S)) -> (f e. F /\ g e. G))
34	33	anim2i 270	. . . . . . . 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 393	. . . . . . . 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 173	. . . . . . 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	8	adantl 305	. . . . . . 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 236	. . . . . 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 256	. . . . . . . 8 |- (((x +v y) = (v +v u) /\ (z +v w) = (v +v u)) -> (x +v y) = (v +v u))
40	39	anim1i 269	. . . . . . 7 |- ((((x +v y) = (v +v u) /\ (z +v w) = (v +v u)) /\ (f +v g) = (v +v u)) -> ((x +v y) = (v +v u) /\ (f +v g) = (v +v u)))
41		pm3.27 260	. . . . . . . 8 |- (((x +v y) = (v +v u) /\ (z +v w) = (v +v u)) -> (z +v w) = (v +v u))
42	41	anim1i 269	. . . . . . 7 |- ((((x +v y) = (v +v u) /\ (z +v w) = (v +v u)) /\ (f +v g) = (v +v u)) -> ((z +v w) = (v +v u) /\ (f +v g) = (v +v u)))
43	40, 42	jca 236	. . . . . 6 |- ((((x +v y) = (v +v u) /\ (z +v w) = (v +v u)) /\ (f +v g) = (v +v u)) -> (((x +v y) = (v +v u) /\ (f +v g) = (v