Theorem latmlej11

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

	Ref	Expression
Hypotheses	latledi.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	latledi.l	⊢ ≤ = ( le ‘ 𝐾 )
	latledi.j	⊢ ∨ = ( join ‘ 𝐾 )
	latledi.m	⊢ ∧ = ( meet ‘ 𝐾 )
Assertion	latmlej11	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑋 ∨ 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		latledi.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		latledi.l	⊢ ≤ = ( le ‘ 𝐾 )
3		latledi.j	⊢ ∨ = ( join ‘ 𝐾 )
4		latledi.m	⊢ ∧ = ( meet ‘ 𝐾 )
5		simpl	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝐾 ∈ Lat )
6	1 4	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
7	6	3adant3r3	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
8		simpr1	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
9	1 3	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑍 ) ∈ 𝐵 )
10	9	3adant3r2	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∨ 𝑍 ) ∈ 𝐵 )
11	1 2 4	latmle1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 )
12	11	3adant3r3	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 )
13	1 2 3	latlej1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → 𝑋 ≤ ( 𝑋 ∨ 𝑍 ) )
14	13	3adant3r2	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑋 ≤ ( 𝑋 ∨ 𝑍 ) )
15	1 2 5 7 8 10 12 14	lattrd	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑋 ∨ 𝑍 ) )