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 
|- ( A e. CH -> 0H C_H A )

Proof

Step Hyp Ref Expression
1 h0elch 
 |-  0H e. CH
2 1 choccli 
 |-  ( _|_ ` 0H ) e. CH
3 chjcl 
 |-  ( ( ( _|_ ` 0H ) e. CH /\ A e. CH ) -> ( ( _|_ ` 0H ) vH A ) e. CH )
4 2 3 mpan 
 |-  ( A e. CH -> ( ( _|_ ` 0H ) vH A ) e. CH )
5 chm0 
 |-  ( ( ( _|_ ` 0H ) vH A ) e. CH -> ( ( ( _|_ ` 0H ) vH A ) i^i 0H ) = 0H )
6 4 5 syl 
 |-  ( A e. CH -> ( ( ( _|_ ` 0H ) vH A ) i^i 0H ) = 0H )
7 chm0 
 |-  ( A e. CH -> ( A i^i 0H ) = 0H )
8 6 7 eqtr4d 
 |-  ( A e. CH -> ( ( ( _|_ ` 0H ) vH A ) i^i 0H ) = ( A i^i 0H ) )
9 incom 
 |-  ( 0H i^i ( ( _|_ ` 0H ) vH A ) ) = ( ( ( _|_ ` 0H ) vH A ) i^i 0H )
10 incom 
 |-  ( 0H i^i A ) = ( A i^i 0H )
11 8 9 10 3eqtr4g 
 |-  ( A e. CH -> ( 0H i^i ( ( _|_ ` 0H ) vH A ) ) = ( 0H i^i A ) )
12 cmbr3 
 |-  ( ( 0H e. CH /\ A e. CH ) -> ( 0H C_H A <-> ( 0H i^i ( ( _|_ ` 0H ) vH A ) ) = ( 0H i^i A ) ) )
13 1 12 mpan 
 |-  ( A e. CH -> ( 0H C_H A <-> ( 0H i^i ( ( _|_ ` 0H ) vH A ) ) = ( 0H i^i A ) ) )
14 11 13 mpbird 
 |-  ( A e. CH -> 0H C_H A )