Description: A lattice element that commutes with two others also commutes with their meet. Theorem 4.2 of Beran p. 49. (Contributed by NM, 11-May-2009) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | fh1.1 | |- A e. CH |
|
| fh1.2 | |- B e. CH |
||
| fh1.3 | |- C e. CH |
||
| fh1.4 | |- A C_H B |
||
| fh1.5 | |- A C_H C |
||
| Assertion | cm2mi | |- A C_H ( B i^i C ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fh1.1 | |- A e. CH |
|
| 2 | fh1.2 | |- B e. CH |
|
| 3 | fh1.3 | |- C e. CH |
|
| 4 | fh1.4 | |- A C_H B |
|
| 5 | fh1.5 | |- A C_H C |
|
| 6 | 2 | choccli | |- ( _|_ ` B ) e. CH |
| 7 | 3 | choccli | |- ( _|_ ` C ) e. CH |
| 8 | 1 2 4 | cmcm2ii | |- A C_H ( _|_ ` B ) |
| 9 | 1 3 5 | cmcm2ii | |- A C_H ( _|_ ` C ) |
| 10 | 1 6 7 8 9 | cm2ji | |- A C_H ( ( _|_ ` B ) vH ( _|_ ` C ) ) |
| 11 | 2 3 | chdmm1i | |- ( _|_ ` ( B i^i C ) ) = ( ( _|_ ` B ) vH ( _|_ ` C ) ) |
| 12 | 10 11 | breqtrri | |- A C_H ( _|_ ` ( B i^i C ) ) |
| 13 | 2 3 | chincli | |- ( B i^i C ) e. CH |
| 14 | 1 13 | cmcm2i | |- ( A C_H ( B i^i C ) <-> A C_H ( _|_ ` ( B i^i C ) ) ) |
| 15 | 12 14 | mpbir | |- A C_H ( B i^i C ) |