Theorem mayetes3i

Description: Mayet's equation E^*_3, derived from E_3. Solution, for n = 3, to open problem in Remark (b) after Theorem 7.1 of Mayet3 p. 1240. (Contributed by NM, 10-May-2009) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mayetes3.a	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	mayetes3.b	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
	mayetes3.c	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
	mayetes3.d	$$⊢D\in {\mathbf{C}}_{\mathscr{H}}$$
	mayetes3.f	$$⊢F\in {\mathbf{C}}_{\mathscr{H}}$$
	mayetes3.g	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
	mayetes3.r	$$⊢R\in {\mathbf{C}}_{\mathscr{H}}$$
	mayetes3.ac	$$⊢A\subseteq \perp \left(C\right)$$
	mayetes3.af	$$⊢A\subseteq \perp \left(F\right)$$
	mayetes3.cf	$$⊢C\subseteq \perp \left(F\right)$$
	mayetes3.ab	$$⊢A\subseteq \perp \left(B\right)$$
	mayetes3.cd	$$⊢C\subseteq \perp \left(D\right)$$
	mayetes3.fg	$$⊢F\subseteq \perp \left(G\right)$$
	mayetes3.rx	$$⊢R\subseteq \perp \left(X\right)$$
	mayetes3.x	$$⊢X=\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F$$
	mayetes3.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)$$
	mayetes3.z	$$⊢Z=\left(B{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}G$$
Assertion	mayetes3i	$$⊢\left(X{\vee }_{\mathscr{H}}R\right)\cap Y\subseteq Z{\vee }_{\mathscr{H}}R$$

Proof

Step	Hyp	Ref	Expression
1		mayetes3.a	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		mayetes3.b	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		mayetes3.c	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
4		mayetes3.d	$$⊢D\in {\mathbf{C}}_{\mathscr{H}}$$
5		mayetes3.f	$$⊢F\in {\mathbf{C}}_{\mathscr{H}}$$
6		mayetes3.g	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
7		mayetes3.r	$$⊢R\in {\mathbf{C}}_{\mathscr{H}}$$
8		mayetes3.ac	$$⊢A\subseteq \perp \left(C\right)$$
9		mayetes3.af	$$⊢A\subseteq \perp \left(F\right)$$
10		mayetes3.cf	$$⊢C\subseteq \perp \left(F\right)$$
11		mayetes3.ab	$$⊢A\subseteq \perp \left(B\right)$$
12		mayetes3.cd	$$⊢C\subseteq \perp \left(D\right)$$
13		mayetes3.fg	$$⊢F\subseteq \perp \left(G\right)$$
14		mayetes3.rx	$$⊢R\subseteq \perp \left(X\right)$$
15		mayetes3.x	$$⊢X=\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F$$
16		mayetes3.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)$$
17		mayetes3.z	$$⊢Z=\left(B{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}G$$
18	1 3	chjcli	$$⊢A{\vee }_{\mathscr{H}}C\in {\mathbf{C}}_{\mathscr{H}}$$
19	18 5	chjcli	$$⊢\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\in {\mathbf{C}}_{\mathscr{H}}$$
20	19 7	chjcomi	$$⊢\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right){\vee }_{\mathscr{H}}R=R{\vee }_{\mathscr{H}}\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right)$$
21	20	eqimssi	$$⊢\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right){\vee }_{\mathscr{H}}R\subseteq R{\vee }_{\mathscr{H}}\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right)$$
22	1 2	chjcli	$$⊢A{\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}$$
23	22 7	chub1i	$$⊢A{\vee }_{\mathscr{H}}B\subseteq \left(A{\vee }_{\mathscr{H}}B\right){\vee }_{\mathscr{H}}R$$
24	1 2 7	chjassi	$$⊢\left(A{\vee }_{\mathscr{H}}B\right){\vee }_{\mathscr{H}}R=A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)$$
25	23 24	sseqtri	$$⊢A{\vee }_{\mathscr{H}}B\subseteq A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)$$
26	2 7	chjcli	$$⊢B{\vee }_{\mathscr{H}}R\in {\mathbf{C}}_{\mathscr{H}}$$
27	1 26	chjcli	$$⊢A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\in {\mathbf{C}}_{\mathscr{H}}$$
28	27 7	chub2i	$$⊢A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\subseteq R{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)$$
29	25 28	sstri	$$⊢A{\vee }_{\mathscr{H}}B\subseteq R{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)$$
30	3 4	chjcli	$$⊢C{\vee }_{\mathscr{H}}D\in {\mathbf{C}}_{\mathscr{H}}$$
31	30 7	chub1i	$$⊢C{\vee }_{\mathscr{H}}D\subseteq \left(C{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}R$$
32	3 4 7	chjassi	$$⊢\left(C{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}R=C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)$$
33	31 32	sseqtri	$$⊢C{\vee }_{\mathscr{H}}D\subseteq C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)$$
34	4 7	chjcli	$$⊢D{\vee }_{\mathscr{H}}R\in {\mathbf{C}}_{\mathscr{H}}$$
35	3 34	chjcli	$$⊢C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\in {\mathbf{C}}_{\mathscr{H}}$$
36	35 7	chub2i	$$⊢C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\subseteq R{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)$$
37	33 36	sstri	$$⊢C{\vee }_{\mathscr{H}}D\subseteq R{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)$$
38		ss2in	$$⊢\left(A{\vee }_{\mathscr{H}}B\subseteq R{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\wedge C{\vee }_{\mathscr{H}}D\subseteq R{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\to \left(A{\vee }_{\mathscr{H}}B\right)\cap \left(C{\vee }_{\mathscr{H}}D\right)\subseteq \left(R{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)$$
39	29 37 38	mp2an	$$⊢\left(A{\vee }_{\mathscr{H}}B\right)\cap \left(C{\vee }_{\mathscr{H}}D\right)\subseteq \left(R{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)$$
40	5 6	chjcli	$$⊢F{\vee }_{\mathscr{H}}G\in {\mathbf{C}}_{\mathscr{H}}$$
41	40 7	chub1i	$$⊢F{\vee }_{\mathscr{H}}G\subseteq \left(F{\vee }_{\mathscr{H}}G\right){\vee }_{\mathscr{H}}R$$
42	5 6 7	chjassi	$$⊢\left(F{\vee }_{\mathscr{H}}G\right){\vee }_{\mathscr{H}}R=F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)$$
43	41 42	sseqtri	$$⊢F{\vee }_{\mathscr{H}}G\subseteq F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)$$
44	6 7	chjcli	$$⊢G{\vee }_{\mathscr{H}}R\in {\mathbf{C}}_{\mathscr{H}}$$
45	5 44	chjcli	$$⊢F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\in {\mathbf{C}}_{\mathscr{H}}$$
46	45 7	chub2i	$$⊢F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\subseteq R{\vee }_{\mathscr{H}}\left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)$$
47	43 46	sstri	$$⊢F{\vee }_{\mathscr{H}}G\subseteq R{\vee }_{\mathscr{H}}\left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)$$
48		ss2in	$$⊢\left(\left(A{\vee }_{\mathscr{H}}B\right)\cap \left(C{\vee }_{\mathscr{H}}D\right)\subseteq \left(R{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\wedge F{\vee }_{\mathscr{H}}G\subseteq R{\vee }_{\mathscr{H}}\left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)\to \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)\subseteq \left(\left(R{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)$$
49	39 47 48	mp2an	$$⊢\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)\subseteq \left(\left(R{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)$$
50		ss2in	$$⊢\left(\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right){\vee }_{\mathscr{H}}R\subseteq R{\vee }_{\mathscr{H}}\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right)\wedge \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)\subseteq \left(\left(R{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)\right)\to \left(\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right){\vee }_{\mathscr{H}}R\right)\cap \left(\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)\right)\subseteq \left(R{\vee }_{\mathscr{H}}\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right)\right)\cap \left(\left(\left(R{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)\right)$$
51	21 49 50	mp2an	$$⊢\left(\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right){\vee }_{\mathscr{H}}R\right)\cap \left(\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)\right)\subseteq \left(R{\vee }_{\mathscr{H}}\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right)\right)\cap \left(\left(\left(R{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)\right)$$
52	27 35	chincli	$$⊢\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\cap \left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\in {\mathbf{C}}_{\mathscr{H}}$$
53	52 45	chincli	$$⊢\left(\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\cap \left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\in {\mathbf{C}}_{\mathscr{H}}$$
54	15 19	eqeltri	$$⊢X\in {\mathbf{C}}_{\mathscr{H}}$$
55	54	choccli	$$⊢\perp \left(X\right)\in {\mathbf{C}}_{\mathscr{H}}$$
56	7 55 14	lecmii	$$⊢R{𝐶}_{\mathscr{H}}\perp \left(X\right)$$
57	7 54	cmcm2i	$$⊢R{𝐶}_{\mathscr{H}}X\leftrightarrow R{𝐶}_{\mathscr{H}}\perp \left(X\right)$$
58	56 57	mpbir	$$⊢R{𝐶}_{\mathscr{H}}X$$
59	58 15	breqtri	$$⊢R{𝐶}_{\mathscr{H}}\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right)$$
60	7 2	chub2i	$$⊢R\subseteq B{\vee }_{\mathscr{H}}R$$
61	26 1	chub2i	$$⊢B{\vee }_{\mathscr{H}}R\subseteq A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)$$
62	60 61	sstri	$$⊢R\subseteq A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)$$
63	7 27 62	lecmii	$$⊢R{𝐶}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)$$
64	7 4	chub2i	$$⊢R\subseteq D{\vee }_{\mathscr{H}}R$$
65	34 3	chub2i	$$⊢D{\vee }_{\mathscr{H}}R\subseteq C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)$$
66	64 65	sstri	$$⊢R\subseteq C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)$$
67	7 35 66	lecmii	$$⊢R{𝐶}_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)$$
68	7 27 35 63 67	cm2mi	$$⊢R{𝐶}_{\mathscr{H}}\left(\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\cap \left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)$$
69	7 6	chub2i	$$⊢R\subseteq G{\vee }_{\mathscr{H}}R$$
70	44 5	chub2i	$$⊢G{\vee }_{\mathscr{H}}R\subseteq F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)$$
71	69 70	sstri	$$⊢R\subseteq F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)$$
72	7 45 71	lecmii	$$⊢R{𝐶}_{\mathscr{H}}\left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)$$
73	7 52 45 68 72	cm2mi	$$⊢R{𝐶}_{\mathscr{H}}\left(\left(\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\cap \left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)$$
74	7 19 53 59 73	fh3i	$$⊢R{\vee }_{\mathscr{H}}\left(\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right)\cap \left(\left(\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\cap \left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)\right)=\left(R{\vee }_{\mathscr{H}}\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(\left(\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\cap \left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)\right)$$
75	7 52 45 68 72	fh3i	$$⊢R{\vee }_{\mathscr{H}}\left(\left(\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\cap \left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)=\left(R{\vee }_{\mathscr{H}}\left(\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\cap \left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)$$
76	7 27 35 63 67	fh3i	$$⊢R{\vee }_{\mathscr{H}}\left(\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\cap \left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)=\left(R{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)$$
77	76	ineq1i	$$⊢\left(R{\vee }_{\mathscr{H}}\left(\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\cap \left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)=\left(\left(R{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)$$
78	75 77	eqtri	$$⊢R{\vee }_{\mathscr{H}}\left(\left(\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\cap \left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)=\left(\left(R{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)$$
79	78	ineq2i	$$⊢\left(R{\vee }_{\mathscr{H}}\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(\left(\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\cap \left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)\right)=\left(R{\vee }_{\mathscr{H}}\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right)\right)\cap \left(\left(\left(R{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)\right)$$
80	74 79	eqtr2i	$$⊢\left(R{\vee }_{\mathscr{H}}\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right)\right)\cap \left(\left(\left(R{\vee }_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\right)\cap \left(R{\vee }_{\mathscr{H}}\left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)\right)=R{\vee }_{\mathscr{H}}\left(\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right)\cap \left(\left(\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\cap \left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)\right)$$
81	51 80	sseqtri	$$⊢\left(\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right){\vee }_{\mathscr{H}}R\right)\cap \left(\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)\right)\subseteq R{\vee }_{\mathscr{H}}\left(\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right)\cap \left(\left(\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\cap \left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)\right)$$
82	2 4	chjcli	$$⊢B{\vee }_{\mathscr{H}}D\in {\mathbf{C}}_{\mathscr{H}}$$
83	82 6	chjcli	$$⊢\left(B{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}G\in {\mathbf{C}}_{\mathscr{H}}$$
84	7 83	chub2i	$$⊢R\subseteq \left(\left(B{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}G\right){\vee }_{\mathscr{H}}R$$
85	1 3	chub1i	$$⊢A\subseteq A{\vee }_{\mathscr{H}}C$$
86	18 5	chub1i	$$⊢A{\vee }_{\mathscr{H}}C\subseteq \left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F$$
87	86 15	sseqtrri	$$⊢A{\vee }_{\mathscr{H}}C\subseteq X$$
88	85 87	sstri	$$⊢A\subseteq X$$
89	1 54	chsscon3i	$$⊢A\subseteq X\leftrightarrow \perp \left(X\right)\subseteq \perp \left(A\right)$$
90	88 89	mpbi	$$⊢\perp \left(X\right)\subseteq \perp \left(A\right)$$
91	14 90	sstri	$$⊢R\subseteq \perp \left(A\right)$$
92	7 1	chsscon2i	$$⊢R\subseteq \perp \left(A\right)\leftrightarrow A\subseteq \perp \left(R\right)$$
93	91 92	mpbi	$$⊢A\subseteq \perp \left(R\right)$$
94	11 93	ssini	$$⊢A\subseteq \perp \left(B\right)\cap \perp \left(R\right)$$
95	2 7	chdmj1i	$$⊢\perp \left(B{\vee }_{\mathscr{H}}R\right)=\perp \left(B\right)\cap \perp \left(R\right)$$
96	94 95	sseqtrri	$$⊢A\subseteq \perp \left(B{\vee }_{\mathscr{H}}R\right)$$
97	3 1	chub2i	$$⊢C\subseteq A{\vee }_{\mathscr{H}}C$$
98	97 87	sstri	$$⊢C\subseteq X$$
99	3 54	chsscon3i	$$⊢C\subseteq X\leftrightarrow \perp \left(X\right)\subseteq \perp \left(C\right)$$
100	98 99	mpbi	$$⊢\perp \left(X\right)\subseteq \perp \left(C\right)$$
101	14 100	sstri	$$⊢R\subseteq \perp \left(C\right)$$
102	7 3	chsscon2i	$$⊢R\subseteq \perp \left(C\right)\leftrightarrow C\subseteq \perp \left(R\right)$$
103	101 102	mpbi	$$⊢C\subseteq \perp \left(R\right)$$
104	12 103	ssini	$$⊢C\subseteq \perp \left(D\right)\cap \perp \left(R\right)$$
105	4 7	chdmj1i	$$⊢\perp \left(D{\vee }_{\mathscr{H}}R\right)=\perp \left(D\right)\cap \perp \left(R\right)$$
106	104 105	sseqtrri	$$⊢C\subseteq \perp \left(D{\vee }_{\mathscr{H}}R\right)$$
107	5 18	chub2i	$$⊢F\subseteq \left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F$$
108	107 15	sseqtrri	$$⊢F\subseteq X$$
109	5 54	chsscon3i	$$⊢F\subseteq X\leftrightarrow \perp \left(X\right)\subseteq \perp \left(F\right)$$
110	108 109	mpbi	$$⊢\perp \left(X\right)\subseteq \perp \left(F\right)$$
111	14 110	sstri	$$⊢R\subseteq \perp \left(F\right)$$
112	7 5	chsscon2i	$$⊢R\subseteq \perp \left(F\right)\leftrightarrow F\subseteq \perp \left(R\right)$$
113	111 112	mpbi	$$⊢F\subseteq \perp \left(R\right)$$
114	13 113	ssini	$$⊢F\subseteq \perp \left(G\right)\cap \perp \left(R\right)$$
115	6 7	chdmj1i	$$⊢\perp \left(G{\vee }_{\mathscr{H}}R\right)=\perp \left(G\right)\cap \perp \left(R\right)$$
116	114 115	sseqtrri	$$⊢F\subseteq \perp \left(G{\vee }_{\mathscr{H}}R\right)$$
117		eqid	$$⊢\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F=\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F$$
118		eqid	$$⊢\left(\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\cap \left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)=\left(\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\cap \left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)$$
119	82 6 7	chjjdiri	$$⊢\left(\left(B{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}G\right){\vee }_{\mathscr{H}}R=\left(\left(B{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}R\right){\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)$$
120	2 4 7	chjjdiri	$$⊢\left(B{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}R=\left(B{\vee }_{\mathscr{H}}R\right){\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)$$
121	120	oveq1i	$$⊢\left(\left(B{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}R\right){\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)=\left(\left(B{\vee }_{\mathscr{H}}R\right){\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right){\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)$$
122	119 121	eqtri	$$⊢\left(\left(B{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}G\right){\vee }_{\mathscr{H}}R=\left(\left(B{\vee }_{\mathscr{H}}R\right){\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right){\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)$$
123	1 26 3 34 5 44 8 9 10 96 106 116 117 118 122	mayete3i	$$⊢\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right)\cap \left(\left(\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\cap \left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)\subseteq \left(\left(B{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}G\right){\vee }_{\mathscr{H}}R$$
124	19 53	chincli	$$⊢\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right)\cap \left(\left(\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\cap \left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)\in {\mathbf{C}}_{\mathscr{H}}$$
125	83 7	chjcli	$$⊢\left(\left(B{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}G\right){\vee }_{\mathscr{H}}R\in {\mathbf{C}}_{\mathscr{H}}$$
126	7 124 125	chlubii	$$⊢\left(R\subseteq \left(\left(B{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}G\right){\vee }_{\mathscr{H}}R\wedge \left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right)\cap \left(\left(\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\cap \left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)\subseteq \left(\left(B{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}G\right){\vee }_{\mathscr{H}}R\right)\to R{\vee }_{\mathscr{H}}\left(\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right)\cap \left(\left(\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\cap \left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)\right)\subseteq \left(\left(B{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}G\right){\vee }_{\mathscr{H}}R$$
127	84 123 126	mp2an	$$⊢R{\vee }_{\mathscr{H}}\left(\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right)\cap \left(\left(\left(A{\vee }_{\mathscr{H}}\left(B{\vee }_{\mathscr{H}}R\right)\right)\cap \left(C{\vee }_{\mathscr{H}}\left(D{\vee }_{\mathscr{H}}R\right)\right)\right)\cap \left(F{\vee }_{\mathscr{H}}\left(G{\vee }_{\mathscr{H}}R\right)\right)\right)\right)\subseteq \left(\left(B{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}G\right){\vee }_{\mathscr{H}}R$$
128	81 127	sstri	$$⊢\left(\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right){\vee }_{\mathscr{H}}R\right)\cap \left(\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)\right)\subseteq \left(\left(B{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}G\right){\vee }_{\mathscr{H}}R$$
129	15	oveq1i	$$⊢X{\vee }_{\mathscr{H}}R=\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right){\vee }_{\mathscr{H}}R$$
130	129 16	ineq12i	$$⊢\left(X{\vee }_{\mathscr{H}}R\right)\cap Y=\left(\left(\left(A{\vee }_{\mathscr{H}}C\right){\vee }_{\mathscr{H}}F\right){\vee }_{\mathscr{H}}R\right)\cap \left(\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)\right)$$
131	17	oveq1i	$$⊢Z{\vee }_{\mathscr{H}}R=\left(\left(B{\vee }_{\mathscr{H}}D\right){\vee }_{\mathscr{H}}G\right){\vee }_{\mathscr{H}}R$$
132	128 130 131	3sstr4i	$$⊢\left(X{\vee }_{\mathscr{H}}R\right)\cap Y\subseteq Z{\vee }_{\mathscr{H}}R$$