# Metamath Proof Explorer

## Theorem chdmj1

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

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

### Proof

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