Theorem mod1ile

Description: The weak direction of the modular law (e.g., pmod1i , atmod1i1 ) that holds in any lattice. (Contributed by NM, 11-May-2012)

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

Proof

Step	Hyp	Ref	Expression
1		modle.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		modle.l	⊢ ≤ = ( le ‘ 𝐾 )
3		modle.j	⊢ ∨ = ( join ‘ 𝐾 )
4		modle.m	⊢ ∧ = ( meet ‘ 𝐾 )
5		simpll	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≤ 𝑍 ) → 𝐾 ∈ Lat )
6		simplr1	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≤ 𝑍 ) → 𝑋 ∈ 𝐵 )
7		simplr2	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≤ 𝑍 ) → 𝑌 ∈ 𝐵 )
8	1 2 3	latlej1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ≤ ( 𝑋 ∨ 𝑌 ) )
9	5 6 7 8	syl3anc	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≤ 𝑍 ) → 𝑋 ≤ ( 𝑋 ∨ 𝑌 ) )
10		simpr	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≤ 𝑍 ) → 𝑋 ≤ 𝑍 )
11	1 3	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
12	5 6 7 11	syl3anc	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≤ 𝑍 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
13		simplr3	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≤ 𝑍 ) → 𝑍 ∈ 𝐵 )
14	1 2 4	latlem12	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ ( 𝑋 ∨ 𝑌 ) ∧ 𝑋 ≤ 𝑍 ) ↔ 𝑋 ≤ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ) )
15	5 6 12 13 14	syl13anc	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≤ 𝑍 ) → ( ( 𝑋 ≤ ( 𝑋 ∨ 𝑌 ) ∧ 𝑋 ≤ 𝑍 ) ↔ 𝑋 ≤ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ) )
16	9 10 15	mpbi2and	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≤ 𝑍 ) → 𝑋 ≤ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) )
17	1 2 3 4	latmlej12	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑌 ∧ 𝑍 ) ≤ ( 𝑋 ∨ 𝑌 ) )
18	5 7 13 6 17	syl13anc	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≤ 𝑍 ) → ( 𝑌 ∧ 𝑍 ) ≤ ( 𝑋 ∨ 𝑌 ) )
19	1 2 4	latmle2	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 ∧ 𝑍 ) ≤ 𝑍 )
20	5 7 13 19	syl3anc	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≤ 𝑍 ) → ( 𝑌 ∧ 𝑍 ) ≤ 𝑍 )
21	1 4	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 ∧ 𝑍 ) ∈ 𝐵 )
22	5 7 13 21	syl3anc	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≤ 𝑍 ) → ( 𝑌 ∧ 𝑍 ) ∈ 𝐵 )
23	1 2 4	latlem12	⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑌 ∧ 𝑍 ) ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( 𝑌 ∧ 𝑍 ) ≤ ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑌 ∧ 𝑍 ) ≤ 𝑍 ) ↔ ( 𝑌 ∧ 𝑍 ) ≤ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ) )
24	5 22 12 13 23	syl13anc	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≤ 𝑍 ) → ( ( ( 𝑌 ∧ 𝑍 ) ≤ ( 𝑋 ∨ 𝑌 ) ∧ ( 𝑌 ∧ 𝑍 ) ≤ 𝑍 ) ↔ ( 𝑌 ∧ 𝑍 ) ≤ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ) )
25	18 20 24	mpbi2and	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≤ 𝑍 ) → ( 𝑌 ∧ 𝑍 ) ≤ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) )
26	1 4	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∈ 𝐵 )
27	5 12 13 26	syl3anc	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≤ 𝑍 ) → ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∈ 𝐵 )
28	1 2 3	latjle12	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑌 ∧ 𝑍 ) ∈ 𝐵 ∧ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∈ 𝐵 ) ) → ( ( 𝑋 ≤ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∧ ( 𝑌 ∧ 𝑍 ) ≤ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ) ↔ ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) ≤ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ) )
29	5 6 22 27 28	syl13anc	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≤ 𝑍 ) → ( ( 𝑋 ≤ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∧ ( 𝑌 ∧ 𝑍 ) ≤ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ) ↔ ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) ≤ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ) )
30	16 25 29	mpbi2and	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≤ 𝑍 ) → ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) ≤ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) )
31	30	ex	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ≤ 𝑍 → ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) ≤ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ) )