This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ C ℋ
chjcl.2 ⊢ B ∈ C ℋ
chjass.3 ⊢ C ∈ C ℋ
Assertion chjassi ⊢ A ∨ ℋ B ∨ ℋ C = A ∨ ℋ B ∨ ℋ C

Proof

Step Hyp Ref Expression
1 ch0le.1 ⊢ A ∈ C ℋ
2 chjcl.2 ⊢ B ∈ C ℋ
3 chjass.3 ⊢ C ∈ C ℋ
4 inass ⊢ ⊥ ⁡ A ∩ ⊥ ⁡ B ∩ ⊥ ⁡ C = ⊥ ⁡ A ∩ ⊥ ⁡ B ∩ ⊥ ⁡ C
5 1 2 chdmj1i ⊢ ⊥ ⁡ A ∨ ℋ B = ⊥ ⁡ A ∩ ⊥ ⁡ B
6 5 ineq1i ⊢ ⊥ ⁡ A ∨ ℋ B ∩ ⊥ ⁡ C = ⊥ ⁡ A ∩ ⊥ ⁡ B ∩ ⊥ ⁡ C
7 2 3 chdmj1i ⊢ ⊥ ⁡ B ∨ ℋ C = ⊥ ⁡ B ∩ ⊥ ⁡ C
8 7 ineq2i ⊢ ⊥ ⁡ A ∩ ⊥ ⁡ B ∨ ℋ C = ⊥ ⁡ A ∩ ⊥ ⁡ B ∩ ⊥ ⁡ C
9 4 6 8 3eqtr4i ⊢ ⊥ ⁡ A ∨ ℋ B ∩ ⊥ ⁡ C = ⊥ ⁡ A ∩ ⊥ ⁡ B ∨ ℋ C
10 9 fveq2i ⊢ ⊥ ⁡ ⊥ ⁡ A ∨ ℋ B ∩ ⊥ ⁡ C = ⊥ ⁡ ⊥ ⁡ A ∩ ⊥ ⁡ B ∨ ℋ C
11 1 2 chjcli ⊢ A ∨ ℋ B ∈ C ℋ
12 11 3 chdmm4i ⊢ ⊥ ⁡ ⊥ ⁡ A ∨ ℋ B ∩ ⊥ ⁡ C = A ∨ ℋ B ∨ ℋ C
13 2 3 chjcli ⊢ B ∨ ℋ C ∈ C ℋ
14 1 13 chdmm4i ⊢ ⊥ ⁡ ⊥ ⁡ A ∩ ⊥ ⁡ B ∨ ℋ C = A ∨ ℋ B ∨ ℋ C
15 10 12 14 3eqtr3i ⊢ A ∨ ℋ B ∨ ℋ C = A ∨ ℋ B ∨ ℋ C