Description: The zero Hilbert lattice element commutes with every element. (Contributed by NM, 16-Jun-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | cm0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | h0elch | |
|
2 | 1 | choccli | |
3 | chjcl | |
|
4 | 2 3 | mpan | |
5 | chm0 | |
|
6 | 4 5 | syl | |
7 | chm0 | |
|
8 | 6 7 | eqtr4d | |
9 | incom | |
|
10 | incom | |
|
11 | 8 9 10 | 3eqtr4g | |
12 | cmbr3 | |
|
13 | 1 12 | mpan | |
14 | 11 13 | mpbird | |