Metamath Proof Explorer

Theorem latmlej11

Description: Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012)

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

Proof

Step Hyp Ref Expression
1 latledi.b 
 |-  B = ( Base ` K )
2 latledi.l 
 |-  .<_ = ( le ` K )
3 latledi.j 
 |-  .\/ = ( join ` K )
4 latledi.m 
 |-  ./\ = ( meet ` K )
5 simpl 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> K e. Lat )
6 1 4 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )
7 6 3adant3r3 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ Y ) e. B )
8 simpr1 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X e. B )
9 1 3 latjcl 
 |-  ( ( K e. Lat /\ X e. B /\ Z e. B ) -> ( X .\/ Z ) e. B )
10 9 3adant3r2 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .\/ Z ) e. B )
11 1 2 4 latmle1 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) .<_ X )
12 11 3adant3r3 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ Y ) .<_ X )
13 1 2 3 latlej1 
 |-  ( ( K e. Lat /\ X e. B /\ Z e. B ) -> X .<_ ( X .\/ Z ) )
14 13 3adant3r2 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X .<_ ( X .\/ Z ) )
15 1 2 5 7 8 10 12 14 lattrd 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ Y ) .<_ ( X .\/ Z ) )