Metamath Proof Explorer

Theorem latmlem2

Description: Add meet to both sides of a lattice ordering. ( sslin analog.) (Contributed by NM, 10-Nov-2011)

Ref Expression
Hypotheses latmle.b
`|- B = ( Base ` K )`
latmle.l
`|- .<_ = ( le ` K )`
latmle.m
`|- ./\ = ( meet ` K )`
Assertion latmlem2
`|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ Y -> ( Z ./\ X ) .<_ ( Z ./\ Y ) ) )`

Proof

Step Hyp Ref Expression
1 latmle.b
` |-  B = ( Base ` K )`
2 latmle.l
` |-  .<_ = ( le ` K )`
3 latmle.m
` |-  ./\ = ( meet ` K )`
4 1 2 3 latmlem1
` |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ Y -> ( X ./\ Z ) .<_ ( Y ./\ Z ) ) )`
5 1 3 latmcom
` |-  ( ( K e. Lat /\ X e. B /\ Z e. B ) -> ( X ./\ Z ) = ( Z ./\ X ) )`
` |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ Z ) = ( Z ./\ X ) )`
` |-  ( ( K e. Lat /\ Y e. B /\ Z e. B ) -> ( Y ./\ Z ) = ( Z ./\ Y ) )`
` |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Y ./\ Z ) = ( Z ./\ Y ) )`
` |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ./\ Z ) .<_ ( Y ./\ Z ) <-> ( Z ./\ X ) .<_ ( Z ./\ Y ) ) )`
` |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ Y -> ( Z ./\ X ) .<_ ( Z ./\ Y ) ) )`