Theorem latledi

Description: An ortholattice is distributive in one ordering direction. ( ledi analog.) (Contributed by NM, 7-Nov-2011)

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

Proof

Step	Hyp	Ref	Expression
1		latledi.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		latledi.l	⊢ ≤ = ( le ‘ 𝐾 )
3		latledi.j	⊢ ∨ = ( join ‘ 𝐾 )
4		latledi.m	⊢ ∧ = ( meet ‘ 𝐾 )
5	1 2 4	latmle1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 )
6	5	3adant3r3	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 )
7	1 2 4	latmle1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑍 ) ≤ 𝑋 )
8	7	3adant3r2	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ 𝑍 ) ≤ 𝑋 )
9	1 4	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
10	9	3adant3r3	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
11	1 4	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑍 ) ∈ 𝐵 )
12	11	3adant3r2	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ 𝑍 ) ∈ 𝐵 )
13		simpr1	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
14	10 12 13	3jca	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑍 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) )
15	1 2 3	latjle12	⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑍 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 ∧ ( 𝑋 ∧ 𝑍 ) ≤ 𝑋 ) ↔ ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ≤ 𝑋 ) )
16	14 15	syldan	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 ∧ ( 𝑋 ∧ 𝑍 ) ≤ 𝑋 ) ↔ ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ≤ 𝑋 ) )
17	6 8 16	mpbi2and	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ≤ 𝑋 )
18	1 2 4	latmle2	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑌 )
19	18	3adant3r3	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑌 )
20	1 2 4	latmle2	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑍 ) ≤ 𝑍 )
21	20	3adant3r2	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ 𝑍 ) ≤ 𝑍 )
22		simpl	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝐾 ∈ Lat )
23		simpr2	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
24		simpr3	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑍 ∈ 𝐵 )
25	1 2 3	latjlej12	⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑋 ∧ 𝑍 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑍 ) ≤ 𝑍 ) → ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ≤ ( 𝑌 ∨ 𝑍 ) ) )
26	22 10 23 12 24 25	syl122anc	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑌 ∧ ( 𝑋 ∧ 𝑍 ) ≤ 𝑍 ) → ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ≤ ( 𝑌 ∨ 𝑍 ) ) )
27	19 21 26	mp2and	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ≤ ( 𝑌 ∨ 𝑍 ) )
28	1 3	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑍 ) ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ∈ 𝐵 )
29	22 10 12 28	syl3anc	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ∈ 𝐵 )
30	1 3	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 ∨ 𝑍 ) ∈ 𝐵 )
31	30	3adant3r1	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 ∨ 𝑍 ) ∈ 𝐵 )
32	1 2 4	latlem12	⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑌 ∨ 𝑍 ) ∈ 𝐵 ) ) → ( ( ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ≤ 𝑋 ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ≤ ( 𝑌 ∨ 𝑍 ) ) ↔ ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ≤ ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) ) )
33	22 29 13 31 32	syl13anc	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ≤ 𝑋 ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ≤ ( 𝑌 ∨ 𝑍 ) ) ↔ ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ≤ ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) ) )
34	17 27 33	mpbi2and	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∨ ( 𝑋 ∧ 𝑍 ) ) ≤ ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) )