Step | Hyp | Ref
| Expression |
1 | | simp1 1054 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
2 | | simp2 1055 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) |
3 | | simp3ll 1125 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → 𝑌 ∈ 𝐵) |
4 | | simp3r 1083 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → (𝑋 ∧ 𝑌) ≤ 𝑊) |
5 | | dihmeetlem14.b |
. . . 4
⊢ 𝐵 = (Base‘𝐾) |
6 | | dihmeetlem14.l |
. . . 4
⊢ ≤ =
(le‘𝐾) |
7 | | dihmeetlem14.j |
. . . 4
⊢ ∨ =
(join‘𝐾) |
8 | | dihmeetlem14.m |
. . . 4
⊢ ∧ =
(meet‘𝐾) |
9 | | dihmeetlem14.a |
. . . 4
⊢ 𝐴 = (Atoms‘𝐾) |
10 | | dihmeetlem14.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
11 | 5, 6, 7, 8, 9, 10 | lhpmcvr6N 34332 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → ∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋)) |
12 | 1, 2, 3, 4, 11 | syl112anc 1322 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → ∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋)) |
13 | | simp3l 1082 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊)) |
14 | | simp2l 1080 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → 𝑋 ∈ 𝐵) |
15 | | simp1l 1078 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → 𝐾 ∈ HL) |
16 | | hllat 33668 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
17 | 15, 16 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → 𝐾 ∈ Lat) |
18 | 5, 8 | latmcom 16898 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑌 ∧ 𝑋) = (𝑋 ∧ 𝑌)) |
19 | 17, 3, 14, 18 | syl3anc 1318 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → (𝑌 ∧ 𝑋) = (𝑋 ∧ 𝑌)) |
20 | 19, 4 | eqbrtrd 4605 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → (𝑌 ∧ 𝑋) ≤ 𝑊) |
21 | 5, 6, 7, 8, 9, 10 | lhpmcvr6N 34332 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ (𝑌 ∧ 𝑋) ≤ 𝑊)) → ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌)) |
22 | 1, 13, 14, 20, 21 | syl112anc 1322 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌)) |
23 | | reeanv 3086 |
. . 3
⊢
(∃𝑞 ∈
𝐴 ∃𝑟 ∈ 𝐴 ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌)) ↔ (∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) |
24 | | simp11 1084 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
25 | | simp12 1085 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) |
26 | 3 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → 𝑌 ∈ 𝐵) |
27 | | simp2l 1080 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → 𝑞 ∈ 𝐴) |
28 | | simp3l1 1159 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → ¬ 𝑞 ≤ 𝑊) |
29 | 27, 28 | jca 553 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → (𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊)) |
30 | | simp2r 1081 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → 𝑟 ∈ 𝐴) |
31 | | simp3r1 1162 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → ¬ 𝑟 ≤ 𝑊) |
32 | 30, 31 | jca 553 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊)) |
33 | | simp3l3 1161 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → 𝑞 ≤ 𝑋) |
34 | | simp3r3 1164 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → 𝑟 ≤ 𝑌) |
35 | | simp13r 1170 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → (𝑋 ∧ 𝑌) ≤ 𝑊) |
36 | 33, 34, 35 | 3jca 1235 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → (𝑞 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) |
37 | | dihmeetlem14.u |
. . . . . . 7
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
38 | | dihmeetlem14.s |
. . . . . . 7
⊢ ⊕ =
(LSSum‘𝑈) |
39 | | dihmeetlem14.i |
. . . . . . 7
⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) |
40 | 5, 6, 10, 7, 8, 9,
37, 38, 39 | dihmeetlem19N 35632 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑞 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊))) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) |
41 | 24, 25, 26, 29, 32, 36, 40 | syl33anc 1333 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌))) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) |
42 | 41 | 3exp 1256 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → ((𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) → (((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌)) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))))) |
43 | 42 | rexlimdvv 3019 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → (∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ((¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌)) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)))) |
44 | 23, 43 | syl5bir 232 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → ((∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑌 ∧ 𝑞 ≤ 𝑋) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌)) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)))) |
45 | 12, 22, 44 | mp2and 711 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) |