Theorem latmlej21

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	latmlej21	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Y ./\ X ) .<_ ( 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	1 4	latmcom	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) = ( Y ./\ X ) )
6	5	3adant3r3	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ Y ) = ( Y ./\ X ) )
7	1 2 3 4	latmlej11	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ Y ) .<_ ( X .\/ Z ) )
8	6 7	eqbrtrrd	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Y ./\ X ) .<_ ( X .\/ Z ) )