Proof of Theorem dihmeetALTN
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl1l 1225 | . . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋(le‘𝐾)𝑊) → 𝐾 ∈ HL) | 
| 2 | 1 | hllatd 39365 | . . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋(le‘𝐾)𝑊) → 𝐾 ∈ Lat) | 
| 3 |  | simpl2 1193 | . . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋(le‘𝐾)𝑊) → 𝑋 ∈ 𝐵) | 
| 4 |  | simpl3 1194 | . . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋(le‘𝐾)𝑊) → 𝑌 ∈ 𝐵) | 
| 5 |  | dihmeetALT.b | . . . . . 6
⊢ 𝐵 = (Base‘𝐾) | 
| 6 |  | dihmeetALT.m | . . . . . 6
⊢  ∧ =
(meet‘𝐾) | 
| 7 | 5, 6 | latmcom 18508 | . . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) = (𝑌 ∧ 𝑋)) | 
| 8 | 2, 3, 4, 7 | syl3anc 1373 | . . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋(le‘𝐾)𝑊) → (𝑋 ∧ 𝑌) = (𝑌 ∧ 𝑋)) | 
| 9 | 8 | fveq2d 6910 | . . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋(le‘𝐾)𝑊) → (𝐼‘(𝑋 ∧ 𝑌)) = (𝐼‘(𝑌 ∧ 𝑋))) | 
| 10 |  | simpl1 1192 | . . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋(le‘𝐾)𝑊) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | 
| 11 |  | simpr 484 | . . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋(le‘𝐾)𝑊) → 𝑋(le‘𝐾)𝑊) | 
| 12 |  | eqid 2737 | . . . . . 6
⊢
(le‘𝐾) =
(le‘𝐾) | 
| 13 |  | dihmeetALT.h | . . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) | 
| 14 |  | dihmeetALT.i | . . . . . 6
⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) | 
| 15 | 5, 12, 6, 13, 14 | dihmeetbN 41305 | . . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 ∈ 𝐵 ∧ 𝑋(le‘𝐾)𝑊)) → (𝐼‘(𝑌 ∧ 𝑋)) = ((𝐼‘𝑌) ∩ (𝐼‘𝑋))) | 
| 16 | 10, 4, 3, 11, 15 | syl112anc 1376 | . . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋(le‘𝐾)𝑊) → (𝐼‘(𝑌 ∧ 𝑋)) = ((𝐼‘𝑌) ∩ (𝐼‘𝑋))) | 
| 17 |  | incom 4209 | . . . 4
⊢ ((𝐼‘𝑌) ∩ (𝐼‘𝑋)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌)) | 
| 18 | 16, 17 | eqtrdi 2793 | . . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋(le‘𝐾)𝑊) → (𝐼‘(𝑌 ∧ 𝑋)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) | 
| 19 | 9, 18 | eqtrd 2777 | . 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋(le‘𝐾)𝑊) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) | 
| 20 |  | simpll1 1213 | . . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ 𝑌(le‘𝐾)𝑊) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | 
| 21 |  | simpll2 1214 | . . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ 𝑌(le‘𝐾)𝑊) → 𝑋 ∈ 𝐵) | 
| 22 |  | simpll3 1215 | . . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ 𝑌(le‘𝐾)𝑊) → 𝑌 ∈ 𝐵) | 
| 23 |  | simpr 484 | . . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ 𝑌(le‘𝐾)𝑊) → 𝑌(le‘𝐾)𝑊) | 
| 24 | 5, 12, 6, 13, 14 | dihmeetbN 41305 | . . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ (𝑌 ∈ 𝐵 ∧ 𝑌(le‘𝐾)𝑊)) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) | 
| 25 | 20, 21, 22, 23, 24 | syl112anc 1376 | . . . . 5
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ 𝑌(le‘𝐾)𝑊) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) | 
| 26 | 25 | adantlr 715 | . . . 4
⊢
((((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊) ∧ 𝑌(le‘𝐾)𝑊) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) | 
| 27 |  | simp1l1 1267 | . . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊 ∧ ¬ 𝑌(le‘𝐾)𝑊) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | 
| 28 |  | simp1l2 1268 | . . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊 ∧ ¬ 𝑌(le‘𝐾)𝑊) → 𝑋 ∈ 𝐵) | 
| 29 |  | simp1r 1199 | . . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊 ∧ ¬ 𝑌(le‘𝐾)𝑊) → ¬ 𝑋(le‘𝐾)𝑊) | 
| 30 |  | simp1l3 1269 | . . . . . . 7
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊 ∧ ¬ 𝑌(le‘𝐾)𝑊) → 𝑌 ∈ 𝐵) | 
| 31 |  | simp3 1139 | . . . . . . 7
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊 ∧ ¬ 𝑌(le‘𝐾)𝑊) → ¬ 𝑌(le‘𝐾)𝑊) | 
| 32 | 30, 31 | jca 511 | . . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊 ∧ ¬ 𝑌(le‘𝐾)𝑊) → (𝑌 ∈ 𝐵 ∧ ¬ 𝑌(le‘𝐾)𝑊)) | 
| 33 |  | simp2 1138 | . . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊 ∧ ¬ 𝑌(le‘𝐾)𝑊) → (𝑋 ∧ 𝑌)(le‘𝐾)𝑊) | 
| 34 |  | eqid 2737 | . . . . . . 7
⊢
(join‘𝐾) =
(join‘𝐾) | 
| 35 |  | eqid 2737 | . . . . . . 7
⊢
(Atoms‘𝐾) =
(Atoms‘𝐾) | 
| 36 |  | eqid 2737 | . . . . . . 7
⊢
((DVecH‘𝐾)‘𝑊) = ((DVecH‘𝐾)‘𝑊) | 
| 37 |  | eqid 2737 | . . . . . . 7
⊢
(LSSum‘((DVecH‘𝐾)‘𝑊)) = (LSSum‘((DVecH‘𝐾)‘𝑊)) | 
| 38 | 5, 12, 13, 34, 6, 35, 36, 37, 14 | dihmeetlem20N 41328 | . . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌(le‘𝐾)𝑊) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊)) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) | 
| 39 | 27, 28, 29, 32, 33, 38 | syl122anc 1381 | . . . . 5
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊 ∧ ¬ 𝑌(le‘𝐾)𝑊) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) | 
| 40 | 39 | 3expa 1119 | . . . 4
⊢
((((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊) ∧ ¬ 𝑌(le‘𝐾)𝑊) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) | 
| 41 | 26, 40 | pm2.61dan 813 | . . 3
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) | 
| 42 |  | simpll1 1213 | . . . 4
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ ¬ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | 
| 43 |  | simpll2 1214 | . . . 4
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ ¬ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊) → 𝑋 ∈ 𝐵) | 
| 44 |  | simpll3 1215 | . . . 4
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ ¬ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊) → 𝑌 ∈ 𝐵) | 
| 45 |  | simpr 484 | . . . 4
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ ¬ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊) → ¬ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊) | 
| 46 | 5, 12, 6, 13, 14 | dihmeetcN 41304 | . . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) | 
| 47 | 42, 43, 44, 45, 46 | syl121anc 1377 | . . 3
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) ∧ ¬ (𝑋 ∧ 𝑌)(le‘𝐾)𝑊) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) | 
| 48 | 41, 47 | pm2.61dan 813 | . 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋(le‘𝐾)𝑊) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) | 
| 49 | 19, 48 | pm2.61dan 813 | 1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) |