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 C 0 𝐶 A

Proof

Step Hyp Ref Expression
1 h0elch 0 C
2 1 choccli 0 C
3 chjcl 0 C A C 0 A C
4 2 3 mpan A C 0 A C
5 chm0 0 A C 0 A 0 = 0
6 4 5 syl A C 0 A 0 = 0
7 chm0 A C A 0 = 0
8 6 7 eqtr4d A C 0 A 0 = A 0
9 incom 0 0 A = 0 A 0
10 incom 0 A = A 0
11 8 9 10 3eqtr4g A C 0 0 A = 0 A
12 cmbr3 0 C A C 0 𝐶 A 0 0 A = 0 A
13 1 12 mpan A C 0 𝐶 A 0 0 A = 0 A
14 11 13 mpbird A C 0 𝐶 A