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 ⊢ 𝐴 ∈ Cℋ
chjcl.2 ⊢ 𝐵 ∈ Cℋ
chjass.3 ⊢ 𝐶 ∈ Cℋ
Assertion chjassi ( ( 𝐴 ∨ℋ 𝐵 ) ∨ℋ 𝐶 ) = ( 𝐴 ∨ℋ ( 𝐵 ∨ℋ 𝐶 ) )

Proof

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