# Metamath Proof Explorer

## Theorem chdmm2

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

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

### Proof

Step Hyp Ref Expression
1 choccl ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to \perp \left({A}\right)\in {\mathbf{C}}_{ℋ}$
2 chdmm1 ${⊢}\left(\perp \left({A}\right)\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left(\perp \left({A}\right)\cap {B}\right)=\perp \left(\perp \left({A}\right)\right){\vee }_{ℋ}\perp \left({B}\right)$
3 1 2 sylan ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left(\perp \left({A}\right)\cap {B}\right)=\perp \left(\perp \left({A}\right)\right){\vee }_{ℋ}\perp \left({B}\right)$
4 ococ ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to \perp \left(\perp \left({A}\right)\right)={A}$
5 4 adantr ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left(\perp \left({A}\right)\right)={A}$
6 5 oveq1d ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left(\perp \left({A}\right)\right){\vee }_{ℋ}\perp \left({B}\right)={A}{\vee }_{ℋ}\perp \left({B}\right)$
7 3 6 eqtrd ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \perp \left(\perp \left({A}\right)\cap {B}\right)={A}{\vee }_{ℋ}\perp \left({B}\right)$