Step | Hyp | Ref
| Expression |
1 | | imsmetlem.1 |
. . 3
⊢ 𝑋 = (BaseSet‘𝑈) |
2 | | fvex 6201 |
. . 3
⊢
(BaseSet‘𝑈)
∈ V |
3 | 1, 2 | eqeltri 2697 |
. 2
⊢ 𝑋 ∈ V |
4 | | imsmetlem.9 |
. . 3
⊢ 𝑈 ∈ NrmCVec |
5 | | imsmetlem.8 |
. . . 4
⊢ 𝐷 = (IndMet‘𝑈) |
6 | 1, 5 | imsdf 27544 |
. . 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 27542 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) = (𝑁‘(𝑥𝐺(-1𝑆𝑦)))) |
12 | 4, 11 | mp3an1 1411 |
. . . 4
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) = (𝑁‘(𝑥𝐺(-1𝑆𝑦)))) |
13 | 12 | eqeq1d 2624 |
. . 3
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐷𝑦) = 0 ↔ (𝑁‘(𝑥𝐺(-1𝑆𝑦))) = 0)) |
14 | | neg1cn 11124 |
. . . . . 6
⊢ -1 ∈
ℂ |
15 | 1, 9 | nvscl 27481 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈
ℂ ∧ 𝑦 ∈
𝑋) → (-1𝑆𝑦) ∈ 𝑋) |
16 | 4, 14, 15 | mp3an12 1414 |
. . . . 5
⊢ (𝑦 ∈ 𝑋 → (-1𝑆𝑦) ∈ 𝑋) |
17 | 1, 8 | nvgcl 27475 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋) → (𝑥𝐺(-1𝑆𝑦)) ∈ 𝑋) |
18 | 4, 17 | mp3an1 1411 |
. . . . 5
⊢ ((𝑥 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋) → (𝑥𝐺(-1𝑆𝑦)) ∈ 𝑋) |
19 | 16, 18 | sylan2 491 |
. . . 4
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐺(-1𝑆𝑦)) ∈ 𝑋) |
20 | | imsmetlem.5 |
. . . . 5
⊢ 𝑍 = (0vec‘𝑈) |
21 | 1, 20, 10 | nvz 27524 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥𝐺(-1𝑆𝑦)) ∈ 𝑋) → ((𝑁‘(𝑥𝐺(-1𝑆𝑦))) = 0 ↔ (𝑥𝐺(-1𝑆𝑦)) = 𝑍)) |
22 | 4, 19, 21 | sylancr 695 |
. . 3
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑁‘(𝑥𝐺(-1𝑆𝑦))) = 0 ↔ (𝑥𝐺(-1𝑆𝑦)) = 𝑍)) |
23 | 1, 20 | nvzcl 27489 |
. . . . . . 7
⊢ (𝑈 ∈ NrmCVec → 𝑍 ∈ 𝑋) |
24 | 4, 23 | ax-mp 5 |
. . . . . 6
⊢ 𝑍 ∈ 𝑋 |
25 | 1, 8 | nvrcan 27479 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ ((𝑥𝐺(-1𝑆𝑦)) ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑍𝐺𝑦) ↔ (𝑥𝐺(-1𝑆𝑦)) = 𝑍)) |
26 | 4, 25 | mpan 706 |
. . . . . 6
⊢ (((𝑥𝐺(-1𝑆𝑦)) ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑍𝐺𝑦) ↔ (𝑥𝐺(-1𝑆𝑦)) = 𝑍)) |
27 | 24, 26 | mp3an2 1412 |
. . . . 5
⊢ (((𝑥𝐺(-1𝑆𝑦)) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑍𝐺𝑦) ↔ (𝑥𝐺(-1𝑆𝑦)) = 𝑍)) |
28 | 19, 27 | sylancom 701 |
. . . 4
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑍𝐺𝑦) ↔ (𝑥𝐺(-1𝑆𝑦)) = 𝑍)) |
29 | | simpl 473 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
30 | 16 | adantl 482 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (-1𝑆𝑦) ∈ 𝑋) |
31 | | simpr 477 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
32 | 1, 8 | nvass 27477 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑥𝐺((-1𝑆𝑦)𝐺𝑦))) |
33 | 4, 32 | mpan 706 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑥𝐺((-1𝑆𝑦)𝐺𝑦))) |
34 | 29, 30, 31, 33 | syl3anc 1326 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑥𝐺((-1𝑆𝑦)𝐺𝑦))) |
35 | 1, 8, 9, 20 | nvlinv 27507 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋) → ((-1𝑆𝑦)𝐺𝑦) = 𝑍) |
36 | 4, 35 | mpan 706 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑋 → ((-1𝑆𝑦)𝐺𝑦) = 𝑍) |
37 | 36 | adantl 482 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((-1𝑆𝑦)𝐺𝑦) = 𝑍) |
38 | 37 | oveq2d 6666 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐺((-1𝑆𝑦)𝐺𝑦)) = (𝑥𝐺𝑍)) |
39 | 1, 8, 20 | nv0rid 27490 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) → (𝑥𝐺𝑍) = 𝑥) |
40 | 4, 39 | mpan 706 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑋 → (𝑥𝐺𝑍) = 𝑥) |
41 | 40 | adantr 481 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐺𝑍) = 𝑥) |
42 | 34, 38, 41 | 3eqtrd 2660 |
. . . . 5
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = 𝑥) |
43 | 1, 8, 20 | nv0lid 27491 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋) → (𝑍𝐺𝑦) = 𝑦) |
44 | 4, 43 | mpan 706 |
. . . . . 6
⊢ (𝑦 ∈ 𝑋 → (𝑍𝐺𝑦) = 𝑦) |
45 | 44 | adantl 482 |
. . . . 5
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑍𝐺𝑦) = 𝑦) |
46 | 42, 45 | eqeq12d 2637 |
. . . 4
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝑥𝐺(-1𝑆𝑦))𝐺𝑦) = (𝑍𝐺𝑦) ↔ 𝑥 = 𝑦)) |
47 | 28, 46 | bitr3d 270 |
. . 3
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑦)) = 𝑍 ↔ 𝑥 = 𝑦)) |
48 | 13, 22, 47 | 3bitrd 294 |
. 2
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦)) |
49 | | simpr 477 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
50 | 1, 9 | nvscl 27481 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈
ℂ ∧ 𝑧 ∈
𝑋) → (-1𝑆𝑧) ∈ 𝑋) |
51 | 4, 14, 50 | mp3an12 1414 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝑋 → (-1𝑆𝑧) ∈ 𝑋) |
52 | 51 | adantr 481 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (-1𝑆𝑧) ∈ 𝑋) |
53 | 1, 8 | nvgcl 27475 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ (-1𝑆𝑧) ∈ 𝑋) → (𝑥𝐺(-1𝑆𝑧)) ∈ 𝑋) |
54 | 4, 53 | mp3an1 1411 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ (-1𝑆𝑧) ∈ 𝑋) → (𝑥𝐺(-1𝑆𝑧)) ∈ 𝑋) |
55 | 49, 52, 54 | syl2anc 693 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑥𝐺(-1𝑆𝑧)) ∈ 𝑋) |
56 | 55 | 3adant3 1081 |
. . . . 5
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐺(-1𝑆𝑧)) ∈ 𝑋) |
57 | 1, 8 | nvgcl 27475 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋) → (𝑧𝐺(-1𝑆𝑦)) ∈ 𝑋) |
58 | 4, 57 | mp3an1 1411 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋) → (𝑧𝐺(-1𝑆𝑦)) ∈ 𝑋) |
59 | 16, 58 | sylan2 491 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑧𝐺(-1𝑆𝑦)) ∈ 𝑋) |
60 | 59 | 3adant2 1080 |
. . . . 5
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑧𝐺(-1𝑆𝑦)) ∈ 𝑋) |
61 | 1, 8, 10 | nvtri 27525 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥𝐺(-1𝑆𝑧)) ∈ 𝑋 ∧ (𝑧𝐺(-1𝑆𝑦)) ∈ 𝑋) → (𝑁‘((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) ≤ ((𝑁‘(𝑥𝐺(-1𝑆𝑧))) + (𝑁‘(𝑧𝐺(-1𝑆𝑦))))) |
62 | 4, 61 | mp3an1 1411 |
. . . . 5
⊢ (((𝑥𝐺(-1𝑆𝑧)) ∈ 𝑋 ∧ (𝑧𝐺(-1𝑆𝑦)) ∈ 𝑋) → (𝑁‘((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) ≤ ((𝑁‘(𝑥𝐺(-1𝑆𝑧))) + (𝑁‘(𝑧𝐺(-1𝑆𝑦))))) |
63 | 56, 60, 62 | syl2anc 693 |
. . . 4
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑁‘((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) ≤ ((𝑁‘(𝑥𝐺(-1𝑆𝑧))) + (𝑁‘(𝑧𝐺(-1𝑆𝑦))))) |
64 | 12 | 3adant1 1079 |
. . . . 5
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) = (𝑁‘(𝑥𝐺(-1𝑆𝑦)))) |
65 | | simp1 1061 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → 𝑧 ∈ 𝑋) |
66 | 16 | 3ad2ant3 1084 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (-1𝑆𝑦) ∈ 𝑋) |
67 | 1, 8 | nvass 27477 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ ((𝑥𝐺(-1𝑆𝑧)) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋)) → (((𝑥𝐺(-1𝑆𝑧))𝐺𝑧)𝐺(-1𝑆𝑦)) = ((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) |
68 | 4, 67 | mpan 706 |
. . . . . . . 8
⊢ (((𝑥𝐺(-1𝑆𝑧)) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (-1𝑆𝑦) ∈ 𝑋) → (((𝑥𝐺(-1𝑆𝑧))𝐺𝑧)𝐺(-1𝑆𝑦)) = ((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) |
69 | 56, 65, 66, 68 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝑥𝐺(-1𝑆𝑧))𝐺𝑧)𝐺(-1𝑆𝑦)) = ((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) |
70 | | simpl 473 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → 𝑧 ∈ 𝑋) |
71 | 1, 8 | nvass 27477 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥 ∈ 𝑋 ∧ (-1𝑆𝑧) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑥𝐺(-1𝑆𝑧))𝐺𝑧) = (𝑥𝐺((-1𝑆𝑧)𝐺𝑧))) |
72 | 4, 71 | mpan 706 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ (-1𝑆𝑧) ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑧))𝐺𝑧) = (𝑥𝐺((-1𝑆𝑧)𝐺𝑧))) |
73 | 49, 52, 70, 72 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑧))𝐺𝑧) = (𝑥𝐺((-1𝑆𝑧)𝐺𝑧))) |
74 | 1, 8, 9, 20 | nvlinv 27507 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → ((-1𝑆𝑧)𝐺𝑧) = 𝑍) |
75 | 4, 74 | mpan 706 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑋 → ((-1𝑆𝑧)𝐺𝑧) = 𝑍) |
76 | 75 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → ((-1𝑆𝑧)𝐺𝑧) = 𝑍) |
77 | 76 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑥𝐺((-1𝑆𝑧)𝐺𝑧)) = (𝑥𝐺𝑍)) |
78 | 40 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑥𝐺𝑍) = 𝑥) |
79 | 73, 77, 78 | 3eqtrd 2660 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑧))𝐺𝑧) = 𝑥) |
80 | 79 | 3adant3 1081 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑧))𝐺𝑧) = 𝑥) |
81 | 80 | oveq1d 6665 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (((𝑥𝐺(-1𝑆𝑧))𝐺𝑧)𝐺(-1𝑆𝑦)) = (𝑥𝐺(-1𝑆𝑦))) |
82 | 69, 81 | eqtr3d 2658 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦))) = (𝑥𝐺(-1𝑆𝑦))) |
83 | 82 | fveq2d 6195 |
. . . . 5
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑁‘((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦)))) = (𝑁‘(𝑥𝐺(-1𝑆𝑦)))) |
84 | 64, 83 | eqtr4d 2659 |
. . . 4
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) = (𝑁‘((𝑥𝐺(-1𝑆𝑧))𝐺(𝑧𝐺(-1𝑆𝑦))))) |
85 | 1, 8, 9, 10, 5 | imsdval2 27542 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑧𝐷𝑥) = (𝑁‘(𝑧𝐺(-1𝑆𝑥)))) |
86 | 4, 85 | mp3an1 1411 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑧𝐷𝑥) = (𝑁‘(𝑧𝐺(-1𝑆𝑥)))) |
87 | 1, 8, 9, 10 | nvdif 27521 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑁‘(𝑧𝐺(-1𝑆𝑥))) = (𝑁‘(𝑥𝐺(-1𝑆𝑧)))) |
88 | 4, 87 | mp3an1 1411 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑁‘(𝑧𝐺(-1𝑆𝑥))) = (𝑁‘(𝑥𝐺(-1𝑆𝑧)))) |
89 | 86, 88 | eqtrd 2656 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑧𝐷𝑥) = (𝑁‘(𝑥𝐺(-1𝑆𝑧)))) |
90 | 89 | 3adant3 1081 |
. . . . 5
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑧𝐷𝑥) = (𝑁‘(𝑥𝐺(-1𝑆𝑧)))) |
91 | 1, 8, 9, 10, 5 | imsdval2 27542 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑧𝐷𝑦) = (𝑁‘(𝑧𝐺(-1𝑆𝑦)))) |
92 | 4, 91 | mp3an1 1411 |
. . . . . 6
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑧𝐷𝑦) = (𝑁‘(𝑧𝐺(-1𝑆𝑦)))) |
93 | 92 | 3adant2 1080 |
. . . . 5
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑧𝐷𝑦) = (𝑁‘(𝑧𝐺(-1𝑆𝑦)))) |
94 | 90, 93 | oveq12d 6668 |
. . . 4
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)) = ((𝑁‘(𝑥𝐺(-1𝑆𝑧))) + (𝑁‘(𝑧𝐺(-1𝑆𝑦))))) |
95 | 63, 84, 94 | 3brtr4d 4685 |
. . 3
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))) |
96 | 95 | 3coml 1272 |
. 2
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦))) |
97 | 3, 7, 48, 96 | ismeti 22130 |
1
⊢ 𝐷 ∈ (Met‘𝑋) |