Proof of Theorem dihord1
Step | Hyp | Ref
| Expression |
1 | | simp11 1084 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
2 | | simp13 1086 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) |
3 | | simp12 1085 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) |
4 | | simp11l 1165 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → 𝐾 ∈ HL) |
5 | | hllat 33668 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → 𝐾 ∈ Lat) |
7 | | simp2r 1081 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → 𝑌 ∈ 𝐵) |
8 | | simp11r 1166 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → 𝑊 ∈ 𝐻) |
9 | | dihjust.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐾) |
10 | | dihjust.h |
. . . . . . 7
⊢ 𝐻 = (LHyp‘𝐾) |
11 | 9, 10 | lhpbase 34302 |
. . . . . 6
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵) |
12 | 8, 11 | syl 17 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → 𝑊 ∈ 𝐵) |
13 | | dihjust.m |
. . . . . 6
⊢ ∧ =
(meet‘𝐾) |
14 | 9, 13 | latmcl 16875 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑌 ∧ 𝑊) ∈ 𝐵) |
15 | 6, 7, 12, 14 | syl3anc 1318 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝑌 ∧ 𝑊) ∈ 𝐵) |
16 | | dihjust.l |
. . . . . 6
⊢ ≤ =
(le‘𝐾) |
17 | 9, 16, 13 | latmle2 16900 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑌 ∧ 𝑊) ≤ 𝑊) |
18 | 6, 7, 12, 17 | syl3anc 1318 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝑌 ∧ 𝑊) ≤ 𝑊) |
19 | 15, 18 | jca 553 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → ((𝑌 ∧ 𝑊) ∈ 𝐵 ∧ (𝑌 ∧ 𝑊) ≤ 𝑊)) |
20 | | simp12l 1167 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → 𝑄 ∈ 𝐴) |
21 | | dihjust.a |
. . . . . . 7
⊢ 𝐴 = (Atoms‘𝐾) |
22 | 9, 21 | atbase 33594 |
. . . . . 6
⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵) |
23 | 20, 22 | syl 17 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → 𝑄 ∈ 𝐵) |
24 | | simp2l 1080 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → 𝑋 ∈ 𝐵) |
25 | 9, 13 | latmcl 16875 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ∈ 𝐵) |
26 | 6, 24, 12, 25 | syl3anc 1318 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝑋 ∧ 𝑊) ∈ 𝐵) |
27 | | dihjust.j |
. . . . . . 7
⊢ ∨ =
(join‘𝐾) |
28 | 9, 27 | latjcl 16874 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ∈ 𝐵) → (𝑄 ∨ (𝑋 ∧ 𝑊)) ∈ 𝐵) |
29 | 6, 23, 26, 28 | syl3anc 1318 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝑄 ∨ (𝑋 ∧ 𝑊)) ∈ 𝐵) |
30 | 9, 16, 27 | latlej1 16883 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ∈ 𝐵) → 𝑄 ≤ (𝑄 ∨ (𝑋 ∧ 𝑊))) |
31 | 6, 23, 26, 30 | syl3anc 1318 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → 𝑄 ≤ (𝑄 ∨ (𝑋 ∧ 𝑊))) |
32 | | simp31 1090 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) |
33 | | simp33 1092 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → 𝑋 ≤ 𝑌) |
34 | 32, 33 | eqbrtrd 4605 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝑄 ∨ (𝑋 ∧ 𝑊)) ≤ 𝑌) |
35 | 9, 16, 6, 23, 29, 7, 31, 34 | lattrd 16881 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → 𝑄 ≤ 𝑌) |
36 | | simp32 1091 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌) |
37 | 35, 36 | breqtrrd 4611 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → 𝑄 ≤ (𝑅 ∨ (𝑌 ∧ 𝑊))) |
38 | | dihjust.u |
. . . 4
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
39 | | dihjust.s |
. . . 4
⊢ ⊕ =
(LSSum‘𝑈) |
40 | | dihjust.i |
. . . 4
⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) |
41 | | dihjust.J |
. . . 4
⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊) |
42 | 9, 16, 27, 21, 10, 38, 39, 40, 41 | cdlemn5 35508 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ ((𝑌 ∧ 𝑊) ∈ 𝐵 ∧ (𝑌 ∧ 𝑊) ≤ 𝑊)) ∧ 𝑄 ≤ (𝑅 ∨ (𝑌 ∧ 𝑊))) → (𝐽‘𝑄) ⊆ ((𝐽‘𝑅) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) |
43 | 1, 2, 3, 19, 37, 42 | syl131anc 1331 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝐽‘𝑄) ⊆ ((𝐽‘𝑅) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) |
44 | 9, 16, 13 | latmlem1 16904 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → (𝑋 ≤ 𝑌 → (𝑋 ∧ 𝑊) ≤ (𝑌 ∧ 𝑊))) |
45 | 6, 24, 7, 12, 44 | syl13anc 1320 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝑋 ≤ 𝑌 → (𝑋 ∧ 𝑊) ≤ (𝑌 ∧ 𝑊))) |
46 | 33, 45 | mpd 15 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝑋 ∧ 𝑊) ≤ (𝑌 ∧ 𝑊)) |
47 | 9, 16, 13 | latmle2 16900 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ≤ 𝑊) |
48 | 6, 24, 12, 47 | syl3anc 1318 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝑋 ∧ 𝑊) ≤ 𝑊) |
49 | 9, 16, 10, 40 | dibord 35466 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋 ∧ 𝑊) ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ≤ 𝑊) ∧ ((𝑌 ∧ 𝑊) ∈ 𝐵 ∧ (𝑌 ∧ 𝑊) ≤ 𝑊)) → ((𝐼‘(𝑋 ∧ 𝑊)) ⊆ (𝐼‘(𝑌 ∧ 𝑊)) ↔ (𝑋 ∧ 𝑊) ≤ (𝑌 ∧ 𝑊))) |
50 | 1, 26, 48, 15, 18, 49 | syl122anc 1327 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → ((𝐼‘(𝑋 ∧ 𝑊)) ⊆ (𝐼‘(𝑌 ∧ 𝑊)) ↔ (𝑋 ∧ 𝑊) ≤ (𝑌 ∧ 𝑊))) |
51 | 46, 50 | mpbird 246 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝐼‘(𝑋 ∧ 𝑊)) ⊆ (𝐼‘(𝑌 ∧ 𝑊))) |
52 | 10, 38, 1 | dvhlmod 35417 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → 𝑈 ∈ LMod) |
53 | | eqid 2610 |
. . . . . . 7
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
54 | 53 | lsssssubg 18779 |
. . . . . 6
⊢ (𝑈 ∈ LMod →
(LSubSp‘𝑈) ⊆
(SubGrp‘𝑈)) |
55 | 52, 54 | syl 17 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈)) |
56 | 16, 21, 10, 38, 41, 53 | diclss 35500 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → (𝐽‘𝑅) ∈ (LSubSp‘𝑈)) |
57 | 1, 2, 56 | syl2anc 691 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝐽‘𝑅) ∈ (LSubSp‘𝑈)) |
58 | 55, 57 | sseldd 3569 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝐽‘𝑅) ∈ (SubGrp‘𝑈)) |
59 | 9, 16, 10, 38, 40, 53 | diblss 35477 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑌 ∧ 𝑊) ∈ 𝐵 ∧ (𝑌 ∧ 𝑊) ≤ 𝑊)) → (𝐼‘(𝑌 ∧ 𝑊)) ∈ (LSubSp‘𝑈)) |
60 | 1, 15, 18, 59 | syl12anc 1316 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝐼‘(𝑌 ∧ 𝑊)) ∈ (LSubSp‘𝑈)) |
61 | 55, 60 | sseldd 3569 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝐼‘(𝑌 ∧ 𝑊)) ∈ (SubGrp‘𝑈)) |
62 | 39 | lsmub2 17895 |
. . . 4
⊢ (((𝐽‘𝑅) ∈ (SubGrp‘𝑈) ∧ (𝐼‘(𝑌 ∧ 𝑊)) ∈ (SubGrp‘𝑈)) → (𝐼‘(𝑌 ∧ 𝑊)) ⊆ ((𝐽‘𝑅) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) |
63 | 58, 61, 62 | syl2anc 691 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝐼‘(𝑌 ∧ 𝑊)) ⊆ ((𝐽‘𝑅) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) |
64 | 51, 63 | sstrd 3578 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝐼‘(𝑋 ∧ 𝑊)) ⊆ ((𝐽‘𝑅) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) |
65 | 16, 21, 10, 38, 41, 53 | diclss 35500 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐽‘𝑄) ∈ (LSubSp‘𝑈)) |
66 | 1, 3, 65 | syl2anc 691 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝐽‘𝑄) ∈ (LSubSp‘𝑈)) |
67 | 55, 66 | sseldd 3569 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝐽‘𝑄) ∈ (SubGrp‘𝑈)) |
68 | 9, 16, 10, 38, 40, 53 | diblss 35477 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋 ∧ 𝑊) ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ≤ 𝑊)) → (𝐼‘(𝑋 ∧ 𝑊)) ∈ (LSubSp‘𝑈)) |
69 | 1, 26, 48, 68 | syl12anc 1316 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝐼‘(𝑋 ∧ 𝑊)) ∈ (LSubSp‘𝑈)) |
70 | 55, 69 | sseldd 3569 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (𝐼‘(𝑋 ∧ 𝑊)) ∈ (SubGrp‘𝑈)) |
71 | 53, 39 | lsmcl 18904 |
. . . . 5
⊢ ((𝑈 ∈ LMod ∧ (𝐽‘𝑅) ∈ (LSubSp‘𝑈) ∧ (𝐼‘(𝑌 ∧ 𝑊)) ∈ (LSubSp‘𝑈)) → ((𝐽‘𝑅) ⊕ (𝐼‘(𝑌 ∧ 𝑊))) ∈ (LSubSp‘𝑈)) |
72 | 52, 57, 60, 71 | syl3anc 1318 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → ((𝐽‘𝑅) ⊕ (𝐼‘(𝑌 ∧ 𝑊))) ∈ (LSubSp‘𝑈)) |
73 | 55, 72 | sseldd 3569 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → ((𝐽‘𝑅) ⊕ (𝐼‘(𝑌 ∧ 𝑊))) ∈ (SubGrp‘𝑈)) |
74 | 39 | lsmlub 17901 |
. . 3
⊢ (((𝐽‘𝑄) ∈ (SubGrp‘𝑈) ∧ (𝐼‘(𝑋 ∧ 𝑊)) ∈ (SubGrp‘𝑈) ∧ ((𝐽‘𝑅) ⊕ (𝐼‘(𝑌 ∧ 𝑊))) ∈ (SubGrp‘𝑈)) → (((𝐽‘𝑄) ⊆ ((𝐽‘𝑅) ⊕ (𝐼‘(𝑌 ∧ 𝑊))) ∧ (𝐼‘(𝑋 ∧ 𝑊)) ⊆ ((𝐽‘𝑅) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ↔ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑅) ⊕ (𝐼‘(𝑌 ∧ 𝑊))))) |
75 | 67, 70, 73, 74 | syl3anc 1318 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → (((𝐽‘𝑄) ⊆ ((𝐽‘𝑅) ⊕ (𝐼‘(𝑌 ∧ 𝑊))) ∧ (𝐼‘(𝑋 ∧ 𝑊)) ⊆ ((𝐽‘𝑅) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) ↔ ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑅) ⊕ (𝐼‘(𝑌 ∧ 𝑊))))) |
76 | 43, 64, 75 | mpbi2and 958 |
1
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋 ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌 ∧ 𝑋 ≤ 𝑌)) → ((𝐽‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑊))) ⊆ ((𝐽‘𝑅) ⊕ (𝐼‘(𝑌 ∧ 𝑊)))) |