| Step | Hyp | Ref
| Expression |
| 1 | | imsmetlem.1 |
. . 3
⊢ 𝑋 = (BaseSet‘𝑈) |
| 2 | 1 | fvexi 6920 |
. 2
⊢ 𝑋 ∈ V |
| 3 | | imsmetlem.9 |
. . 3
⊢ 𝑈 ∈ NrmCVec |
| 4 | | imsmetlem.8 |
. . . 4
⊢ 𝐷 = (IndMet‘𝑈) |
| 5 | 1, 4 | imsdf 30708 |
. . 3
⊢ (𝑈 ∈ NrmCVec → 𝐷:(𝑋 × 𝑋)⟶ℝ) |
| 6 | 3, 5 | ax-mp 5 |
. 2
⊢ 𝐷:(𝑋 × 𝑋)⟶ℝ |
| 7 | | imsmetlem.2 |
. . . . . 6
⊢ 𝐺 = ( +𝑣
‘𝑈) |
| 8 | | imsmetlem.4 |
. . . . . 6
⊢ 𝑆 = (
·𝑠OLD ‘𝑈) |
| 9 | | imsmetlem.6 |
. . . . . 6
⊢ 𝑁 =
(normCV‘𝑈) |
| 10 | 1, 7, 8, 9, 4 | imsdval2 30706 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) = (𝑁‘(𝑥𝐺(-1𝑆𝑦)))) |
| 11 | 3, 10 | mp3an1 1450 |
. . . 4
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) = (𝑁‘(𝑥𝐺(-1𝑆𝑦)))) |
| 12 | 11 | eqeq1d 2739 |
. . 3
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐷𝑦) = 0 ↔ (𝑁‘(𝑥𝐺(-1𝑆𝑦))) = 0)) |
| 13 | | neg1cn 12380 |
. . . . . 6
⊢ -1 ∈
ℂ |
| 14 | 1, 8 | nvscl 30645 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈
ℂ ∧ 𝑦 ∈
𝑋) → (-1𝑆𝑦) ∈ 𝑋) |
| 15 | 3, 13, 14 | mp3an12 1453 |
. . . . 5
⊢ (𝑦 ∈ 𝑋 → (-1𝑆𝑦) ∈ 𝑋) |
| 16 | 1, 7 | nvgcl 30639 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋) → (𝑥𝐺(-1𝑆𝑦)) ∈ 𝑋) |
| 17 | 3, 16 | mp3an1 1450 |
. . . . 5
⊢ ((𝑥 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋) → (𝑥𝐺(-1𝑆𝑦)) ∈ 𝑋) |
| 18 | 15, 17 | sylan2 593 |
. . . 4
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐺(-1𝑆𝑦)) ∈ 𝑋) |
| 19 | | imsmetlem.5 |
. . . . 5
⊢ 𝑍 = (0vec‘𝑈) |
| 20 | 1, 19, 9 | nvz 30688 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥𝐺(-1𝑆𝑦)) ∈ 𝑋) → ((𝑁‘(𝑥𝐺(-1𝑆𝑦))) = 0 ↔ (𝑥𝐺(-1𝑆𝑦)) = 𝑍)) |
| 21 | 3, 18, 20 | sylancr 587 |
. . 3
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑁‘(𝑥𝐺(-1𝑆𝑦))) = 0 ↔ (𝑥𝐺(-1𝑆𝑦)) = 𝑍)) |
| 22 | 1, 19 | nvzcl 30653 |
. . . . . . 7
⊢ (𝑈 ∈ NrmCVec → 𝑍 ∈ 𝑋) |
| 23 | 3, 22 | ax-mp 5 |
. . . . . 6
⊢ 𝑍 ∈ 𝑋 |
| 24 | 1, 7 | nvrcan 30643 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ ((𝑥𝐺(-1𝑆𝑦)) ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑍𝐺𝑦) ↔ (𝑥𝐺(-1𝑆𝑦)) = 𝑍)) |
| 25 | 3, 24 | mpan 690 |
. . . . . 6
⊢ (((𝑥𝐺(-1𝑆𝑦)) ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑍𝐺𝑦) ↔ (𝑥𝐺(-1𝑆𝑦)) = 𝑍)) |
| 26 | 23, 25 | mp3an2 1451 |
. . . . 5
⊢ (((𝑥𝐺(-1𝑆𝑦)) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑍𝐺𝑦) ↔ (𝑥𝐺(-1𝑆𝑦)) = 𝑍)) |
| 27 | 18, 26 | sylancom 588 |
. . . 4
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑍𝐺𝑦) ↔ (𝑥𝐺(-1𝑆𝑦)) = 𝑍)) |
| 28 | | simpl 482 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
| 29 | 15 | adantl 481 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (-1𝑆𝑦) ∈ 𝑋) |
| 30 | | simpr 484 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
| 31 | 1, 7 | nvass 30641 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑥𝐺((-1𝑆𝑦)𝐺𝑦))) |
| 32 | 3, 31 | mpan 690 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑥𝐺((-1𝑆𝑦)𝐺𝑦))) |
| 33 | 28, 29, 30, 32 | syl3anc 1373 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑥𝐺((-1𝑆𝑦)𝐺𝑦))) |
| 34 | 1, 7, 8, 19 | nvlinv 30671 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋) → ((-1𝑆𝑦)𝐺𝑦) = 𝑍) |
| 35 | 3, 34 | mpan 690 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑋 → ((-1𝑆𝑦)𝐺𝑦) = 𝑍) |
| 36 | 35 | adantl 481 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((-1𝑆𝑦)𝐺𝑦) = 𝑍) |
| 37 | 36 | oveq2d 7447 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐺((-1𝑆𝑦)𝐺𝑦)) = (𝑥𝐺𝑍)) |
| 38 | 1, 7, 19 | nv0rid 30654 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) → (𝑥𝐺𝑍) = 𝑥) |
| 39 | 3, 38 | mpan 690 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑋 → (𝑥𝐺𝑍) = 𝑥) |
| 40 | 39 | adantr 480 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐺𝑍) = 𝑥) |
| 41 | 33, 37, 40 | 3eqtrd 2781 |
. . . . 5
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = 𝑥) |
| 42 | 1, 7, 19 | nv0lid 30655 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋) → (𝑍𝐺𝑦) = 𝑦) |
| 43 | 3, 42 | mpan 690 |
. . . . . 6
⊢ (𝑦 ∈ 𝑋 → (𝑍𝐺𝑦) = 𝑦) |
| 44 | 43 | adantl 481 |
. . . . 5
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑍𝐺𝑦) = 𝑦) |
| 45 | 41, 44 | eqeq12d 2753 |
. . . 4
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑍𝐺𝑦) ↔ 𝑥 = 𝑦)) |
| 46 | 27, 45 | bitr3d 281 |
. . 3
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑦)) = 𝑍 ↔ 𝑥 = 𝑦)) |
| 47 | 12, 21, 46 | 3bitrd 305 |
. 2
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦)) |
| 48 | | simpr 484 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
| 49 | 1, 8 | nvscl 30645 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈
ℂ ∧ 𝑧 ∈
𝑋) → (-1𝑆𝑧) ∈ 𝑋) |
| 50 | 3, 13, 49 | mp3an12 1453 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝑋 → (-1𝑆𝑧) ∈ 𝑋) |
| 51 | 50 | adantr 480 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (-1𝑆𝑧) ∈ 𝑋) |
| 52 | 1, 7 | nvgcl 30639 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ (-1𝑆𝑧) ∈ 𝑋) → (𝑥𝐺(-1𝑆𝑧)) ∈ 𝑋) |
| 53 | 3, 52 | mp3an1 1450 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ (-1𝑆𝑧) ∈ 𝑋) → (𝑥𝐺(-1𝑆𝑧)) ∈ 𝑋) |
| 54 | 48, 51, 53 | syl2anc 584 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑥𝐺(-1𝑆𝑧)) ∈ 𝑋) |
| 55 | 54 | 3adant3 1133 |
. . . . 5
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐺(-1𝑆𝑧)) ∈ 𝑋) |
| 56 | 1, 7 | nvgcl 30639 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋) → (𝑧𝐺(-1𝑆𝑦)) ∈ 𝑋) |
| 57 | 3, 56 | mp3an1 1450 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋) → (𝑧𝐺(-1𝑆𝑦)) ∈ 𝑋) |
| 58 | 15, 57 | sylan2 593 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑧𝐺(-1𝑆𝑦)) ∈ 𝑋) |
| 59 | 58 | 3adant2 1132 |
. . . . 5
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑧𝐺(-1𝑆𝑦)) ∈ 𝑋) |
| 60 | 1, 7, 9 | nvtri 30689 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥𝐺(-1𝑆𝑧)) ∈ 𝑋 ∧ (𝑧𝐺(-1𝑆𝑦)) ∈ 𝑋) → (𝑁‘((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) ≤ ((𝑁‘(𝑥𝐺(-1𝑆𝑧))) + (𝑁‘(𝑧𝐺(-1𝑆𝑦))))) |
| 61 | 3, 60 | mp3an1 1450 |
. . . . 5
⊢ (((𝑥𝐺(-1𝑆𝑧)) ∈ 𝑋 ∧ (𝑧𝐺(-1𝑆𝑦)) ∈ 𝑋) → (𝑁‘((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) ≤ ((𝑁‘(𝑥𝐺(-1𝑆𝑧))) + (𝑁‘(𝑧𝐺(-1𝑆𝑦))))) |
| 62 | 55, 59, 61 | syl2anc 584 |
. . . 4
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑁‘((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) ≤ ((𝑁‘(𝑥𝐺(-1𝑆𝑧))) + (𝑁‘(𝑧𝐺(-1𝑆𝑦))))) |
| 63 | 11 | 3adant1 1131 |
. . . . 5
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) = (𝑁‘(𝑥𝐺(-1𝑆𝑦)))) |
| 64 | | simp1 1137 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 𝑧 ∈ 𝑋) |
| 65 | 15 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (-1𝑆𝑦) ∈ 𝑋) |
| 66 | 1, 7 | nvass 30641 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ ((𝑥𝐺(-1𝑆𝑧)) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋)) → (((𝑥𝐺(-1𝑆𝑧))𝐺𝑧)𝐺(-1𝑆𝑦)) = ((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) |
| 67 | 3, 66 | mpan 690 |
. . . . . . . 8
⊢ (((𝑥𝐺(-1𝑆𝑧)) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋) → (((𝑥𝐺(-1𝑆𝑧))𝐺𝑧)𝐺(-1𝑆𝑦)) = ((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) |
| 68 | 55, 64, 65, 67 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝑥𝐺(-1𝑆𝑧))𝐺𝑧)𝐺(-1𝑆𝑦)) = ((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) |
| 69 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → 𝑧 ∈ 𝑋) |
| 70 | 1, 7 | nvass 30641 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥 ∈ 𝑋 ∧ (-1𝑆𝑧) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑥𝐺(-1𝑆𝑧))𝐺𝑧) = (𝑥𝐺((-1𝑆𝑧)𝐺𝑧))) |
| 71 | 3, 70 | mpan 690 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ (-1𝑆𝑧) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑧))𝐺𝑧) = (𝑥𝐺((-1𝑆𝑧)𝐺𝑧))) |
| 72 | 48, 51, 69, 71 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑧))𝐺𝑧) = (𝑥𝐺((-1𝑆𝑧)𝐺𝑧))) |
| 73 | 1, 7, 8, 19 | nvlinv 30671 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → ((-1𝑆𝑧)𝐺𝑧) = 𝑍) |
| 74 | 3, 73 | mpan 690 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑋 → ((-1𝑆𝑧)𝐺𝑧) = 𝑍) |
| 75 | 74 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → ((-1𝑆𝑧)𝐺𝑧) = 𝑍) |
| 76 | 75 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑥𝐺((-1𝑆𝑧)𝐺𝑧)) = (𝑥𝐺𝑍)) |
| 77 | 39 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑥𝐺𝑍) = 𝑥) |
| 78 | 72, 76, 77 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑧))𝐺𝑧) = 𝑥) |
| 79 | 78 | 3adant3 1133 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑧))𝐺𝑧) = 𝑥) |
| 80 | 79 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝑥𝐺(-1𝑆𝑧))𝐺𝑧)𝐺(-1𝑆𝑦)) = (𝑥𝐺(-1𝑆𝑦))) |
| 81 | 68, 80 | eqtr3d 2779 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦))) = (𝑥𝐺(-1𝑆𝑦))) |
| 82 | 81 | fveq2d 6910 |
. . . . 5
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑁‘((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) = (𝑁‘(𝑥𝐺(-1𝑆𝑦)))) |
| 83 | 63, 82 | eqtr4d 2780 |
. . . 4
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) = (𝑁‘((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦))))) |
| 84 | 1, 7, 8, 9, 4 | imsdval2 30706 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑧𝐷𝑥) = (𝑁‘(𝑧𝐺(-1𝑆𝑥)))) |
| 85 | 3, 84 | mp3an1 1450 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑧𝐷𝑥) = (𝑁‘(𝑧𝐺(-1𝑆𝑥)))) |
| 86 | 1, 7, 8, 9 | nvdif 30685 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑁‘(𝑧𝐺(-1𝑆𝑥))) = (𝑁‘(𝑥𝐺(-1𝑆𝑧)))) |
| 87 | 3, 86 | mp3an1 1450 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑁‘(𝑧𝐺(-1𝑆𝑥))) = (𝑁‘(𝑥𝐺(-1𝑆𝑧)))) |
| 88 | 85, 87 | eqtrd 2777 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑧𝐷𝑥) = (𝑁‘(𝑥𝐺(-1𝑆𝑧)))) |
| 89 | 88 | 3adant3 1133 |
. . . . 5
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑧𝐷𝑥) = (𝑁‘(𝑥𝐺(-1𝑆𝑧)))) |
| 90 | 1, 7, 8, 9, 4 | imsdval2 30706 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑧𝐷𝑦) = (𝑁‘(𝑧𝐺(-1𝑆𝑦)))) |
| 91 | 3, 90 | mp3an1 1450 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑧𝐷𝑦) = (𝑁‘(𝑧𝐺(-1𝑆𝑦)))) |
| 92 | 91 | 3adant2 1132 |
. . . . 5
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑧𝐷𝑦) = (𝑁‘(𝑧𝐺(-1𝑆𝑦)))) |
| 93 | 89, 92 | oveq12d 7449 |
. . . 4
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((𝑁‘(𝑥𝐺(-1𝑆𝑧))) + (𝑁‘(𝑧𝐺(-1𝑆𝑦))))) |
| 94 | 62, 83, 93 | 3brtr4d 5175 |
. . 3
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))) |
| 95 | 94 | 3coml 1128 |
. 2
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))) |
| 96 | 2, 6, 47, 95 | ismeti 24335 |
1
⊢ 𝐷 ∈ (Met‘𝑋) |