Theorem 3oalem2 9525

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 +h y)) /\ ((z e. C /\ w e. S) /\ v = (z +h w))) -> v e. (B +H (R i^i (S +H ((B +H C) i^i (R +H S))))))

Distinct variable groups:   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 9018	. . . 4 |- B e. SH
3		3oalem1.3	. . . . . 6 |- R e. CH
4	3	chshi 9018	. . . . 5 |- R e. SH
5		3oalem1.4	. . . . . . 7 |- S e. CH
6	5	chshi 9018	. . . . . 6 |- S e. SH
7		3oalem1.2	. . . . . . . . 9 |- C e. CH
8	7	chshi 9018	. . . . . . . 8 |- C e. SH
9	2, 8	shscl 9196	. . . . . . 7 |- (B +H C) e. SH
10	4, 6	shscl 9196	. . . . . . 7 |- (R +H S) e. SH
11	9, 10	shincl 9246	. . . . . 6 |- ((B +H C) i^i (R +H S)) e. SH
12	6, 11	shscl 9196	. . . . 5 |- (S +H ((B +H C) i^i (R +H S))) e. SH
13	4, 12	shincl 9246	. . . 4 |- (R i^i (S +H ((B +H C) i^i (R +H S)))) e. SH
14	2, 13	shsva 9248	. . 3 |- ((x e. B /\ y e. (R i^i (S +H ((B +H C) i^i (R +H S))))) -> (x +h y) e. (B +H (R i^i (S +H ((B +H C) i^i (R +H S))))))
15		pm3.26 319	. . . 4 |- ((x e. B /\ y e. R) -> x e. B)
16	15	ad2antrr 404	. . 3 |- ((((x e. B /\ y e. R) /\ v = (x +h y)) /\ ((z e. C /\ w e. S) /\ v = (z +h w))) -> x e. B)
17		pm3.27 323	. . . . . 6 |- ((x e. B /\ y e. R) -> y e. R)
18	17	ad2antrr 404	. . . . 5 |- ((((x e. B /\ y e. R) /\ v = (x +h y)) /\ ((z e. C /\ w e. S) /\ v = (z +h w))) -> y e. R)
19	1, 7, 3, 5	3oalem1 9524	. . . . . . 7 |- ((((x e. B /\ y e. R) /\ v = (x +h y)) /\ ((z e. C /\ w e. S) /\ v = (z +h w))) -> (((x e. H~ /\ y e. H~) /\ v e. H~) /\ (z e. H~ /\ w e. H~)))
20		hvaddsub12t 8828	. . . . . . . . . . 11 |- ((y e. H~ /\ w e. H~ /\ w e. H~) -> (y +h (w -h w)) = (w +h (y -h w)))
21	20	3anidm23 881	. . . . . . . . . 10 |- ((y e. H~ /\ w e. H~) -> (y +h (w -h w)) = (w +h (y -h w)))
22		hvsubidt 8816	. . . . . . . . . . . 12 |- (w e. H~ -> (w -h w) = 0h)
23	22	opreq2d 3961	. . . . . . . . . . 11 |- (w e. H~ -> (y +h (w -h w)) = (y +h 0h))
24		ax-hvaddid 8795	. . . . . . . . . . 11 |- (y e. H~ -> (y +h 0h) = y)
25	23, 24	sylan9eqr 1521	. . . . . . . . . 10 |- ((y e. H~ /\ w e. H~) -> (y +h (w -h w)) = y)
26	21, 25	eqtr3d 1501	. . . . . . . . 9 |- ((y e. H~ /\ w e. H~) -> (w +h (y -h w)) = y)
27	26	ad2ant2l 408	. . . . . . . 8 |- (((x e. H~ /\ y e. H~) /\ (z e. H~ /\ w e. H~)) -> (w +h (y -h w)) = y)
28	27	adantlr 393	. . . . . . 7 |- ((((x e. H~ /\ y e. H~) /\ v e. H~) /\ (z e. H~ /\ w e. H~)) -> (w +h (y -h w)) = y)
29	19, 28	syl 10	. . . . . 6 |- ((((x e. B /\ y e. R) /\ v = (x +h y)) /\ ((z e. C /\ w e. S) /\ v = (z +h w))) -> (w +h (y -h w)) = y)
30	6, 11	shsva 9248	. . . . . . 7 |- ((w e. S /\ (y -h w) e. ((B +H C) i^i (R +H S))) -> (w +h (y -h w)) e. (S +H ((B +H C) i^i (R +H S))))
31		pm3.27 323	. . . . . . . 8 |- ((z e. C /\ w e. S) -> w e. S)
32	31	ad2antrl 406	. . . . . . 7 |- ((((x e. B /\ y e. R) /\ v = (x +h y)) /\ ((z e. C /\ w e. S) /\ v = (z +h w))) -> w e. S)
33		eqtr2t 1485	. . . . . . . . . . . . 13 |- ((v = (x +h y) /\ v = (z +h w)) -> (x +h y) = (z +h w))
34	33	opreq1d 3960	. . . . . . . . . . . 12 |- ((v = (x +h y) /\ v = (z +h w)) -> ((x +h y) -h (x +h w)) = ((z +h w) -h (x +h w)))
35	34	ad2ant2l 408	. . . . . . . . . . 11 |- ((((x e. B /\ y e. R) /\ v = (x +h y)) /\ ((z e. C /\ w e. S) /\ v = (z +h w))) -> ((x +h y) -h (x +h w)) = ((z +h w) -h (x +h w)))
36		pm3.26 319	. . . . . . . . . . . . . . . 16 |- ((x e. H~ /\ y e. H~) -> x e. H~)
37	36	anim1i 334	. . . . . . . . . . . . . . 15 |- (((x e. H~ /\ y e. H~) /\ w e. H~) -> (x e. H~ /\ w e. H~))
38		hvsub4t 8827	. . . . . . . . . . . . . . 15 |- (((x e. H~ /\ y e. H~) /\ (x e. H~ /\ w e. H~)) -> ((x +h y) -h (x +h w)) = ((x -h x) +h (y -h w)))
39	37, 38	syldan 467	. . . . . . . . . . . . . 14 |- (((x e. H~ /\ y e. H~) /\ w e. H~) -> ((x +h y) -h (x +h w)) = ((x -h x) +h (y -h w)))
40		hvsubidt 8816	. . . . . . . . . . . . . . . 16 |- (x e. H~ -> (x -h x) = 0h)
41	40	ad2antrr 404	. . . . . . . . . . . . . . 15 |- (((x e. H~ /\ y e. H~) /\ w e. H~) -> (x -h x) = 0h)
42	41	opreq1d 3960	. . . . . . . . . . . . . 14 |- (((x e. H~ /\ y e. H~) /\ w e. H~) -> ((x -h x) +h (y -h w)) = (0h +h (y -h w)))
43		hvsubclt 8808	. . . . . . . . . . . . . . . 16 |- ((y e. H~ /\ w e. H~) -> (y -h w) e. H~)
44		hvaddid2t 8813	. . . . . . . . . . . . . . . 16 |- ((y -h w) e. H~ -> (0h +h (y -h w)) = (y -h w))
45	43, 44	syl 10	. . . . . . . . . . . . . . 15 |- ((y e. H~ /\ w e. H~) -> (0h +h (y -h w)) = (y -h w))
46	45	adantll 392	. . . . . . . . . . . . . 14 |- (((x e. H~ /\ y e. H~) /\ w e. H~) -> (0h +h (y -h w)) = (y -h w))
47	39, 42, 46	3eqtrd 1503	. . . . . . . . . . . . 13 |- (((x e. H~ /\ y e. H~) /\ w e. H~) -> ((x +h y) -h (x +h w)) = (y -h w))
48	47	ad2ant2rl 411	. . . . . . . . . . . 12 |- ((((x e. H~ /\ y e. H~) /\ v e. H~) /\ (z e. H~ /\ w e. H~)) -> ((x +h y) -h (x +h w)) = (y -h w))
49	19, 48	syl 10	. . . . . . . . . . 11 |- ((((x e. B /\ y e. R) /\ v = (x +h y)) /\ ((z e. C /\ w e. S) /\ v = (z +h w))) -> ((x +h y) -h (x +h w)) = (y -h w))
50		hvsub4t 8827	. . . . . . . . . . . . . . . 16 |- (((z e. H~ /\ w e. H~) /\ (x e. H~ /\ w e. H~)) -> ((z +h w) -h (x +h w)) = ((z -h x) +h (w -h w)))
51		pm3.27 323	. . . . . . . . . . . . . . . 16 |- ((x e. H~ /\ (z e. H~ /\ w e. H~)) -> (z e. H~ /\ w e. H~))
52		pm3.27 323	. . . . . . . . . . . . . . . . 17 |- ((z e. H~ /\ w e. H~) -> w e. H~)
53	52	anim2i 335	. . . . . . . . . . . . . . . 16 |- ((x e. H~ /\ (z e. H~ /\ w e. H~)) -> (x e. H~ /\ w e. H~))
54	50, 51, 53	sylanc 471	. . . . . . . . . . . . . . 15 |- ((x e. H~ /\ (z e. H~ /\ w e. H~)) -> ((z +h w) -h (x +h w)) = ((z -h x) +h (w -h w)))
55	22	ad2antll 407	. . . . . . . . . . . . . . . 16 |- ((x e. H~ /\ (z e. H~ /\ w e. H~)) -> (w -h w) = 0h)
56	55	opreq2d 3961	. . . . . . . . . . . . . . 15 |- ((x e. H~ /\ (z e. H~ /\ w e. H~)) -> ((z -h x) +h (w -h w)) = ((z -h x) +h 0h))
57		hvsubclt 8808	. . . . . . . . . . . . . . . . . 18 |- ((z e. H~ /\ x e. H~) -> (z -h x) e. H~)
58		ax-hvaddid 8795	. . . . . . . . . . . . . . . . . 18 |- ((z -h x) e. H~ -> ((z -h x) +h 0h) = (z -h x))
59	57, 58	syl 10	. . . . . . . . . . . . . . . . 17 |- ((z e. H~ /\ x e. H~) -> ((z -h x) +h 0h) = (z -h x))
60	59	ancoms 436	. . . . . . . . . . . . . . . 16 |- ((x e. H~ /\ z e. H~) -> ((z -h x) +h 0h) = (z -h x))
61	60	adantrr 395	. . . . . . . . . . . . . . 15 |- ((x e. H~ /\ (z e. H~ /\ w e. H~)) -> ((z -h x) +h 0h) = (z -h x))
62	54, 56, 61	3eqtrd 1503	. . . . . . . . . . . . . 14 |- ((x e. H~ /\ (z e. H~ /\ w e. H~)) -> ((z +h w) -h (x +h w)) = (z -h x))
63	62	adantlr 393	. . . . . . . . . . . . 13 |- (((x e. H~ /\ y e. H~) /\ (z e. H~ /\ w e. H~)) -> ((z +h w) -h (x +h w)) = (z -h x))
64	63	adantlr 393	. . . . . . . . . . . 12 |- ((((x e. H~