This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ≤ 𝑍 → ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) ≤ ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ) )