Theorem 5oalem2 5545

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 +v y) = (z +v w)) -> (x -v 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 5337	. . . . 5 |- ((x e. A /\ z e. C) -> (x -v z) e. (A +H C))
4		pm3.26 256	. . . . 5 |- ((x e. A /\ y e. B) -> x e. A)
5		pm3.26 256	. . . . 5 |- ((z e. C /\ w e. D) -> z e. C)
6	3, 4, 5	syl2an 349	. . . 4 |- (((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) -> (x -v z) e. (A +H C))
7	6	adantr 306	. . 3 |- ((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (x +v y) = (z +v w)) -> (x -v z) e. (A +H C))
8		5oalem2.4	. . . . . . . 8 |- D e. SH
9		5oalem2.2	. . . . . . . 8 |- B e. SH
10	8, 9	shsvs 5337	. . . . . . 7 |- ((w e. D /\ y e. B) -> (w -v y) e. (D +H B))
11		ancom 333	. . . . . . 7 |- ((y e. B /\ w e. D) <-> (w e. D /\ y e. B))
12	9, 8	shscom 5333	. . . . . . . 8 |- (B +H D) = (D +H B)
13	12	eleq2i 1153	. . . . . . 7 |- ((w -v y) e. (B +H D) <-> (w -v y) e. (D +H B))
14	10, 11, 13	3imtr4 192	. . . . . 6 |- ((y e. B /\ w e. D) -> (w -v y) e. (B +H D))
15		pm3.27 260	. . . . . 6 |- ((x e. A /\ y e. B) -> y e. B)
16		pm3.27 260	. . . . . 6 |- ((z e. C /\ w e. D) -> w e. D)
17	14, 15, 16	syl2an 349	. . . . 5 |- (((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) -> (w -v y) e. (B +H D))
18	17	adantr 306	. . . 4 |- ((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (x +v y) = (z +v w)) -> (w -v y) e. (B +H D))
19		opreq1 3006	. . . . . . . 8 |- ((x +v y) = (z +v w) -> ((x +v y) -v (z +v y)) = ((z +v w) -v (z +v y)))
20	19	adantl 305	. . . . . . 7 |- ((((x e. H~ /\ y e. H~) /\ (z e. H~ /\ w e. H~)) /\ (x +v y) = (z +v w)) -> ((x +v y) -v (z +v y)) = ((z +v w) -v (z +v y)))
21		hvsub4t 5014	. . . . . . . . . . 11 |- (((x e. H~ /\ y e. H~) /\ (z e. H~ /\ y e. H~)) -> ((x +v y) -v (z +v y)) = ((x -v z) +v (y -v y)))
22		pm3.26 256	. . . . . . . . . . 11 |- (((x e. H~ /\ y e. H~) /\ z e. H~) -> (x e. H~ /\ y e. H~))
23		pm3.27 260	. . . . . . . . . . . . 13 |- ((x e. H~ /\ y e. H~) -> y e. H~)
24	23	anim2i 270	. . . . . . . . . . . 12 |- ((z e. H~ /\ (x e. H~ /\ y e. H~)) -> (z e. H~ /\ y e. H~))
25	24	ancoms 334	. . . . . . . . . . 11 |- (((x e. H~ /\ y e. H~) /\ z e. H~) -> (z e. H~ /\ y e. H~))
26	21, 22, 25	sylanc 361	. . . . . . . . . 10 |- (((x e. H~ /\ y e. H~) /\ z e. H~) -> ((x +v y) -v (z +v y)) = ((x -v z) +v (y -v y)))
27		hvsubidt 5005	. . . . . . . . . . . 12 |- (y e. H~ -> (y -v y) = 0v)
28	27	opreq2d 3013	. . . . . . . . . . 11 |- (y e. H~ -> ((x -v z) +v (y -v y)) = ((x -v z) +v 0v))
29	28	ad2antlr 321	. . . . . . . . . 10 |- (((x e. H~ /\ y e. H~) /\ z e. H~) -> ((x -v z) +v (y -v y)) = ((x -v z) +v 0v))
30		hvsubclt 4998	. . . . . . . . . . . 12 |- ((x e. H~ /\ z e. H~) -> (x -v z) e. H~)
31		ax-hvaddid 4988	. . . . . . . . . . . 12 |- ((x -v z) e. H~ -> ((x -v z) +v 0v) = (x -v z))
32	30, 31	syl 12	. . . . . . . . . . 11 |- ((x e. H~ /\ z e. H~) -> ((x -v z) +v 0v) = (x -v z))
33	32	adantlr 310	. . . . . . . . . 10 |- (((x e. H~ /\ y e. H~) /\ z e. H~) -> ((x -v z) +v 0v) = (x -v z))
34	26, 29, 33	3eqtrd 1132	. . . . . . . . 9 |- (((x e. H~ /\ y e. H~) /\ z e. H~) -> ((x +v y) -v (z +v y)) = (x -v z))
35	34	adantrr 312	. . . . . . . 8 |- (((x e. H~ /\ y e. H~) /\ (z e. H~ /\ w e. H~)) -> ((x +v y) -v (z +v y)) = (x -v z))
36	35	adantr 306	. . . . . . 7 |- ((((x e. H~ /\ y e. H~) /\ (z e. H~ /\ w e. H~)) /\ (x +v y) = (z +v w)) -> ((x +v y) -v (z +v y)) = (x -v z))
37		hvsub4t 5014	. . . . . . . . . . 11 |- (((z e. H~ /\ w e. H~) /\ (z e. H~ /\ y e. H~)) -> ((z +v w) -v (z +v y)) = ((z -v z) +v (w -v y)))
38		pm3.27 260	. . . . . . . . . . 11 |- ((y e. H~ /\ (z e. H~ /\ w e. H~)) -> (z e. H~ /\ w e. H~))
39		pm3.26 256	. . . . . . . . . . . . 13 |- ((z e. H~ /\ w e. H~) -> z e. H~)
40	39	anim1i 269	. . . . . . . . . . . 12 |- (((z e. H~ /\ w e. H~) /\ y e. H~) -> (z e. H~ /\ y e. H~))
41	40	ancoms 334	. . . . . . . . . . 11 |- ((y e. H~ /\ (z e. H~ /\ w e. H~)) -> (z e. H~ /\ y e. H~))
42	37, 38, 41	sylanc 361	. . . . . . . . . 10 |- ((y e. H~ /\ (z e. H~ /\ w e. H~)) -> ((z +v w) -v (z +v y)) = ((z -v z) +v (w -v y)))
43		hvsubidt 5005	. . . . . . . . . . . 12 |- (z e. H~ -> (z -v z) = 0v)
44	43	opreq1d 3012	. . . . . . . . . . 11 |- (z e. H~ -> ((z -v z) +v (w -v y)) = (0v +v (w -v y)))
45	44	ad2antrl 322	. . . . . . . . . 10 |- ((y e. H~ /\ (z e. H~ /\ w e. H~)) -> ((z -v z) +v (w -v y)) = (0v +v (w -v y)))
46		hvsubclt 4998	. . . . . . . . . . . . 13 |- ((w e. H~ /\ y e. H~) -> (w -v y) e. H~)
47		hvaddid2t 5003	. . . . . . . . . . . . 13 |- ((w -v y) e. H~ -> (0v +v (w -v y)) = (w -v y))
48	46, 47	syl 12	. . . . . . . . . . . 12 |- ((w e. H~ /\ y e. H~) -> (0v +v (w -v y)) = (w -v y))
49	48	ancoms 334	. . . . . . . . . . 11 |- ((y e. H~ /\ w e. H~) -> (0v +v (w -v y)) = (w -v y))
50	49	adantrl 311	. . . . . . . . . 10 |- ((y e. H~ /\ (z e. H~ /\ w e. H~)) -> (0v +v (w -v y)) = (w -v y))
51	42, 45, 50	3eqtrd 1132	. . . . . . . . 9 |- ((y e. H~ /\ (z e. H~ /\ w e. H~)) -> ((z +v w) -v (z +v y)) = (w -v y))
52	51	adantll 309	. . . . . . . 8 |- (((x e. H~ /\ y e. H~) /\ (z e. H~ /\ w e. H~)) -> ((z +v w) -v (z +v y)) = (w -v y))
53	52	adantr 306	. . . . . . 7 |- ((((x e. H~ /\ y e. H~) /\ (z e. H~ /\ w e. H~)) /\ (x +v y) = (z +v w)) -> ((z +v w) -v (z +v y)) = (w -v y))
54	20, 36, 53	3eqtr3d 1133	. . . . . 6 |- ((((x e. H~ /\ y e. H~) /\ (z e. H~ /\ w e. H~)) /\ (x +v y) = (z +v w)) -> (x -v z) = (w -v y))
55	54	eleq1d 1155	. . . . 5 |- ((((x e. H~ /\ y e. H~) /\ (z e. H~ /\ w e. H~)) /\ (x +v y) = (z +v w)) -> ((x -v z) e. (B +H D) <-> (w -v y) e. (B +H D)))
56	1	shel 5120	. . . . . . 7 |- (x e. A -> x e. H~)
57	9	shel 5120	. . . . . . 7 |- (y e. B -> y e. H~)
58	56, 57	anim12i 268	. . . . . 6 |- ((x e. A /\ y e. B) -> (x e. H~ /\ y e. H~))
59	2	shel 5120	. . . . . . 7 |- (z e. C -> z e. H~)
60	8	shel 5120	. . . . . . 7 |- (w e. D -> w e. H~)
61	59, 60	anim12i 268	. . . . . 6 |- ((z e. C /\ w e. D) -> (z e. H~ /\ w e. H~))
62	58, 61	anim12i 268	. . . . 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~)))
63	55, 62	sylan 343	. . . 4 |- ((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (x +v y) = (z +v w)) -> ((x -v z) e. (B +H D) <-> (w -v y) e. (B +H D)))
64	18, 63	mpbird 171	. . 3 |- ((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (x +v y) = (z +v w)) -> (x -v z) e. (B +H D))
65	7, 64	jca 236	. 2 |- ((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (x +v y) = (z +v w)) -> ((x -v z) e. (A +H C) /\ (x -v