Step | Hyp | Ref
| Expression |
1 | | blocni.u |
. . . . . 6
⊢ 𝑈 ∈ NrmCVec |
2 | | blocnilem.1 |
. . . . . . 7
⊢ 𝑋 = (BaseSet‘𝑈) |
3 | | blocni.8 |
. . . . . . 7
⊢ 𝐶 = (IndMet‘𝑈) |
4 | 2, 3 | imsxmet 28619 |
. . . . . 6
⊢ (𝑈 ∈ NrmCVec → 𝐶 ∈ (∞Met‘𝑋)) |
5 | 1, 4 | ax-mp 5 |
. . . . 5
⊢ 𝐶 ∈ (∞Met‘𝑋) |
6 | | blocni.w |
. . . . . 6
⊢ 𝑊 ∈ NrmCVec |
7 | | eqid 2738 |
. . . . . . 7
⊢
(BaseSet‘𝑊) =
(BaseSet‘𝑊) |
8 | | blocni.d |
. . . . . . 7
⊢ 𝐷 = (IndMet‘𝑊) |
9 | 7, 8 | imsxmet 28619 |
. . . . . 6
⊢ (𝑊 ∈ NrmCVec → 𝐷 ∈
(∞Met‘(BaseSet‘𝑊))) |
10 | 6, 9 | ax-mp 5 |
. . . . 5
⊢ 𝐷 ∈
(∞Met‘(BaseSet‘𝑊)) |
11 | | 1rp 12469 |
. . . . . 6
⊢ 1 ∈
ℝ+ |
12 | | blocni.j |
. . . . . . 7
⊢ 𝐽 = (MetOpen‘𝐶) |
13 | | blocni.k |
. . . . . . 7
⊢ 𝐾 = (MetOpen‘𝐷) |
14 | 12, 13 | metcnpi3 23292 |
. . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈
(∞Met‘(BaseSet‘𝑊))) ∧ (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 1 ∈ ℝ+))
→ ∃𝑦 ∈
ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) |
15 | 11, 14 | mpanr2 704 |
. . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈
(∞Met‘(BaseSet‘𝑊))) ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) |
16 | 5, 10, 15 | mpanl12 702 |
. . . 4
⊢ (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) |
17 | | rpreccl 12491 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ+
→ (1 / 𝑦) ∈
ℝ+) |
18 | 17 | rpred 12507 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ+
→ (1 / 𝑦) ∈
ℝ) |
19 | 18 | ad2antlr 727 |
. . . . . 6
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧
∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → (1 / 𝑦) ∈ ℝ) |
20 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢ (
−𝑣 ‘𝑈) = ( −𝑣
‘𝑈) |
21 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢
(normCV‘𝑈) = (normCV‘𝑈) |
22 | 2, 20, 21, 3 | imsdval 28613 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑥𝐶𝑃) = ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃))) |
23 | 1, 22 | mp3an1 1449 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑥𝐶𝑃) = ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃))) |
24 | 23 | breq1d 5037 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑥𝐶𝑃) ≤ 𝑦 ↔ ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦)) |
25 | | blocni.l |
. . . . . . . . . . . . . . . . 17
⊢ 𝑇 ∈ 𝐿 |
26 | | blocni.4 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐿 = (𝑈 LnOp 𝑊) |
27 | 2, 7, 26 | lnof 28682 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑇:𝑋⟶(BaseSet‘𝑊)) |
28 | 1, 6, 25, 27 | mp3an 1462 |
. . . . . . . . . . . . . . . 16
⊢ 𝑇:𝑋⟶(BaseSet‘𝑊) |
29 | 28 | ffvelrni 6854 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑋 → (𝑇‘𝑥) ∈ (BaseSet‘𝑊)) |
30 | 28 | ffvelrni 6854 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ 𝑋 → (𝑇‘𝑃) ∈ (BaseSet‘𝑊)) |
31 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢ (
−𝑣 ‘𝑊) = ( −𝑣
‘𝑊) |
32 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢
(normCV‘𝑊) = (normCV‘𝑊) |
33 | 7, 31, 32, 8 | imsdval 28613 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑇‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇‘𝑃) ∈ (BaseSet‘𝑊)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))) |
34 | 6, 33 | mp3an1 1449 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇‘𝑃) ∈ (BaseSet‘𝑊)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))) |
35 | 29, 30, 34 | syl2an 599 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))) |
36 | 1, 6, 25 | 3pm3.2i 1340 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) |
37 | 2, 20, 31, 26 | lnosub 28686 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋)) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))) |
38 | 36, 37 | mpan 690 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))) |
39 | 38 | fveq2d 6672 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))) |
40 | 35, 39 | eqtr4d 2776 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)))) |
41 | 40 | breq1d 5037 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1 ↔
((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) |
42 | 24, 41 | imbi12d 348 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔
(((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1))) |
43 | 42 | ancoms 462 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔
(((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1))) |
44 | 43 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔
(((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1))) |
45 | 44 | ralbidva 3108 |
. . . . . . . 8
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) →
(∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1))) |
46 | | 2fveq3 6673 |
. . . . . . . . . . . 12
⊢ (𝑧 = (0vec‘𝑈) →
((normCV‘𝑊)‘(𝑇‘𝑧)) = ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈)))) |
47 | | fveq2 6668 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (0vec‘𝑈) →
((normCV‘𝑈)‘𝑧) = ((normCV‘𝑈)‘(0vec‘𝑈))) |
48 | 47 | oveq2d 7180 |
. . . . . . . . . . . 12
⊢ (𝑧 = (0vec‘𝑈) → ((1 / 𝑦) ·
((normCV‘𝑈)‘𝑧)) = ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈)))) |
49 | 46, 48 | breq12d 5040 |
. . . . . . . . . . 11
⊢ (𝑧 = (0vec‘𝑈) →
(((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ ((1 / 𝑦) ·
((normCV‘𝑈)‘(0vec‘𝑈))))) |
50 | 1 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑈 ∈ NrmCVec) |
51 | | simpll 767 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑃 ∈ 𝑋) |
52 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℝ+) |
53 | 2, 21 | nvcl 28588 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → ((normCV‘𝑈)‘𝑧) ∈ ℝ) |
54 | 1, 53 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 ∈ 𝑋 → ((normCV‘𝑈)‘𝑧) ∈ ℝ) |
55 | 54 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) →
((normCV‘𝑈)‘𝑧) ∈ ℝ) |
56 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(0vec‘𝑈) = (0vec‘𝑈) |
57 | 2, 56, 21 | nvgt0 28601 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → (𝑧 ≠ (0vec‘𝑈) ↔ 0 <
((normCV‘𝑈)‘𝑧))) |
58 | 1, 57 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 ∈ 𝑋 → (𝑧 ≠ (0vec‘𝑈) ↔ 0 <
((normCV‘𝑈)‘𝑧))) |
59 | 58 | biimpa 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) → 0 <
((normCV‘𝑈)‘𝑧)) |
60 | 55, 59 | elrpd 12504 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) →
((normCV‘𝑈)‘𝑧) ∈
ℝ+) |
61 | | rpdivcl 12490 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℝ+
∧ ((normCV‘𝑈)‘𝑧) ∈ ℝ+) → (𝑦 /
((normCV‘𝑈)‘𝑧)) ∈
ℝ+) |
62 | 52, 60, 61 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈
ℝ+) |
63 | 62 | rpcnd 12509 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ) |
64 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑧 ∈ 𝑋) |
65 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (
·𝑠OLD ‘𝑈) = ( ·𝑠OLD
‘𝑈) |
66 | 2, 65 | nvscl 28553 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑦 /
((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋) → ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧) ∈ 𝑋) |
67 | 50, 63, 64, 66 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧) ∈ 𝑋) |
68 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (
+𝑣 ‘𝑈) = ( +𝑣 ‘𝑈) |
69 | 2, 68, 20 | nvpncan2 28580 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧) ∈ 𝑋) → ((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) |
70 | 50, 51, 67, 69 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) |
71 | 70 | fveq2d 6672 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = ((normCV‘𝑈)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))) |
72 | 62 | rprege0d 12514 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 /
((normCV‘𝑈)‘𝑧)))) |
73 | 2, 65, 21 | nvsge0 28591 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∈ NrmCVec ∧ ((𝑦 /
((normCV‘𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 /
((normCV‘𝑈)‘𝑧))) ∧ 𝑧 ∈ 𝑋) → ((normCV‘𝑈)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑈)‘𝑧))) |
74 | 50, 72, 64, 73 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑈)‘𝑧))) |
75 | | rpcn 12475 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℂ) |
76 | 75 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ∈ ℂ) |
77 | 54 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘𝑧) ∈ ℝ) |
78 | 77 | recnd 10740 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘𝑧) ∈ ℂ) |
79 | 2, 56, 21 | nvz 28596 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → (((normCV‘𝑈)‘𝑧) = 0 ↔ 𝑧 = (0vec‘𝑈))) |
80 | 1, 79 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ 𝑋 → (((normCV‘𝑈)‘𝑧) = 0 ↔ 𝑧 = (0vec‘𝑈))) |
81 | 80 | necon3bid 2978 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ 𝑋 → (((normCV‘𝑈)‘𝑧) ≠ 0 ↔ 𝑧 ≠ (0vec‘𝑈))) |
82 | 81 | biimpar 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) →
((normCV‘𝑈)‘𝑧) ≠ 0) |
83 | 82 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘𝑧) ≠ 0) |
84 | 76, 78, 83 | divcan1d 11488 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑈)‘𝑧)) = 𝑦) |
85 | 71, 74, 84 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = 𝑦) |
86 | | rpre 12473 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ) |
87 | 86 | leidd 11277 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ≤ 𝑦) |
88 | 87 | ad2antlr 727 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ≤ 𝑦) |
89 | 85, 88 | eqbrtrd 5049 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦) |
90 | 2, 68 | nvgcl 28547 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧) ∈ 𝑋) → (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) ∈ 𝑋) |
91 | 50, 51, 67, 90 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) ∈ 𝑋) |
92 | | fvoveq1 7187 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) |
93 | 92 | breq1d 5037 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 ↔ ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦)) |
94 | | fvoveq1 7187 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) |
95 | 94 | fveq2d 6672 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)))) |
96 | 95 | breq1d 5037 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → (((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1 ↔
((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1)) |
97 | 93, 96 | imbi12d 348 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → ((((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) ↔
(((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1))) |
98 | 97 | rspcv 3519 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃( +𝑣
‘𝑈)((𝑦 /
((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) ∈ 𝑋 → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) →
(((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1))) |
99 | 91, 98 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) →
(((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1))) |
100 | 89, 99 | mpid 44 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) →
((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1)) |
101 | 28 | ffvelrni 6854 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑋 → (𝑇‘𝑧) ∈ (BaseSet‘𝑊)) |
102 | 7, 32 | nvcl 28588 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑇‘𝑧) ∈ (BaseSet‘𝑊)) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ) |
103 | 6, 101, 102 | sylancr 590 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝑋 → ((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ) |
104 | 103 | ad2antrl 728 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ) |
105 | | 1red 10713 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 1 ∈
ℝ) |
106 | 104, 105,
62 | lemuldiv2d 12557 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))) ≤ 1 ↔
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))))) |
107 | 70 | fveq2d 6672 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))) |
108 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (
·𝑠OLD ‘𝑊) = ( ·𝑠OLD
‘𝑊) |
109 | 2, 65, 108, 26 | lnomul 28687 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋)) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧))) |
110 | 36, 109 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 /
((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧))) |
111 | 63, 64, 110 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧))) |
112 | 107, 111 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧))) |
113 | 112 | fveq2d 6672 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧)))) |
114 | 6 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑊 ∈ NrmCVec) |
115 | 101 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘𝑧) ∈ (BaseSet‘𝑊)) |
116 | 7, 108, 32 | nvsge0 28591 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ NrmCVec ∧ ((𝑦 /
((normCV‘𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 /
((normCV‘𝑈)‘𝑧))) ∧ (𝑇‘𝑧) ∈ (BaseSet‘𝑊)) → ((normCV‘𝑊)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧))) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧)))) |
117 | 114, 72, 115, 116 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑊)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧))) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧)))) |
118 | 113, 117 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧)))) |
119 | 118 | breq1d 5037 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
(((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1 ↔ ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))) ≤ 1)) |
120 | | rpcnne0 12483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℝ+
→ (𝑦 ∈ ℂ
∧ 𝑦 ≠
0)) |
121 | | rpcnne0 12483 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((normCV‘𝑈)‘𝑧) ∈ ℝ+ →
(((normCV‘𝑈)‘𝑧) ∈ ℂ ∧
((normCV‘𝑈)‘𝑧) ≠ 0)) |
122 | | recdiv 11417 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) ∧
(((normCV‘𝑈)‘𝑧) ∈ ℂ ∧
((normCV‘𝑈)‘𝑧) ≠ 0)) → (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))) = (((normCV‘𝑈)‘𝑧) / 𝑦)) |
123 | 120, 121,
122 | syl2an 599 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℝ+
∧ ((normCV‘𝑈)‘𝑧) ∈ ℝ+) → (1 /
(𝑦 /
((normCV‘𝑈)‘𝑧))) = (((normCV‘𝑈)‘𝑧) / 𝑦)) |
124 | 52, 60, 123 | syl2an 599 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (1 / (𝑦 /
((normCV‘𝑈)‘𝑧))) = (((normCV‘𝑈)‘𝑧) / 𝑦)) |
125 | | rpne0 12481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ≠
0) |
126 | 125 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ≠ 0) |
127 | 78, 76, 126 | divrec2d 11491 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
(((normCV‘𝑈)‘𝑧) / 𝑦) = ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) |
128 | 124, 127 | eqtr2d 2774 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((1 / 𝑦) ·
((normCV‘𝑈)‘𝑧)) = (1 / (𝑦 / ((normCV‘𝑈)‘𝑧)))) |
129 | 128 | breq2d 5039 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
(((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))))) |
130 | 106, 119,
129 | 3bitr4d 314 |
. . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
(((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1 ↔
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) |
131 | 100, 130 | sylibd 242 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) |
132 | 131 | anassrs 471 |
. . . . . . . . . . . . 13
⊢ ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 ≠ (0vec‘𝑈)) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) |
133 | 132 | imp 410 |
. . . . . . . . . . . 12
⊢
(((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 ≠ (0vec‘𝑈)) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) |
134 | 133 | an32s 652 |
. . . . . . . . . . 11
⊢
(((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) ∧ 𝑧 ≠ (0vec‘𝑈)) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) |
135 | | eqid 2738 |
. . . . . . . . . . . . . . . . . 18
⊢
(0vec‘𝑊) = (0vec‘𝑊) |
136 | 2, 7, 56, 135, 26 | lno0 28683 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → (𝑇‘(0vec‘𝑈)) =
(0vec‘𝑊)) |
137 | 1, 6, 25, 136 | mp3an 1462 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇‘(0vec‘𝑈)) =
(0vec‘𝑊) |
138 | 137 | fveq2i 6671 |
. . . . . . . . . . . . . . 15
⊢
((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) =
((normCV‘𝑊)‘(0vec‘𝑊)) |
139 | 135, 32 | nvz0 28595 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ NrmCVec →
((normCV‘𝑊)‘(0vec‘𝑊)) = 0) |
140 | 6, 139 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
((normCV‘𝑊)‘(0vec‘𝑊)) = 0 |
141 | 138, 140 | eqtri 2761 |
. . . . . . . . . . . . . 14
⊢
((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) = 0 |
142 | | 0le0 11810 |
. . . . . . . . . . . . . 14
⊢ 0 ≤
0 |
143 | 141, 142 | eqbrtri 5048 |
. . . . . . . . . . . . 13
⊢
((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ 0 |
144 | 17 | rpcnd 12509 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ+
→ (1 / 𝑦) ∈
ℂ) |
145 | 56, 21 | nvz0 28595 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑈 ∈ NrmCVec →
((normCV‘𝑈)‘(0vec‘𝑈)) = 0) |
146 | 1, 145 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
((normCV‘𝑈)‘(0vec‘𝑈)) = 0 |
147 | 146 | oveq2i 7175 |
. . . . . . . . . . . . . . 15
⊢ ((1 /
𝑦) ·
((normCV‘𝑈)‘(0vec‘𝑈))) = ((1 / 𝑦) · 0) |
148 | | mul01 10890 |
. . . . . . . . . . . . . . 15
⊢ ((1 /
𝑦) ∈ ℂ →
((1 / 𝑦) · 0) =
0) |
149 | 147, 148 | syl5eq 2785 |
. . . . . . . . . . . . . 14
⊢ ((1 /
𝑦) ∈ ℂ →
((1 / 𝑦) ·
((normCV‘𝑈)‘(0vec‘𝑈))) = 0) |
150 | 144, 149 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ+
→ ((1 / 𝑦) ·
((normCV‘𝑈)‘(0vec‘𝑈))) = 0) |
151 | 143, 150 | breqtrrid 5065 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ+
→ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ ((1 / 𝑦) ·
((normCV‘𝑈)‘(0vec‘𝑈)))) |
152 | 151 | ad3antlr 731 |
. . . . . . . . . . 11
⊢ ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) →
((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ ((1 / 𝑦) ·
((normCV‘𝑈)‘(0vec‘𝑈)))) |
153 | 49, 134, 152 | pm2.61ne 3019 |
. . . . . . . . . 10
⊢ ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) |
154 | 153 | ex 416 |
. . . . . . . . 9
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) |
155 | 154 | ralrimdva 3101 |
. . . . . . . 8
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) →
(∀𝑥 ∈ 𝑋
(((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) → ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) |
156 | 45, 155 | sylbid 243 |
. . . . . . 7
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) →
(∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) → ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) |
157 | 156 | imp 410 |
. . . . . 6
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧
∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) |
158 | | oveq1 7171 |
. . . . . . . . 9
⊢ (𝑥 = (1 / 𝑦) → (𝑥 · ((normCV‘𝑈)‘𝑧)) = ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) |
159 | 158 | breq2d 5039 |
. . . . . . . 8
⊢ (𝑥 = (1 / 𝑦) → (((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) |
160 | 159 | ralbidv 3109 |
. . . . . . 7
⊢ (𝑥 = (1 / 𝑦) → (∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)) ↔ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) |
161 | 160 | rspcev 3524 |
. . . . . 6
⊢ (((1 /
𝑦) ∈ ℝ ∧
∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))) |
162 | 19, 157, 161 | syl2anc 587 |
. . . . 5
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧
∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))) |
163 | 162 | rexlimdva2 3196 |
. . . 4
⊢ (𝑃 ∈ 𝑋 → (∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))) |
164 | 16, 163 | syl5 34 |
. . 3
⊢ (𝑃 ∈ 𝑋 → (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))) |
165 | 164 | imp 410 |
. 2
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))) |
166 | | blocni.5 |
. . . 4
⊢ 𝐵 = (𝑈 BLnOp 𝑊) |
167 | 2, 21, 32, 26, 166, 1, 6 | isblo3i 28728 |
. . 3
⊢ (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))) |
168 | 25, 167 | mpbiran 709 |
. 2
⊢ (𝑇 ∈ 𝐵 ↔ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))) |
169 | 165, 168 | sylibr 237 |
1
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑇 ∈ 𝐵) |