Proof of Theorem dihmeetALTN
Step | Hyp | Ref
| Expression |
1 | | simpl1l 1132 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋(le‘𝐾)𝑊) → 𝐾 ∈ HL) |
2 | | hllat 34968 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋(le‘𝐾)𝑊) → 𝐾 ∈ Lat) |
4 | | simpl2 1085 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋(le‘𝐾)𝑊) → 𝑋 ∈ 𝐵) |
5 | | simpl3 1086 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋(le‘𝐾)𝑊) → 𝑌 ∈ 𝐵) |
6 | | dihmeetALT.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐾) |
7 | | dihmeetALT.m |
. . . . . 6
⊢ ∧ =
(meet‘𝐾) |
8 | 6, 7 | latmcom 17122 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) = (𝑌 ∧ 𝑋)) |
9 | 3, 4, 5, 8 | syl3anc 1366 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋(le‘𝐾)𝑊) → (𝑋 ∧ 𝑌) = (𝑌 ∧ 𝑋)) |
10 | 9 | fveq2d 6233 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋(le‘𝐾)𝑊) → (𝐼‘(𝑋 ∧ 𝑌)) = (𝐼‘(𝑌 ∧ 𝑋))) |
11 | | simpl1 1084 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋(le‘𝐾)𝑊) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
12 | | simpr 476 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋(le‘𝐾)𝑊) → 𝑋(le‘𝐾)𝑊) |
13 | | eqid 2651 |
. . . . . 6
⊢
(le‘𝐾) =
(le‘𝐾) |
14 | | dihmeetALT.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
15 | | dihmeetALT.i |
. . . . . 6
⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) |
16 | 6, 13, 7, 14, 15 | dihmeetbN 36909 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 ∈ 𝐵 ∧ 𝑋(le‘𝐾)𝑊)) → (𝐼‘(𝑌 ∧ 𝑋)) = ((𝐼‘𝑌) ∩ (𝐼‘𝑋))) |
17 | 11, 5, 4, 12, 16 | syl112anc 1370 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋(le‘𝐾)𝑊) → (𝐼‘(𝑌 ∧ 𝑋)) = ((𝐼‘𝑌) ∩ (𝐼‘𝑋))) |
18 | | incom 3838 |
. . . 4
⊢ ((𝐼‘𝑌) ∩ (𝐼‘𝑋)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)) |
19 | 17, 18 | syl6eq 2701 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋(le‘𝐾)𝑊) → (𝐼‘(𝑌 ∧ 𝑋)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) |
20 | 10, 19 | eqtrd 2685 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋(le‘𝐾)𝑊) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) |
21 | | simpll1 1120 |
. . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ 𝑌(le‘𝐾)𝑊) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
22 | | simpll2 1121 |
. . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ 𝑌(le‘𝐾)𝑊) → 𝑋 ∈ 𝐵) |
23 | | simpll3 1122 |
. . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ 𝑌(le‘𝐾)𝑊) → 𝑌 ∈ 𝐵) |
24 | | simpr 476 |
. . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ 𝑌(le‘𝐾)𝑊) → 𝑌(le‘𝐾)𝑊) |
25 | 6, 13, 7, 14, 15 | dihmeetbN 36909 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ (𝑌 ∈ 𝐵 ∧ 𝑌(le‘𝐾)𝑊)) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) |
26 | 21, 22, 23, 24, 25 | syl112anc 1370 |
. . . . 5
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ 𝑌(le‘𝐾)𝑊) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) |
27 | 26 | adantlr 751 |
. . . 4
⊢
((((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊) ∧ 𝑌(le‘𝐾)𝑊) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) |
28 | | simp1l1 1174 |
. . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊 ∧ ¬ 𝑌(le‘𝐾)𝑊) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
29 | | simp1l2 1175 |
. . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊 ∧ ¬ 𝑌(le‘𝐾)𝑊) → 𝑋 ∈ 𝐵) |
30 | | simp1r 1106 |
. . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊 ∧ ¬ 𝑌(le‘𝐾)𝑊) → ¬ 𝑋(le‘𝐾)𝑊) |
31 | | simp1l3 1176 |
. . . . . . 7
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊 ∧ ¬ 𝑌(le‘𝐾)𝑊) → 𝑌 ∈ 𝐵) |
32 | | simp3 1083 |
. . . . . . 7
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊 ∧ ¬ 𝑌(le‘𝐾)𝑊) → ¬ 𝑌(le‘𝐾)𝑊) |
33 | 31, 32 | jca 553 |
. . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊 ∧ ¬ 𝑌(le‘𝐾)𝑊) → (𝑌 ∈ 𝐵 ∧ ¬ 𝑌(le‘𝐾)𝑊)) |
34 | | simp2 1082 |
. . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊 ∧ ¬ 𝑌(le‘𝐾)𝑊) → (𝑋 ∧ 𝑌)(le‘𝐾)𝑊) |
35 | | eqid 2651 |
. . . . . . 7
⊢
(join‘𝐾) =
(join‘𝐾) |
36 | | eqid 2651 |
. . . . . . 7
⊢
(Atoms‘𝐾) =
(Atoms‘𝐾) |
37 | | eqid 2651 |
. . . . . . 7
⊢
((DVecH‘𝐾)‘𝑊) = ((DVecH‘𝐾)‘𝑊) |
38 | | eqid 2651 |
. . . . . . 7
⊢
(LSSum‘((DVecH‘𝐾)‘𝑊)) = (LSSum‘((DVecH‘𝐾)‘𝑊)) |
39 | 6, 13, 14, 35, 7, 36, 37, 38, 15 | dihmeetlem20N 36932 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌(le‘𝐾)𝑊) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊)) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) |
40 | 28, 29, 30, 33, 34, 39 | syl122anc 1375 |
. . . . 5
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊 ∧ ¬ 𝑌(le‘𝐾)𝑊) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) |
41 | 40 | 3expa 1284 |
. . . 4
⊢
((((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊) ∧ ¬ 𝑌(le‘𝐾)𝑊) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) |
42 | 27, 41 | pm2.61dan 849 |
. . 3
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) |
43 | | simpll1 1120 |
. . . 4
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ ¬ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
44 | | simpll2 1121 |
. . . 4
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ ¬ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊) → 𝑋 ∈ 𝐵) |
45 | | simpll3 1122 |
. . . 4
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ ¬ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊) → 𝑌 ∈ 𝐵) |
46 | | simpr 476 |
. . . 4
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ ¬ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊) → ¬ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊) |
47 | 6, 13, 7, 14, 15 | dihmeetcN 36908 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) |
48 | 43, 44, 45, 46, 47 | syl121anc 1371 |
. . 3
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ ¬ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) |
49 | 42, 48 | pm2.61dan 849 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) |
50 | 20, 49 | pm2.61dan 849 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) |