Theorem latmlej12

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	latmlej12	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ Y ) .<_ ( Z .\/ X ) )

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