# Metamath Proof Explorer

## 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}}_{ℋ}$
mayetes3.b ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
mayetes3.c ${⊢}{C}\in {\mathbf{C}}_{ℋ}$
mayetes3.d ${⊢}{D}\in {\mathbf{C}}_{ℋ}$
mayetes3.f ${⊢}{F}\in {\mathbf{C}}_{ℋ}$
mayetes3.g ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
mayetes3.r ${⊢}{R}\in {\mathbf{C}}_{ℋ}$
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 }_{ℋ}{C}\right){\vee }_{ℋ}{F}$
mayetes3.y ${⊢}{Y}=\left(\left({A}{\vee }_{ℋ}{B}\right)\cap \left({C}{\vee }_{ℋ}{D}\right)\right)\cap \left({F}{\vee }_{ℋ}{G}\right)$
mayetes3.z ${⊢}{Z}=\left({B}{\vee }_{ℋ}{D}\right){\vee }_{ℋ}{G}$
Assertion mayetes3i ${⊢}\left({X}{\vee }_{ℋ}{R}\right)\cap {Y}\subseteq {Z}{\vee }_{ℋ}{R}$

### Proof

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