# Metamath Proof Explorer

## Theorem dmdmd

Description: The dual modular pair property expressed in terms of the modular pair property, that hold in Hilbert lattices. Remark 29.6 of MaedaMaeda p. 130. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion dmdmd ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{𝑀}_{ℋ}^{*}{B}↔\perp \left({A}\right){𝑀}_{ℋ}\perp \left({B}\right)\right)$

### Proof

Step Hyp Ref Expression
1 sseq1 ${⊢}{y}=\perp \left({x}\right)\to \left({y}\subseteq \perp \left({B}\right)↔\perp \left({x}\right)\subseteq \perp \left({B}\right)\right)$
2 oveq1 ${⊢}{y}=\perp \left({x}\right)\to {y}{\vee }_{ℋ}\perp \left({A}\right)=\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)$
3 2 ineq1d ${⊢}{y}=\perp \left({x}\right)\to \left({y}{\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)=\left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)$
4 oveq1 ${⊢}{y}=\perp \left({x}\right)\to {y}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)=\perp \left({x}\right){\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)$
5 3 4 eqeq12d ${⊢}{y}=\perp \left({x}\right)\to \left(\left({y}{\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)={y}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)↔\left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)=\perp \left({x}\right){\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)$
6 1 5 imbi12d ${⊢}{y}=\perp \left({x}\right)\to \left(\left({y}\subseteq \perp \left({B}\right)\to \left({y}{\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)={y}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)↔\left(\perp \left({x}\right)\subseteq \perp \left({B}\right)\to \left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)=\perp \left({x}\right){\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)\right)$
7 6 rspccv ${⊢}\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq \perp \left({B}\right)\to \left({y}{\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)={y}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)\to \left(\perp \left({x}\right)\in {\mathbf{C}}_{ℋ}\to \left(\perp \left({x}\right)\subseteq \perp \left({B}\right)\to \left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)=\perp \left({x}\right){\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)\right)$
8 choccl ${⊢}{x}\in {\mathbf{C}}_{ℋ}\to \perp \left({x}\right)\in {\mathbf{C}}_{ℋ}$
9 8 imim1i ${⊢}\left(\perp \left({x}\right)\in {\mathbf{C}}_{ℋ}\to \left(\perp \left({x}\right)\subseteq \perp \left({B}\right)\to \left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)=\perp \left({x}\right){\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)\right)\to \left({x}\in {\mathbf{C}}_{ℋ}\to \left(\perp \left({x}\right)\subseteq \perp \left({B}\right)\to \left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)=\perp \left({x}\right){\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)\right)$
10 9 com12 ${⊢}{x}\in {\mathbf{C}}_{ℋ}\to \left(\left(\perp \left({x}\right)\in {\mathbf{C}}_{ℋ}\to \left(\perp \left({x}\right)\subseteq \perp \left({B}\right)\to \left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)=\perp \left({x}\right){\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)\right)\to \left(\perp \left({x}\right)\subseteq \perp \left({B}\right)\to \left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)=\perp \left({x}\right){\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)\right)$
11 10 adantl ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left(\perp \left({x}\right)\in {\mathbf{C}}_{ℋ}\to \left(\perp \left({x}\right)\subseteq \perp \left({B}\right)\to \left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)=\perp \left({x}\right){\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)\right)\to \left(\perp \left({x}\right)\subseteq \perp \left({B}\right)\to \left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)=\perp \left({x}\right){\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)\right)$
12 chsscon3 ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left({B}\subseteq {x}↔\perp \left({x}\right)\subseteq \perp \left({B}\right)\right)$
13 12 biimpd ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left({B}\subseteq {x}\to \perp \left({x}\right)\subseteq \perp \left({B}\right)\right)$
14 13 adantll ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left({B}\subseteq {x}\to \perp \left({x}\right)\subseteq \perp \left({B}\right)\right)$
15 fveq2 ${⊢}\left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)=\perp \left({x}\right){\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\to \perp \left(\left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)\right)=\perp \left(\perp \left({x}\right){\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)$
16 choccl ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to \perp \left({A}\right)\in {\mathbf{C}}_{ℋ}$
17 chjcl ${⊢}\left(\perp \left({x}\right)\in {\mathbf{C}}_{ℋ}\wedge \perp \left({A}\right)\in {\mathbf{C}}_{ℋ}\right)\to \perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\in {\mathbf{C}}_{ℋ}$
18 8 16 17 syl2an ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\in {\mathbf{C}}_{ℋ}$
19 chdmm3 ${⊢}\left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left(\left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)\right)=\perp \left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right){\vee }_{ℋ}{B}$
20 18 19 sylan ${⊢}\left(\left({x}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left(\left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)\right)=\perp \left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right){\vee }_{ℋ}{B}$
21 chdmj4 ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)={x}\cap {A}$
22 21 adantr ${⊢}\left(\left({x}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)={x}\cap {A}$
23 22 oveq1d ${⊢}\left(\left({x}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right){\vee }_{ℋ}{B}=\left({x}\cap {A}\right){\vee }_{ℋ}{B}$
24 20 23 eqtrd ${⊢}\left(\left({x}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left(\left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)\right)=\left({x}\cap {A}\right){\vee }_{ℋ}{B}$
25 24 anasss ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge \left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\right)\to \perp \left(\left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)\right)=\left({x}\cap {A}\right){\vee }_{ℋ}{B}$
26 choccl ${⊢}{B}\in {\mathbf{C}}_{ℋ}\to \perp \left({B}\right)\in {\mathbf{C}}_{ℋ}$
27 chincl ${⊢}\left(\perp \left({A}\right)\in {\mathbf{C}}_{ℋ}\wedge \perp \left({B}\right)\in {\mathbf{C}}_{ℋ}\right)\to \perp \left({A}\right)\cap \perp \left({B}\right)\in {\mathbf{C}}_{ℋ}$
28 16 26 27 syl2an ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left({A}\right)\cap \perp \left({B}\right)\in {\mathbf{C}}_{ℋ}$
29 chdmj2 ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge \perp \left({A}\right)\cap \perp \left({B}\right)\in {\mathbf{C}}_{ℋ}\right)\to \perp \left(\perp \left({x}\right){\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)={x}\cap \perp \left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)$
30 28 29 sylan2 ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge \left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\right)\to \perp \left(\perp \left({x}\right){\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)={x}\cap \perp \left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)$
31 chdmm4 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)={A}{\vee }_{ℋ}{B}$
32 31 adantl ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge \left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\right)\to \perp \left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)={A}{\vee }_{ℋ}{B}$
33 32 ineq2d ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge \left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\right)\to {x}\cap \perp \left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)={x}\cap \left({A}{\vee }_{ℋ}{B}\right)$
34 30 33 eqtrd ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge \left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\right)\to \perp \left(\perp \left({x}\right){\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)={x}\cap \left({A}{\vee }_{ℋ}{B}\right)$
35 25 34 eqeq12d ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge \left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\right)\to \left(\perp \left(\left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)\right)=\perp \left(\perp \left({x}\right){\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)↔\left({x}\cap {A}\right){\vee }_{ℋ}{B}={x}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)$
36 35 ancoms ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left(\perp \left(\left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)\right)=\perp \left(\perp \left({x}\right){\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)↔\left({x}\cap {A}\right){\vee }_{ℋ}{B}={x}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)$
37 15 36 syl5ib ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)=\perp \left({x}\right){\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\to \left({x}\cap {A}\right){\vee }_{ℋ}{B}={x}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)$
38 14 37 imim12d ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left(\perp \left({x}\right)\subseteq \perp \left({B}\right)\to \left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)=\perp \left({x}\right){\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)\to \left({B}\subseteq {x}\to \left({x}\cap {A}\right){\vee }_{ℋ}{B}={x}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)$
39 11 38 syld ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left(\perp \left({x}\right)\in {\mathbf{C}}_{ℋ}\to \left(\perp \left({x}\right)\subseteq \perp \left({B}\right)\to \left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)=\perp \left({x}\right){\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)\right)\to \left({B}\subseteq {x}\to \left({x}\cap {A}\right){\vee }_{ℋ}{B}={x}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)$
40 39 ex ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({x}\in {\mathbf{C}}_{ℋ}\to \left(\left(\perp \left({x}\right)\in {\mathbf{C}}_{ℋ}\to \left(\perp \left({x}\right)\subseteq \perp \left({B}\right)\to \left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)=\perp \left({x}\right){\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)\right)\to \left({B}\subseteq {x}\to \left({x}\cap {A}\right){\vee }_{ℋ}{B}={x}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)\right)$
41 40 com23 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left(\perp \left({x}\right)\in {\mathbf{C}}_{ℋ}\to \left(\perp \left({x}\right)\subseteq \perp \left({B}\right)\to \left(\perp \left({x}\right){\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)=\perp \left({x}\right){\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)\right)\to \left({x}\in {\mathbf{C}}_{ℋ}\to \left({B}\subseteq {x}\to \left({x}\cap {A}\right){\vee }_{ℋ}{B}={x}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)\right)$
42 7 41 syl5 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left(\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq \perp \left({B}\right)\to \left({y}{\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)={y}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)\to \left({x}\in {\mathbf{C}}_{ℋ}\to \left({B}\subseteq {x}\to \left({x}\cap {A}\right){\vee }_{ℋ}{B}={x}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)\right)$
43 42 ralrimdv ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left(\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq \perp \left({B}\right)\to \left({y}{\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)={y}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)\to \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {x}\to \left({x}\cap {A}\right){\vee }_{ℋ}{B}={x}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)$
44 sseq2 ${⊢}{x}=\perp \left({y}\right)\to \left({B}\subseteq {x}↔{B}\subseteq \perp \left({y}\right)\right)$
45 ineq1 ${⊢}{x}=\perp \left({y}\right)\to {x}\cap {A}=\perp \left({y}\right)\cap {A}$
46 45 oveq1d ${⊢}{x}=\perp \left({y}\right)\to \left({x}\cap {A}\right){\vee }_{ℋ}{B}=\left(\perp \left({y}\right)\cap {A}\right){\vee }_{ℋ}{B}$
47 ineq1 ${⊢}{x}=\perp \left({y}\right)\to {x}\cap \left({A}{\vee }_{ℋ}{B}\right)=\perp \left({y}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)$
48 46 47 eqeq12d ${⊢}{x}=\perp \left({y}\right)\to \left(\left({x}\cap {A}\right){\vee }_{ℋ}{B}={x}\cap \left({A}{\vee }_{ℋ}{B}\right)↔\left(\perp \left({y}\right)\cap {A}\right){\vee }_{ℋ}{B}=\perp \left({y}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\right)$
49 44 48 imbi12d ${⊢}{x}=\perp \left({y}\right)\to \left(\left({B}\subseteq {x}\to \left({x}\cap {A}\right){\vee }_{ℋ}{B}={x}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)↔\left({B}\subseteq \perp \left({y}\right)\to \left(\perp \left({y}\right)\cap {A}\right){\vee }_{ℋ}{B}=\perp \left({y}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)$
50 49 rspccv ${⊢}\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {x}\to \left({x}\cap {A}\right){\vee }_{ℋ}{B}={x}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\to \left(\perp \left({y}\right)\in {\mathbf{C}}_{ℋ}\to \left({B}\subseteq \perp \left({y}\right)\to \left(\perp \left({y}\right)\cap {A}\right){\vee }_{ℋ}{B}=\perp \left({y}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)$
51 choccl ${⊢}{y}\in {\mathbf{C}}_{ℋ}\to \perp \left({y}\right)\in {\mathbf{C}}_{ℋ}$
52 51 imim1i ${⊢}\left(\perp \left({y}\right)\in {\mathbf{C}}_{ℋ}\to \left({B}\subseteq \perp \left({y}\right)\to \left(\perp \left({y}\right)\cap {A}\right){\vee }_{ℋ}{B}=\perp \left({y}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)\to \left({y}\in {\mathbf{C}}_{ℋ}\to \left({B}\subseteq \perp \left({y}\right)\to \left(\perp \left({y}\right)\cap {A}\right){\vee }_{ℋ}{B}=\perp \left({y}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)$
53 52 com12 ${⊢}{y}\in {\mathbf{C}}_{ℋ}\to \left(\left(\perp \left({y}\right)\in {\mathbf{C}}_{ℋ}\to \left({B}\subseteq \perp \left({y}\right)\to \left(\perp \left({y}\right)\cap {A}\right){\vee }_{ℋ}{B}=\perp \left({y}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)\to \left({B}\subseteq \perp \left({y}\right)\to \left(\perp \left({y}\right)\cap {A}\right){\vee }_{ℋ}{B}=\perp \left({y}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)$
54 53 adantl ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\wedge {y}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left(\perp \left({y}\right)\in {\mathbf{C}}_{ℋ}\to \left({B}\subseteq \perp \left({y}\right)\to \left(\perp \left({y}\right)\cap {A}\right){\vee }_{ℋ}{B}=\perp \left({y}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)\to \left({B}\subseteq \perp \left({y}\right)\to \left(\perp \left({y}\right)\cap {A}\right){\vee }_{ℋ}{B}=\perp \left({y}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)$
55 chsscon2 ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {y}\in {\mathbf{C}}_{ℋ}\right)\to \left({B}\subseteq \perp \left({y}\right)↔{y}\subseteq \perp \left({B}\right)\right)$
56 55 biimprd ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {y}\in {\mathbf{C}}_{ℋ}\right)\to \left({y}\subseteq \perp \left({B}\right)\to {B}\subseteq \perp \left({y}\right)\right)$
57 56 adantll ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\wedge {y}\in {\mathbf{C}}_{ℋ}\right)\to \left({y}\subseteq \perp \left({B}\right)\to {B}\subseteq \perp \left({y}\right)\right)$
58 fveq2 ${⊢}\left(\perp \left({y}\right)\cap {A}\right){\vee }_{ℋ}{B}=\perp \left({y}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\to \perp \left(\left(\perp \left({y}\right)\cap {A}\right){\vee }_{ℋ}{B}\right)=\perp \left(\perp \left({y}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\right)$
59 chincl ${⊢}\left(\perp \left({y}\right)\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left({y}\right)\cap {A}\in {\mathbf{C}}_{ℋ}$
60 51 59 sylan ${⊢}\left({y}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left({y}\right)\cap {A}\in {\mathbf{C}}_{ℋ}$
61 chdmj1 ${⊢}\left(\perp \left({y}\right)\cap {A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left(\left(\perp \left({y}\right)\cap {A}\right){\vee }_{ℋ}{B}\right)=\perp \left(\perp \left({y}\right)\cap {A}\right)\cap \perp \left({B}\right)$
62 60 61 sylan ${⊢}\left(\left({y}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left(\left(\perp \left({y}\right)\cap {A}\right){\vee }_{ℋ}{B}\right)=\perp \left(\perp \left({y}\right)\cap {A}\right)\cap \perp \left({B}\right)$
63 chdmm2 ${⊢}\left({y}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left(\perp \left({y}\right)\cap {A}\right)={y}{\vee }_{ℋ}\perp \left({A}\right)$
64 63 adantr ${⊢}\left(\left({y}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left(\perp \left({y}\right)\cap {A}\right)={y}{\vee }_{ℋ}\perp \left({A}\right)$
65 64 ineq1d ${⊢}\left(\left({y}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left(\perp \left({y}\right)\cap {A}\right)\cap \perp \left({B}\right)=\left({y}{\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)$
66 62 65 eqtrd ${⊢}\left(\left({y}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left(\left(\perp \left({y}\right)\cap {A}\right){\vee }_{ℋ}{B}\right)=\left({y}{\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)$
67 66 anasss ${⊢}\left({y}\in {\mathbf{C}}_{ℋ}\wedge \left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\right)\to \perp \left(\left(\perp \left({y}\right)\cap {A}\right){\vee }_{ℋ}{B}\right)=\left({y}{\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)$
68 chjcl ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to {A}{\vee }_{ℋ}{B}\in {\mathbf{C}}_{ℋ}$
69 chdmm2 ${⊢}\left({y}\in {\mathbf{C}}_{ℋ}\wedge {A}{\vee }_{ℋ}{B}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left(\perp \left({y}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\right)={y}{\vee }_{ℋ}\perp \left({A}{\vee }_{ℋ}{B}\right)$
70 68 69 sylan2 ${⊢}\left({y}\in {\mathbf{C}}_{ℋ}\wedge \left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\right)\to \perp \left(\perp \left({y}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\right)={y}{\vee }_{ℋ}\perp \left({A}{\vee }_{ℋ}{B}\right)$
71 chdmj1 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left({A}{\vee }_{ℋ}{B}\right)=\perp \left({A}\right)\cap \perp \left({B}\right)$
72 71 adantl ${⊢}\left({y}\in {\mathbf{C}}_{ℋ}\wedge \left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\right)\to \perp \left({A}{\vee }_{ℋ}{B}\right)=\perp \left({A}\right)\cap \perp \left({B}\right)$
73 72 oveq2d ${⊢}\left({y}\in {\mathbf{C}}_{ℋ}\wedge \left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\right)\to {y}{\vee }_{ℋ}\perp \left({A}{\vee }_{ℋ}{B}\right)={y}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)$
74 70 73 eqtrd ${⊢}\left({y}\in {\mathbf{C}}_{ℋ}\wedge \left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\right)\to \perp \left(\perp \left({y}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\right)={y}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)$
75 67 74 eqeq12d ${⊢}\left({y}\in {\mathbf{C}}_{ℋ}\wedge \left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\right)\to \left(\perp \left(\left(\perp \left({y}\right)\cap {A}\right){\vee }_{ℋ}{B}\right)=\perp \left(\perp \left({y}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\right)↔\left({y}{\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)={y}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)$
76 75 ancoms ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\wedge {y}\in {\mathbf{C}}_{ℋ}\right)\to \left(\perp \left(\left(\perp \left({y}\right)\cap {A}\right){\vee }_{ℋ}{B}\right)=\perp \left(\perp \left({y}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\right)↔\left({y}{\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)={y}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)$
77 58 76 syl5ib ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\wedge {y}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left(\perp \left({y}\right)\cap {A}\right){\vee }_{ℋ}{B}=\perp \left({y}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\to \left({y}{\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)={y}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)$
78 57 77 imim12d ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\wedge {y}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({B}\subseteq \perp \left({y}\right)\to \left(\perp \left({y}\right)\cap {A}\right){\vee }_{ℋ}{B}=\perp \left({y}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\to \left({y}\subseteq \perp \left({B}\right)\to \left({y}{\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)={y}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)\right)$
79 54 78 syld ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\wedge {y}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left(\perp \left({y}\right)\in {\mathbf{C}}_{ℋ}\to \left({B}\subseteq \perp \left({y}\right)\to \left(\perp \left({y}\right)\cap {A}\right){\vee }_{ℋ}{B}=\perp \left({y}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)\to \left({y}\subseteq \perp \left({B}\right)\to \left({y}{\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)={y}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)\right)$
80 79 ex ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({y}\in {\mathbf{C}}_{ℋ}\to \left(\left(\perp \left({y}\right)\in {\mathbf{C}}_{ℋ}\to \left({B}\subseteq \perp \left({y}\right)\to \left(\perp \left({y}\right)\cap {A}\right){\vee }_{ℋ}{B}=\perp \left({y}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)\to \left({y}\subseteq \perp \left({B}\right)\to \left({y}{\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)={y}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)\right)\right)$
81 80 com23 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left(\perp \left({y}\right)\in {\mathbf{C}}_{ℋ}\to \left({B}\subseteq \perp \left({y}\right)\to \left(\perp \left({y}\right)\cap {A}\right){\vee }_{ℋ}{B}=\perp \left({y}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)\to \left({y}\in {\mathbf{C}}_{ℋ}\to \left({y}\subseteq \perp \left({B}\right)\to \left({y}{\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)={y}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)\right)\right)$
82 50 81 syl5 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left(\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {x}\to \left({x}\cap {A}\right){\vee }_{ℋ}{B}={x}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\to \left({y}\in {\mathbf{C}}_{ℋ}\to \left({y}\subseteq \perp \left({B}\right)\to \left({y}{\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)={y}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)\right)\right)$
83 82 ralrimdv ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left(\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {x}\to \left({x}\cap {A}\right){\vee }_{ℋ}{B}={x}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\to \forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq \perp \left({B}\right)\to \left({y}{\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)={y}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)\right)$
84 43 83 impbid ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left(\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq \perp \left({B}\right)\to \left({y}{\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)={y}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {x}\to \left({x}\cap {A}\right){\vee }_{ℋ}{B}={x}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)$
85 mdbr ${⊢}\left(\perp \left({A}\right)\in {\mathbf{C}}_{ℋ}\wedge \perp \left({B}\right)\in {\mathbf{C}}_{ℋ}\right)\to \left(\perp \left({A}\right){𝑀}_{ℋ}\perp \left({B}\right)↔\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq \perp \left({B}\right)\to \left({y}{\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)={y}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)\right)$
86 16 26 85 syl2an ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left(\perp \left({A}\right){𝑀}_{ℋ}\perp \left({B}\right)↔\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq \perp \left({B}\right)\to \left({y}{\vee }_{ℋ}\perp \left({A}\right)\right)\cap \perp \left({B}\right)={y}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)\right)$
87 dmdbr ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{𝑀}_{ℋ}^{*}{B}↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {x}\to \left({x}\cap {A}\right){\vee }_{ℋ}{B}={x}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)$
88 84 86 87 3bitr4rd ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{𝑀}_{ℋ}^{*}{B}↔\perp \left({A}\right){𝑀}_{ℋ}\perp \left({B}\right)\right)$