# Metamath Proof Explorer

## Theorem chdmj1i

Description: De Morgan's law for join 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 chdmj1i ${⊢}\perp \left({A}{\vee }_{ℋ}{B}\right)=\perp \left({A}\right)\cap \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 2 chdmm4i ${⊢}\perp \left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)={A}{\vee }_{ℋ}{B}$
4 3 fveq2i ${⊢}\perp \left(\perp \left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)=\perp \left({A}{\vee }_{ℋ}{B}\right)$
5 1 choccli ${⊢}\perp \left({A}\right)\in {\mathbf{C}}_{ℋ}$
6 2 choccli ${⊢}\perp \left({B}\right)\in {\mathbf{C}}_{ℋ}$
7 5 6 chincli ${⊢}\perp \left({A}\right)\cap \perp \left({B}\right)\in {\mathbf{C}}_{ℋ}$
8 7 pjococi ${⊢}\perp \left(\perp \left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\right)=\perp \left({A}\right)\cap \perp \left({B}\right)$
9 4 8 eqtr3i ${⊢}\perp \left({A}{\vee }_{ℋ}{B}\right)=\perp \left({A}\right)\cap \perp \left({B}\right)$