| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | blocni.u | . . . . . 6
⊢ 𝑈 ∈ NrmCVec | 
| 2 |  | blocnilem.1 | . . . . . . 7
⊢ 𝑋 = (BaseSet‘𝑈) | 
| 3 |  | blocni.8 | . . . . . . 7
⊢ 𝐶 = (IndMet‘𝑈) | 
| 4 | 2, 3 | imsxmet 30712 | . . . . . 6
⊢ (𝑈 ∈ NrmCVec → 𝐶 ∈ (∞Met‘𝑋)) | 
| 5 | 1, 4 | ax-mp 5 | . . . . 5
⊢ 𝐶 ∈ (∞Met‘𝑋) | 
| 6 |  | blocni.w | . . . . . 6
⊢ 𝑊 ∈ NrmCVec | 
| 7 |  | eqid 2736 | . . . . . . 7
⊢
(BaseSet‘𝑊) =
(BaseSet‘𝑊) | 
| 8 |  | blocni.d | . . . . . . 7
⊢ 𝐷 = (IndMet‘𝑊) | 
| 9 | 7, 8 | imsxmet 30712 | . . . . . 6
⊢ (𝑊 ∈ NrmCVec → 𝐷 ∈
(∞Met‘(BaseSet‘𝑊))) | 
| 10 | 6, 9 | ax-mp 5 | . . . . 5
⊢ 𝐷 ∈
(∞Met‘(BaseSet‘𝑊)) | 
| 11 |  | 1rp 13039 | . . . . . 6
⊢ 1 ∈
ℝ+ | 
| 12 |  | blocni.j | . . . . . . 7
⊢ 𝐽 = (MetOpen‘𝐶) | 
| 13 |  | blocni.k | . . . . . . 7
⊢ 𝐾 = (MetOpen‘𝐷) | 
| 14 | 12, 13 | metcnpi3 24560 | . . . . . 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 13062 | . . . . . . . 8
⊢ (𝑦 ∈ ℝ+
→ (1 / 𝑦) ∈
ℝ+) | 
| 18 | 17 | rpred 13078 | . . . . . . 7
⊢ (𝑦 ∈ ℝ+
→ (1 / 𝑦) ∈
ℝ) | 
| 19 | 18 | ad2antlr 727 | . . . . . 6
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧
∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → (1 / 𝑦) ∈ ℝ) | 
| 20 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢ (
−𝑣 ‘𝑈) = ( −𝑣
‘𝑈) | 
| 21 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(normCV‘𝑈) = (normCV‘𝑈) | 
| 22 | 2, 20, 21, 3 | imsdval 30706 | . . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑥𝐶𝑃) = ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃))) | 
| 23 | 1, 22 | mp3an1 1449 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑥𝐶𝑃) = ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃))) | 
| 24 | 23 | breq1d 5152 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑥𝐶𝑃) ≤ 𝑦 ↔ ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦)) | 
| 25 |  | blocni.l | . . . . . . . . . . . . . . . . 17
⊢ 𝑇 ∈ 𝐿 | 
| 26 |  | blocni.4 | . . . . . . . . . . . . . . . . . 18
⊢ 𝐿 = (𝑈 LnOp 𝑊) | 
| 27 | 2, 7, 26 | lnof 30775 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑇:𝑋⟶(BaseSet‘𝑊)) | 
| 28 | 1, 6, 25, 27 | mp3an 1462 | . . . . . . . . . . . . . . . 16
⊢ 𝑇:𝑋⟶(BaseSet‘𝑊) | 
| 29 | 28 | ffvelcdmi 7102 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑋 → (𝑇‘𝑥) ∈ (BaseSet‘𝑊)) | 
| 30 | 28 | ffvelcdmi 7102 | . . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ 𝑋 → (𝑇‘𝑃) ∈ (BaseSet‘𝑊)) | 
| 31 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢ (
−𝑣 ‘𝑊) = ( −𝑣
‘𝑊) | 
| 32 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢
(normCV‘𝑊) = (normCV‘𝑊) | 
| 33 | 7, 31, 32, 8 | imsdval 30706 | . . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑇‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇‘𝑃) ∈ (BaseSet‘𝑊)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))) | 
| 34 | 6, 33 | mp3an1 1449 | . . . . . . . . . . . . . . 15
⊢ (((𝑇‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇‘𝑃) ∈ (BaseSet‘𝑊)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))) | 
| 35 | 29, 30, 34 | syl2an 596 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))) | 
| 36 | 1, 6, 25 | 3pm3.2i 1339 | . . . . . . . . . . . . . . . 16
⊢ (𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) | 
| 37 | 2, 20, 31, 26 | lnosub 30779 | . . . . . . . . . . . . . . . 16
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋)) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))) | 
| 38 | 36, 37 | mpan 690 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃))) | 
| 39 | 38 | fveq2d 6909 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘((𝑇‘𝑥)( −𝑣 ‘𝑊)(𝑇‘𝑃)))) | 
| 40 | 35, 39 | eqtr4d 2779 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) = ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)))) | 
| 41 | 40 | breq1d 5152 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1 ↔
((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) | 
| 42 | 24, 41 | imbi12d 344 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔
(((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1))) | 
| 43 | 42 | ancoms 458 | . . . . . . . . . 10
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔
(((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1))) | 
| 44 | 43 | adantlr 715 | . . . . . . . . 9
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑥 ∈ 𝑋) → (((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔
(((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1))) | 
| 45 | 44 | ralbidva 3175 | . . . . . . . 8
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) →
(∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) ↔ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1))) | 
| 46 |  | 2fveq3 6910 | . . . . . . . . . . . 12
⊢ (𝑧 = (0vec‘𝑈) →
((normCV‘𝑊)‘(𝑇‘𝑧)) = ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈)))) | 
| 47 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑧 = (0vec‘𝑈) →
((normCV‘𝑈)‘𝑧) = ((normCV‘𝑈)‘(0vec‘𝑈))) | 
| 48 | 47 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝑧 = (0vec‘𝑈) → ((1 / 𝑦) ·
((normCV‘𝑈)‘𝑧)) = ((1 / 𝑦) · ((normCV‘𝑈)‘(0vec‘𝑈)))) | 
| 49 | 46, 48 | breq12d 5155 | . . . . . . . . . . 11
⊢ (𝑧 = (0vec‘𝑈) →
(((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ ((1 / 𝑦) ·
((normCV‘𝑈)‘(0vec‘𝑈))))) | 
| 50 | 1 | a1i 11 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑈 ∈ NrmCVec) | 
| 51 |  | simpll 766 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑃 ∈ 𝑋) | 
| 52 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℝ+) | 
| 53 | 2, 21 | nvcl 30681 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → ((normCV‘𝑈)‘𝑧) ∈ ℝ) | 
| 54 | 1, 53 | mpan 690 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 ∈ 𝑋 → ((normCV‘𝑈)‘𝑧) ∈ ℝ) | 
| 55 | 54 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) →
((normCV‘𝑈)‘𝑧) ∈ ℝ) | 
| 56 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(0vec‘𝑈) = (0vec‘𝑈) | 
| 57 | 2, 56, 21 | nvgt0 30694 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → (𝑧 ≠ (0vec‘𝑈) ↔ 0 <
((normCV‘𝑈)‘𝑧))) | 
| 58 | 1, 57 | mpan 690 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 ∈ 𝑋 → (𝑧 ≠ (0vec‘𝑈) ↔ 0 <
((normCV‘𝑈)‘𝑧))) | 
| 59 | 58 | biimpa 476 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) → 0 <
((normCV‘𝑈)‘𝑧)) | 
| 60 | 55, 59 | elrpd 13075 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) →
((normCV‘𝑈)‘𝑧) ∈
ℝ+) | 
| 61 |  | rpdivcl 13061 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℝ+
∧ ((normCV‘𝑈)‘𝑧) ∈ ℝ+) → (𝑦 /
((normCV‘𝑈)‘𝑧)) ∈
ℝ+) | 
| 62 | 52, 60, 61 | syl2an 596 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈
ℝ+) | 
| 63 | 62 | rpcnd 13080 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ) | 
| 64 |  | simprl 770 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑧 ∈ 𝑋) | 
| 65 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (
·𝑠OLD ‘𝑈) = ( ·𝑠OLD
‘𝑈) | 
| 66 | 2, 65 | nvscl 30646 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑦 /
((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋) → ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧) ∈ 𝑋) | 
| 67 | 50, 63, 64, 66 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧) ∈ 𝑋) | 
| 68 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (
+𝑣 ‘𝑈) = ( +𝑣 ‘𝑈) | 
| 69 | 2, 68, 20 | nvpncan2 30673 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧) ∈ 𝑋) → ((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) | 
| 70 | 50, 51, 67, 69 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) | 
| 71 | 70 | fveq2d 6909 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = ((normCV‘𝑈)‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))) | 
| 72 | 62 | rprege0d 13085 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℝ ∧ 0 ≤ (𝑦 /
((normCV‘𝑈)‘𝑧)))) | 
| 73 | 2, 65, 21 | nvsge0 30684 | . . . . . . . . . . . . . . . . . . 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 13046 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℂ) | 
| 76 | 75 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ∈ ℂ) | 
| 77 | 54 | ad2antrl 728 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘𝑧) ∈ ℝ) | 
| 78 | 77 | recnd 11290 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘𝑧) ∈ ℂ) | 
| 79 | 2, 56, 21 | nvz 30689 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑧 ∈ 𝑋) → (((normCV‘𝑈)‘𝑧) = 0 ↔ 𝑧 = (0vec‘𝑈))) | 
| 80 | 1, 79 | mpan 690 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ 𝑋 → (((normCV‘𝑈)‘𝑧) = 0 ↔ 𝑧 = (0vec‘𝑈))) | 
| 81 | 80 | necon3bid 2984 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ 𝑋 → (((normCV‘𝑈)‘𝑧) ≠ 0 ↔ 𝑧 ≠ (0vec‘𝑈))) | 
| 82 | 81 | biimpar 477 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈)) →
((normCV‘𝑈)‘𝑧) ≠ 0) | 
| 83 | 82 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘𝑧) ≠ 0) | 
| 84 | 76, 78, 83 | divcan1d 12045 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑈)‘𝑧)) = 𝑦) | 
| 85 | 71, 74, 84 | 3eqtrd 2780 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = 𝑦) | 
| 86 |  | rpre 13044 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ) | 
| 87 | 86 | leidd 11830 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ≤ 𝑦) | 
| 88 | 87 | ad2antlr 727 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ≤ 𝑦) | 
| 89 | 85, 88 | eqbrtrd 5164 | . . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦) | 
| 90 | 2, 68 | nvgcl 30640 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑃 ∈ 𝑋 ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧) ∈ 𝑋) → (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) ∈ 𝑋) | 
| 91 | 50, 51, 67, 90 | syl3anc 1372 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) ∈ 𝑋) | 
| 92 |  | fvoveq1 7455 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → ((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) = ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) | 
| 93 | 92 | breq1d 5152 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 ↔ ((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦)) | 
| 94 |  | fvoveq1 7455 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → (𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃)) = (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) | 
| 95 | 94 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) = ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)))) | 
| 96 | 95 | breq1d 5152 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → (((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1 ↔
((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1)) | 
| 97 | 93, 96 | imbi12d 344 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) → ((((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) ↔
(((normCV‘𝑈)‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1))) | 
| 98 | 97 | rspcv 3617 | . . . . . . . . . . . . . . . . 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 | ffvelcdmi 7102 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ 𝑋 → (𝑇‘𝑧) ∈ (BaseSet‘𝑊)) | 
| 102 | 7, 32 | nvcl 30681 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑇‘𝑧) ∈ (BaseSet‘𝑊)) → ((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ) | 
| 103 | 6, 101, 102 | sylancr 587 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝑋 → ((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ) | 
| 104 | 103 | ad2antrl 728 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ∈ ℝ) | 
| 105 |  | 1red 11263 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 1 ∈
ℝ) | 
| 106 | 104, 105,
62 | lemuldiv2d 13128 | . . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))) ≤ 1 ↔
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))))) | 
| 107 | 70 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))) | 
| 108 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (
·𝑠OLD ‘𝑊) = ( ·𝑠OLD
‘𝑊) | 
| 109 | 2, 65, 108, 26 | lnomul 30780 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ ((𝑦 / ((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋)) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧))) | 
| 110 | 36, 109 | mpan 690 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 /
((normCV‘𝑈)‘𝑧)) ∈ ℂ ∧ 𝑧 ∈ 𝑋) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧))) | 
| 111 | 63, 64, 110 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧))) | 
| 112 | 107, 111 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃)) = ((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑊)(𝑇‘𝑧))) | 
| 113 | 112 | fveq2d 6909 | . . . . . . . . . . . . . . . . . 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 30684 | . . . . . . . . . . . . . . . . . . 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 2776 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) = ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧)))) | 
| 119 | 118 | breq1d 5152 | . . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
(((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1 ↔ ((𝑦 / ((normCV‘𝑈)‘𝑧)) · ((normCV‘𝑊)‘(𝑇‘𝑧))) ≤ 1)) | 
| 120 |  | rpcnne0 13054 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℝ+
→ (𝑦 ∈ ℂ
∧ 𝑦 ≠
0)) | 
| 121 |  | rpcnne0 13054 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((normCV‘𝑈)‘𝑧) ∈ ℝ+ →
(((normCV‘𝑈)‘𝑧) ∈ ℂ ∧
((normCV‘𝑈)‘𝑧) ≠ 0)) | 
| 122 |  | recdiv 11974 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) ∧
(((normCV‘𝑈)‘𝑧) ∈ ℂ ∧
((normCV‘𝑈)‘𝑧) ≠ 0)) → (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))) = (((normCV‘𝑈)‘𝑧) / 𝑦)) | 
| 123 | 120, 121,
122 | syl2an 596 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℝ+
∧ ((normCV‘𝑈)‘𝑧) ∈ ℝ+) → (1 /
(𝑦 /
((normCV‘𝑈)‘𝑧))) = (((normCV‘𝑈)‘𝑧) / 𝑦)) | 
| 124 | 52, 60, 123 | syl2an 596 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (1 / (𝑦 /
((normCV‘𝑈)‘𝑧))) = (((normCV‘𝑈)‘𝑧) / 𝑦)) | 
| 125 |  | rpne0 13052 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ≠
0) | 
| 126 | 125 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → 𝑦 ≠ 0) | 
| 127 | 78, 76, 126 | divrec2d 12048 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
(((normCV‘𝑈)‘𝑧) / 𝑦) = ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) | 
| 128 | 124, 127 | eqtr2d 2777 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → ((1 / 𝑦) ·
((normCV‘𝑈)‘𝑧)) = (1 / (𝑦 / ((normCV‘𝑈)‘𝑧)))) | 
| 129 | 128 | breq2d 5154 | . . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
(((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (1 / (𝑦 / ((normCV‘𝑈)‘𝑧))))) | 
| 130 | 106, 119,
129 | 3bitr4d 311 | . . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) →
(((normCV‘𝑊)‘(𝑇‘((𝑃( +𝑣 ‘𝑈)((𝑦 / ((normCV‘𝑈)‘𝑧))( ·𝑠OLD
‘𝑈)𝑧))( −𝑣 ‘𝑈)𝑃))) ≤ 1 ↔
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) | 
| 131 | 100, 130 | sylibd 239 | . . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ (𝑧 ∈ 𝑋 ∧ 𝑧 ≠ (0vec‘𝑈))) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) | 
| 132 | 131 | anassrs 467 | . . . . . . . . . . . . 13
⊢ ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 ≠ (0vec‘𝑈)) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) | 
| 133 | 132 | imp 406 | . . . . . . . . . . . 12
⊢
(((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ 𝑧 ≠ (0vec‘𝑈)) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) | 
| 134 | 133 | an32s 652 | . . . . . . . . . . 11
⊢
(((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) ∧ 𝑧 ≠ (0vec‘𝑈)) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) | 
| 135 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢
(0vec‘𝑊) = (0vec‘𝑊) | 
| 136 | 2, 7, 56, 135, 26 | lno0 30776 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → (𝑇‘(0vec‘𝑈)) =
(0vec‘𝑊)) | 
| 137 | 1, 6, 25, 136 | mp3an 1462 | . . . . . . . . . . . . . . . 16
⊢ (𝑇‘(0vec‘𝑈)) =
(0vec‘𝑊) | 
| 138 | 137 | fveq2i 6908 | . . . . . . . . . . . . . . 15
⊢
((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) =
((normCV‘𝑊)‘(0vec‘𝑊)) | 
| 139 | 135, 32 | nvz0 30688 | . . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ NrmCVec →
((normCV‘𝑊)‘(0vec‘𝑊)) = 0) | 
| 140 | 6, 139 | ax-mp 5 | . . . . . . . . . . . . . . 15
⊢
((normCV‘𝑊)‘(0vec‘𝑊)) = 0 | 
| 141 | 138, 140 | eqtri 2764 | . . . . . . . . . . . . . 14
⊢
((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) = 0 | 
| 142 |  | 0le0 12368 | . . . . . . . . . . . . . 14
⊢ 0 ≤
0 | 
| 143 | 141, 142 | eqbrtri 5163 | . . . . . . . . . . . . 13
⊢
((normCV‘𝑊)‘(𝑇‘(0vec‘𝑈))) ≤ 0 | 
| 144 | 17 | rpcnd 13080 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ+
→ (1 / 𝑦) ∈
ℂ) | 
| 145 | 56, 21 | nvz0 30688 | . . . . . . . . . . . . . . . . 17
⊢ (𝑈 ∈ NrmCVec →
((normCV‘𝑈)‘(0vec‘𝑈)) = 0) | 
| 146 | 1, 145 | ax-mp 5 | . . . . . . . . . . . . . . . 16
⊢
((normCV‘𝑈)‘(0vec‘𝑈)) = 0 | 
| 147 | 146 | oveq2i 7443 | . . . . . . . . . . . . . . 15
⊢ ((1 /
𝑦) ·
((normCV‘𝑈)‘(0vec‘𝑈))) = ((1 / 𝑦) · 0) | 
| 148 |  | mul01 11441 | . . . . . . . . . . . . . . 15
⊢ ((1 /
𝑦) ∈ ℂ →
((1 / 𝑦) · 0) =
0) | 
| 149 | 147, 148 | eqtrid 2788 | . . . . . . . . . . . . . 14
⊢ ((1 /
𝑦) ∈ ℂ →
((1 / 𝑦) ·
((normCV‘𝑈)‘(0vec‘𝑈))) = 0) | 
| 150 | 144, 149 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ+
→ ((1 / 𝑦) ·
((normCV‘𝑈)‘(0vec‘𝑈))) = 0) | 
| 151 | 143, 150 | breqtrrid 5180 | . . . . . . . . . . . 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 3026 | . . . . . . . . . 10
⊢ ((((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) ∧ ∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1)) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) | 
| 154 | 153 | ex 412 | . . . . . . . . 9
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧ 𝑧 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 (((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) →
((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) | 
| 155 | 154 | ralrimdva 3153 | . . . . . . . 8
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) →
(∀𝑥 ∈ 𝑋
(((normCV‘𝑈)‘(𝑥( −𝑣 ‘𝑈)𝑃)) ≤ 𝑦 → ((normCV‘𝑊)‘(𝑇‘(𝑥( −𝑣 ‘𝑈)𝑃))) ≤ 1) → ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) | 
| 156 | 45, 155 | sylbid 240 | . . . . . . 7
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) →
(∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) → ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) | 
| 157 | 156 | imp 406 | . . . . . 6
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧
∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) | 
| 158 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝑥 = (1 / 𝑦) → (𝑥 · ((normCV‘𝑈)‘𝑧)) = ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) | 
| 159 | 158 | breq2d 5154 | . . . . . . . 8
⊢ (𝑥 = (1 / 𝑦) → (((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)) ↔ ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) | 
| 160 | 159 | ralbidv 3177 | . . . . . . 7
⊢ (𝑥 = (1 / 𝑦) → (∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)) ↔ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧)))) | 
| 161 | 160 | rspcev 3621 | . . . . . 6
⊢ (((1 /
𝑦) ∈ ℝ ∧
∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ ((1 / 𝑦) · ((normCV‘𝑈)‘𝑧))) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))) | 
| 162 | 19, 157, 161 | syl2anc 584 | . . . . 5
⊢ (((𝑃 ∈ 𝑋 ∧ 𝑦 ∈ ℝ+) ∧
∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))) | 
| 163 | 162 | rexlimdva2 3156 | . . . 4
⊢ (𝑃 ∈ 𝑋 → (∃𝑦 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ((𝑥𝐶𝑃) ≤ 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑃)) ≤ 1) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))) | 
| 164 | 16, 163 | syl5 34 | . . 3
⊢ (𝑃 ∈ 𝑋 → (𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))) | 
| 165 | 164 | imp 406 | . 2
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))) | 
| 166 |  | blocni.5 | . . . 4
⊢ 𝐵 = (𝑈 BLnOp 𝑊) | 
| 167 | 2, 21, 32, 26, 166, 1, 6 | isblo3i 30821 | . . 3
⊢ (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧)))) | 
| 168 | 25, 167 | mpbiran 709 | . 2
⊢ (𝑇 ∈ 𝐵 ↔ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑋 ((normCV‘𝑊)‘(𝑇‘𝑧)) ≤ (𝑥 · ((normCV‘𝑈)‘𝑧))) | 
| 169 | 165, 168 | sylibr 234 | 1
⊢ ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑇 ∈ 𝐵) |