Theorem mod2ile

Description: The weak direction of the modular law (e.g., pmod2iN ) 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	mod2ile	⊢ ( ( 𝐾 ∈ 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		simplr3	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑍 ≤ 𝑋 ) → 𝑍 ∈ 𝐵 )
7		simplr2	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑍 ≤ 𝑋 ) → 𝑌 ∈ 𝐵 )
8		simplr1	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑍 ≤ 𝑋 ) → 𝑋 ∈ 𝐵 )
9	6 7 8	3jca	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑍 ≤ 𝑋 ) → ( 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) )
10	5 9	jca	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑍 ≤ 𝑋 ) → ( 𝐾 ∈ Lat ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) )
11		simpr	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑍 ≤ 𝑋 ) → 𝑍 ≤ 𝑋 )
12	1 2 3 4	mod1ile	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑍 ≤ 𝑋 → ( 𝑍 ∨ ( 𝑌 ∧ 𝑋 ) ) ≤ ( ( 𝑍 ∨ 𝑌 ) ∧ 𝑋 ) ) )
13	10 11 12	sylc	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑍 ≤ 𝑋 ) → ( 𝑍 ∨ ( 𝑌 ∧ 𝑋 ) ) ≤ ( ( 𝑍 ∨ 𝑌 ) ∧ 𝑋 ) )
14	1 4	latmcom	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) = ( 𝑌 ∧ 𝑋 ) )
15	5 8 7 14	syl3anc	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑍 ≤ 𝑋 ) → ( 𝑋 ∧ 𝑌 ) = ( 𝑌 ∧ 𝑋 ) )
16	15	oveq1d	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑍 ≤ 𝑋 ) → ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑍 ) = ( ( 𝑌 ∧ 𝑋 ) ∨ 𝑍 ) )
17	1 4	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 ∧ 𝑋 ) ∈ 𝐵 )
18	5 7 8 17	syl3anc	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑍 ≤ 𝑋 ) → ( 𝑌 ∧ 𝑋 ) ∈ 𝐵 )
19	1 3	latjcom	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑌 ∧ 𝑋 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑌 ∧ 𝑋 ) ∨ 𝑍 ) = ( 𝑍 ∨ ( 𝑌 ∧ 𝑋 ) ) )
20	5 18 6 19	syl3anc	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑍 ≤ 𝑋 ) → ( ( 𝑌 ∧ 𝑋 ) ∨ 𝑍 ) = ( 𝑍 ∨ ( 𝑌 ∧ 𝑋 ) ) )
21	16 20	eqtrd	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑍 ≤ 𝑋 ) → ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑍 ) = ( 𝑍 ∨ ( 𝑌 ∧ 𝑋 ) ) )
22	1 3	latjcom	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 ∨ 𝑍 ) = ( 𝑍 ∨ 𝑌 ) )
23	5 7 6 22	syl3anc	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑍 ≤ 𝑋 ) → ( 𝑌 ∨ 𝑍 ) = ( 𝑍 ∨ 𝑌 ) )
24	23	oveq2d	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑍 ≤ 𝑋 ) → ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) = ( 𝑋 ∧ ( 𝑍 ∨ 𝑌 ) ) )
25	1 3	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑍 ∨ 𝑌 ) ∈ 𝐵 )
26	5 6 7 25	syl3anc	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑍 ≤ 𝑋 ) → ( 𝑍 ∨ 𝑌 ) ∈ 𝐵 )
27	1 4	latmcom	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑍 ∨ 𝑌 ) ∈ 𝐵 ) → ( 𝑋 ∧ ( 𝑍 ∨ 𝑌 ) ) = ( ( 𝑍 ∨ 𝑌 ) ∧ 𝑋 ) )
28	5 8 26 27	syl3anc	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑍 ≤ 𝑋 ) → ( 𝑋 ∧ ( 𝑍 ∨ 𝑌 ) ) = ( ( 𝑍 ∨ 𝑌 ) ∧ 𝑋 ) )
29	24 28	eqtrd	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑍 ≤ 𝑋 ) → ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) = ( ( 𝑍 ∨ 𝑌 ) ∧ 𝑋 ) )
30	13 21 29	3brtr4d	⊢ ( ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑍 ≤ 𝑋 ) → ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑍 ) ≤ ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) )
31	30	ex	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑍 ≤ 𝑋 → ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑍 ) ≤ ( 𝑋 ∧ ( 𝑌 ∨ 𝑍 ) ) ) )