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ℋ 𝐶ℋ 𝐴 )