Step | Hyp | Ref
| Expression |
1 | | blocni.u |
. . . . . 6
⊢ 𝑈 ∈ NrmCVec |
2 | | blocnilem.1 |
. . . . . . 7
⊢ 𝑋 = (BaseSet‘𝑈) |
3 | | blocni.8 |
. . . . . . 7
⊢ 𝐶 = (IndMet‘𝑈) |
4 | 2, 3 | imsxmet 27886 |
. . . . . 6
⊢ (𝑈 ∈ NrmCVec → 𝐶 ∈ (∞Met‘𝑋)) |
5 | 1, 4 | ax-mp 5 |
. . . . 5
⊢ 𝐶 ∈ (∞Met‘𝑋) |
6 | | blocni.w |
. . . . . 6
⊢ 𝑊 ∈ NrmCVec |
7 | | eqid 2771 |
. . . . . . 7
⊢
(BaseSet‘𝑊) =
(BaseSet‘𝑊) |
8 | | blocni.d |
. . . . . . 7
⊢ 𝐷 = (IndMet‘𝑊) |
9 | 7, 8 | imsxmet 27886 |
. . . . . 6
⊢ (𝑊 ∈ NrmCVec → 𝐷 ∈
(∞Met‘(BaseSet‘𝑊))) |
10 | 6, 9 | ax-mp 5 |
. . . . 5
⊢ 𝐷 ∈
(∞Met‘(BaseSet‘𝑊)) |
11 | | 1rp 12038 |
. . . . . 6
⊢ 1 ∈
ℝ+ |
12 | | blocni.j |
. . . . . . 7
⊢ 𝐽 = (MetOpen‘𝐶) |
13 | | blocni.k |
. . . . . . 7
⊢ 𝐾 = (MetOpen‘𝐷) |
14 | 12, 13 | metcnpi3 22570 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈
(∞Met‘(BaseSet‘𝑊))) ∧ (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 1 ∈ ℝ+))
→ ∃𝑦 ∈
ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) |
15 | 11, 14 | mpanr2 684 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈
(∞Met‘(BaseSet‘𝑊))) ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) |
16 | 5, 10, 15 | mpanl12 682 |
. . . 4
⊢ (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) |
17 | | rpreccl 12059 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
→ (1 / 𝑦) ∈
ℝ+) |
18 | 17 | rpred 12074 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ+
→ (1 / 𝑦) ∈
ℝ) |
19 | 18 | ad2antlr 706 |
. . . . . . 7
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧
∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → (1 / 𝑦) ∈ ℝ) |
20 | | eqid 2771 |
. . . . . . . . . . . . . . . 16
⊢ (
−𝑣 ‘𝑈) = ( −𝑣
‘𝑈) |
21 | | eqid 2771 |
. . . . . . . . . . . . . . . 16
⊢
(normCV‘𝑈) = (normCV‘𝑈) |
22 | 2, 20, 21, 3 | imsdval 27880 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑥𝐶𝑃) = ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃))) |
23 | 1, 22 | mp3an1 1559 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑥𝐶𝑃) = ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃))) |
24 | 23 | breq1d 4797 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑥𝐶𝑃) ≤ 𝑦 ↔ ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦)) |
25 | | blocni.l |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑇 ∈ 𝐿 |
26 | | blocni.4 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐿 = (𝑈 LnOp 𝑊) |
27 | 2, 7, 26 | lnof 27949 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑇:𝑋⟶(BaseSet‘𝑊)) |
28 | 1, 6, 25, 27 | mp3an 1572 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑇:𝑋⟶(BaseSet‘𝑊) |
29 | 28 | ffvelrni 6503 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝑋 → (𝑇‘𝑥) ∈ (BaseSet‘𝑊)) |
30 | 28 | ffvelrni 6503 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ 𝑋 → (𝑇‘𝑃) ∈ (BaseSet‘𝑊)) |
31 | | eqid 2771 |
. . . . . . . . . . . . . . . . . 18
⊢ (
−𝑣 ‘𝑊) = ( −𝑣
‘𝑊) |
32 | | eqid 2771 |
. . . . . . . . . . . . . . . . . 18
⊢
(normCV‘𝑊) = (normCV‘𝑊) |
33 | 7, 31, 32, 8 | imsdval 27880 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑇‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇‘𝑃) ∈ (BaseSet‘𝑊)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))) |
34 | 6, 33 | mp3an1 1559 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇‘𝑃) ∈ (BaseSet‘𝑊)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))) |
35 | 29, 30, 34 | syl2an 583 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))) |
36 | 1, 6, 25 | 3pm3.2i 1423 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) |
37 | 2, 20, 31, 26 | lnosub 27953 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋)) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))) |
38 | 36, 37 | mpan 670 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))) |
39 | 38 | fveq2d 6337 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))) |
40 | 35, 39 | eqtr4d 2808 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)))) |
41 | 40 | breq1d 4797 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1 ↔
((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) |
42 | 24, 41 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔
(((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1))) |
43 | 42 | ancoms 446 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔
(((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1))) |
44 | 43 | adantlr 694 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔
(((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1))) |
45 | 44 | ralbidva 3134 |
. . . . . . . . 9
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) →
(∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1))) |
46 | | fveq2 6333 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (0vec‘𝑈) → (𝑇‘𝑧) = (𝑇‘(0vec‘𝑈))) |
47 | 46 | fveq2d 6337 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (0vec‘𝑈) →
((normCV‘𝑊)‘(𝑇‘𝑧)) = ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈)))) |
48 | | fveq2 6333 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (0vec‘𝑈) →
((normCV‘𝑈)‘𝑧) = ((normCV‘𝑈)‘(0vec‘𝑈))) |
49 | 48 | oveq2d 6811 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (0vec‘𝑈) → ((1 / 𝑦) ·
((normCV‘𝑈)‘𝑧)) = ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈)))) |
50 | 47, 49 | breq12d 4800 |
. . . . . . . . . . . 12
⊢ (𝑧 = (0vec‘𝑈) →
(((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ ((1 / 𝑦) ·
((normCV‘𝑈)‘(0vec‘𝑈))))) |
51 | 1 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑈 ∈ NrmCVec) |
52 | | simpll 750 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑃 ∈ 𝑋) |
53 | | simpr 471 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℝ+) |
54 | 2, 21 | nvcl 27855 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → ((normCV‘𝑈)‘𝑧) ∈ ℝ) |
55 | 1, 54 | mpan 670 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ 𝑋 → ((normCV‘𝑈)‘𝑧) ∈ ℝ) |
56 | 55 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) →
((normCV‘𝑈)‘𝑧) ∈ ℝ) |
57 | | eqid 2771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(0vec‘𝑈) = (0vec‘𝑈) |
58 | 2, 57, 21 | nvgt0 27868 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → (𝑧 ≠ (0vec‘𝑈) ↔ 0 <
((normCV‘𝑈)‘𝑧))) |
59 | 1, 58 | mpan 670 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ 𝑋 → (𝑧 ≠ (0vec‘𝑈) ↔ 0 <
((normCV‘𝑈)‘𝑧))) |
60 | 59 | biimpa 462 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) → 0 <
((normCV‘𝑈)‘𝑧)) |
61 | 56, 60 | elrpd 12071 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) →
((normCV‘𝑈)‘𝑧) ∈
ℝ+) |
62 | | rpdivcl 12058 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℝ+
∧ ((normCV‘𝑈)‘𝑧) ∈ ℝ+) → (𝑦 /
((normCV‘𝑈)‘𝑧)) ∈
ℝ+) |
63 | 53, 61, 62 | syl2an 583 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈
ℝ+) |
64 | 63 | rpcnd 12076 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ) |
65 | | simprl 754 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑧 ∈ 𝑋) |
66 | | eqid 2771 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (
·𝑠OLD ‘𝑈) = ( ·𝑠OLD
‘𝑈) |
67 | 2, 66 | nvscl 27820 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑦 /
((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋) → ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧) ∈ 𝑋) |
68 | 51, 64, 65, 67 | syl3anc 1476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧) ∈ 𝑋) |
69 | | eqid 2771 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (
+𝑣 ‘𝑈) = ( +𝑣 ‘𝑈) |
70 | 2, 69, 20 | nvpncan2 27847 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧) ∈ 𝑋) → ((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) |
71 | 51, 52, 68, 70 | syl3anc 1476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) |
72 | 71 | fveq2d 6337 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = ((normCV‘𝑈)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))) |
73 | 63 | rprege0d 12081 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 /
((normCV‘𝑈)‘𝑧)))) |
74 | 2, 66, 21 | nvsge0 27858 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 ∈ NrmCVec ∧ ((𝑦 /
((normCV‘𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 /
((normCV‘𝑈)‘𝑧))) ∧ 𝑧 ∈ 𝑋) → ((normCV‘𝑈)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑈)‘𝑧))) |
75 | 51, 73, 65, 74 | syl3anc 1476 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑈)‘𝑧))) |
76 | | rpcn 12043 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℂ) |
77 | 76 | ad2antlr 706 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ∈ ℂ) |
78 | 55 | ad2antrl 707 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘𝑧) ∈ ℝ) |
79 | 78 | recnd 10273 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘𝑧) ∈ ℂ) |
80 | 2, 57, 21 | nvz 27863 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → (((normCV‘𝑈)‘𝑧) = 0 ↔ 𝑧 = (0vec‘𝑈))) |
81 | 1, 80 | mpan 670 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈ 𝑋 → (((normCV‘𝑈)‘𝑧) = 0 ↔ 𝑧 = (0vec‘𝑈))) |
82 | 81 | necon3bid 2987 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ 𝑋 → (((normCV‘𝑈)‘𝑧) ≠ 0 ↔ 𝑧 ≠ (0vec‘𝑈))) |
83 | 82 | biimpar 463 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) →
((normCV‘𝑈)‘𝑧) ≠ 0) |
84 | 83 | adantl 467 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘𝑧) ≠ 0) |
85 | 77, 79, 84 | divcan1d 11007 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑈)‘𝑧)) = 𝑦) |
86 | 72, 75, 85 | 3eqtrd 2809 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = 𝑦) |
87 | | rpre 12041 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ) |
88 | 87 | leidd 10799 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ≤ 𝑦) |
89 | 88 | ad2antlr 706 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ≤ 𝑦) |
90 | 86, 89 | eqbrtrd 4809 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦) |
91 | 2, 69 | nvgcl 27814 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧) ∈ 𝑋) → (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) ∈ 𝑋) |
92 | 51, 52, 68, 91 | syl3anc 1476 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) ∈ 𝑋) |
93 | | fvoveq1 6818 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) |
94 | 93 | breq1d 4797 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 ↔ ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦)) |
95 | | fvoveq1 6818 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) |
96 | 95 | fveq2d 6337 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)))) |
97 | 96 | breq1d 4797 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → (((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1 ↔
((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1)) |
98 | 94, 97 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → ((((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) ↔
(((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1))) |
99 | 98 | rspcv 3456 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃( +𝑣
‘𝑈)((𝑦 /
((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) →
(((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1))) |
100 | 92, 99 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) →
(((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1))) |
101 | 90, 100 | mpid 44 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) →
((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1)) |
102 | 28 | ffvelrni 6503 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ 𝑋 → (𝑇‘𝑧) ∈ (BaseSet‘𝑊)) |
103 | 7, 32 | nvcl 27855 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑇‘𝑧) ∈ (BaseSet‘𝑊)) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ) |
104 | 6, 102, 103 | sylancr 575 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑋 → ((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ) |
105 | 104 | ad2antrl 707 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ) |
106 | | 1red 10260 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 1 ∈
ℝ) |
107 | 105, 106,
63 | lemuldiv2d 12124 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))) ≤ 1 ↔
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))))) |
108 | 71 | fveq2d 6337 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))) |
109 | | eqid 2771 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (
·𝑠OLD ‘𝑊) = ( ·𝑠OLD
‘𝑊) |
110 | 2, 66, 109, 26 | lnomul 27954 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋)) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧))) |
111 | 36, 110 | mpan 670 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑦 /
((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧))) |
112 | 64, 65, 111 | syl2anc 573 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧))) |
113 | 108, 112 | eqtrd 2805 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧))) |
114 | 113 | fveq2d 6337 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧)))) |
115 | 6 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑊 ∈ NrmCVec) |
116 | 102 | ad2antrl 707 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘𝑧) ∈ (BaseSet‘𝑊)) |
117 | 7, 109, 32 | nvsge0 27858 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ NrmCVec ∧ ((𝑦 /
((normCV‘𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 /
((normCV‘𝑈)‘𝑧))) ∧ (𝑇‘𝑧) ∈ (BaseSet‘𝑊)) → ((normCV‘𝑊)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧))) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧)))) |
118 | 115, 73, 116, 117 | syl3anc 1476 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑊)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧))) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧)))) |
119 | 114, 118 | eqtrd 2805 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧)))) |
120 | 119 | breq1d 4797 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
(((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1 ↔ ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))) ≤ 1)) |
121 | | rpcnne0 12052 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℝ+
→ (𝑦 ∈ ℂ
∧ 𝑦 ≠
0)) |
122 | | rpcnne0 12052 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((normCV‘𝑈)‘𝑧) ∈ ℝ+ →
(((normCV‘𝑈)‘𝑧) ∈ ℂ ∧
((normCV‘𝑈)‘𝑧) ≠ 0)) |
123 | | recdiv 10936 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) ∧
(((normCV‘𝑈)‘𝑧) ∈ ℂ ∧
((normCV‘𝑈)‘𝑧) ≠ 0)) → (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))) = (((normCV‘𝑈)‘𝑧) / 𝑦)) |
124 | 121, 122,
123 | syl2an 583 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ+
∧ ((normCV‘𝑈)‘𝑧) ∈ ℝ+) → (1 /
(𝑦 /
((normCV‘𝑈)‘𝑧))) = (((normCV‘𝑈)‘𝑧) / 𝑦)) |
125 | 53, 61, 124 | syl2an 583 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (1 / (𝑦 /
((normCV‘𝑈)‘𝑧))) = (((normCV‘𝑈)‘𝑧) / 𝑦)) |
126 | | rpne0 12050 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ≠
0) |
127 | 126 | ad2antlr 706 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ≠ 0) |
128 | 79, 77, 127 | divrec2d 11010 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
(((normCV‘𝑈)‘𝑧) / 𝑦) = ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) |
129 | 125, 128 | eqtr2d 2806 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((1 / 𝑦) ·
((normCV‘𝑈)‘𝑧)) = (1 / (𝑦 / ((normCV‘𝑈)‘𝑧)))) |
130 | 129 | breq2d 4799 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
(((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))))) |
131 | 107, 120,
130 | 3bitr4d 300 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
(((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1 ↔
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) |
132 | 101, 131 | sylibd 229 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) |
133 | 132 | anassrs 453 |
. . . . . . . . . . . . . 14
⊢ ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 ≠ (0vec‘𝑈)) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) |
134 | 133 | imp 393 |
. . . . . . . . . . . . 13
⊢
(((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 ≠ (0vec‘𝑈)) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) |
135 | 134 | an32s 631 |
. . . . . . . . . . . 12
⊢
(((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) ∧ 𝑧 ≠ (0vec‘𝑈)) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) |
136 | | eqid 2771 |
. . . . . . . . . . . . . . . . . . 19
⊢
(0vec‘𝑊) = (0vec‘𝑊) |
137 | 2, 7, 57, 136, 26 | lno0 27950 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → (𝑇‘(0vec‘𝑈)) =
(0vec‘𝑊)) |
138 | 1, 6, 25, 137 | mp3an 1572 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑇‘(0vec‘𝑈)) =
(0vec‘𝑊) |
139 | 138 | fveq2i 6336 |
. . . . . . . . . . . . . . . 16
⊢
((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) =
((normCV‘𝑊)‘(0vec‘𝑊)) |
140 | 136, 32 | nvz0 27862 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ NrmCVec →
((normCV‘𝑊)‘(0vec‘𝑊)) = 0) |
141 | 6, 140 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
((normCV‘𝑊)‘(0vec‘𝑊)) = 0 |
142 | 139, 141 | eqtri 2793 |
. . . . . . . . . . . . . . 15
⊢
((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) = 0 |
143 | | 0le0 11315 |
. . . . . . . . . . . . . . 15
⊢ 0 ≤
0 |
144 | 142, 143 | eqbrtri 4808 |
. . . . . . . . . . . . . 14
⊢
((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ 0 |
145 | 17 | rpcnd 12076 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ+
→ (1 / 𝑦) ∈
ℂ) |
146 | 57, 21 | nvz0 27862 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈 ∈ NrmCVec →
((normCV‘𝑈)‘(0vec‘𝑈)) = 0) |
147 | 1, 146 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
((normCV‘𝑈)‘(0vec‘𝑈)) = 0 |
148 | 147 | oveq2i 6806 |
. . . . . . . . . . . . . . . 16
⊢ ((1 /
𝑦) ·
((normCV‘𝑈)‘(0vec‘𝑈))) = ((1 / 𝑦) · 0) |
149 | | mul01 10420 |
. . . . . . . . . . . . . . . 16
⊢ ((1 /
𝑦) ∈ ℂ →
((1 / 𝑦) · 0) =
0) |
150 | 148, 149 | syl5eq 2817 |
. . . . . . . . . . . . . . 15
⊢ ((1 /
𝑦) ∈ ℂ →
((1 / 𝑦) ·
((normCV‘𝑈)‘(0vec‘𝑈))) = 0) |
151 | 145, 150 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ+
→ ((1 / 𝑦) ·
((normCV‘𝑈)‘(0vec‘𝑈))) = 0) |
152 | 144, 151 | syl5breqr 4825 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ+
→ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ ((1 / 𝑦) ·
((normCV‘𝑈)‘(0vec‘𝑈)))) |
153 | 152 | ad3antlr 710 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) →
((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ ((1 / 𝑦) ·
((normCV‘𝑈)‘(0vec‘𝑈)))) |
154 | 50, 135, 153 | pm2.61ne 3028 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) |
155 | 154 | ex 397 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) |
156 | 155 | ralrimdva 3118 |
. . . . . . . . 9
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) →
(∀𝑥 ∈ 𝑋
(((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) → ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) |
157 | 45, 156 | sylbid 230 |
. . . . . . . 8
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) →
(∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) → ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) |
158 | 157 | imp 393 |
. . . . . . 7
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧
∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) |
159 | | oveq1 6802 |
. . . . . . . . . 10
⊢ (𝑥 = (1 / 𝑦) → (𝑥 · ((normCV‘𝑈)‘𝑧)) = ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) |
160 | 159 | breq2d 4799 |
. . . . . . . . 9
⊢ (𝑥 = (1 / 𝑦) → (((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) |
161 | 160 | ralbidv 3135 |
. . . . . . . 8
⊢ (𝑥 = (1 / 𝑦) → (∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)) ↔ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) |
162 | 161 | rspcev 3460 |
. . . . . . 7
⊢ (((1 /
𝑦) ∈ ℝ ∧
∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))) |
163 | 19, 158, 162 | syl2anc 573 |
. . . . . 6
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧
∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))) |
164 | 163 | ex 397 |
. . . . 5
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) →
(∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))) |
165 | 164 | rexlimdva 3179 |
. . . 4
⊢ (𝑃 ∈ 𝑋 → (∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))) |
166 | 16, 165 | syl5 34 |
. . 3
⊢ (𝑃 ∈ 𝑋 → (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))) |
167 | 166 | imp 393 |
. 2
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))) |
168 | | blocni.5 |
. . . 4
⊢ 𝐵 = (𝑈 BLnOp 𝑊) |
169 | 2, 21, 32, 26, 168, 1, 6 | isblo3i 27995 |
. . 3
⊢ (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))) |
170 | 25, 169 | mpbiran 688 |
. 2
⊢ (𝑇 ∈ 𝐵 ↔ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))) |
171 | 167, 170 | sylibr 224 |
1
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑇 ∈ 𝐵) |