# Metamath Proof Explorer

## Theorem chdmm4

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

Ref Expression
Assertion 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}$

### Proof

Step Hyp Ref Expression
1 choccl ${⊢}{B}\in {\mathbf{C}}_{ℋ}\to \perp \left({B}\right)\in {\mathbf{C}}_{ℋ}$
2 chdmm2 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge \perp \left({B}\right)\in {\mathbf{C}}_{ℋ}\right)\to \perp \left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)={A}{\vee }_{ℋ}\perp \left(\perp \left({B}\right)\right)$
3 1 2 sylan2 ${⊢}\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 }_{ℋ}\perp \left(\perp \left({B}\right)\right)$
4 ococ ${⊢}{B}\in {\mathbf{C}}_{ℋ}\to \perp \left(\perp \left({B}\right)\right)={B}$
5 4 adantl ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left(\perp \left({B}\right)\right)={B}$
6 5 oveq2d ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to {A}{\vee }_{ℋ}\perp \left(\perp \left({B}\right)\right)={A}{\vee }_{ℋ}{B}$
7 3 6 eqtrd ${⊢}\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}$