Theorem latmlem1

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

	Ref	Expression
Hypotheses	latmle.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	latmle.l	⊢ ≤ = ( le ‘ 𝐾 )
	latmle.m	⊢ ∧ = ( meet ‘ 𝐾 )
Assertion	latmlem1	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ≤ 𝑌 → ( 𝑋 ∧ 𝑍 ) ≤ ( 𝑌 ∧ 𝑍 ) ) )

Proof

Step	Hyp	Ref	Expression
1		latmle.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		latmle.l	⊢ ≤ = ( le ‘ 𝐾 )
3		latmle.m	⊢ ∧ = ( meet ‘ 𝐾 )
4	1 2 3	latmle1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑍 ) ≤ 𝑋 )
5	4	3adant3r2	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ 𝑍 ) ≤ 𝑋 )
6		simpl	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝐾 ∈ Lat )
7	1 3	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑍 ) ∈ 𝐵 )
8	7	3adant3r2	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ 𝑍 ) ∈ 𝐵 )
9		simpr1	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
10		simpr2	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
11	1 2	lattr	⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑋 ∧ 𝑍 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( 𝑋 ∧ 𝑍 ) ≤ 𝑋 ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 ∧ 𝑍 ) ≤ 𝑌 ) )
12	6 8 9 10 11	syl13anc	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( 𝑋 ∧ 𝑍 ) ≤ 𝑋 ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 ∧ 𝑍 ) ≤ 𝑌 ) )
13	5 12	mpand	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ≤ 𝑌 → ( 𝑋 ∧ 𝑍 ) ≤ 𝑌 ) )
14	1 2 3	latmle2	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑍 ) ≤ 𝑍 )
15	14	3adant3r2	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ 𝑍 ) ≤ 𝑍 )
16	13 15	jctird	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ≤ 𝑌 → ( ( 𝑋 ∧ 𝑍 ) ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑍 ) ≤ 𝑍 ) ) )
17		simpr3	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑍 ∈ 𝐵 )
18	8 10 17	3jca	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑍 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) )
19	1 2 3	latlem12	⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑋 ∧ 𝑍 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( 𝑋 ∧ 𝑍 ) ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑍 ) ≤ 𝑍 ) ↔ ( 𝑋 ∧ 𝑍 ) ≤ ( 𝑌 ∧ 𝑍 ) ) )
20	18 19	syldan	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( 𝑋 ∧ 𝑍 ) ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑍 ) ≤ 𝑍 ) ↔ ( 𝑋 ∧ 𝑍 ) ≤ ( 𝑌 ∧ 𝑍 ) ) )
21	16 20	sylibd	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ≤ 𝑌 → ( 𝑋 ∧ 𝑍 ) ≤ ( 𝑌 ∧ 𝑍 ) ) )