Step | Hyp | Ref
| Expression |
1 | | imsmetlem.1 |
. . 3
⊢ 𝑋 = (BaseSet‘𝑈) |
2 | | fvex 6113 |
. . 3
⊢
(BaseSet‘𝑈)
∈ V |
3 | 1, 2 | eqeltri 2684 |
. 2
⊢ 𝑋 ∈ V |
4 | | imsmetlem.9 |
. . 3
⊢ 𝑈 ∈ NrmCVec |
5 | | imsmetlem.8 |
. . . 4
⊢ 𝐷 = (IndMet‘𝑈) |
6 | 1, 5 | imsdf 26928 |
. . 3
⊢ (𝑈 ∈ NrmCVec → 𝐷:(𝑋 × 𝑋)⟶ℝ) |
7 | 4, 6 | ax-mp 5 |
. 2
⊢ 𝐷:(𝑋 × 𝑋)⟶ℝ |
8 | | imsmetlem.2 |
. . . . . 6
⊢ 𝐺 = ( +𝑣
‘𝑈) |
9 | | imsmetlem.4 |
. . . . . 6
⊢ 𝑆 = (
·𝑠OLD ‘𝑈) |
10 | | imsmetlem.6 |
. . . . . 6
⊢ 𝑁 =
(normCV‘𝑈) |
11 | 1, 8, 9, 10, 5 | imsdval2 26926 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) = (𝑁‘(𝑥𝐺(-1𝑆𝑦)))) |
12 | 4, 11 | mp3an1 1403 |
. . . 4
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) = (𝑁‘(𝑥𝐺(-1𝑆𝑦)))) |
13 | 12 | eqeq1d 2612 |
. . 3
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐷𝑦) = 0 ↔ (𝑁‘(𝑥𝐺(-1𝑆𝑦))) = 0)) |
14 | | neg1cn 11001 |
. . . . . 6
⊢ -1 ∈
ℂ |
15 | 1, 9 | nvscl 26865 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈
ℂ ∧ 𝑦 ∈
𝑋) → (-1𝑆𝑦) ∈ 𝑋) |
16 | 4, 14, 15 | mp3an12 1406 |
. . . . 5
⊢ (𝑦 ∈ 𝑋 → (-1𝑆𝑦) ∈ 𝑋) |
17 | 1, 8 | nvgcl 26859 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋) → (𝑥𝐺(-1𝑆𝑦)) ∈ 𝑋) |
18 | 4, 17 | mp3an1 1403 |
. . . . 5
⊢ ((𝑥 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋) → (𝑥𝐺(-1𝑆𝑦)) ∈ 𝑋) |
19 | 16, 18 | sylan2 490 |
. . . 4
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐺(-1𝑆𝑦)) ∈ 𝑋) |
20 | | imsmetlem.5 |
. . . . 5
⊢ 𝑍 = (0vec‘𝑈) |
21 | 1, 20, 10 | nvz 26908 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥𝐺(-1𝑆𝑦)) ∈ 𝑋) → ((𝑁‘(𝑥𝐺(-1𝑆𝑦))) = 0 ↔ (𝑥𝐺(-1𝑆𝑦)) = 𝑍)) |
22 | 4, 19, 21 | sylancr 694 |
. . 3
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑁‘(𝑥𝐺(-1𝑆𝑦))) = 0 ↔ (𝑥𝐺(-1𝑆𝑦)) = 𝑍)) |
23 | 1, 20 | nvzcl 26873 |
. . . . . . 7
⊢ (𝑈 ∈ NrmCVec → 𝑍 ∈ 𝑋) |
24 | 4, 23 | ax-mp 5 |
. . . . . 6
⊢ 𝑍 ∈ 𝑋 |
25 | 1, 8 | nvrcan 26863 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ ((𝑥𝐺(-1𝑆𝑦)) ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑍𝐺𝑦) ↔ (𝑥𝐺(-1𝑆𝑦)) = 𝑍)) |
26 | 4, 25 | mpan 702 |
. . . . . 6
⊢ (((𝑥𝐺(-1𝑆𝑦)) ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑍𝐺𝑦) ↔ (𝑥𝐺(-1𝑆𝑦)) = 𝑍)) |
27 | 24, 26 | mp3an2 1404 |
. . . . 5
⊢ (((𝑥𝐺(-1𝑆𝑦)) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑍𝐺𝑦) ↔ (𝑥𝐺(-1𝑆𝑦)) = 𝑍)) |
28 | 19, 27 | sylancom 698 |
. . . 4
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑍𝐺𝑦) ↔ (𝑥𝐺(-1𝑆𝑦)) = 𝑍)) |
29 | | simpl 472 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
30 | 16 | adantl 481 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (-1𝑆𝑦) ∈ 𝑋) |
31 | | simpr 476 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
32 | 1, 8 | nvass 26861 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑥𝐺((-1𝑆𝑦)𝐺𝑦))) |
33 | 4, 32 | mpan 702 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑥𝐺((-1𝑆𝑦)𝐺𝑦))) |
34 | 29, 30, 31, 33 | syl3anc 1318 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑥𝐺((-1𝑆𝑦)𝐺𝑦))) |
35 | 1, 8, 9, 20 | nvlinv 26891 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋) → ((-1𝑆𝑦)𝐺𝑦) = 𝑍) |
36 | 4, 35 | mpan 702 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑋 → ((-1𝑆𝑦)𝐺𝑦) = 𝑍) |
37 | 36 | adantl 481 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((-1𝑆𝑦)𝐺𝑦) = 𝑍) |
38 | 37 | oveq2d 6565 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐺((-1𝑆𝑦)𝐺𝑦)) = (𝑥𝐺𝑍)) |
39 | 1, 8, 20 | nv0rid 26874 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) → (𝑥𝐺𝑍) = 𝑥) |
40 | 4, 39 | mpan 702 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑋 → (𝑥𝐺𝑍) = 𝑥) |
41 | 40 | adantr 480 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐺𝑍) = 𝑥) |
42 | 34, 38, 41 | 3eqtrd 2648 |
. . . . 5
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = 𝑥) |
43 | 1, 8, 20 | nv0lid 26875 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋) → (𝑍𝐺𝑦) = 𝑦) |
44 | 4, 43 | mpan 702 |
. . . . . 6
⊢ (𝑦 ∈ 𝑋 → (𝑍𝐺𝑦) = 𝑦) |
45 | 44 | adantl 481 |
. . . . 5
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑍𝐺𝑦) = 𝑦) |
46 | 42, 45 | eqeq12d 2625 |
. . . 4
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑍𝐺𝑦) ↔ 𝑥 = 𝑦)) |
47 | 28, 46 | bitr3d 269 |
. . 3
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑦)) = 𝑍 ↔ 𝑥 = 𝑦)) |
48 | 13, 22, 47 | 3bitrd 293 |
. 2
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦)) |
49 | | simpr 476 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
50 | 1, 9 | nvscl 26865 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈
ℂ ∧ 𝑧 ∈
𝑋) → (-1𝑆𝑧) ∈ 𝑋) |
51 | 4, 14, 50 | mp3an12 1406 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝑋 → (-1𝑆𝑧) ∈ 𝑋) |
52 | 51 | adantr 480 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (-1𝑆𝑧) ∈ 𝑋) |
53 | 1, 8 | nvgcl 26859 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ (-1𝑆𝑧) ∈ 𝑋) → (𝑥𝐺(-1𝑆𝑧)) ∈ 𝑋) |
54 | 4, 53 | mp3an1 1403 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ (-1𝑆𝑧) ∈ 𝑋) → (𝑥𝐺(-1𝑆𝑧)) ∈ 𝑋) |
55 | 49, 52, 54 | syl2anc 691 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑥𝐺(-1𝑆𝑧)) ∈ 𝑋) |
56 | 55 | 3adant3 1074 |
. . . . 5
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐺(-1𝑆𝑧)) ∈ 𝑋) |
57 | 1, 8 | nvgcl 26859 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋) → (𝑧𝐺(-1𝑆𝑦)) ∈ 𝑋) |
58 | 4, 57 | mp3an1 1403 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋) → (𝑧𝐺(-1𝑆𝑦)) ∈ 𝑋) |
59 | 16, 58 | sylan2 490 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑧𝐺(-1𝑆𝑦)) ∈ 𝑋) |
60 | 59 | 3adant2 1073 |
. . . . 5
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑧𝐺(-1𝑆𝑦)) ∈ 𝑋) |
61 | 1, 8, 10 | nvtri 26909 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥𝐺(-1𝑆𝑧)) ∈ 𝑋 ∧ (𝑧𝐺(-1𝑆𝑦)) ∈ 𝑋) → (𝑁‘((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) ≤ ((𝑁‘(𝑥𝐺(-1𝑆𝑧))) + (𝑁‘(𝑧𝐺(-1𝑆𝑦))))) |
62 | 4, 61 | mp3an1 1403 |
. . . . 5
⊢ (((𝑥𝐺(-1𝑆𝑧)) ∈ 𝑋 ∧ (𝑧𝐺(-1𝑆𝑦)) ∈ 𝑋) → (𝑁‘((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) ≤ ((𝑁‘(𝑥𝐺(-1𝑆𝑧))) + (𝑁‘(𝑧𝐺(-1𝑆𝑦))))) |
63 | 56, 60, 62 | syl2anc 691 |
. . . 4
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑁‘((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) ≤ ((𝑁‘(𝑥𝐺(-1𝑆𝑧))) + (𝑁‘(𝑧𝐺(-1𝑆𝑦))))) |
64 | 12 | 3adant1 1072 |
. . . . 5
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) = (𝑁‘(𝑥𝐺(-1𝑆𝑦)))) |
65 | | simp1 1054 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 𝑧 ∈ 𝑋) |
66 | 16 | 3ad2ant3 1077 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (-1𝑆𝑦) ∈ 𝑋) |
67 | 1, 8 | nvass 26861 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ ((𝑥𝐺(-1𝑆𝑧)) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋)) → (((𝑥𝐺(-1𝑆𝑧))𝐺𝑧)𝐺(-1𝑆𝑦)) = ((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) |
68 | 4, 67 | mpan 702 |
. . . . . . . 8
⊢ (((𝑥𝐺(-1𝑆𝑧)) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋) → (((𝑥𝐺(-1𝑆𝑧))𝐺𝑧)𝐺(-1𝑆𝑦)) = ((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) |
69 | 56, 65, 66, 68 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝑥𝐺(-1𝑆𝑧))𝐺𝑧)𝐺(-1𝑆𝑦)) = ((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) |
70 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → 𝑧 ∈ 𝑋) |
71 | 1, 8 | nvass 26861 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥 ∈ 𝑋 ∧ (-1𝑆𝑧) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑥𝐺(-1𝑆𝑧))𝐺𝑧) = (𝑥𝐺((-1𝑆𝑧)𝐺𝑧))) |
72 | 4, 71 | mpan 702 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ (-1𝑆𝑧) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑧))𝐺𝑧) = (𝑥𝐺((-1𝑆𝑧)𝐺𝑧))) |
73 | 49, 52, 70, 72 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑧))𝐺𝑧) = (𝑥𝐺((-1𝑆𝑧)𝐺𝑧))) |
74 | 1, 8, 9, 20 | nvlinv 26891 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → ((-1𝑆𝑧)𝐺𝑧) = 𝑍) |
75 | 4, 74 | mpan 702 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑋 → ((-1𝑆𝑧)𝐺𝑧) = 𝑍) |
76 | 75 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → ((-1𝑆𝑧)𝐺𝑧) = 𝑍) |
77 | 76 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑥𝐺((-1𝑆𝑧)𝐺𝑧)) = (𝑥𝐺𝑍)) |
78 | 40 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑥𝐺𝑍) = 𝑥) |
79 | 73, 77, 78 | 3eqtrd 2648 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑧))𝐺𝑧) = 𝑥) |
80 | 79 | 3adant3 1074 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑧))𝐺𝑧) = 𝑥) |
81 | 80 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝑥𝐺(-1𝑆𝑧))𝐺𝑧)𝐺(-1𝑆𝑦)) = (𝑥𝐺(-1𝑆𝑦))) |
82 | 69, 81 | eqtr3d 2646 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦))) = (𝑥𝐺(-1𝑆𝑦))) |
83 | 82 | fveq2d 6107 |
. . . . 5
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑁‘((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) = (𝑁‘(𝑥𝐺(-1𝑆𝑦)))) |
84 | 64, 83 | eqtr4d 2647 |
. . . 4
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) = (𝑁‘((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦))))) |
85 | 1, 8, 9, 10, 5 | imsdval2 26926 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑧𝐷𝑥) = (𝑁‘(𝑧𝐺(-1𝑆𝑥)))) |
86 | 4, 85 | mp3an1 1403 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑧𝐷𝑥) = (𝑁‘(𝑧𝐺(-1𝑆𝑥)))) |
87 | 1, 8, 9, 10 | nvdif 26905 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑁‘(𝑧𝐺(-1𝑆𝑥))) = (𝑁‘(𝑥𝐺(-1𝑆𝑧)))) |
88 | 4, 87 | mp3an1 1403 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑁‘(𝑧𝐺(-1𝑆𝑥))) = (𝑁‘(𝑥𝐺(-1𝑆𝑧)))) |
89 | 86, 88 | eqtrd 2644 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑧𝐷𝑥) = (𝑁‘(𝑥𝐺(-1𝑆𝑧)))) |
90 | 89 | 3adant3 1074 |
. . . . 5
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑧𝐷𝑥) = (𝑁‘(𝑥𝐺(-1𝑆𝑧)))) |
91 | 1, 8, 9, 10, 5 | imsdval2 26926 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑧𝐷𝑦) = (𝑁‘(𝑧𝐺(-1𝑆𝑦)))) |
92 | 4, 91 | mp3an1 1403 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑧𝐷𝑦) = (𝑁‘(𝑧𝐺(-1𝑆𝑦)))) |
93 | 92 | 3adant2 1073 |
. . . . 5
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑧𝐷𝑦) = (𝑁‘(𝑧𝐺(-1𝑆𝑦)))) |
94 | 90, 93 | oveq12d 6567 |
. . . 4
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((𝑁‘(𝑥𝐺(-1𝑆𝑧))) + (𝑁‘(𝑧𝐺(-1𝑆𝑦))))) |
95 | 63, 84, 94 | 3brtr4d 4615 |
. . 3
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))) |
96 | 95 | 3coml 1264 |
. 2
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))) |
97 | 3, 7, 48, 96 | ismeti 21940 |
1
⊢ 𝐷 ∈ (Met‘𝑋) |