Description: An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | latlej.b | |- B = ( Base ` K ) |
|
latlej.l | |- .<_ = ( le ` K ) |
||
latlej.j | |- .\/ = ( join ` K ) |
||
Assertion | latnlej2l | |- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ -. X .<_ ( Y .\/ Z ) ) -> -. X .<_ Y ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | latlej.b | |- B = ( Base ` K ) |
|
2 | latlej.l | |- .<_ = ( le ` K ) |
|
3 | latlej.j | |- .\/ = ( join ` K ) |
|
4 | 1 2 3 | latnlej2 | |- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ -. X .<_ ( Y .\/ Z ) ) -> ( -. X .<_ Y /\ -. X .<_ Z ) ) |
5 | 4 | simpld | |- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ -. X .<_ ( Y .\/ Z ) ) -> -. X .<_ Y ) |