Theorem 3oalem2 5553

Description: Lemma for 3OA (weak) orthoarguesian law.

Hypotheses

Ref	Expression
3oalem1.1	|- B e. CH
3oalem1.2	|- C e. CH
3oalem1.3	|- R e. CH
3oalem1.4	|- S e. CH

Assertion

Ref	Expression
3oalem2	|- ((((x e. B /\ y e. R) /\ v = (x +v y)) /\ ((z e. C /\ w e. S) /\ v = (z +v w))) -> v e. (B +H (R i^i (S +H ((B +H C) i^i (R +H S))))))

Distinct variable group(s):   x,y,z,w,v,B   x,C,y,z,w,v   x,R,y,z,w,v   x,S,y,z,w,v

Proof of Theorem 3oalem2

Step	Hyp	Ref	Expression
1		3oalem1.1	. . . . 5 |- B e. CH
2	1	chshi 5132	. . . 4 |- B e. SH
3		3oalem1.3	. . . . . 6 |- R e. CH
4	3	chshi 5132	. . . . 5 |- R e. SH
5		3oalem1.4	. . . . . . 7 |- S e. CH
6	5	chshi 5132	. . . . . 6 |- S e. SH
7		3oalem1.2	. . . . . . . . 9 |- C e. CH
8	7	chshi 5132	. . . . . . . 8 |- C e. SH
9	2, 8	shscl 5282	. . . . . . 7 |- (B +H C) e. SH
10	4, 6	shscl 5282	. . . . . . 7 |- (R +H S) e. SH
11	9, 10	shincl 5332	. . . . . 6 |- ((B +H C) i^i (R +H S)) e. SH
12	6, 11	shscl 5282	. . . . 5 |- (S +H ((B +H C) i^i (R +H S))) e. SH
13	4, 12	shincl 5332	. . . 4 |- (R i^i (S +H ((B +H C) i^i (R +H S)))) e. SH
14	2, 13	shsva 5334	. . 3 |- ((x e. B /\ y e. (R i^i (S +H ((B +H C) i^i (R +H S))))) -> (x +v y) e. (B +H (R i^i (S +H ((B +H C) i^i (R +H S))))))
15		pm3.26 256	. . . 4 |- ((x e. B /\ y e. R) -> x e. B)
16	15	ad2antll 320	. . 3 |- ((((x e. B /\ y e. R) /\ v = (x +v y)) /\ ((z e. C /\ w e. S) /\ v = (z +v w))) -> x e. B)
17		pm3.27 260	. . . . . 6 |- ((x e. B /\ y e. R) -> y e. R)
18	17	ad2antll 320	. . . . 5 |- ((((x e. B /\ y e. R) /\ v = (x +v y)) /\ ((z e. C /\ w e. S) /\ v = (z +v w))) -> y e. R)
19	1, 7, 3, 5	3oalem1 5552	. . . . . . 7 |- ((((x e. B /\ y e. R) /\ v = (x +v y)) /\ ((z e. C /\ w e. S) /\ v = (z +v w))) -> (((x e. H~ /\ y e. H~) /\ v e. H~) /\ (z e. H~ /\ w e. H~)))
20		hvaddsub12t 5015	. . . . . . . . . . . . 13 |- ((y e. H~ /\ w e. H~ /\ w e. H~) -> (y +v (w -v w)) = (w +v (y -v w)))
21	20	3expb 613	. . . . . . . . . . . 12 |- ((y e. H~ /\ (w e. H~ /\ w e. H~)) -> (y +v (w -v w)) = (w +v (y -v w)))
22	21	anabsan2 387	. . . . . . . . . . 11 |- ((y e. H~ /\ w e. H~) -> (y +v (w -v w)) = (w +v (y -v w)))
23		hvsubidt 5005	. . . . . . . . . . . . 13 |- (w e. H~ -> (w -v w) = 0v)
24	23	opreq2d 3013	. . . . . . . . . . . 12 |- (w e. H~ -> (y +v (w -v w)) = (y +v 0v))
25		ax-hvaddid 4988	. . . . . . . . . . . 12 |- (y e. H~ -> (y +v 0v) = y)
26	24, 25	sylan9eqr 1145	. . . . . . . . . . 11 |- ((y e. H~ /\ w e. H~) -> (y +v (w -v w)) = y)
27	22, 26	eqtr3d 1130	. . . . . . . . . 10 |- ((y e. H~ /\ w e. H~) -> (w +v (y -v w)) = y)
28	27	adantrl 311	. . . . . . . . 9 |- ((y e. H~ /\ (z e. H~ /\ w e. H~)) -> (w +v (y -v w)) = y)
29	28	adantll 309	. . . . . . . 8 |- (((x e. H~ /\ y e. H~) /\ (z e. H~ /\ w e. H~)) -> (w +v (y -v w)) = y)
30	29	adantlr 310	. . . . . . 7 |- ((((x e. H~ /\ y e. H~) /\ v e. H~) /\ (z e. H~ /\ w e. H~)) -> (w +v (y -v w)) = y)
31	19, 30	syl 12	. . . . . 6 |- ((((x e. B /\ y e. R) /\ v = (x +v y)) /\ ((z e. C /\ w e. S) /\ v = (z +v w))) -> (w +v (y -v w)) = y)
32	6, 11	shsva 5334	. . . . . . 7 |- ((w e. S /\ (y -v w) e. ((B +H C) i^i (R +H S))) -> (w +v (y -v w)) e. (S +H ((B +H C) i^i (R +H S))))
33		pm3.27 260	. . . . . . . 8 |- ((z e. C /\ w e. S) -> w e. S)
34	33	ad2antrl 322	. . . . . . 7 |- ((((x e. B /\ y e. R) /\ v = (x +v y)) /\ ((z e. C /\ w e. S) /\ v = (z +v w))) -> w e. S)
35		cleq1 1107	. . . . . . . . . . . . . . 15 |- (v = (x +v y) -> (v = (z +v w) <-> (x +v y) = (z +v w)))
36	35	biimpa 324	. . . . . . . . . . . . . 14 |- ((v = (x +v y) /\ v = (z +v w)) -> (x +v y) = (z +v w))
37	36	opreq1d 3012	. . . . . . . . . . . . 13 |- ((v = (x +v y) /\ v = (z +v w)) -> ((x +v y) -v (x +v w)) = ((z +v w) -v (x +v w)))
38	37	adantrl 311	. . . . . . . . . . . 12 |- ((v = (x +v y) /\ ((z e. C /\ w e. S) /\ v = (z +v w))) -> ((x +v y) -v (x +v w)) = ((z +v w) -v (x +v w)))
39	38	adantll 309	. . . . . . . . . . 11 |- ((((x e. B /\ y e. R) /\ v = (x +v y)) /\ ((z e. C /\ w e. S) /\ v = (z +v w))) -> ((x +v y) -v (x +v w)) = ((z +v w) -v (x +v w)))
40		hvsub4t 5014	. . . . . . . . . . . . . . . 16 |- (((x e. H~ /\ y e. H~) /\ (x e. H~ /\ w e. H~)) -> ((x +v y) -v (x +v w)) = ((x -v x) +v (y -v w)))
41		pm3.26 256	. . . . . . . . . . . . . . . 16 |- (((x e. H~ /\ y e. H~) /\ w e. H~) -> (x e. H~ /\ y e. H~))
42		pm3.26 256	. . . . . . . . . . . . . . . . 17 |- ((x e. H~ /\ y e. H~) -> x e. H~)
43	42	anim1i 269	. . . . . . . . . . . . . . . 16 |- (((x e. H~ /\ y e. H~) /\ w e. H~) -> (x e. H~ /\ w e. H~))
44	40, 41, 43	sylanc 361	. . . . . . . . . . . . . . 15 |- (((x e. H~ /\ y e. H~) /\ w e. H~) -> ((x +v y) -v (x +v w)) = ((x -v x) +v (y -v w)))
45		hvsubidt 5005	. . . . . . . . . . . . . . . . 17 |- (x e. H~ -> (x -v x) = 0v)
46	45	ad2antll 320	. . . . . . . . . . . . . . . 16 |- (((x e. H~ /\ y e. H~) /\ w e. H~) -> (x -v x) = 0v)
47	46	opreq1d 3012	. . . . . . . . . . . . . . 15 |- (((x e. H~ /\ y e. H~) /\ w e. H~) -> ((x -v x) +v (y -v w)) = (0v +v (y -v w)))
48		hvsubclt 4998	. . . . . . . . . . . . . . . . 17 |- ((y e. H~ /\ w e. H~) -> (y -v w) e. H~)
49		hvaddid2t 5003	. . . . . . . . . . . . . . . . 17 |- ((y -v w) e. H~ -> (0v +v (y -v w)) = (y -v w))
50	48, 49	syl 12	. . . . . . . . . . . . . . . 16 |- ((y e. H~ /\ w e. H~) -> (0v +v (y -v w)) = (y -v w))
51	50	adantll 309	. . . . . . . . . . . . . . 15 |- (((x e. H~ /\ y e. H~) /\ w e. H~) -> (0v +v (y -v w)) = (y -v w))
52	44, 47, 51	3eqtrd 1132	. . . . . . . . . . . . . 14 |- (((x e. H~ /\ y e. H~) /\ w e. H~) -> ((x +v y) -v (x +v w)) = (y -v w))
53	52	adantrl 311	. . . . . . . . . . . . 13 |- (((x e. H~ /\ y e. H~) /\ (z e. H~ /\ w e. H~)) -> ((x +v y) -v (x +v w)) = (y -v w))
54	53	adantlr 310	. . . . . . . . . . . 12 |- ((((x e. H~ /\ y e. H~) /\ v e. H~) /\ (z e. H~ /\ w e. H~)) -> ((x +v y) -v (x +v w)) = (y -v w))
55	19, 54	syl 12	. . . . . . . . . . 11 |- ((((x e. B /\ y e. R) /\ v = (x +v y)) /\ ((z e. C /\ w e. S) /\ v = (z +v w))) -> ((x +v y) -v (x +v w)) = (y -v w))
56		hvsub4t 5014	. . . . . . . . . . . . . . . 16 |- (((z e. H~ /\ w e. H~) /\ (x e. H~ /\ w e. H~)) -> ((z +v w) -v (x +v w)) = ((z -v x) +v (w -v w)))
57		pm3.27 260	. . . . . . . . . . . . . . . 16 |- ((x e. H~ /\ (z e. H~ /\ w e. H~)) -> (z e. H~ /\ w e. H~))
58		pm3.27 260	. . . . . . . . . . . . . . . . 17 |- ((z e. H~ /\ w e. H~) -> w e. H~)
59	58	anim2i 270	. . . . . . . . . . . . . . . 16 |- ((x e. H~ /\ (z e. H~ /\ w e. H~)) -> (x e. H~ /\ w e. H~))
60	56, 57, 59	sylanc 361	. . . . . . . . . . . . . . 15 |- ((x e. H~ /\ (z e. H~ /\ w e. H~)) -> ((z +v w) -v (x +v w)) = ((z -v x) +v (w -v w)))
61	23	ad2antrr 323	. . . . . . . . . . . . . . . 16 |- ((x e. H~ /\ (z e. H~ /\ w e. H~)) -> (w -v w) = 0v)
62	61	opreq2d 3013	. . . . . . . . . . . . . . 15 |- ((x e. H~ /\ (z e. H~ /\ w e. H~)) -> ((z -v x) +v (w -v w)) = ((z -v x) +v 0v))
63		hvsubclt 4998	. . . . . . . . . . . . . . . . . 18 |- ((z e. H~ /\ x e. H~) -> (z -v x) e. H~)
64		ax-hvaddid 4988	. . . . . . . . . . . . . . . . . 18 |- ((z -v x) e. H~ -> ((z -v x) +v 0v) = (z -v x))
65	63, 64	syl 12	. . . . . . . . . . . . . . . . 17 |- ((z e.