Step | Hyp | Ref
| Expression |
1 | | blocni.u |
. . . . . 6
⊢ 𝑈 ∈ NrmCVec |
2 | | blocnilem.1 |
. . . . . . 7
⊢ 𝑋 = (BaseSet‘𝑈) |
3 | | blocni.8 |
. . . . . . 7
⊢ 𝐶 = (IndMet‘𝑈) |
4 | 2, 3 | imsxmet 27547 |
. . . . . 6
⊢ (𝑈 ∈ NrmCVec → 𝐶 ∈ (∞Met‘𝑋)) |
5 | 1, 4 | ax-mp 5 |
. . . . 5
⊢ 𝐶 ∈ (∞Met‘𝑋) |
6 | | blocni.w |
. . . . . 6
⊢ 𝑊 ∈ NrmCVec |
7 | | eqid 2622 |
. . . . . . 7
⊢
(BaseSet‘𝑊) =
(BaseSet‘𝑊) |
8 | | blocni.d |
. . . . . . 7
⊢ 𝐷 = (IndMet‘𝑊) |
9 | 7, 8 | imsxmet 27547 |
. . . . . 6
⊢ (𝑊 ∈ NrmCVec → 𝐷 ∈
(∞Met‘(BaseSet‘𝑊))) |
10 | 6, 9 | ax-mp 5 |
. . . . 5
⊢ 𝐷 ∈
(∞Met‘(BaseSet‘𝑊)) |
11 | | 1rp 11836 |
. . . . . 6
⊢ 1 ∈
ℝ+ |
12 | | blocni.j |
. . . . . . 7
⊢ 𝐽 = (MetOpen‘𝐶) |
13 | | blocni.k |
. . . . . . 7
⊢ 𝐾 = (MetOpen‘𝐷) |
14 | 12, 13 | metcnpi3 22351 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈
(∞Met‘(BaseSet‘𝑊))) ∧ (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 1 ∈ ℝ+))
→ ∃𝑦 ∈
ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) |
15 | 11, 14 | mpanr2 720 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈
(∞Met‘(BaseSet‘𝑊))) ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) |
16 | 5, 10, 15 | mpanl12 718 |
. . . 4
⊢ (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) |
17 | | rpreccl 11857 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
→ (1 / 𝑦) ∈
ℝ+) |
18 | 17 | rpred 11872 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ+
→ (1 / 𝑦) ∈
ℝ) |
19 | 18 | ad2antlr 763 |
. . . . . . 7
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧
∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → (1 / 𝑦) ∈ ℝ) |
20 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢ (
−𝑣 ‘𝑈) = ( −𝑣
‘𝑈) |
21 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢
(normCV‘𝑈) = (normCV‘𝑈) |
22 | 2, 20, 21, 3 | imsdval 27541 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑥𝐶𝑃) = ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃))) |
23 | 1, 22 | mp3an1 1411 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑥𝐶𝑃) = ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃))) |
24 | 23 | breq1d 4663 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑥𝐶𝑃) ≤ 𝑦 ↔ ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦)) |
25 | | blocni.l |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑇 ∈ 𝐿 |
26 | | blocni.4 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐿 = (𝑈 LnOp 𝑊) |
27 | 2, 7, 26 | lnof 27610 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑇:𝑋⟶(BaseSet‘𝑊)) |
28 | 1, 6, 25, 27 | mp3an 1424 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑇:𝑋⟶(BaseSet‘𝑊) |
29 | 28 | ffvelrni 6358 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝑋 → (𝑇‘𝑥) ∈ (BaseSet‘𝑊)) |
30 | 28 | ffvelrni 6358 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ 𝑋 → (𝑇‘𝑃) ∈ (BaseSet‘𝑊)) |
31 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢ (
−𝑣 ‘𝑊) = ( −𝑣
‘𝑊) |
32 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢
(normCV‘𝑊) = (normCV‘𝑊) |
33 | 7, 31, 32, 8 | imsdval 27541 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑇‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇‘𝑃) ∈ (BaseSet‘𝑊)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))) |
34 | 6, 33 | mp3an1 1411 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇‘𝑃) ∈ (BaseSet‘𝑊)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))) |
35 | 29, 30, 34 | syl2an 494 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))) |
36 | 1, 6, 25 | 3pm3.2i 1239 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) |
37 | 2, 20, 31, 26 | lnosub 27614 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋)) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))) |
38 | 36, 37 | mpan 706 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))) |
39 | 38 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))) |
40 | 35, 39 | eqtr4d 2659 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)))) |
41 | 40 | breq1d 4663 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1 ↔
((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) |
42 | 24, 41 | imbi12d 334 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔
(((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1))) |
43 | 42 | ancoms 469 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔
(((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1))) |
44 | 43 | adantlr 751 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔
(((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1))) |
45 | 44 | ralbidva 2985 |
. . . . . . . . 9
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) →
(∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1))) |
46 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (0vec‘𝑈) → (𝑇‘𝑧) = (𝑇‘(0vec‘𝑈))) |
47 | 46 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (0vec‘𝑈) →
((normCV‘𝑊)‘(𝑇‘𝑧)) = ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈)))) |
48 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (0vec‘𝑈) →
((normCV‘𝑈)‘𝑧) = ((normCV‘𝑈)‘(0vec‘𝑈))) |
49 | 48 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (0vec‘𝑈) → ((1 / 𝑦) ·
((normCV‘𝑈)‘𝑧)) = ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈)))) |
50 | 47, 49 | breq12d 4666 |
. . . . . . . . . . . 12
⊢ (𝑧 = (0vec‘𝑈) →
(((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ ((1 / 𝑦) ·
((normCV‘𝑈)‘(0vec‘𝑈))))) |
51 | 1 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑈 ∈ NrmCVec) |
52 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑃 ∈ 𝑋) |
53 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℝ+) |
54 | 2, 21 | nvcl 27516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → ((normCV‘𝑈)‘𝑧) ∈ ℝ) |
55 | 1, 54 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ 𝑋 → ((normCV‘𝑈)‘𝑧) ∈ ℝ) |
56 | 55 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) →
((normCV‘𝑈)‘𝑧) ∈ ℝ) |
57 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(0vec‘𝑈) = (0vec‘𝑈) |
58 | 2, 57, 21 | nvgt0 27529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → (𝑧 ≠ (0vec‘𝑈) ↔ 0 <
((normCV‘𝑈)‘𝑧))) |
59 | 1, 58 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ 𝑋 → (𝑧 ≠ (0vec‘𝑈) ↔ 0 <
((normCV‘𝑈)‘𝑧))) |
60 | 59 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) → 0 <
((normCV‘𝑈)‘𝑧)) |
61 | 56, 60 | elrpd 11869 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) →
((normCV‘𝑈)‘𝑧) ∈
ℝ+) |
62 | | rpdivcl 11856 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℝ+
∧ ((normCV‘𝑈)‘𝑧) ∈ ℝ+) → (𝑦 /
((normCV‘𝑈)‘𝑧)) ∈
ℝ+) |
63 | 53, 61, 62 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈
ℝ+) |
64 | 63 | rpcnd 11874 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ) |
65 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑧 ∈ 𝑋) |
66 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (
·𝑠OLD ‘𝑈) = ( ·𝑠OLD
‘𝑈) |
67 | 2, 66 | nvscl 27481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑦 /
((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋) → ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧) ∈ 𝑋) |
68 | 51, 64, 65, 67 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧) ∈ 𝑋) |
69 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (
+𝑣 ‘𝑈) = ( +𝑣 ‘𝑈) |
70 | 2, 69, 20 | nvpncan2 27508 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧) ∈ 𝑋) → ((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) |
71 | 51, 52, 68, 70 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) |
72 | 71 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = ((normCV‘𝑈)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))) |
73 | 63 | rprege0d 11879 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 /
((normCV‘𝑈)‘𝑧)))) |
74 | 2, 66, 21 | nvsge0 27519 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 ∈ NrmCVec ∧ ((𝑦 /
((normCV‘𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 /
((normCV‘𝑈)‘𝑧))) ∧ 𝑧 ∈ 𝑋) → ((normCV‘𝑈)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑈)‘𝑧))) |
75 | 51, 73, 65, 74 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑈)‘𝑧))) |
76 | | rpcn 11841 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℂ) |
77 | 76 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ∈ ℂ) |
78 | 55 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘𝑧) ∈ ℝ) |
79 | 78 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘𝑧) ∈ ℂ) |
80 | 2, 57, 21 | nvz 27524 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → (((normCV‘𝑈)‘𝑧) = 0 ↔ 𝑧 = (0vec‘𝑈))) |
81 | 1, 80 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈ 𝑋 → (((normCV‘𝑈)‘𝑧) = 0 ↔ 𝑧 = (0vec‘𝑈))) |
82 | 81 | necon3bid 2838 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ 𝑋 → (((normCV‘𝑈)‘𝑧) ≠ 0 ↔ 𝑧 ≠ (0vec‘𝑈))) |
83 | 82 | biimpar 502 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) →
((normCV‘𝑈)‘𝑧) ≠ 0) |
84 | 83 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘𝑧) ≠ 0) |
85 | 77, 79, 84 | divcan1d 10802 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑈)‘𝑧)) = 𝑦) |
86 | 72, 75, 85 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = 𝑦) |
87 | | rpre 11839 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ) |
88 | 87 | leidd 10594 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ≤ 𝑦) |
89 | 88 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ≤ 𝑦) |
90 | 86, 89 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦) |
91 | 2, 69 | nvgcl 27475 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧) ∈ 𝑋) → (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) ∈ 𝑋) |
92 | 51, 52, 68, 91 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) ∈ 𝑋) |
93 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → (𝑥( −𝑣 ‘𝑈)𝑃) = ((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) |
94 | 93 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) |
95 | 94 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 ↔ ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦)) |
96 | 93 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) |
97 | 96 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)))) |
98 | 97 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → (((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1 ↔
((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1)) |
99 | 95, 98 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → ((((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) ↔
(((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1))) |
100 | 99 | rspcv 3305 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃( +𝑣
‘𝑈)((𝑦 /
((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) →
(((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1))) |
101 | 92, 100 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) →
(((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1))) |
102 | 90, 101 | mpid 44 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) →
((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1)) |
103 | 28 | ffvelrni 6358 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ 𝑋 → (𝑇‘𝑧) ∈ (BaseSet‘𝑊)) |
104 | 7, 32 | nvcl 27516 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑇‘𝑧) ∈ (BaseSet‘𝑊)) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ) |
105 | 6, 103, 104 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑋 → ((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ) |
106 | 105 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ) |
107 | | 1red 10055 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 1 ∈
ℝ) |
108 | 106, 107,
63 | lemuldiv2d 11922 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))) ≤ 1 ↔
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))))) |
109 | 71 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))) |
110 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (
·𝑠OLD ‘𝑊) = ( ·𝑠OLD
‘𝑊) |
111 | 2, 66, 110, 26 | lnomul 27615 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋)) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧))) |
112 | 36, 111 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑦 /
((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧))) |
113 | 64, 65, 112 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧))) |
114 | 109, 113 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧))) |
115 | 114 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧)))) |
116 | 6 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑊 ∈ NrmCVec) |
117 | 103 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘𝑧) ∈ (BaseSet‘𝑊)) |
118 | 7, 110, 32 | nvsge0 27519 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ NrmCVec ∧ ((𝑦 /
((normCV‘𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 /
((normCV‘𝑈)‘𝑧))) ∧ (𝑇‘𝑧) ∈ (BaseSet‘𝑊)) → ((normCV‘𝑊)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧))) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧)))) |
119 | 116, 73, 117, 118 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑊)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧))) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧)))) |
120 | 115, 119 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧)))) |
121 | 120 | breq1d 4663 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
(((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1 ↔ ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))) ≤ 1)) |
122 | | rpcnne0 11850 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℝ+
→ (𝑦 ∈ ℂ
∧ 𝑦 ≠
0)) |
123 | | rpcnne0 11850 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((normCV‘𝑈)‘𝑧) ∈ ℝ+ →
(((normCV‘𝑈)‘𝑧) ∈ ℂ ∧
((normCV‘𝑈)‘𝑧) ≠ 0)) |
124 | | recdiv 10731 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) ∧
(((normCV‘𝑈)‘𝑧) ∈ ℂ ∧
((normCV‘𝑈)‘𝑧) ≠ 0)) → (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))) = (((normCV‘𝑈)‘𝑧) / 𝑦)) |
125 | 122, 123,
124 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ ℝ+
∧ ((normCV‘𝑈)‘𝑧) ∈ ℝ+) → (1 /
(𝑦 /
((normCV‘𝑈)‘𝑧))) = (((normCV‘𝑈)‘𝑧) / 𝑦)) |
126 | 53, 61, 125 | syl2an 494 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (1 / (𝑦 /
((normCV‘𝑈)‘𝑧))) = (((normCV‘𝑈)‘𝑧) / 𝑦)) |
127 | | rpne0 11848 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ≠
0) |
128 | 127 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ≠ 0) |
129 | 79, 77, 128 | divrec2d 10805 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
(((normCV‘𝑈)‘𝑧) / 𝑦) = ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) |
130 | 126, 129 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((1 / 𝑦) ·
((normCV‘𝑈)‘𝑧)) = (1 / (𝑦 / ((normCV‘𝑈)‘𝑧)))) |
131 | 130 | breq2d 4665 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
(((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))))) |
132 | 108, 121,
131 | 3bitr4d 300 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
(((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1 ↔
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) |
133 | 102, 132 | sylibd 229 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) |
134 | 133 | anassrs 680 |
. . . . . . . . . . . . . 14
⊢ ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 ≠ (0vec‘𝑈)) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) |
135 | 134 | imp 445 |
. . . . . . . . . . . . 13
⊢
(((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 ≠ (0vec‘𝑈)) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) |
136 | 135 | an32s 846 |
. . . . . . . . . . . 12
⊢
(((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) ∧ 𝑧 ≠ (0vec‘𝑈)) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) |
137 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢
(0vec‘𝑊) = (0vec‘𝑊) |
138 | 2, 7, 57, 137, 26 | lno0 27611 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → (𝑇‘(0vec‘𝑈)) =
(0vec‘𝑊)) |
139 | 1, 6, 25, 138 | mp3an 1424 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑇‘(0vec‘𝑈)) =
(0vec‘𝑊) |
140 | 139 | fveq2i 6194 |
. . . . . . . . . . . . . . . 16
⊢
((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) =
((normCV‘𝑊)‘(0vec‘𝑊)) |
141 | 137, 32 | nvz0 27523 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ NrmCVec →
((normCV‘𝑊)‘(0vec‘𝑊)) = 0) |
142 | 6, 141 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
((normCV‘𝑊)‘(0vec‘𝑊)) = 0 |
143 | 140, 142 | eqtri 2644 |
. . . . . . . . . . . . . . 15
⊢
((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) = 0 |
144 | | 0le0 11110 |
. . . . . . . . . . . . . . 15
⊢ 0 ≤
0 |
145 | 143, 144 | eqbrtri 4674 |
. . . . . . . . . . . . . 14
⊢
((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ 0 |
146 | 17 | rpcnd 11874 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ+
→ (1 / 𝑦) ∈
ℂ) |
147 | 57, 21 | nvz0 27523 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑈 ∈ NrmCVec →
((normCV‘𝑈)‘(0vec‘𝑈)) = 0) |
148 | 1, 147 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
((normCV‘𝑈)‘(0vec‘𝑈)) = 0 |
149 | 148 | oveq2i 6661 |
. . . . . . . . . . . . . . . 16
⊢ ((1 /
𝑦) ·
((normCV‘𝑈)‘(0vec‘𝑈))) = ((1 / 𝑦) · 0) |
150 | | mul01 10215 |
. . . . . . . . . . . . . . . 16
⊢ ((1 /
𝑦) ∈ ℂ →
((1 / 𝑦) · 0) =
0) |
151 | 149, 150 | syl5eq 2668 |
. . . . . . . . . . . . . . 15
⊢ ((1 /
𝑦) ∈ ℂ →
((1 / 𝑦) ·
((normCV‘𝑈)‘(0vec‘𝑈))) = 0) |
152 | 146, 151 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ+
→ ((1 / 𝑦) ·
((normCV‘𝑈)‘(0vec‘𝑈))) = 0) |
153 | 145, 152 | syl5breqr 4691 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ+
→ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ ((1 / 𝑦) ·
((normCV‘𝑈)‘(0vec‘𝑈)))) |
154 | 153 | ad3antlr 767 |
. . . . . . . . . . . 12
⊢ ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) →
((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ ((1 / 𝑦) ·
((normCV‘𝑈)‘(0vec‘𝑈)))) |
155 | 50, 136, 154 | pm2.61ne 2879 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) |
156 | 155 | ex 450 |
. . . . . . . . . 10
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) |
157 | 156 | ralrimdva 2969 |
. . . . . . . . 9
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) →
(∀𝑥 ∈ 𝑋
(((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) → ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) |
158 | 45, 157 | sylbid 230 |
. . . . . . . 8
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) →
(∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) → ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) |
159 | 158 | imp 445 |
. . . . . . 7
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧
∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) |
160 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑥 = (1 / 𝑦) → (𝑥 · ((normCV‘𝑈)‘𝑧)) = ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) |
161 | 160 | breq2d 4665 |
. . . . . . . . 9
⊢ (𝑥 = (1 / 𝑦) → (((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) |
162 | 161 | ralbidv 2986 |
. . . . . . . 8
⊢ (𝑥 = (1 / 𝑦) → (∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)) ↔ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) |
163 | 162 | rspcev 3309 |
. . . . . . 7
⊢ (((1 /
𝑦) ∈ ℝ ∧
∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))) |
164 | 19, 159, 163 | syl2anc 693 |
. . . . . 6
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧
∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))) |
165 | 164 | ex 450 |
. . . . 5
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) →
(∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))) |
166 | 165 | rexlimdva 3031 |
. . . 4
⊢ (𝑃 ∈ 𝑋 → (∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))) |
167 | 16, 166 | syl5 34 |
. . 3
⊢ (𝑃 ∈ 𝑋 → (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))) |
168 | 167 | imp 445 |
. 2
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))) |
169 | | blocni.5 |
. . . 4
⊢ 𝐵 = (𝑈 BLnOp 𝑊) |
170 | 2, 21, 32, 26, 169, 1, 6 | isblo3i 27656 |
. . 3
⊢ (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))) |
171 | 25, 170 | mpbiran 953 |
. 2
⊢ (𝑇 ∈ 𝐵 ↔ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))) |
172 | 168, 171 | sylibr 224 |
1
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑇 ∈ 𝐵) |