# Metamath Proof Explorer

## Theorem chdmj4

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

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

### Proof

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