# Metamath Proof Explorer

## Theorem chdmj2

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

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

### Proof

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