# Metamath Proof Explorer

## Theorem chdmm1i

Description: De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses ch0le.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
chjcl.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
Assertion chdmm1i ${⊢}\perp \left({A}\cap {B}\right)=\perp \left({A}\right){\vee }_{ℋ}\perp \left({B}\right)$

### Proof

Step Hyp Ref Expression
1 ch0le.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
2 chjcl.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
3 1 choccli ${⊢}\perp \left({A}\right)\in {\mathbf{C}}_{ℋ}$
4 2 choccli ${⊢}\perp \left({B}\right)\in {\mathbf{C}}_{ℋ}$
5 3 4 chub1i ${⊢}\perp \left({A}\right)\subseteq \perp \left({A}\right){\vee }_{ℋ}\perp \left({B}\right)$
6 3 4 chjcli ${⊢}\perp \left({A}\right){\vee }_{ℋ}\perp \left({B}\right)\in {\mathbf{C}}_{ℋ}$
7 1 6 chsscon1i ${⊢}\perp \left({A}\right)\subseteq \perp \left({A}\right){\vee }_{ℋ}\perp \left({B}\right)↔\perp \left(\perp \left({A}\right){\vee }_{ℋ}\perp \left({B}\right)\right)\subseteq {A}$
8 5 7 mpbi ${⊢}\perp \left(\perp \left({A}\right){\vee }_{ℋ}\perp \left({B}\right)\right)\subseteq {A}$
9 4 3 chub2i ${⊢}\perp \left({B}\right)\subseteq \perp \left({A}\right){\vee }_{ℋ}\perp \left({B}\right)$
10 2 6 chsscon1i ${⊢}\perp \left({B}\right)\subseteq \perp \left({A}\right){\vee }_{ℋ}\perp \left({B}\right)↔\perp \left(\perp \left({A}\right){\vee }_{ℋ}\perp \left({B}\right)\right)\subseteq {B}$
11 9 10 mpbi ${⊢}\perp \left(\perp \left({A}\right){\vee }_{ℋ}\perp \left({B}\right)\right)\subseteq {B}$
12 8 11 ssini ${⊢}\perp \left(\perp \left({A}\right){\vee }_{ℋ}\perp \left({B}\right)\right)\subseteq {A}\cap {B}$
13 1 2 chincli ${⊢}{A}\cap {B}\in {\mathbf{C}}_{ℋ}$
14 6 13 chsscon1i ${⊢}\perp \left(\perp \left({A}\right){\vee }_{ℋ}\perp \left({B}\right)\right)\subseteq {A}\cap {B}↔\perp \left({A}\cap {B}\right)\subseteq \perp \left({A}\right){\vee }_{ℋ}\perp \left({B}\right)$
15 12 14 mpbi ${⊢}\perp \left({A}\cap {B}\right)\subseteq \perp \left({A}\right){\vee }_{ℋ}\perp \left({B}\right)$
16 inss1 ${⊢}{A}\cap {B}\subseteq {A}$
17 13 1 chsscon3i ${⊢}{A}\cap {B}\subseteq {A}↔\perp \left({A}\right)\subseteq \perp \left({A}\cap {B}\right)$
18 16 17 mpbi ${⊢}\perp \left({A}\right)\subseteq \perp \left({A}\cap {B}\right)$
19 inss2 ${⊢}{A}\cap {B}\subseteq {B}$
20 13 2 chsscon3i ${⊢}{A}\cap {B}\subseteq {B}↔\perp \left({B}\right)\subseteq \perp \left({A}\cap {B}\right)$
21 19 20 mpbi ${⊢}\perp \left({B}\right)\subseteq \perp \left({A}\cap {B}\right)$
22 13 choccli ${⊢}\perp \left({A}\cap {B}\right)\in {\mathbf{C}}_{ℋ}$
23 3 4 22 chlubii ${⊢}\left(\perp \left({A}\right)\subseteq \perp \left({A}\cap {B}\right)\wedge \perp \left({B}\right)\subseteq \perp \left({A}\cap {B}\right)\right)\to \perp \left({A}\right){\vee }_{ℋ}\perp \left({B}\right)\subseteq \perp \left({A}\cap {B}\right)$
24 18 21 23 mp2an ${⊢}\perp \left({A}\right){\vee }_{ℋ}\perp \left({B}\right)\subseteq \perp \left({A}\cap {B}\right)$
25 15 24 eqssi ${⊢}\perp \left({A}\cap {B}\right)=\perp \left({A}\right){\vee }_{ℋ}\perp \left({B}\right)$