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 ⊢ B = Base K
omlmod.l ⊢ ≤ ˙ = ≤ K
omlmod.j ⊢ ∨ ˙ = join ⁡ K
omlmod.m ⊢ ∧ ˙ = meet ⁡ K
omlmod.c ⊢ C = cm ⁡ K
Assertion omlmod1i2N ⊢ K ∈ OML ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ X ≤ ˙ Z ∧ Y C Z → X ∨ ˙ Y ∧ ˙ Z = X ∨ ˙ Y ∧ ˙ Z

Proof

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