# Metamath Proof Explorer

## Theorem chdmm1

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

Ref Expression
Assertion chdmm1 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left({A}\cap {B}\right)=\perp \left({A}\right){\vee }_{ℋ}\perp \left({B}\right)$

### Proof

Step Hyp Ref Expression
1 ineq1 ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\to {A}\cap {B}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\cap {B}$
2 1 fveq2d ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\to \perp \left({A}\cap {B}\right)=\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\cap {B}\right)$
3 fveq2 ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\to \perp \left({A}\right)=\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\right)$
4 3 oveq1d ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\to \perp \left({A}\right){\vee }_{ℋ}\perp \left({B}\right)=\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\right){\vee }_{ℋ}\perp \left({B}\right)$
5 2 4 eqeq12d ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\to \left(\perp \left({A}\cap {B}\right)=\perp \left({A}\right){\vee }_{ℋ}\perp \left({B}\right)↔\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\cap {B}\right)=\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\right){\vee }_{ℋ}\perp \left({B}\right)\right)$
6 ineq2 ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\to if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\cap {B}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\cap if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)$
7 6 fveq2d ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\to \perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\cap {B}\right)=\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\cap if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\right)$
8 fveq2 ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\to \perp \left({B}\right)=\perp \left(if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\right)$
9 8 oveq2d ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\to \perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\right){\vee }_{ℋ}\perp \left({B}\right)=\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\right){\vee }_{ℋ}\perp \left(if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\right)$
10 7 9 eqeq12d ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\to \left(\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\cap {B}\right)=\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\right){\vee }_{ℋ}\perp \left({B}\right)↔\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\cap if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\right)=\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\right){\vee }_{ℋ}\perp \left(if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\right)\right)$
11 ifchhv ${⊢}if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\in {\mathbf{C}}_{ℋ}$
12 ifchhv ${⊢}if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\in {\mathbf{C}}_{ℋ}$
13 11 12 chdmm1i ${⊢}\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\cap if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\right)=\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\right){\vee }_{ℋ}\perp \left(if\left({B}\in {\mathbf{C}}_{ℋ},{B},ℋ\right)\right)$
14 5 10 13 dedth2h ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left({A}\cap {B}\right)=\perp \left({A}\right){\vee }_{ℋ}\perp \left({B}\right)$