Proof of Theorem llnmod2i2
Step | Hyp | Ref
| Expression |
1 | | simp11 1091 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑌 ≤ 𝑋) → 𝐾 ∈ HL) |
2 | | hllat 34650 |
. . . 4
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑌 ≤ 𝑋) → 𝐾 ∈ Lat) |
4 | | simp13 1093 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑌 ≤ 𝑋) → 𝑌 ∈ 𝐵) |
5 | | simp2l 1087 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑌 ≤ 𝑋) → 𝑃 ∈ 𝐴) |
6 | | simp2r 1088 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑌 ≤ 𝑋) → 𝑄 ∈ 𝐴) |
7 | | atmod.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐾) |
8 | | atmod.j |
. . . . . 6
⊢ ∨ =
(join‘𝐾) |
9 | | atmod.a |
. . . . . 6
⊢ 𝐴 = (Atoms‘𝐾) |
10 | 7, 8, 9 | hlatjcl 34653 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ 𝐵) |
11 | 1, 5, 6, 10 | syl3anc 1326 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑌 ≤ 𝑋) → (𝑃 ∨ 𝑄) ∈ 𝐵) |
12 | | simp12 1092 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑌 ≤ 𝑋) → 𝑋 ∈ 𝐵) |
13 | | atmod.m |
. . . . 5
⊢ ∧ =
(meet‘𝐾) |
14 | 7, 13 | latmcl 17052 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((𝑃 ∨ 𝑄) ∧ 𝑋) ∈ 𝐵) |
15 | 3, 11, 12, 14 | syl3anc 1326 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑌 ≤ 𝑋) → ((𝑃 ∨ 𝑄) ∧ 𝑋) ∈ 𝐵) |
16 | 7, 8 | latjcom 17059 |
. . 3
⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ ((𝑃 ∨ 𝑄) ∧ 𝑋) ∈ 𝐵) → (𝑌 ∨ ((𝑃 ∨ 𝑄) ∧ 𝑋)) = (((𝑃 ∨ 𝑄) ∧ 𝑋) ∨ 𝑌)) |
17 | 3, 4, 15, 16 | syl3anc 1326 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑌 ≤ 𝑋) → (𝑌 ∨ ((𝑃 ∨ 𝑄) ∧ 𝑋)) = (((𝑃 ∨ 𝑄) ∧ 𝑋) ∨ 𝑌)) |
18 | 7, 8 | latjcl 17051 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵) → (𝑌 ∨ (𝑃 ∨ 𝑄)) ∈ 𝐵) |
19 | 3, 4, 11, 18 | syl3anc 1326 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑌 ≤ 𝑋) → (𝑌 ∨ (𝑃 ∨ 𝑄)) ∈ 𝐵) |
20 | 7, 13 | latmcom 17075 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ (𝑌 ∨ (𝑃 ∨ 𝑄)) ∈ 𝐵) → (𝑋 ∧ (𝑌 ∨ (𝑃 ∨ 𝑄))) = ((𝑌 ∨ (𝑃 ∨ 𝑄)) ∧ 𝑋)) |
21 | 3, 12, 19, 20 | syl3anc 1326 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑌 ≤ 𝑋) → (𝑋 ∧ (𝑌 ∨ (𝑃 ∨ 𝑄))) = ((𝑌 ∨ (𝑃 ∨ 𝑄)) ∧ 𝑋)) |
22 | 7, 8 | latjcom 17059 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑃 ∨ 𝑄) ∨ 𝑌) = (𝑌 ∨ (𝑃 ∨ 𝑄))) |
23 | 3, 11, 4, 22 | syl3anc 1326 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑌 ≤ 𝑋) → ((𝑃 ∨ 𝑄) ∨ 𝑌) = (𝑌 ∨ (𝑃 ∨ 𝑄))) |
24 | 23 | oveq2d 6666 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑌 ≤ 𝑋) → (𝑋 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑌)) = (𝑋 ∧ (𝑌 ∨ (𝑃 ∨ 𝑄)))) |
25 | | simp3 1063 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑌 ≤ 𝑋) → 𝑌 ≤ 𝑋) |
26 | | atmod.l |
. . . . 5
⊢ ≤ =
(le‘𝐾) |
27 | 7, 26, 8, 13, 9 | llnmod1i2 35146 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑌 ≤ 𝑋) → (𝑌 ∨ ((𝑃 ∨ 𝑄) ∧ 𝑋)) = ((𝑌 ∨ (𝑃 ∨ 𝑄)) ∧ 𝑋)) |
28 | 1, 4, 12, 5, 6, 25, 27 | syl321anc 1348 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑌 ≤ 𝑋) → (𝑌 ∨ ((𝑃 ∨ 𝑄) ∧ 𝑋)) = ((𝑌 ∨ (𝑃 ∨ 𝑄)) ∧ 𝑋)) |
29 | 21, 24, 28 | 3eqtr4d 2666 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑌 ≤ 𝑋) → (𝑋 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑌)) = (𝑌 ∨ ((𝑃 ∨ 𝑄) ∧ 𝑋))) |
30 | 7, 13 | latmcom 17075 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵) → (𝑋 ∧ (𝑃 ∨ 𝑄)) = ((𝑃 ∨ 𝑄) ∧ 𝑋)) |
31 | 3, 12, 11, 30 | syl3anc 1326 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑌 ≤ 𝑋) → (𝑋 ∧ (𝑃 ∨ 𝑄)) = ((𝑃 ∨ 𝑄) ∧ 𝑋)) |
32 | 31 | oveq1d 6665 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑌 ≤ 𝑋) → ((𝑋 ∧ (𝑃 ∨ 𝑄)) ∨ 𝑌) = (((𝑃 ∨ 𝑄) ∧ 𝑋) ∨ 𝑌)) |
33 | 17, 29, 32 | 3eqtr4rd 2667 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑌 ≤ 𝑋) → ((𝑋 ∧ (𝑃 ∨ 𝑄)) ∨ 𝑌) = (𝑋 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑌))) |