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

Metamath Proof Explorer

Theorem cm0

Description: The zero Hilbert lattice element commutes with every element. (Contributed by NM, 16-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion cm0 ( 𝐴 ∈ Cℋ → 0ℋ 𝐶ℋ 𝐴 )

Proof

Step Hyp Ref Expression
1 h0elch ⊢ 0ℋ ∈ Cℋ
2 1 choccli ⊢ ( ⊥ ‘ 0ℋ ) ∈ Cℋ
3 chjcl ⊢ ( ( ( ⊥ ‘ 0ℋ ) ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( ( ⊥ ‘ 0ℋ ) ∨ℋ 𝐴 ) ∈ Cℋ )
4 2 3 mpan ⊢ ( 𝐴 ∈ Cℋ → ( ( ⊥ ‘ 0ℋ ) ∨ℋ 𝐴 ) ∈ Cℋ )
5 chm0 ⊢ ( ( ( ⊥ ‘ 0ℋ ) ∨ℋ 𝐴 ) ∈ Cℋ → ( ( ( ⊥ ‘ 0ℋ ) ∨ℋ 𝐴 ) ∩ 0ℋ ) = 0ℋ )
6 4 5 syl ⊢ ( 𝐴 ∈ Cℋ → ( ( ( ⊥ ‘ 0ℋ ) ∨ℋ 𝐴 ) ∩ 0ℋ ) = 0ℋ )
7 chm0 ⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 ∩ 0ℋ ) = 0ℋ )
8 6 7 eqtr4d ⊢ ( 𝐴 ∈ Cℋ → ( ( ( ⊥ ‘ 0ℋ ) ∨ℋ 𝐴 ) ∩ 0ℋ ) = ( 𝐴 ∩ 0ℋ ) )
9 incom ⊢ ( 0ℋ ∩ ( ( ⊥ ‘ 0ℋ ) ∨ℋ 𝐴 ) ) = ( ( ( ⊥ ‘ 0ℋ ) ∨ℋ 𝐴 ) ∩ 0ℋ )
10 incom ⊢ ( 0ℋ ∩ 𝐴 ) = ( 𝐴 ∩ 0ℋ )
11 8 9 10 3eqtr4g ⊢ ( 𝐴 ∈ Cℋ → ( 0ℋ ∩ ( ( ⊥ ‘ 0ℋ ) ∨ℋ 𝐴 ) ) = ( 0ℋ ∩ 𝐴 ) )
12 cmbr3 ⊢ ( ( 0ℋ ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 0ℋ 𝐶ℋ 𝐴 ↔ ( 0ℋ ∩ ( ( ⊥ ‘ 0ℋ ) ∨ℋ 𝐴 ) ) = ( 0ℋ ∩ 𝐴 ) ) )
13 1 12 mpan ⊢ ( 𝐴 ∈ Cℋ → ( 0ℋ 𝐶ℋ 𝐴 ↔ ( 0ℋ ∩ ( ( ⊥ ‘ 0ℋ ) ∨ℋ 𝐴 ) ) = ( 0ℋ ∩ 𝐴 ) ) )
14 11 13 mpbird ⊢ ( 𝐴 ∈ Cℋ → 0ℋ 𝐶ℋ 𝐴 )