Metamath Proof Explorer

Theorem omlmod1i2N

Description: Analogue of modular law atmod1i2 that holds in any OML. (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses omlmod.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
omlmod.l ⊢ ≤ = ( le ‘ 𝐾 )
omlmod.j ⊢ ∨ = ( join ‘ 𝐾 )
omlmod.m ⊢ ∧ = ( meet ‘ 𝐾 )
omlmod.c ⊢ 𝐶 = ( cm ‘ 𝐾 )
Assertion omlmod1i2N ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) = ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) )

Proof

Step Hyp Ref Expression
1 omlmod.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 omlmod.l ⊢ ≤ = ( le ‘ 𝐾 )
3 omlmod.j ⊢ ∨ = ( join ‘ 𝐾 )
4 omlmod.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 omlmod.c ⊢ 𝐶 = ( cm ‘ 𝐾 )
6 simp1 ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → 𝐾 ∈ OML )
7 simp23 ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → 𝑍 ∈ 𝐵 )
8 simp21 ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → 𝑋 ∈ 𝐵 )
9 simp22 ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → 𝑌 ∈ 𝐵 )
10 simp3l ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → 𝑋 ≤ 𝑍 )
11 1 2 5 lecmtN ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑍 → 𝑋 𝐶 𝑍 ) )
12 6 8 7 11 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( 𝑋 ≤ 𝑍 → 𝑋 𝐶 𝑍 ) )
13 10 12 mpd ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → 𝑋 𝐶 𝑍 )
14 1 5 cmtcomN ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑍 ↔ 𝑍 𝐶 𝑋 ) )
15 6 8 7 14 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( 𝑋 𝐶 𝑍 ↔ 𝑍 𝐶 𝑋 ) )
16 13 15 mpbid ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → 𝑍 𝐶 𝑋 )
17 simp3r ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → 𝑌 𝐶 𝑍 )
18 1 5 cmtcomN ⊢ ( ( 𝐾 ∈ OML ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 𝐶 𝑍 ↔ 𝑍 𝐶 𝑌 ) )
19 6 9 7 18 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( 𝑌 𝐶 𝑍 ↔ 𝑍 𝐶 𝑌 ) )
20 17 19 mpbid ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → 𝑍 𝐶 𝑌 )
21 1 3 4 5 omlfh1N ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 𝐶 𝑋 ∧ 𝑍 𝐶 𝑌 ) ) → ( 𝑍 ∧ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝑍 ∧ 𝑋 ) ∨ ( 𝑍 ∧ 𝑌 ) ) )
22 6 7 8 9 16 20 21 syl132anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( 𝑍 ∧ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝑍 ∧ 𝑋 ) ∨ ( 𝑍 ∧ 𝑌 ) ) )
23 omllat ⊢ ( 𝐾 ∈ OML → 𝐾 ∈ Lat )
24 23 3ad2ant1 ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → 𝐾 ∈ Lat )
25 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
26 24 8 9 25 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
27 1 4 latmcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑍 ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ) → ( 𝑍 ∧ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) )
28 24 7 26 27 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( 𝑍 ∧ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) )
29 1 2 4 latleeqm2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑍 ↔ ( 𝑍 ∧ 𝑋 ) = 𝑋 ) )
30 24 8 7 29 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( 𝑋 ≤ 𝑍 ↔ ( 𝑍 ∧ 𝑋 ) = 𝑋 ) )
31 10 30 mpbid ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( 𝑍 ∧ 𝑋 ) = 𝑋 )
32 1 4 latmcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑍 ∧ 𝑌 ) = ( 𝑌 ∧ 𝑍 ) )
33 24 7 9 32 syl3anc ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( 𝑍 ∧ 𝑌 ) = ( 𝑌 ∧ 𝑍 ) )
34 31 33 oveq12d ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( ( 𝑍 ∧ 𝑋 ) ∨ ( 𝑍 ∧ 𝑌 ) ) = ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) )
35 22 28 34 3eqtr3rd ⊢ ( ( 𝐾 ∈ OML ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( 𝑋 ∨ ( 𝑌 ∧ 𝑍 ) ) = ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) )