# Metamath Proof Explorer

## Theorem chjassi

Description: Associative law for Hilbert lattice join. From definition of lattice in Kalmbach p. 14. (Contributed by NM, 10-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses ch0le.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
chjcl.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
chjass.3 ${⊢}{C}\in {\mathbf{C}}_{ℋ}$
Assertion chjassi ${⊢}\left({A}{\vee }_{ℋ}{B}\right){\vee }_{ℋ}{C}={A}{\vee }_{ℋ}\left({B}{\vee }_{ℋ}{C}\right)$

### Proof

Step Hyp Ref Expression
1 ch0le.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
2 chjcl.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
3 chjass.3 ${⊢}{C}\in {\mathbf{C}}_{ℋ}$
4 inass ${⊢}\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\cap \perp \left({C}\right)=\perp \left({A}\right)\cap \left(\perp \left({B}\right)\cap \perp \left({C}\right)\right)$
5 1 2 chdmj1i ${⊢}\perp \left({A}{\vee }_{ℋ}{B}\right)=\perp \left({A}\right)\cap \perp \left({B}\right)$
6 5 ineq1i ${⊢}\perp \left({A}{\vee }_{ℋ}{B}\right)\cap \perp \left({C}\right)=\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right)\cap \perp \left({C}\right)$
7 2 3 chdmj1i ${⊢}\perp \left({B}{\vee }_{ℋ}{C}\right)=\perp \left({B}\right)\cap \perp \left({C}\right)$
8 7 ineq2i ${⊢}\perp \left({A}\right)\cap \perp \left({B}{\vee }_{ℋ}{C}\right)=\perp \left({A}\right)\cap \left(\perp \left({B}\right)\cap \perp \left({C}\right)\right)$
9 4 6 8 3eqtr4i ${⊢}\perp \left({A}{\vee }_{ℋ}{B}\right)\cap \perp \left({C}\right)=\perp \left({A}\right)\cap \perp \left({B}{\vee }_{ℋ}{C}\right)$
10 9 fveq2i ${⊢}\perp \left(\perp \left({A}{\vee }_{ℋ}{B}\right)\cap \perp \left({C}\right)\right)=\perp \left(\perp \left({A}\right)\cap \perp \left({B}{\vee }_{ℋ}{C}\right)\right)$
11 1 2 chjcli ${⊢}{A}{\vee }_{ℋ}{B}\in {\mathbf{C}}_{ℋ}$
12 11 3 chdmm4i ${⊢}\perp \left(\perp \left({A}{\vee }_{ℋ}{B}\right)\cap \perp \left({C}\right)\right)=\left({A}{\vee }_{ℋ}{B}\right){\vee }_{ℋ}{C}$
13 2 3 chjcli ${⊢}{B}{\vee }_{ℋ}{C}\in {\mathbf{C}}_{ℋ}$
14 1 13 chdmm4i ${⊢}\perp \left(\perp \left({A}\right)\cap \perp \left({B}{\vee }_{ℋ}{C}\right)\right)={A}{\vee }_{ℋ}\left({B}{\vee }_{ℋ}{C}\right)$
15 10 12 14 3eqtr3i ${⊢}\left({A}{\vee }_{ℋ}{B}\right){\vee }_{ℋ}{C}={A}{\vee }_{ℋ}\left({B}{\vee }_{ℋ}{C}\right)$