Theorem 5oalem2 9517

Description: Lemma for orthoarguesian law 5OA.

Hypotheses

Ref	Expression
5oalem2.1	|- A e. SH
5oalem2.2	|- B e. SH
5oalem2.3	|- C e. SH
5oalem2.4	|- D e. SH

Assertion

Ref	Expression
5oalem2	|- ((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (x +h y) = (z +h w)) -> (x -h z) e. ((A +H C) i^i (B +H D)))

Proof of Theorem 5oalem2

Step	Hyp	Ref	Expression
1		5oalem2.1	. . . . . 6 |- A e. SH
2		5oalem2.3	. . . . . 6 |- C e. SH
3	1, 2	shsvs 9251	. . . . 5 |- ((x e. A /\ z e. C) -> (x -h z) e. (A +H C))
4	3	ad2ant2r 409	. . . 4 |- (((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) -> (x -h z) e. (A +H C))
5	4	adantr 389	. . 3 |- ((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (x +h y) = (z +h w)) -> (x -h z) e. (A +H C))
6		5oalem2.4	. . . . . . . 8 |- D e. SH
7		5oalem2.2	. . . . . . . 8 |- B e. SH
8	6, 7	shsvs 9251	. . . . . . 7 |- ((w e. D /\ y e. B) -> (w -h y) e. (D +H B))
9		ancom 435	. . . . . . 7 |- ((y e. B /\ w e. D) <-> (w e. D /\ y e. B))
10	7, 6	shscom 9247	. . . . . . . 8 |- (B +H D) = (D +H B)
11	10	eleq2i 1530	. . . . . . 7 |- ((w -h y) e. (B +H D) <-> (w -h y) e. (D +H B))
12	8, 9, 11	3imtr4 219	. . . . . 6 |- ((y e. B /\ w e. D) -> (w -h y) e. (B +H D))
13	12	ad2ant2l 408	. . . . 5 |- (((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) -> (w -h y) e. (B +H D))
14	13	adantr 389	. . . 4 |- ((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (x +h y) = (z +h w)) -> (w -h y) e. (B +H D))
15		opreq1 3953	. . . . . . . 8 |- ((x +h y) = (z +h w) -> ((x +h y) -h (z +h y)) = ((z +h w) -h (z +h y)))
16	15	adantl 388	. . . . . . 7 |- ((((x e. H~ /\ y e. H~) /\ (z e. H~ /\ w e. H~)) /\ (x +h y) = (z +h w)) -> ((x +h y) -h (z +h y)) = ((z +h w) -h (z +h y)))
17		pm3.27 323	. . . . . . . . . . . . 13 |- ((x e. H~ /\ y e. H~) -> y e. H~)
18	17	anim2i 335	. . . . . . . . . . . 12 |- ((z e. H~ /\ (x e. H~ /\ y e. H~)) -> (z e. H~ /\ y e. H~))
19	18	ancoms 436	. . . . . . . . . . 11 |- (((x e. H~ /\ y e. H~) /\ z e. H~) -> (z e. H~ /\ y e. H~))
20		hvsub4t 8827	. . . . . . . . . . 11 |- (((x e. H~ /\ y e. H~) /\ (z e. H~ /\ y e. H~)) -> ((x +h y) -h (z +h y)) = ((x -h z) +h (y -h y)))
21	19, 20	syldan 467	. . . . . . . . . 10 |- (((x e. H~ /\ y e. H~) /\ z e. H~) -> ((x +h y) -h (z +h y)) = ((x -h z) +h (y -h y)))
22		hvsubidt 8816	. . . . . . . . . . . 12 |- (y e. H~ -> (y -h y) = 0h)
23	22	opreq2d 3961	. . . . . . . . . . 11 |- (y e. H~ -> ((x -h z) +h (y -h y)) = ((x -h z) +h 0h))
24	23	ad2antlr 405	. . . . . . . . . 10 |- (((x e. H~ /\ y e. H~) /\ z e. H~) -> ((x -h z) +h (y -h y)) = ((x -h z) +h 0h))
25		hvsubclt 8808	. . . . . . . . . . . 12 |- ((x e. H~ /\ z e. H~) -> (x -h z) e. H~)
26		ax-hvaddid 8795	. . . . . . . . . . . 12 |- ((x -h z) e. H~ -> ((x -h z) +h 0h) = (x -h z))
27	25, 26	syl 10	. . . . . . . . . . 11 |- ((x e. H~ /\ z e. H~) -> ((x -h z) +h 0h) = (x -h z))
28	27	adantlr 393	. . . . . . . . . 10 |- (((x e. H~ /\ y e. H~) /\ z e. H~) -> ((x -h z) +h 0h) = (x -h z))
29	21, 24, 28	3eqtrd 1503	. . . . . . . . 9 |- (((x e. H~ /\ y e. H~) /\ z e. H~) -> ((x +h y) -h (z +h y)) = (x -h z))
30	29	adantrr 395	. . . . . . . 8 |- (((x e. H~ /\ y e. H~) /\ (z e. H~ /\ w e. H~)) -> ((x +h y) -h (z +h y)) = (x -h z))
31	30	adantr 389	. . . . . . 7 |- ((((x e. H~ /\ y e. H~) /\ (z e. H~ /\ w e. H~)) /\ (x +h y) = (z +h w)) -> ((x +h y) -h (z +h y)) = (x -h z))
32		hvsub4t 8827	. . . . . . . . . . 11 |- (((z e. H~ /\ w e. H~) /\ (z e. H~ /\ y e. H~)) -> ((z +h w) -h (z +h y)) = ((z -h z) +h (w -h y)))
33		pm3.27 323	. . . . . . . . . . 11 |- ((y e. H~ /\ (z e. H~ /\ w e. H~)) -> (z e. H~ /\ w e. H~))
34		pm3.26 319	. . . . . . . . . . . . 13 |- ((z e. H~ /\ w e. H~) -> z e. H~)
35	34	anim1i 334	. . . . . . . . . . . 12 |- (((z e. H~ /\ w e. H~) /\ y e. H~) -> (z e. H~ /\ y e. H~))
36	35	ancoms 436	. . . . . . . . . . 11 |- ((y e. H~ /\ (z e. H~ /\ w e. H~)) -> (z e. H~ /\ y e. H~))
37	32, 33, 36	sylanc 471	. . . . . . . . . 10 |- ((y e. H~ /\ (z e. H~ /\ w e. H~)) -> ((z +h w) -h (z +h y)) = ((z -h z) +h (w -h y)))
38		hvsubidt 8816	. . . . . . . . . . . 12 |- (z e. H~ -> (z -h z) = 0h)
39	38	opreq1d 3960	. . . . . . . . . . 11 |- (z e. H~ -> ((z -h z) +h (w -h y)) = (0h +h (w -h y)))
40	39	ad2antrl 406	. . . . . . . . . 10 |- ((y e. H~ /\ (z e. H~ /\ w e. H~)) -> ((z -h z) +h (w -h y)) = (0h +h (w -h y)))
41		hvsubclt 8808	. . . . . . . . . . . . 13 |- ((w e. H~ /\ y e. H~) -> (w -h y) e. H~)
42		hvaddid2t 8813	. . . . . . . . . . . . 13 |- ((w -h y) e. H~ -> (0h +h (w -h y)) = (w -h y))
43	41, 42	syl 10	. . . . . . . . . . . 12 |- ((w e. H~ /\ y e. H~) -> (0h +h (w -h y)) = (w -h y))
44	43	ancoms 436	. . . . . . . . . . 11 |- ((y e. H~ /\ w e. H~) -> (0h +h (w -h y)) = (w -h y))
45	44	adantrl 394	. . . . . . . . . 10 |- ((y e. H~ /\ (z e. H~ /\ w e. H~)) -> (0h +h (w -h y)) = (w -h y))
46	37, 40, 45	3eqtrd 1503	. . . . . . . . 9 |- ((y e. H~ /\ (z e. H~ /\ w e. H~)) -> ((z +h w) -h (z +h y)) = (w -h y))
47	46	adantll 392	. . . . . . . 8 |- (((x e. H~ /\ y e. H~) /\ (z e. H~ /\ w e. H~)) -> ((z +h w) -h (z +h y)) = (w -h y))
48	47	adantr 389	. . . . . . 7 |- ((((x e. H~ /\ y e. H~) /\ (z e. H~ /\ w e. H~)) /\ (x +h y) = (z +h w)) -> ((z +h w) -h (z +h y)) = (w -h y))
49	16, 31, 48	3eqtr3d 1507	. . . . . 6 |- ((((x e. H~ /\ y e. H~) /\ (z e. H~ /\ w e. H~)) /\ (x +h y) = (z +h w)) -> (x -h z) = (w -h y))
50	49	eleq1d 1532	. . . . 5 |- ((((x e. H~ /\ y e. H~) /\ (z e. H~ /\ w e. H~)) /\ (x +h y) = (z +h w)) -> ((x -h z) e. (B +H D) <-> (w -h y) e. (B +H D)))
51	1	shel 9003	. . . . . . 7 |- (x e. A -> x e. H~)
52	7	shel 9003	. . . . . . 7 |- (y e. B -> y e. H~)
53	51, 52	anim12i 333	. . . . . 6 |- ((x e. A /\ y e. B) -> (x e. H~ /\ y e. H~))
54	2	shel 9003	. . . . . . 7 |- (z e. C -> z e. H~)
55	6	shel 9003	. . . . . . 7 |- (w e. D -> w e. H~)
56	54, 55	anim12i 333	. . . . . 6 |- ((z e. C /\ w e. D) -> (z e. H~ /\ w e. H~))
57	53, 56	anim12i 333	. . . . 5 |- (((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) -> ((x e. H~ /\ y e. H~) /\ (z e. H~ /\ w e. H~)))
58	50, 57	sylan 448	. . . 4 |- ((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (x +h y) = (z +h w)) -> ((x -h z) e. (B +H D) <-> (w -h y) e. (B +H D)))
59	14, 58	mpbird 196	. . 3 |- ((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (x +h y) = (z +h w)) -> (x -h z) e. (B +H D))
60	5, 59	jca 288	. 2 |- ((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (x +h y) = (z +h w)) -> ((x -h z) e. (A +H C) /\ (x -h z) e. (B +H D)))
61		elin 2197	. 2 |- ((x -h z) e. ((A +H C) i^i (B +H D)) <-> ((x -h z) e. (A