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 AC0𝐶A

Proof

Step Hyp Ref Expression
1 h0elch 0C
2 1 choccli 0C
3 chjcl 0CAC0AC
4 2 3 mpan AC0AC
5 chm0 0AC0A0=0
6 4 5 syl AC0A0=0
7 chm0 ACA0=0
8 6 7 eqtr4d AC0A0=A0
9 incom 00A=0A0
10 incom 0A=A0
11 8 9 10 3eqtr4g AC00A=0A
12 cmbr3 0CAC0𝐶A00A=0A
13 1 12 mpan AC0𝐶A00A=0A
14 11 13 mpbird AC0𝐶A