Proof of Theorem htthlem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | htthlem.8 | . 2
⊢ (𝜑 → 𝑇 ∈ 𝐿) | 
| 2 |  | htthlem.6 | . . . . . . . . . 10
⊢ 𝑈 ∈
CHilOLD | 
| 3 | 2 | hlnvi 30911 | . . . . . . . . 9
⊢ 𝑈 ∈ NrmCVec | 
| 4 |  | htth.1 | . . . . . . . . . . . . 13
⊢ 𝑋 = (BaseSet‘𝑈) | 
| 5 |  | htth.3 | . . . . . . . . . . . . 13
⊢ 𝐿 = (𝑈 LnOp 𝑈) | 
| 6 | 4, 4, 5 | lnof 30774 | . . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑈 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑇:𝑋⟶𝑋) | 
| 7 | 3, 3, 6 | mp3an12 1453 | . . . . . . . . . . 11
⊢ (𝑇 ∈ 𝐿 → 𝑇:𝑋⟶𝑋) | 
| 8 | 1, 7 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝑇:𝑋⟶𝑋) | 
| 9 | 8 | ffvelcdmda 7104 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑇‘𝑥) ∈ 𝑋) | 
| 10 |  | htthlem.5 | . . . . . . . . . 10
⊢ 𝑁 =
(normCV‘𝑈) | 
| 11 | 4, 10 | nvcl 30680 | . . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑇‘𝑥) ∈ 𝑋) → (𝑁‘(𝑇‘𝑥)) ∈ ℝ) | 
| 12 | 3, 9, 11 | sylancr 587 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑁‘(𝑇‘𝑥)) ∈ ℝ) | 
| 13 | 8 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑇‘𝑧) ∈ 𝑋) | 
| 14 |  | htth.2 | . . . . . . . . . . . . . . . . 17
⊢ 𝑃 =
(·𝑖OLD‘𝑈) | 
| 15 |  | hlph 30908 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑈 ∈ CHilOLD
→ 𝑈 ∈
CPreHilOLD) | 
| 16 | 2, 15 | ax-mp 5 | . . . . . . . . . . . . . . . . 17
⊢ 𝑈 ∈
CPreHilOLD | 
| 17 |  | htthlem.7 | . . . . . . . . . . . . . . . . 17
⊢ 𝑊 = 〈〈 + , ·
〉, abs〉 | 
| 18 |  | eqid 2737 | . . . . . . . . . . . . . . . . 17
⊢ (𝑈 BLnOp 𝑊) = (𝑈 BLnOp 𝑊) | 
| 19 |  | eqid 2737 | . . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ 𝑋 ↦ (𝑤𝑃(𝑇‘𝑧))) = (𝑤 ∈ 𝑋 ↦ (𝑤𝑃(𝑇‘𝑧))) | 
| 20 | 4, 14, 16, 17, 18, 19 | ipblnfi 30874 | . . . . . . . . . . . . . . . 16
⊢ ((𝑇‘𝑧) ∈ 𝑋 → (𝑤 ∈ 𝑋 ↦ (𝑤𝑃(𝑇‘𝑧))) ∈ (𝑈 BLnOp 𝑊)) | 
| 21 | 13, 20 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑤 ∈ 𝑋 ↦ (𝑤𝑃(𝑇‘𝑧))) ∈ (𝑈 BLnOp 𝑊)) | 
| 22 |  | htthlem.10 | . . . . . . . . . . . . . . 15
⊢ 𝐹 = (𝑧 ∈ 𝑋 ↦ (𝑤 ∈ 𝑋 ↦ (𝑤𝑃(𝑇‘𝑧)))) | 
| 23 | 21, 22 | fmptd 7134 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:𝑋⟶(𝑈 BLnOp 𝑊)) | 
| 24 | 23 | ffund 6740 | . . . . . . . . . . . . 13
⊢ (𝜑 → Fun 𝐹) | 
| 25 | 24 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → Fun 𝐹) | 
| 26 |  | id 22 | . . . . . . . . . . . . 13
⊢ (𝑤 ∈ 𝐾 → 𝑤 ∈ 𝐾) | 
| 27 |  | htthlem.11 | . . . . . . . . . . . . 13
⊢ 𝐾 = (𝐹 “ {𝑧 ∈ 𝑋 ∣ (𝑁‘𝑧) ≤ 1}) | 
| 28 | 26, 27 | eleqtrdi 2851 | . . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝐾 → 𝑤 ∈ (𝐹 “ {𝑧 ∈ 𝑋 ∣ (𝑁‘𝑧) ≤ 1})) | 
| 29 |  | fvelima 6974 | . . . . . . . . . . . 12
⊢ ((Fun
𝐹 ∧ 𝑤 ∈ (𝐹 “ {𝑧 ∈ 𝑋 ∣ (𝑁‘𝑧) ≤ 1})) → ∃𝑦 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘𝑧) ≤ 1} (𝐹‘𝑦) = 𝑤) | 
| 30 | 25, 28, 29 | syl2an 596 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑤 ∈ 𝐾) → ∃𝑦 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘𝑧) ≤ 1} (𝐹‘𝑦) = 𝑤) | 
| 31 | 30 | ex 412 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑤 ∈ 𝐾 → ∃𝑦 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘𝑧) ≤ 1} (𝐹‘𝑦) = 𝑤)) | 
| 32 |  | fveq2 6906 | . . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑦 → (𝑁‘𝑧) = (𝑁‘𝑦)) | 
| 33 | 32 | breq1d 5153 | . . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑦 → ((𝑁‘𝑧) ≤ 1 ↔ (𝑁‘𝑦) ≤ 1)) | 
| 34 | 33 | elrab 3692 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘𝑧) ≤ 1} ↔ (𝑦 ∈ 𝑋 ∧ (𝑁‘𝑦) ≤ 1)) | 
| 35 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = 𝑦 → (𝑇‘𝑧) = (𝑇‘𝑦)) | 
| 36 | 35 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 𝑦 → (𝑤𝑃(𝑇‘𝑧)) = (𝑤𝑃(𝑇‘𝑦))) | 
| 37 | 36 | mpteq2dv 5244 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑦 → (𝑤 ∈ 𝑋 ↦ (𝑤𝑃(𝑇‘𝑧))) = (𝑤 ∈ 𝑋 ↦ (𝑤𝑃(𝑇‘𝑦)))) | 
| 38 | 37, 22, 4 | mptfvmpt 7248 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ 𝑋 → (𝐹‘𝑦) = (𝑤 ∈ 𝑋 ↦ (𝑤𝑃(𝑇‘𝑦)))) | 
| 39 | 38 | fveq1d 6908 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝑋 → ((𝐹‘𝑦)‘𝑥) = ((𝑤 ∈ 𝑋 ↦ (𝑤𝑃(𝑇‘𝑦)))‘𝑥)) | 
| 40 |  | oveq1 7438 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝑥 → (𝑤𝑃(𝑇‘𝑦)) = (𝑥𝑃(𝑇‘𝑦))) | 
| 41 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ 𝑋 ↦ (𝑤𝑃(𝑇‘𝑦))) = (𝑤 ∈ 𝑋 ↦ (𝑤𝑃(𝑇‘𝑦))) | 
| 42 |  | ovex 7464 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥𝑃(𝑇‘𝑦)) ∈ V | 
| 43 | 40, 41, 42 | fvmpt 7016 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝑋 → ((𝑤 ∈ 𝑋 ↦ (𝑤𝑃(𝑇‘𝑦)))‘𝑥) = (𝑥𝑃(𝑇‘𝑦))) | 
| 44 | 39, 43 | sylan9eqr 2799 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑦)‘𝑥) = (𝑥𝑃(𝑇‘𝑦))) | 
| 45 | 44 | ad2ant2lr 748 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∧ (𝑁‘𝑦) ≤ 1)) → ((𝐹‘𝑦)‘𝑥) = (𝑥𝑃(𝑇‘𝑦))) | 
| 46 |  | htthlem.9 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑃(𝑇‘𝑦)) = ((𝑇‘𝑥)𝑃𝑦)) | 
| 47 |  | rsp2 3277 | . . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑃(𝑇‘𝑦)) = ((𝑇‘𝑥)𝑃𝑦) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝑃(𝑇‘𝑦)) = ((𝑇‘𝑥)𝑃𝑦))) | 
| 48 | 46, 47 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥𝑃(𝑇‘𝑦)) = ((𝑇‘𝑥)𝑃𝑦))) | 
| 49 | 48 | impl 455 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑥𝑃(𝑇‘𝑦)) = ((𝑇‘𝑥)𝑃𝑦)) | 
| 50 | 49 | adantrr 717 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∧ (𝑁‘𝑦) ≤ 1)) → (𝑥𝑃(𝑇‘𝑦)) = ((𝑇‘𝑥)𝑃𝑦)) | 
| 51 | 45, 50 | eqtrd 2777 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∧ (𝑁‘𝑦) ≤ 1)) → ((𝐹‘𝑦)‘𝑥) = ((𝑇‘𝑥)𝑃𝑦)) | 
| 52 | 51 | fveq2d 6910 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∧ (𝑁‘𝑦) ≤ 1)) → (abs‘((𝐹‘𝑦)‘𝑥)) = (abs‘((𝑇‘𝑥)𝑃𝑦))) | 
| 53 |  | simpl 482 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝑋 ∧ (𝑁‘𝑦) ≤ 1) → 𝑦 ∈ 𝑋) | 
| 54 | 4, 14 | dipcl 30731 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑇‘𝑥) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑇‘𝑥)𝑃𝑦) ∈ ℂ) | 
| 55 | 3, 54 | mp3an1 1450 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑇‘𝑥) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑇‘𝑥)𝑃𝑦) ∈ ℂ) | 
| 56 | 9, 53, 55 | syl2an 596 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∧ (𝑁‘𝑦) ≤ 1)) → ((𝑇‘𝑥)𝑃𝑦) ∈ ℂ) | 
| 57 | 56 | abscld 15475 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∧ (𝑁‘𝑦) ≤ 1)) → (abs‘((𝑇‘𝑥)𝑃𝑦)) ∈ ℝ) | 
| 58 | 12 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∧ (𝑁‘𝑦) ≤ 1)) → (𝑁‘(𝑇‘𝑥)) ∈ ℝ) | 
| 59 | 4, 10 | nvcl 30680 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋) → (𝑁‘𝑦) ∈ ℝ) | 
| 60 | 3, 59 | mpan 690 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ 𝑋 → (𝑁‘𝑦) ∈ ℝ) | 
| 61 | 60 | ad2antrl 728 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∧ (𝑁‘𝑦) ≤ 1)) → (𝑁‘𝑦) ∈ ℝ) | 
| 62 | 58, 61 | remulcld 11291 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∧ (𝑁‘𝑦) ≤ 1)) → ((𝑁‘(𝑇‘𝑥)) · (𝑁‘𝑦)) ∈ ℝ) | 
| 63 | 4, 10, 14, 16 | sii 30873 | . . . . . . . . . . . . . . . 16
⊢ (((𝑇‘𝑥) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (abs‘((𝑇‘𝑥)𝑃𝑦)) ≤ ((𝑁‘(𝑇‘𝑥)) · (𝑁‘𝑦))) | 
| 64 | 9, 53, 63 | syl2an 596 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∧ (𝑁‘𝑦) ≤ 1)) → (abs‘((𝑇‘𝑥)𝑃𝑦)) ≤ ((𝑁‘(𝑇‘𝑥)) · (𝑁‘𝑦))) | 
| 65 |  | 1red 11262 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∧ (𝑁‘𝑦) ≤ 1)) → 1 ∈
ℝ) | 
| 66 | 4, 10 | nvge0 30692 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑇‘𝑥) ∈ 𝑋) → 0 ≤ (𝑁‘(𝑇‘𝑥))) | 
| 67 | 3, 9, 66 | sylancr 587 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 0 ≤ (𝑁‘(𝑇‘𝑥))) | 
| 68 | 12, 67 | jca 511 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑁‘(𝑇‘𝑥)) ∈ ℝ ∧ 0 ≤ (𝑁‘(𝑇‘𝑥)))) | 
| 69 | 68 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∧ (𝑁‘𝑦) ≤ 1)) → ((𝑁‘(𝑇‘𝑥)) ∈ ℝ ∧ 0 ≤ (𝑁‘(𝑇‘𝑥)))) | 
| 70 |  | simprr 773 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∧ (𝑁‘𝑦) ≤ 1)) → (𝑁‘𝑦) ≤ 1) | 
| 71 |  | lemul2a 12122 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑁‘𝑦) ∈ ℝ ∧ 1 ∈ ℝ ∧
((𝑁‘(𝑇‘𝑥)) ∈ ℝ ∧ 0 ≤ (𝑁‘(𝑇‘𝑥)))) ∧ (𝑁‘𝑦) ≤ 1) → ((𝑁‘(𝑇‘𝑥)) · (𝑁‘𝑦)) ≤ ((𝑁‘(𝑇‘𝑥)) · 1)) | 
| 72 | 61, 65, 69, 70, 71 | syl31anc 1375 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∧ (𝑁‘𝑦) ≤ 1)) → ((𝑁‘(𝑇‘𝑥)) · (𝑁‘𝑦)) ≤ ((𝑁‘(𝑇‘𝑥)) · 1)) | 
| 73 | 58 | recnd 11289 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∧ (𝑁‘𝑦) ≤ 1)) → (𝑁‘(𝑇‘𝑥)) ∈ ℂ) | 
| 74 | 73 | mulridd 11278 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∧ (𝑁‘𝑦) ≤ 1)) → ((𝑁‘(𝑇‘𝑥)) · 1) = (𝑁‘(𝑇‘𝑥))) | 
| 75 | 72, 74 | breqtrd 5169 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∧ (𝑁‘𝑦) ≤ 1)) → ((𝑁‘(𝑇‘𝑥)) · (𝑁‘𝑦)) ≤ (𝑁‘(𝑇‘𝑥))) | 
| 76 | 57, 62, 58, 64, 75 | letrd 11418 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∧ (𝑁‘𝑦) ≤ 1)) → (abs‘((𝑇‘𝑥)𝑃𝑦)) ≤ (𝑁‘(𝑇‘𝑥))) | 
| 77 | 52, 76 | eqbrtrd 5165 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑋 ∧ (𝑁‘𝑦) ≤ 1)) → (abs‘((𝐹‘𝑦)‘𝑥)) ≤ (𝑁‘(𝑇‘𝑥))) | 
| 78 | 34, 77 | sylan2b 594 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘𝑧) ≤ 1}) → (abs‘((𝐹‘𝑦)‘𝑥)) ≤ (𝑁‘(𝑇‘𝑥))) | 
| 79 |  | fveq1 6905 | . . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑦) = 𝑤 → ((𝐹‘𝑦)‘𝑥) = (𝑤‘𝑥)) | 
| 80 | 79 | fveq2d 6910 | . . . . . . . . . . . . 13
⊢ ((𝐹‘𝑦) = 𝑤 → (abs‘((𝐹‘𝑦)‘𝑥)) = (abs‘(𝑤‘𝑥))) | 
| 81 | 80 | breq1d 5153 | . . . . . . . . . . . 12
⊢ ((𝐹‘𝑦) = 𝑤 → ((abs‘((𝐹‘𝑦)‘𝑥)) ≤ (𝑁‘(𝑇‘𝑥)) ↔ (abs‘(𝑤‘𝑥)) ≤ (𝑁‘(𝑇‘𝑥)))) | 
| 82 | 78, 81 | syl5ibcom 245 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘𝑧) ≤ 1}) → ((𝐹‘𝑦) = 𝑤 → (abs‘(𝑤‘𝑥)) ≤ (𝑁‘(𝑇‘𝑥)))) | 
| 83 | 82 | rexlimdva 3155 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∃𝑦 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘𝑧) ≤ 1} (𝐹‘𝑦) = 𝑤 → (abs‘(𝑤‘𝑥)) ≤ (𝑁‘(𝑇‘𝑥)))) | 
| 84 | 31, 83 | syld 47 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑤 ∈ 𝐾 → (abs‘(𝑤‘𝑥)) ≤ (𝑁‘(𝑇‘𝑥)))) | 
| 85 | 84 | ralrimiv 3145 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑤 ∈ 𝐾 (abs‘(𝑤‘𝑥)) ≤ (𝑁‘(𝑇‘𝑥))) | 
| 86 |  | brralrspcev 5203 | . . . . . . . 8
⊢ (((𝑁‘(𝑇‘𝑥)) ∈ ℝ ∧ ∀𝑤 ∈ 𝐾 (abs‘(𝑤‘𝑥)) ≤ (𝑁‘(𝑇‘𝑥))) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝐾 (abs‘(𝑤‘𝑥)) ≤ 𝑧) | 
| 87 | 12, 85, 86 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝐾 (abs‘(𝑤‘𝑥)) ≤ 𝑧) | 
| 88 | 87 | ralrimiva 3146 | . . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝐾 (abs‘(𝑤‘𝑥)) ≤ 𝑧) | 
| 89 |  | imassrn 6089 | . . . . . . . . 9
⊢ (𝐹 “ {𝑧 ∈ 𝑋 ∣ (𝑁‘𝑧) ≤ 1}) ⊆ ran 𝐹 | 
| 90 | 27, 89 | eqsstri 4030 | . . . . . . . 8
⊢ 𝐾 ⊆ ran 𝐹 | 
| 91 | 23 | frnd 6744 | . . . . . . . 8
⊢ (𝜑 → ran 𝐹 ⊆ (𝑈 BLnOp 𝑊)) | 
| 92 | 90, 91 | sstrid 3995 | . . . . . . 7
⊢ (𝜑 → 𝐾 ⊆ (𝑈 BLnOp 𝑊)) | 
| 93 |  | hlobn 30907 | . . . . . . . . 9
⊢ (𝑈 ∈ CHilOLD
→ 𝑈 ∈
CBan) | 
| 94 | 2, 93 | ax-mp 5 | . . . . . . . 8
⊢ 𝑈 ∈ CBan | 
| 95 | 17 | cnnv 30696 | . . . . . . . 8
⊢ 𝑊 ∈ NrmCVec | 
| 96 | 17 | cnnvnm 30700 | . . . . . . . . 9
⊢ abs =
(normCV‘𝑊) | 
| 97 |  | eqid 2737 | . . . . . . . . 9
⊢ (𝑈 normOpOLD 𝑊) = (𝑈 normOpOLD 𝑊) | 
| 98 | 4, 96, 97 | ubth 30892 | . . . . . . . 8
⊢ ((𝑈 ∈ CBan ∧ 𝑊 ∈ NrmCVec ∧ 𝐾 ⊆ (𝑈 BLnOp 𝑊)) → (∀𝑥 ∈ 𝑋 ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝐾 (abs‘(𝑤‘𝑥)) ≤ 𝑧 ↔ ∃𝑦 ∈ ℝ ∀𝑤 ∈ 𝐾 ((𝑈 normOpOLD 𝑊)‘𝑤) ≤ 𝑦)) | 
| 99 | 94, 95, 98 | mp3an12 1453 | . . . . . . 7
⊢ (𝐾 ⊆ (𝑈 BLnOp 𝑊) → (∀𝑥 ∈ 𝑋 ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝐾 (abs‘(𝑤‘𝑥)) ≤ 𝑧 ↔ ∃𝑦 ∈ ℝ ∀𝑤 ∈ 𝐾 ((𝑈 normOpOLD 𝑊)‘𝑤) ≤ 𝑦)) | 
| 100 | 92, 99 | syl 17 | . . . . . 6
⊢ (𝜑 → (∀𝑥 ∈ 𝑋 ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝐾 (abs‘(𝑤‘𝑥)) ≤ 𝑧 ↔ ∃𝑦 ∈ ℝ ∀𝑤 ∈ 𝐾 ((𝑈 normOpOLD 𝑊)‘𝑤) ≤ 𝑦)) | 
| 101 | 88, 100 | mpbid 232 | . . . . 5
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑤 ∈ 𝐾 ((𝑈 normOpOLD 𝑊)‘𝑤) ≤ 𝑦) | 
| 102 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ (𝑁‘𝑥) ≤ 1)) → (𝑥 ∈ 𝑋 ∧ (𝑁‘𝑥) ≤ 1)) | 
| 103 |  | fveq2 6906 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑥 → (𝑁‘𝑧) = (𝑁‘𝑥)) | 
| 104 | 103 | breq1d 5153 | . . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 → ((𝑁‘𝑧) ≤ 1 ↔ (𝑁‘𝑥) ≤ 1)) | 
| 105 | 104 | elrab 3692 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘𝑧) ≤ 1} ↔ (𝑥 ∈ 𝑋 ∧ (𝑁‘𝑥) ≤ 1)) | 
| 106 | 102, 105 | sylibr 234 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ (𝑁‘𝑥) ≤ 1)) → 𝑥 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘𝑧) ≤ 1}) | 
| 107 | 22, 21 | dmmptd 6713 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom 𝐹 = 𝑋) | 
| 108 | 107 | eleq2d 2827 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝑋)) | 
| 109 | 108 | biimpar 477 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ dom 𝐹) | 
| 110 |  | funfvima 7250 | . . . . . . . . . . . . . . . 16
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘𝑧) ≤ 1} → (𝐹‘𝑥) ∈ (𝐹 “ {𝑧 ∈ 𝑋 ∣ (𝑁‘𝑧) ≤ 1}))) | 
| 111 | 24, 110 | sylan 580 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘𝑧) ≤ 1} → (𝐹‘𝑥) ∈ (𝐹 “ {𝑧 ∈ 𝑋 ∣ (𝑁‘𝑧) ≤ 1}))) | 
| 112 | 109, 111 | syldan 591 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘𝑧) ≤ 1} → (𝐹‘𝑥) ∈ (𝐹 “ {𝑧 ∈ 𝑋 ∣ (𝑁‘𝑧) ≤ 1}))) | 
| 113 | 112 | ad2ant2r 747 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ (𝑁‘𝑥) ≤ 1)) → (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘𝑧) ≤ 1} → (𝐹‘𝑥) ∈ (𝐹 “ {𝑧 ∈ 𝑋 ∣ (𝑁‘𝑧) ≤ 1}))) | 
| 114 | 106, 113 | mpd 15 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ (𝑁‘𝑥) ≤ 1)) → (𝐹‘𝑥) ∈ (𝐹 “ {𝑧 ∈ 𝑋 ∣ (𝑁‘𝑧) ≤ 1})) | 
| 115 | 114, 27 | eleqtrrdi 2852 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ (𝑁‘𝑥) ≤ 1)) → (𝐹‘𝑥) ∈ 𝐾) | 
| 116 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑤 = (𝐹‘𝑥) → ((𝑈 normOpOLD 𝑊)‘𝑤) = ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥))) | 
| 117 | 116 | breq1d 5153 | . . . . . . . . . . . 12
⊢ (𝑤 = (𝐹‘𝑥) → (((𝑈 normOpOLD 𝑊)‘𝑤) ≤ 𝑦 ↔ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) | 
| 118 | 117 | rspcv 3618 | . . . . . . . . . . 11
⊢ ((𝐹‘𝑥) ∈ 𝐾 → (∀𝑤 ∈ 𝐾 ((𝑈 normOpOLD 𝑊)‘𝑤) ≤ 𝑦 → ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) | 
| 119 | 115, 118 | syl 17 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ (𝑁‘𝑥) ≤ 1)) → (∀𝑤 ∈ 𝐾 ((𝑈 normOpOLD 𝑊)‘𝑤) ≤ 𝑦 → ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) | 
| 120 | 12 | ad2ant2r 747 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → (𝑁‘(𝑇‘𝑥)) ∈ ℝ) | 
| 121 | 120, 120 | remulcld 11291 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → ((𝑁‘(𝑇‘𝑥)) · (𝑁‘(𝑇‘𝑥))) ∈ ℝ) | 
| 122 | 23 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) ∈ (𝑈 BLnOp 𝑊)) | 
| 123 | 17 | cnnvba 30698 | . . . . . . . . . . . . . . . . . . . 20
⊢ ℂ =
(BaseSet‘𝑊) | 
| 124 | 4, 123, 97, 18 | nmblore 30805 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ (𝐹‘𝑥) ∈ (𝑈 BLnOp 𝑊)) → ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ∈ ℝ) | 
| 125 | 3, 95, 124 | mp3an12 1453 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑥) ∈ (𝑈 BLnOp 𝑊) → ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ∈ ℝ) | 
| 126 | 122, 125 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ∈ ℝ) | 
| 127 | 126 | ad2ant2r 747 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ∈ ℝ) | 
| 128 | 127, 120 | remulcld 11291 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → (((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) · (𝑁‘(𝑇‘𝑥))) ∈ ℝ) | 
| 129 |  | simplr 769 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → 𝑦 ∈ ℝ) | 
| 130 | 129, 120 | remulcld 11291 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → (𝑦 · (𝑁‘(𝑇‘𝑥))) ∈ ℝ) | 
| 131 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 = 𝑥 → (𝑇‘𝑧) = (𝑇‘𝑥)) | 
| 132 | 131 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = 𝑥 → (𝑤𝑃(𝑇‘𝑧)) = (𝑤𝑃(𝑇‘𝑥))) | 
| 133 | 132 | mpteq2dv 5244 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = 𝑥 → (𝑤 ∈ 𝑋 ↦ (𝑤𝑃(𝑇‘𝑧))) = (𝑤 ∈ 𝑋 ↦ (𝑤𝑃(𝑇‘𝑥)))) | 
| 134 | 133, 22, 4 | mptfvmpt 7248 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ 𝑋 → (𝐹‘𝑥) = (𝑤 ∈ 𝑋 ↦ (𝑤𝑃(𝑇‘𝑥)))) | 
| 135 | 134 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥) = (𝑤 ∈ 𝑋 ↦ (𝑤𝑃(𝑇‘𝑥)))) | 
| 136 | 135 | fveq1d 6908 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹‘𝑥)‘(𝑇‘𝑥)) = ((𝑤 ∈ 𝑋 ↦ (𝑤𝑃(𝑇‘𝑥)))‘(𝑇‘𝑥))) | 
| 137 |  | oveq1 7438 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = (𝑇‘𝑥) → (𝑤𝑃(𝑇‘𝑥)) = ((𝑇‘𝑥)𝑃(𝑇‘𝑥))) | 
| 138 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ 𝑋 ↦ (𝑤𝑃(𝑇‘𝑥))) = (𝑤 ∈ 𝑋 ↦ (𝑤𝑃(𝑇‘𝑥))) | 
| 139 |  | ovex 7464 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑇‘𝑥)𝑃(𝑇‘𝑥)) ∈ V | 
| 140 | 137, 138,
139 | fvmpt 7016 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑇‘𝑥) ∈ 𝑋 → ((𝑤 ∈ 𝑋 ↦ (𝑤𝑃(𝑇‘𝑥)))‘(𝑇‘𝑥)) = ((𝑇‘𝑥)𝑃(𝑇‘𝑥))) | 
| 141 | 9, 140 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑤 ∈ 𝑋 ↦ (𝑤𝑃(𝑇‘𝑥)))‘(𝑇‘𝑥)) = ((𝑇‘𝑥)𝑃(𝑇‘𝑥))) | 
| 142 | 136, 141 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹‘𝑥)‘(𝑇‘𝑥)) = ((𝑇‘𝑥)𝑃(𝑇‘𝑥))) | 
| 143 | 142 | ad2ant2r 747 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → ((𝐹‘𝑥)‘(𝑇‘𝑥)) = ((𝑇‘𝑥)𝑃(𝑇‘𝑥))) | 
| 144 | 9 | ad2ant2r 747 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → (𝑇‘𝑥) ∈ 𝑋) | 
| 145 | 4, 10, 14 | ipidsq 30729 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑇‘𝑥) ∈ 𝑋) → ((𝑇‘𝑥)𝑃(𝑇‘𝑥)) = ((𝑁‘(𝑇‘𝑥))↑2)) | 
| 146 | 3, 144, 145 | sylancr 587 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → ((𝑇‘𝑥)𝑃(𝑇‘𝑥)) = ((𝑁‘(𝑇‘𝑥))↑2)) | 
| 147 | 143, 146 | eqtrd 2777 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → ((𝐹‘𝑥)‘(𝑇‘𝑥)) = ((𝑁‘(𝑇‘𝑥))↑2)) | 
| 148 | 147 | fveq2d 6910 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → (abs‘((𝐹‘𝑥)‘(𝑇‘𝑥))) = (abs‘((𝑁‘(𝑇‘𝑥))↑2))) | 
| 149 |  | resqcl 14164 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁‘(𝑇‘𝑥)) ∈ ℝ → ((𝑁‘(𝑇‘𝑥))↑2) ∈ ℝ) | 
| 150 |  | sqge0 14176 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁‘(𝑇‘𝑥)) ∈ ℝ → 0 ≤ ((𝑁‘(𝑇‘𝑥))↑2)) | 
| 151 | 149, 150 | absidd 15461 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁‘(𝑇‘𝑥)) ∈ ℝ → (abs‘((𝑁‘(𝑇‘𝑥))↑2)) = ((𝑁‘(𝑇‘𝑥))↑2)) | 
| 152 | 120, 151 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → (abs‘((𝑁‘(𝑇‘𝑥))↑2)) = ((𝑁‘(𝑇‘𝑥))↑2)) | 
| 153 | 120 | recnd 11289 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → (𝑁‘(𝑇‘𝑥)) ∈ ℂ) | 
| 154 | 153 | sqvald 14183 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → ((𝑁‘(𝑇‘𝑥))↑2) = ((𝑁‘(𝑇‘𝑥)) · (𝑁‘(𝑇‘𝑥)))) | 
| 155 | 148, 152,
154 | 3eqtrd 2781 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → (abs‘((𝐹‘𝑥)‘(𝑇‘𝑥))) = ((𝑁‘(𝑇‘𝑥)) · (𝑁‘(𝑇‘𝑥)))) | 
| 156 | 122 | ad2ant2r 747 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → (𝐹‘𝑥) ∈ (𝑈 BLnOp 𝑊)) | 
| 157 | 4, 10, 96, 97, 18, 3, 95 | nmblolbi 30819 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘𝑥) ∈ (𝑈 BLnOp 𝑊) ∧ (𝑇‘𝑥) ∈ 𝑋) → (abs‘((𝐹‘𝑥)‘(𝑇‘𝑥))) ≤ (((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) · (𝑁‘(𝑇‘𝑥)))) | 
| 158 | 156, 144,
157 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → (abs‘((𝐹‘𝑥)‘(𝑇‘𝑥))) ≤ (((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) · (𝑁‘(𝑇‘𝑥)))) | 
| 159 | 155, 158 | eqbrtrrd 5167 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → ((𝑁‘(𝑇‘𝑥)) · (𝑁‘(𝑇‘𝑥))) ≤ (((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) · (𝑁‘(𝑇‘𝑥)))) | 
| 160 | 3, 144, 66 | sylancr 587 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → 0 ≤ (𝑁‘(𝑇‘𝑥))) | 
| 161 |  | simprr 773 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦) | 
| 162 | 127, 129,
120, 160, 161 | lemul1ad 12207 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → (((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) · (𝑁‘(𝑇‘𝑥))) ≤ (𝑦 · (𝑁‘(𝑇‘𝑥)))) | 
| 163 | 121, 128,
130, 159, 162 | letrd 11418 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → ((𝑁‘(𝑇‘𝑥)) · (𝑁‘(𝑇‘𝑥))) ≤ (𝑦 · (𝑁‘(𝑇‘𝑥)))) | 
| 164 |  | lemul1 12119 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁‘(𝑇‘𝑥)) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ ((𝑁‘(𝑇‘𝑥)) ∈ ℝ ∧ 0 < (𝑁‘(𝑇‘𝑥)))) → ((𝑁‘(𝑇‘𝑥)) ≤ 𝑦 ↔ ((𝑁‘(𝑇‘𝑥)) · (𝑁‘(𝑇‘𝑥))) ≤ (𝑦 · (𝑁‘(𝑇‘𝑥))))) | 
| 165 | 164 | biimprd 248 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁‘(𝑇‘𝑥)) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ ((𝑁‘(𝑇‘𝑥)) ∈ ℝ ∧ 0 < (𝑁‘(𝑇‘𝑥)))) → (((𝑁‘(𝑇‘𝑥)) · (𝑁‘(𝑇‘𝑥))) ≤ (𝑦 · (𝑁‘(𝑇‘𝑥))) → (𝑁‘(𝑇‘𝑥)) ≤ 𝑦)) | 
| 166 | 165 | 3expia 1122 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁‘(𝑇‘𝑥)) ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((𝑁‘(𝑇‘𝑥)) ∈ ℝ ∧ 0 < (𝑁‘(𝑇‘𝑥))) → (((𝑁‘(𝑇‘𝑥)) · (𝑁‘(𝑇‘𝑥))) ≤ (𝑦 · (𝑁‘(𝑇‘𝑥))) → (𝑁‘(𝑇‘𝑥)) ≤ 𝑦))) | 
| 167 | 166 | expdimp 452 | . . . . . . . . . . . . . . 15
⊢ ((((𝑁‘(𝑇‘𝑥)) ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑁‘(𝑇‘𝑥)) ∈ ℝ) → (0 < (𝑁‘(𝑇‘𝑥)) → (((𝑁‘(𝑇‘𝑥)) · (𝑁‘(𝑇‘𝑥))) ≤ (𝑦 · (𝑁‘(𝑇‘𝑥))) → (𝑁‘(𝑇‘𝑥)) ≤ 𝑦))) | 
| 168 | 120, 129,
120, 167 | syl21anc 838 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → (0 < (𝑁‘(𝑇‘𝑥)) → (((𝑁‘(𝑇‘𝑥)) · (𝑁‘(𝑇‘𝑥))) ≤ (𝑦 · (𝑁‘(𝑇‘𝑥))) → (𝑁‘(𝑇‘𝑥)) ≤ 𝑦))) | 
| 169 | 163, 168 | mpid 44 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → (0 < (𝑁‘(𝑇‘𝑥)) → (𝑁‘(𝑇‘𝑥)) ≤ 𝑦)) | 
| 170 |  | 0red 11264 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → 0 ∈ ℝ) | 
| 171 | 4, 123, 18 | blof 30804 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ (𝐹‘𝑥) ∈ (𝑈 BLnOp 𝑊)) → (𝐹‘𝑥):𝑋⟶ℂ) | 
| 172 | 3, 95, 171 | mp3an12 1453 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑥) ∈ (𝑈 BLnOp 𝑊) → (𝐹‘𝑥):𝑋⟶ℂ) | 
| 173 | 122, 172 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐹‘𝑥):𝑋⟶ℂ) | 
| 174 | 173 | ad2ant2r 747 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → (𝐹‘𝑥):𝑋⟶ℂ) | 
| 175 | 4, 123, 97 | nmooge0 30786 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ (𝐹‘𝑥):𝑋⟶ℂ) → 0 ≤ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥))) | 
| 176 | 3, 95, 175 | mp3an12 1453 | . . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑥):𝑋⟶ℂ → 0 ≤ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥))) | 
| 177 | 174, 176 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → 0 ≤ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥))) | 
| 178 | 170, 127,
129, 177, 161 | letrd 11418 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → 0 ≤ 𝑦) | 
| 179 |  | breq1 5146 | . . . . . . . . . . . . . 14
⊢ (0 =
(𝑁‘(𝑇‘𝑥)) → (0 ≤ 𝑦 ↔ (𝑁‘(𝑇‘𝑥)) ≤ 𝑦)) | 
| 180 | 178, 179 | syl5ibcom 245 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → (0 = (𝑁‘(𝑇‘𝑥)) → (𝑁‘(𝑇‘𝑥)) ≤ 𝑦)) | 
| 181 |  | 0re 11263 | . . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ | 
| 182 |  | leloe 11347 | . . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ ∧ (𝑁‘(𝑇‘𝑥)) ∈ ℝ) → (0 ≤ (𝑁‘(𝑇‘𝑥)) ↔ (0 < (𝑁‘(𝑇‘𝑥)) ∨ 0 = (𝑁‘(𝑇‘𝑥))))) | 
| 183 | 181, 120,
182 | sylancr 587 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → (0 ≤ (𝑁‘(𝑇‘𝑥)) ↔ (0 < (𝑁‘(𝑇‘𝑥)) ∨ 0 = (𝑁‘(𝑇‘𝑥))))) | 
| 184 | 160, 183 | mpbid 232 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → (0 < (𝑁‘(𝑇‘𝑥)) ∨ 0 = (𝑁‘(𝑇‘𝑥)))) | 
| 185 | 169, 180,
184 | mpjaod 861 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦)) → (𝑁‘(𝑇‘𝑥)) ≤ 𝑦) | 
| 186 | 185 | expr 456 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) → (((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦 → (𝑁‘(𝑇‘𝑥)) ≤ 𝑦)) | 
| 187 | 186 | adantrr 717 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ (𝑁‘𝑥) ≤ 1)) → (((𝑈 normOpOLD 𝑊)‘(𝐹‘𝑥)) ≤ 𝑦 → (𝑁‘(𝑇‘𝑥)) ≤ 𝑦)) | 
| 188 | 119, 187 | syld 47 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ (𝑥 ∈ 𝑋 ∧ (𝑁‘𝑥) ≤ 1)) → (∀𝑤 ∈ 𝐾 ((𝑈 normOpOLD 𝑊)‘𝑤) ≤ 𝑦 → (𝑁‘(𝑇‘𝑥)) ≤ 𝑦)) | 
| 189 | 188 | expr 456 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) → ((𝑁‘𝑥) ≤ 1 → (∀𝑤 ∈ 𝐾 ((𝑈 normOpOLD 𝑊)‘𝑤) ≤ 𝑦 → (𝑁‘(𝑇‘𝑥)) ≤ 𝑦))) | 
| 190 | 189 | com23 86 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) → (∀𝑤 ∈ 𝐾 ((𝑈 normOpOLD 𝑊)‘𝑤) ≤ 𝑦 → ((𝑁‘𝑥) ≤ 1 → (𝑁‘(𝑇‘𝑥)) ≤ 𝑦))) | 
| 191 | 190 | ralrimdva 3154 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (∀𝑤 ∈ 𝐾 ((𝑈 normOpOLD 𝑊)‘𝑤) ≤ 𝑦 → ∀𝑥 ∈ 𝑋 ((𝑁‘𝑥) ≤ 1 → (𝑁‘(𝑇‘𝑥)) ≤ 𝑦))) | 
| 192 | 191 | reximdva 3168 | . . . . 5
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑤 ∈ 𝐾 ((𝑈 normOpOLD 𝑊)‘𝑤) ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝑋 ((𝑁‘𝑥) ≤ 1 → (𝑁‘(𝑇‘𝑥)) ≤ 𝑦))) | 
| 193 | 101, 192 | mpd 15 | . . . 4
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝑋 ((𝑁‘𝑥) ≤ 1 → (𝑁‘(𝑇‘𝑥)) ≤ 𝑦)) | 
| 194 |  | eqid 2737 | . . . . . 6
⊢ (𝑈 normOpOLD 𝑈) = (𝑈 normOpOLD 𝑈) | 
| 195 | 4, 4, 10, 10, 194, 3, 3 | nmobndi 30794 | . . . . 5
⊢ (𝑇:𝑋⟶𝑋 → (((𝑈 normOpOLD 𝑈)‘𝑇) ∈ ℝ ↔ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝑋 ((𝑁‘𝑥) ≤ 1 → (𝑁‘(𝑇‘𝑥)) ≤ 𝑦))) | 
| 196 | 8, 195 | syl 17 | . . . 4
⊢ (𝜑 → (((𝑈 normOpOLD 𝑈)‘𝑇) ∈ ℝ ↔ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝑋 ((𝑁‘𝑥) ≤ 1 → (𝑁‘(𝑇‘𝑥)) ≤ 𝑦))) | 
| 197 | 193, 196 | mpbird 257 | . . 3
⊢ (𝜑 → ((𝑈 normOpOLD 𝑈)‘𝑇) ∈ ℝ) | 
| 198 |  | ltpnf 13162 | . . 3
⊢ (((𝑈 normOpOLD 𝑈)‘𝑇) ∈ ℝ → ((𝑈 normOpOLD 𝑈)‘𝑇) < +∞) | 
| 199 | 197, 198 | syl 17 | . 2
⊢ (𝜑 → ((𝑈 normOpOLD 𝑈)‘𝑇) < +∞) | 
| 200 |  | htth.4 | . . . 4
⊢ 𝐵 = (𝑈 BLnOp 𝑈) | 
| 201 | 194, 5, 200 | isblo 30801 | . . 3
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑈 ∈ NrmCVec) → (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ ((𝑈 normOpOLD 𝑈)‘𝑇) < +∞))) | 
| 202 | 3, 3, 201 | mp2an 692 | . 2
⊢ (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ ((𝑈 normOpOLD 𝑈)‘𝑇) < +∞)) | 
| 203 | 1, 199, 202 | sylanbrc 583 | 1
⊢ (𝜑 → 𝑇 ∈ 𝐵) |