Theorem mayete3i

Description: Mayet's equation E_3. Part of Theorem 4.1 of Mayet3 p. 1223. (Contributed by NM, 22-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mayete3.a	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	mayete3.b	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
	mayete3.c	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
	mayete3.d	$$⊢D\in {\mathbf{C}}_{\mathscr{H}}$$
	mayete3.f	$$⊢F\in {\mathbf{C}}_{\mathscr{H}}$$
	mayete3.g	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
	mayete3.ac	$$⊢A\subseteq \perp \left(C\right)$$
	mayete3.af	$$⊢A\subseteq \perp \left(F\right)$$
	mayete3.cf	$$⊢C\subseteq \perp \left(F\right)$$
	mayete3.ab	$$⊢A\subseteq \perp \left(B\right)$$
	mayete3.cd	$$⊢C\subseteq \perp \left(D\right)$$
	mayete3.fg	$$⊢F\subseteq \perp \left(G\right)$$
	mayete3.x	$$⊢X=\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F$$
	mayete3.y	$$⊢Y=\left(\left(A{\vee }_{\mathscr{H}}B\right)\cap \left(C{\vee }_{\mathscr{H}}D\right)\right)\cap \left(F{\vee }_{\mathscr{H}}G\right)$$
	mayete3.z	$$⊢Z=\left(B{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}G$$
Assertion	mayete3i	$$⊢X\cap Y\subseteq Z$$

Proof

Step	Hyp	Ref	Expression
1		mayete3.a	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		mayete3.b	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		mayete3.c	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
4		mayete3.d	$$⊢D\in {\mathbf{C}}_{\mathscr{H}}$$
5		mayete3.f	$$⊢F\in {\mathbf{C}}_{\mathscr{H}}$$
6		mayete3.g	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
7		mayete3.ac	$$⊢A\subseteq \perp \left(C\right)$$
8		mayete3.af	$$⊢A\subseteq \perp \left(F\right)$$
9		mayete3.cf	$$⊢C\subseteq \perp \left(F\right)$$
10		mayete3.ab	$$⊢A\subseteq \perp \left(B\right)$$
11		mayete3.cd	$$⊢C\subseteq \perp \left(D\right)$$
12		mayete3.fg	$$⊢F\subseteq \perp \left(G\right)$$
13		mayete3.x	$$⊢X=\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F$$
14		mayete3.y	$$⊢Y=\left(\left(A{\vee }_{\mathscr{H}}B\right)\cap \left(C{\vee }_{\mathscr{H}}D\right)\right)\cap \left(F{\vee }_{\mathscr{H}}G\right)$$
15		mayete3.z	$$⊢Z=\left(B{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}G$$
16		elin	$$⊢x\in \left(X\cap Y\right)\leftrightarrow \left(x\in X\wedge x\in Y\right)$$
17	1 3	chjcli	$$⊢A{\vee }_{\mathscr{H}}C\in {\mathbf{C}}_{\mathscr{H}}$$
18	17 5	chjcli	$$⊢\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\in {\mathbf{C}}_{\mathscr{H}}$$
19	18	cheli	$$⊢x\in \left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right)\to x\in \mathscr{H}$$
20	19 13	eleq2s	$$⊢x\in X\to x\in \mathscr{H}$$
21	20	adantr	$$⊢\left(x\in X\wedge x\in Y\right)\to x\in \mathscr{H}$$
22	16 21	sylbi	$$⊢x\in \left(X\cap Y\right)\to x\in \mathscr{H}$$
23		ax-hvmulid	$$⊢x\in \mathscr{H}\to 1{\cdot }_{ℎ}x=x$$
24		2cn	$$⊢2\in ℂ$$
25		2ne0	$$⊢2\ne 0$$
26		recid2	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)\to \left(\frac{1}{2}\right)\cdot 2=1$$
27	24 25 26	mp2an	$$⊢\left(\frac{1}{2}\right)\cdot 2=1$$
28	27	oveq1i	$$⊢\left(\frac{1}{2}\right)\cdot 2{\cdot }_{ℎ}x=1{\cdot }_{ℎ}x$$
29		halfcn	$$⊢\frac{1}{2}\in ℂ$$
30		ax-hvmulass	$$⊢\left(\frac{1}{2}\in ℂ\wedge 2\in ℂ\wedge x\in \mathscr{H}\right)\to \left(\frac{1}{2}\right)\cdot 2{\cdot }_{ℎ}x=\left(\frac{1}{2}\right){\cdot }_{ℎ}\left(2{\cdot }_{ℎ}x\right)$$
31	29 24 30	mp3an12	$$⊢x\in \mathscr{H}\to \left(\frac{1}{2}\right)\cdot 2{\cdot }_{ℎ}x=\left(\frac{1}{2}\right){\cdot }_{ℎ}\left(2{\cdot }_{ℎ}x\right)$$
32	28 31	syl5eqr	$$⊢x\in \mathscr{H}\to 1{\cdot }_{ℎ}x=\left(\frac{1}{2}\right){\cdot }_{ℎ}\left(2{\cdot }_{ℎ}x\right)$$
33	23 32	eqtr3d	$$⊢x\in \mathscr{H}\to x=\left(\frac{1}{2}\right){\cdot }_{ℎ}\left(2{\cdot }_{ℎ}x\right)$$
34	22 33	syl	$$⊢x\in \left(X\cap Y\right)\to x=\left(\frac{1}{2}\right){\cdot }_{ℎ}\left(2{\cdot }_{ℎ}x\right)$$
35		hv2times	$$⊢x\in \mathscr{H}\to 2{\cdot }_{ℎ}x=x{+}_{ℎ}x$$
36	35	oveq1d	$$⊢x\in \mathscr{H}\to \left(2{\cdot }_{ℎ}x\right){+}_{ℎ}x=\left(x{+}_{ℎ}x\right){+}_{ℎ}x$$
37	22 36	syl	$$⊢x\in \left(X\cap Y\right)\to \left(2{\cdot }_{ℎ}x\right){+}_{ℎ}x=\left(x{+}_{ℎ}x\right){+}_{ℎ}x$$
38		inss2	$$⊢X\cap Y\subseteq Y$$
39	38	sseli	$$⊢x\in \left(X\cap Y\right)\to x\in Y$$
40	14	elin2	$$⊢x\in Y\leftrightarrow \left(x\in \left(\left(A{\vee }_{\mathscr{H}}B\right)\cap \left(C{\vee }_{\mathscr{H}}D\right)\right)\wedge x\in \left(F{\vee }_{\mathscr{H}}G\right)\right)$$
41		elin	$$⊢x\in \left(\left(A{\vee }_{\mathscr{H}}B\right)\cap \left(C{\vee }_{\mathscr{H}}D\right)\right)\leftrightarrow \left(x\in \left(A{\vee }_{\mathscr{H}}B\right)\wedge x\in \left(C{\vee }_{\mathscr{H}}D\right)\right)$$
42	1 2	pjdsi	$$⊢\left(x\in \left(A{\vee }_{\mathscr{H}}B\right)\wedge A\subseteq \perp \left(B\right)\right)\to x={\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right)$$
43	10 42	mpan2	$$⊢x\in \left(A{\vee }_{\mathscr{H}}B\right)\to x={\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right)$$
44	3 4	pjdsi	$$⊢\left(x\in \left(C{\vee }_{\mathscr{H}}D\right)\wedge C\subseteq \perp \left(D\right)\right)\to x={\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)$$
45	11 44	mpan2	$$⊢x\in \left(C{\vee }_{\mathscr{H}}D\right)\to x={\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)$$
46	43 45	oveqan12d	$$⊢\left(x\in \left(A{\vee }_{\mathscr{H}}B\right)\wedge x\in \left(C{\vee }_{\mathscr{H}}D\right)\right)\to x{+}_{ℎ}x=\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right)$$
47	41 46	sylbi	$$⊢x\in \left(\left(A{\vee }_{\mathscr{H}}B\right)\cap \left(C{\vee }_{\mathscr{H}}D\right)\right)\to x{+}_{ℎ}x=\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right)$$
48		inss1	$$⊢\left(A{\vee }_{\mathscr{H}}B\right)\cap \left(C{\vee }_{\mathscr{H}}D\right)\subseteq A{\vee }_{\mathscr{H}}B$$
49	48	sseli	$$⊢x\in \left(\left(A{\vee }_{\mathscr{H}}B\right)\cap \left(C{\vee }_{\mathscr{H}}D\right)\right)\to x\in \left(A{\vee }_{\mathscr{H}}B\right)$$
50	1 2	chjcli	$$⊢A{\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}$$
51	50	cheli	$$⊢x\in \left(A{\vee }_{\mathscr{H}}B\right)\to x\in \mathscr{H}$$
52	1	pjhcli	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right)\in \mathscr{H}$$
53	2	pjhcli	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right)\in \mathscr{H}$$
54	3	pjhcli	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\in \mathscr{H}$$
55	4	pjhcli	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\in \mathscr{H}$$
56		hvadd4	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right)\in \mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right)\in \mathscr{H}\right)\wedge \left({\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\in \mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\in \mathscr{H}\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right)$$
57	52 53 54 55 56	syl22anc	$$⊢x\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right)$$
58	49 51 57	3syl	$$⊢x\in \left(\left(A{\vee }_{\mathscr{H}}B\right)\cap \left(C{\vee }_{\mathscr{H}}D\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right)$$
59	47 58	eqtrd	$$⊢x\in \left(\left(A{\vee }_{\mathscr{H}}B\right)\cap \left(C{\vee }_{\mathscr{H}}D\right)\right)\to x{+}_{ℎ}x=\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right)$$
60	5 6	pjdsi	$$⊢\left(x\in \left(F{\vee }_{\mathscr{H}}G\right)\wedge F\subseteq \perp \left(G\right)\right)\to x={\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)$$
61	12 60	mpan2	$$⊢x\in \left(F{\vee }_{\mathscr{H}}G\right)\to x={\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)$$
62	59 61	oveqan12d	$$⊢\left(x\in \left(\left(A{\vee }_{\mathscr{H}}B\right)\cap \left(C{\vee }_{\mathscr{H}}D\right)\right)\wedge x\in \left(F{\vee }_{\mathscr{H}}G\right)\right)\to \left(x{+}_{ℎ}x\right){+}_{ℎ}x=\left(\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)$$
63	40 62	sylbi	$$⊢x\in Y\to \left(x{+}_{ℎ}x\right){+}_{ℎ}x=\left(\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)$$
64	39 63	syl	$$⊢x\in \left(X\cap Y\right)\to \left(x{+}_{ℎ}x\right){+}_{ℎ}x=\left(\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)$$
65		hvaddcl	$$⊢\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right)\in \mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\in \mathscr{H}$$
66	52 54 65	syl2anc	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\in \mathscr{H}$$
67		hvaddcl	$$⊢\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right)\in \mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\in \mathscr{H}$$
68	53 55 67	syl2anc	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\in \mathscr{H}$$
69	5	pjhcli	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right)\in \mathscr{H}$$
70	6	pjhcli	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\in \mathscr{H}$$
71		hvadd4	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\in \mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\in \mathscr{H}\right)\wedge \left({\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right)\in \mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\in \mathscr{H}\right)\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)=\left(\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right)\right){+}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)$$
72	66 68 69 70 71	syl22anc	$$⊢x\in \mathscr{H}\to \left(\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)=\left(\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right)\right){+}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)$$
73	22 72	syl	$$⊢x\in \left(X\cap Y\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right)\right){+}_{ℎ}\left({\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)=\left(\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right)\right){+}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)$$
74	37 64 73	3eqtrd	$$⊢x\in \left(X\cap Y\right)\to \left(2{\cdot }_{ℎ}x\right){+}_{ℎ}x=\left(\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right)\right){+}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)$$
75		inss1	$$⊢X\cap Y\subseteq X$$
76	75	sseli	$$⊢x\in \left(X\cap Y\right)\to x\in X$$
77	76 13	eleqtrdi	$$⊢x\in \left(X\cap Y\right)\to x\in \left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right)$$
78	1 3 5	pjds3i	$$⊢\left(\left(x\in \left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right)\wedge A\subseteq \perp \left(C\right)\right)\wedge \left(A\subseteq \perp \left(F\right)\wedge C\subseteq \perp \left(F\right)\right)\right)\to x=\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right)$$
79	8 9 78	mpanr12	$$⊢\left(x\in \left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right)\wedge A\subseteq \perp \left(C\right)\right)\to x=\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right)$$
80	77 7 79	sylancl	$$⊢x\in \left(X\cap Y\right)\to x=\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right)$$
81	74 80	oveq12d	$$⊢x\in \left(X\cap Y\right)\to \left(\left(2{\cdot }_{ℎ}x\right){+}_{ℎ}x\right){-}_{ℎ}x=\left(\left(\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right)\right){+}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\right){-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right)\right)$$
82		hvmulcl	$$⊢\left(2\in ℂ\wedge x\in \mathscr{H}\right)\to 2{\cdot }_{ℎ}x\in \mathscr{H}$$
83	24 82	mpan	$$⊢x\in \mathscr{H}\to 2{\cdot }_{ℎ}x\in \mathscr{H}$$
84		hvpncan	$$⊢\left(2{\cdot }_{ℎ}x\in \mathscr{H}\wedge x\in \mathscr{H}\right)\to \left(\left(2{\cdot }_{ℎ}x\right){+}_{ℎ}x\right){-}_{ℎ}x=2{\cdot }_{ℎ}x$$
85	83 84	mpancom	$$⊢x\in \mathscr{H}\to \left(\left(2{\cdot }_{ℎ}x\right){+}_{ℎ}x\right){-}_{ℎ}x=2{\cdot }_{ℎ}x$$
86	22 85	syl	$$⊢x\in \left(X\cap Y\right)\to \left(\left(2{\cdot }_{ℎ}x\right){+}_{ℎ}x\right){-}_{ℎ}x=2{\cdot }_{ℎ}x$$
87	81 86	eqtr3d	$$⊢x\in \left(X\cap Y\right)\to \left(\left(\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right)\right){+}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\right){-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right)\right)=2{\cdot }_{ℎ}x$$
88		hvaddcl	$$⊢\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\in \mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right)\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right)\in \mathscr{H}$$
89	66 69 88	syl2anc	$$⊢x\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right)\in \mathscr{H}$$
90		hvaddcl	$$⊢\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\in \mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\in \mathscr{H}$$
91	68 70 90	syl2anc	$$⊢x\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\in \mathscr{H}$$
92		hvpncan2	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right)\in \mathscr{H}\wedge \left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\in \mathscr{H}\right)\to \left(\left(\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right)\right){+}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\right){-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)$$
93	89 91 92	syl2anc	$$⊢x\in \mathscr{H}\to \left(\left(\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right)\right){+}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\right){-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)$$
94	22 93	syl	$$⊢x\in \left(X\cap Y\right)\to \left(\left(\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right)\right){+}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\right)\right){-}_{ℎ}\left(\left({\mathrm{proj}}_{ℎ}\left(A\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(C\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(F\right)\left(x\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)$$
95	87 94	eqtr3d	$$⊢x\in \left(X\cap Y\right)\to 2{\cdot }_{ℎ}x=\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)$$
96	2	pjcli	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right)\in B$$
97	4	pjcli	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\in D$$
98	2	chshii	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
99	4	chshii	$$⊢D\in {\mathbf{S}}_{\mathscr{H}}$$
100	98 99	shsvai	$$⊢\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right)\in B\wedge {\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\in D\right)\to {\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\in \left(B{+}_{\mathscr{H}}D\right)$$
101	96 97 100	syl2anc	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\in \left(B{+}_{\mathscr{H}}D\right)$$
102	6	pjcli	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\in G$$
103	98 99	shscli	$$⊢B{+}_{\mathscr{H}}D\in {\mathbf{S}}_{\mathscr{H}}$$
104	6	chshii	$$⊢G\in {\mathbf{S}}_{\mathscr{H}}$$
105	103 104	shsvai	$$⊢\left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\in \left(B{+}_{\mathscr{H}}D\right)\wedge {\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\in G\right)\to \left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\in \left(\left(B{+}_{\mathscr{H}}D\right){+}_{\mathscr{H}}G\right)$$
106	101 102 105	syl2anc	$$⊢x\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\in \left(\left(B{+}_{\mathscr{H}}D\right){+}_{\mathscr{H}}G\right)$$
107	22 106	syl	$$⊢x\in \left(X\cap Y\right)\to \left({\mathrm{proj}}_{ℎ}\left(B\right)\left(x\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(D\right)\left(x\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(x\right)\in \left(\left(B{+}_{\mathscr{H}}D\right){+}_{\mathscr{H}}G\right)$$
108	95 107	eqeltrd	$$⊢x\in \left(X\cap Y\right)\to 2{\cdot }_{ℎ}x\in \left(\left(B{+}_{\mathscr{H}}D\right){+}_{\mathscr{H}}G\right)$$
109	103 104	shscli	$$⊢\left(B{+}_{\mathscr{H}}D\right){+}_{\mathscr{H}}G\in {\mathbf{S}}_{\mathscr{H}}$$
110		shmulcl	$$⊢\left(\left(B{+}_{\mathscr{H}}D\right){+}_{\mathscr{H}}G\in {\mathbf{S}}_{\mathscr{H}}\wedge \frac{1}{2}\in ℂ\wedge 2{\cdot }_{ℎ}x\in \left(\left(B{+}_{\mathscr{H}}D\right){+}_{\mathscr{H}}G\right)\right)\to \left(\frac{1}{2}\right){\cdot }_{ℎ}\left(2{\cdot }_{ℎ}x\right)\in \left(\left(B{+}_{\mathscr{H}}D\right){+}_{\mathscr{H}}G\right)$$
111	109 29 110	mp3an12	$$⊢2{\cdot }_{ℎ}x\in \left(\left(B{+}_{\mathscr{H}}D\right){+}_{\mathscr{H}}G\right)\to \left(\frac{1}{2}\right){\cdot }_{ℎ}\left(2{\cdot }_{ℎ}x\right)\in \left(\left(B{+}_{\mathscr{H}}D\right){+}_{\mathscr{H}}G\right)$$
112	108 111	syl	$$⊢x\in \left(X\cap Y\right)\to \left(\frac{1}{2}\right){\cdot }_{ℎ}\left(2{\cdot }_{ℎ}x\right)\in \left(\left(B{+}_{\mathscr{H}}D\right){+}_{\mathscr{H}}G\right)$$
113	34 112	eqeltrd	$$⊢x\in \left(X\cap Y\right)\to x\in \left(\left(B{+}_{\mathscr{H}}D\right){+}_{\mathscr{H}}G\right)$$
114	113	ssriv	$$⊢X\cap Y\subseteq \left(B{+}_{\mathscr{H}}D\right){+}_{\mathscr{H}}G$$
115	2 4	chsleji	$$⊢B{+}_{\mathscr{H}}D\subseteq B{\vee }_{\mathscr{H}}D$$
116	2 4	chjcli	$$⊢B{\vee }_{\mathscr{H}}D\in {\mathbf{C}}_{\mathscr{H}}$$
117	116	chshii	$$⊢B{\vee }_{\mathscr{H}}D\in {\mathbf{S}}_{\mathscr{H}}$$
118	103 117 104	shlessi	$$⊢B{+}_{\mathscr{H}}D\subseteq B{\vee }_{\mathscr{H}}D\to \left(B{+}_{\mathscr{H}}D\right){+}_{\mathscr{H}}G\subseteq \left(B{\vee }_{\mathscr{H}}D\right){+}_{\mathscr{H}}G$$
119	115 118	ax-mp	$$⊢\left(B{+}_{\mathscr{H}}D\right){+}_{\mathscr{H}}G\subseteq \left(B{\vee }_{\mathscr{H}}D\right){+}_{\mathscr{H}}G$$
120	114 119	sstri	$$⊢X\cap Y\subseteq \left(B{\vee }_{\mathscr{H}}D\right){+}_{\mathscr{H}}G$$
121	116 6	chsleji	$$⊢\left(B{\vee }_{\mathscr{H}}D\right){+}_{\mathscr{H}}G\subseteq \left(B{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}G$$
122	120 121	sstri	$$⊢X\cap Y\subseteq \left(B{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}G$$
123	122 15	sseqtrri	$$⊢X\cap Y\subseteq Z$$