Metamath Proof Explorer


Theorem lecmi

Description: Comparable Hilbert lattice elements commute. Theorem 2.3(iii) of Beran p. 40. (Contributed by NM, 16-Jan-2005) (New usage is discouraged.)

Ref Expression
Hypotheses pjoml2.1
|- A e. CH
pjoml2.2
|- B e. CH
Assertion lecmi
|- ( A C_ B -> A C_H B )

Proof

Step Hyp Ref Expression
1 pjoml2.1
 |-  A e. CH
2 pjoml2.2
 |-  B e. CH
3 ssinss1
 |-  ( A C_ B -> ( A i^i ( ( _|_ ` A ) vH B ) ) C_ B )
4 1 2 cmbr4i
 |-  ( A C_H B <-> ( A i^i ( ( _|_ ` A ) vH B ) ) C_ B )
5 3 4 sylibr
 |-  ( A C_ B -> A C_H B )