MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  htthlem Structured version   Visualization version   GIF version

Theorem htthlem 26946
Description: Lemma for htth 26947. The collection 𝐾, which consists of functions 𝐹(𝑧)(𝑤) = ⟨𝑤𝑇(𝑧)⟩ = ⟨𝑇(𝑤) ∣ 𝑧 for each 𝑧 in the unit ball, is a collection of bounded linear functions by ipblnfi 26873, so by the Uniform Boundedness theorem ubth 26891, there is a uniform bound 𝑦 on 𝐹(𝑥) ∥ for all 𝑥 in the unit ball. Then 𝑇(𝑥) ∣ ↑2 = ⟨𝑇(𝑥) ∣ 𝑇(𝑥)⟩ = 𝐹(𝑥)( 𝑇(𝑥)) ≤ 𝑦𝑇(𝑥) ∣, so 𝑇(𝑥) ∣ ≤ 𝑦 and 𝑇 is bounded. (Contributed by NM, 11-Jan-2008.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
htth.1 𝑋 = (BaseSet‘𝑈)
htth.2 𝑃 = (·𝑖OLD𝑈)
htth.3 𝐿 = (𝑈 LnOp 𝑈)
htth.4 𝐵 = (𝑈 BLnOp 𝑈)
htthlem.5 𝑁 = (normCV𝑈)
htthlem.6 𝑈 ∈ CHilOLD
htthlem.7 𝑊 = ⟨⟨ + , · ⟩, abs⟩
htthlem.8 (𝜑𝑇𝐿)
htthlem.9 (𝜑 → ∀𝑥𝑋𝑦𝑋 (𝑥𝑃(𝑇𝑦)) = ((𝑇𝑥)𝑃𝑦))
htthlem.10 𝐹 = (𝑧𝑋 ↦ (𝑤𝑋 ↦ (𝑤𝑃(𝑇𝑧))))
htthlem.11 𝐾 = (𝐹 “ {𝑧𝑋 ∣ (𝑁𝑧) ≤ 1})
Assertion
Ref Expression
htthlem (𝜑𝑇𝐵)
Distinct variable groups:   𝑦,𝑤,𝐹   𝑥,𝑤,𝑧,𝐾,𝑦   𝑤,𝑁,𝑥,𝑦,𝑧   𝑤,𝑃,𝑧   𝑤,𝑊,𝑥,𝑦,𝑧   𝜑,𝑤,𝑥,𝑦,𝑧   𝑤,𝑇,𝑥,𝑦,𝑧   𝑤,𝑈,𝑥,𝑦,𝑧   𝑤,𝑋,𝑥,𝑦,𝑧
Allowed substitution hints:   𝐵(𝑥,𝑦,𝑧,𝑤)   𝑃(𝑥,𝑦)   𝐹(𝑥,𝑧)   𝐿(𝑥,𝑦,𝑧,𝑤)

Proof of Theorem htthlem
StepHypRef Expression
1 htthlem.8 . 2 (𝜑𝑇𝐿)
2 htthlem.6 . . . . . . . . . 10 𝑈 ∈ CHilOLD
32hlnvi 26920 . . . . . . . . 9 𝑈 ∈ NrmCVec
4 htth.1 . . . . . . . . . . . . 13 𝑋 = (BaseSet‘𝑈)
5 htth.3 . . . . . . . . . . . . 13 𝐿 = (𝑈 LnOp 𝑈)
64, 4, 5lnof 26772 . . . . . . . . . . . 12 ((𝑈 ∈ NrmCVec ∧ 𝑈 ∈ NrmCVec ∧ 𝑇𝐿) → 𝑇:𝑋𝑋)
73, 3, 6mp3an12 1405 . . . . . . . . . . 11 (𝑇𝐿𝑇:𝑋𝑋)
81, 7syl 17 . . . . . . . . . 10 (𝜑𝑇:𝑋𝑋)
98ffvelrnda 6151 . . . . . . . . 9 ((𝜑𝑥𝑋) → (𝑇𝑥) ∈ 𝑋)
10 htthlem.5 . . . . . . . . . 10 𝑁 = (normCV𝑈)
114, 10nvcl 26664 . . . . . . . . 9 ((𝑈 ∈ NrmCVec ∧ (𝑇𝑥) ∈ 𝑋) → (𝑁‘(𝑇𝑥)) ∈ ℝ)
123, 9, 11sylancr 693 . . . . . . . 8 ((𝜑𝑥𝑋) → (𝑁‘(𝑇𝑥)) ∈ ℝ)
138ffvelrnda 6151 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑋) → (𝑇𝑧) ∈ 𝑋)
14 htth.2 . . . . . . . . . . . . . . . . 17 𝑃 = (·𝑖OLD𝑈)
15 hlph 26917 . . . . . . . . . . . . . . . . . 18 (𝑈 ∈ CHilOLD𝑈 ∈ CPreHilOLD)
162, 15ax-mp 5 . . . . . . . . . . . . . . . . 17 𝑈 ∈ CPreHilOLD
17 htthlem.7 . . . . . . . . . . . . . . . . 17 𝑊 = ⟨⟨ + , · ⟩, abs⟩
18 eqid 2514 . . . . . . . . . . . . . . . . 17 (𝑈 BLnOp 𝑊) = (𝑈 BLnOp 𝑊)
19 eqid 2514 . . . . . . . . . . . . . . . . 17 (𝑤𝑋 ↦ (𝑤𝑃(𝑇𝑧))) = (𝑤𝑋 ↦ (𝑤𝑃(𝑇𝑧)))
204, 14, 16, 17, 18, 19ipblnfi 26873 . . . . . . . . . . . . . . . 16 ((𝑇𝑧) ∈ 𝑋 → (𝑤𝑋 ↦ (𝑤𝑃(𝑇𝑧))) ∈ (𝑈 BLnOp 𝑊))
2113, 20syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑋) → (𝑤𝑋 ↦ (𝑤𝑃(𝑇𝑧))) ∈ (𝑈 BLnOp 𝑊))
22 htthlem.10 . . . . . . . . . . . . . . 15 𝐹 = (𝑧𝑋 ↦ (𝑤𝑋 ↦ (𝑤𝑃(𝑇𝑧))))
2321, 22fmptd 6176 . . . . . . . . . . . . . 14 (𝜑𝐹:𝑋⟶(𝑈 BLnOp 𝑊))
24 ffun 5846 . . . . . . . . . . . . . 14 (𝐹:𝑋⟶(𝑈 BLnOp 𝑊) → Fun 𝐹)
2523, 24syl 17 . . . . . . . . . . . . 13 (𝜑 → Fun 𝐹)
2625adantr 479 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → Fun 𝐹)
27 id 22 . . . . . . . . . . . . 13 (𝑤𝐾𝑤𝐾)
28 htthlem.11 . . . . . . . . . . . . 13 𝐾 = (𝐹 “ {𝑧𝑋 ∣ (𝑁𝑧) ≤ 1})
2927, 28syl6eleq 2602 . . . . . . . . . . . 12 (𝑤𝐾𝑤 ∈ (𝐹 “ {𝑧𝑋 ∣ (𝑁𝑧) ≤ 1}))
30 fvelima 6042 . . . . . . . . . . . 12 ((Fun 𝐹𝑤 ∈ (𝐹 “ {𝑧𝑋 ∣ (𝑁𝑧) ≤ 1})) → ∃𝑦 ∈ {𝑧𝑋 ∣ (𝑁𝑧) ≤ 1} (𝐹𝑦) = 𝑤)
3126, 29, 30syl2an 492 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑤𝐾) → ∃𝑦 ∈ {𝑧𝑋 ∣ (𝑁𝑧) ≤ 1} (𝐹𝑦) = 𝑤)
3231ex 448 . . . . . . . . . 10 ((𝜑𝑥𝑋) → (𝑤𝐾 → ∃𝑦 ∈ {𝑧𝑋 ∣ (𝑁𝑧) ≤ 1} (𝐹𝑦) = 𝑤))
33 fveq2 5987 . . . . . . . . . . . . . . 15 (𝑧 = 𝑦 → (𝑁𝑧) = (𝑁𝑦))
3433breq1d 4491 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → ((𝑁𝑧) ≤ 1 ↔ (𝑁𝑦) ≤ 1))
3534elrab 3235 . . . . . . . . . . . . 13 (𝑦 ∈ {𝑧𝑋 ∣ (𝑁𝑧) ≤ 1} ↔ (𝑦𝑋 ∧ (𝑁𝑦) ≤ 1))
36 fveq2 5987 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑦 → (𝑇𝑧) = (𝑇𝑦))
3736oveq2d 6442 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑦 → (𝑤𝑃(𝑇𝑧)) = (𝑤𝑃(𝑇𝑦)))
3837mpteq2dv 4571 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑦 → (𝑤𝑋 ↦ (𝑤𝑃(𝑇𝑧))) = (𝑤𝑋 ↦ (𝑤𝑃(𝑇𝑦))))
394hlex 26926 . . . . . . . . . . . . . . . . . . . . 21 𝑋 ∈ V
4039mptex 6267 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝑋 ↦ (𝑤𝑃(𝑇𝑦))) ∈ V
4138, 22, 40fvmpt 6075 . . . . . . . . . . . . . . . . . . 19 (𝑦𝑋 → (𝐹𝑦) = (𝑤𝑋 ↦ (𝑤𝑃(𝑇𝑦))))
4241fveq1d 5989 . . . . . . . . . . . . . . . . . 18 (𝑦𝑋 → ((𝐹𝑦)‘𝑥) = ((𝑤𝑋 ↦ (𝑤𝑃(𝑇𝑦)))‘𝑥))
43 oveq1 6433 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑥 → (𝑤𝑃(𝑇𝑦)) = (𝑥𝑃(𝑇𝑦)))
44 eqid 2514 . . . . . . . . . . . . . . . . . . 19 (𝑤𝑋 ↦ (𝑤𝑃(𝑇𝑦))) = (𝑤𝑋 ↦ (𝑤𝑃(𝑇𝑦)))
45 ovex 6454 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑃(𝑇𝑦)) ∈ V
4643, 44, 45fvmpt 6075 . . . . . . . . . . . . . . . . . 18 (𝑥𝑋 → ((𝑤𝑋 ↦ (𝑤𝑃(𝑇𝑦)))‘𝑥) = (𝑥𝑃(𝑇𝑦)))
4742, 46sylan9eqr 2570 . . . . . . . . . . . . . . . . 17 ((𝑥𝑋𝑦𝑋) → ((𝐹𝑦)‘𝑥) = (𝑥𝑃(𝑇𝑦)))
4847ad2ant2lr 779 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑋) ∧ (𝑦𝑋 ∧ (𝑁𝑦) ≤ 1)) → ((𝐹𝑦)‘𝑥) = (𝑥𝑃(𝑇𝑦)))
49 htthlem.9 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑥𝑋𝑦𝑋 (𝑥𝑃(𝑇𝑦)) = ((𝑇𝑥)𝑃𝑦))
50 rsp2 2824 . . . . . . . . . . . . . . . . . . 19 (∀𝑥𝑋𝑦𝑋 (𝑥𝑃(𝑇𝑦)) = ((𝑇𝑥)𝑃𝑦) → ((𝑥𝑋𝑦𝑋) → (𝑥𝑃(𝑇𝑦)) = ((𝑇𝑥)𝑃𝑦)))
5149, 50syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑥𝑋𝑦𝑋) → (𝑥𝑃(𝑇𝑦)) = ((𝑇𝑥)𝑃𝑦)))
5251impl 647 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑋) ∧ 𝑦𝑋) → (𝑥𝑃(𝑇𝑦)) = ((𝑇𝑥)𝑃𝑦))
5352adantrr 748 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑋) ∧ (𝑦𝑋 ∧ (𝑁𝑦) ≤ 1)) → (𝑥𝑃(𝑇𝑦)) = ((𝑇𝑥)𝑃𝑦))
5448, 53eqtrd 2548 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ (𝑦𝑋 ∧ (𝑁𝑦) ≤ 1)) → ((𝐹𝑦)‘𝑥) = ((𝑇𝑥)𝑃𝑦))
5554fveq2d 5991 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑋) ∧ (𝑦𝑋 ∧ (𝑁𝑦) ≤ 1)) → (abs‘((𝐹𝑦)‘𝑥)) = (abs‘((𝑇𝑥)𝑃𝑦)))
56 simpl 471 . . . . . . . . . . . . . . . . 17 ((𝑦𝑋 ∧ (𝑁𝑦) ≤ 1) → 𝑦𝑋)
574, 14dipcl 26727 . . . . . . . . . . . . . . . . . 18 ((𝑈 ∈ NrmCVec ∧ (𝑇𝑥) ∈ 𝑋𝑦𝑋) → ((𝑇𝑥)𝑃𝑦) ∈ ℂ)
583, 57mp3an1 1402 . . . . . . . . . . . . . . . . 17 (((𝑇𝑥) ∈ 𝑋𝑦𝑋) → ((𝑇𝑥)𝑃𝑦) ∈ ℂ)
599, 56, 58syl2an 492 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑋) ∧ (𝑦𝑋 ∧ (𝑁𝑦) ≤ 1)) → ((𝑇𝑥)𝑃𝑦) ∈ ℂ)
6059abscld 13882 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ (𝑦𝑋 ∧ (𝑁𝑦) ≤ 1)) → (abs‘((𝑇𝑥)𝑃𝑦)) ∈ ℝ)
6112adantr 479 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑋) ∧ (𝑦𝑋 ∧ (𝑁𝑦) ≤ 1)) → (𝑁‘(𝑇𝑥)) ∈ ℝ)
624, 10nvcl 26664 . . . . . . . . . . . . . . . . . 18 ((𝑈 ∈ NrmCVec ∧ 𝑦𝑋) → (𝑁𝑦) ∈ ℝ)
633, 62mpan 701 . . . . . . . . . . . . . . . . 17 (𝑦𝑋 → (𝑁𝑦) ∈ ℝ)
6463ad2antrl 759 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑋) ∧ (𝑦𝑋 ∧ (𝑁𝑦) ≤ 1)) → (𝑁𝑦) ∈ ℝ)
6561, 64remulcld 9825 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ (𝑦𝑋 ∧ (𝑁𝑦) ≤ 1)) → ((𝑁‘(𝑇𝑥)) · (𝑁𝑦)) ∈ ℝ)
664, 10, 14, 16sii 26871 . . . . . . . . . . . . . . . 16 (((𝑇𝑥) ∈ 𝑋𝑦𝑋) → (abs‘((𝑇𝑥)𝑃𝑦)) ≤ ((𝑁‘(𝑇𝑥)) · (𝑁𝑦)))
679, 56, 66syl2an 492 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ (𝑦𝑋 ∧ (𝑁𝑦) ≤ 1)) → (abs‘((𝑇𝑥)𝑃𝑦)) ≤ ((𝑁‘(𝑇𝑥)) · (𝑁𝑦)))
68 1red 9810 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑋) ∧ (𝑦𝑋 ∧ (𝑁𝑦) ≤ 1)) → 1 ∈ ℝ)
694, 10nvge0 26679 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 ∈ NrmCVec ∧ (𝑇𝑥) ∈ 𝑋) → 0 ≤ (𝑁‘(𝑇𝑥)))
703, 9, 69sylancr 693 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥𝑋) → 0 ≤ (𝑁‘(𝑇𝑥)))
7112, 70jca 552 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝑋) → ((𝑁‘(𝑇𝑥)) ∈ ℝ ∧ 0 ≤ (𝑁‘(𝑇𝑥))))
7271adantr 479 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑋) ∧ (𝑦𝑋 ∧ (𝑁𝑦) ≤ 1)) → ((𝑁‘(𝑇𝑥)) ∈ ℝ ∧ 0 ≤ (𝑁‘(𝑇𝑥))))
73 simprr 791 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑋) ∧ (𝑦𝑋 ∧ (𝑁𝑦) ≤ 1)) → (𝑁𝑦) ≤ 1)
74 lemul2a 10627 . . . . . . . . . . . . . . . . 17 ((((𝑁𝑦) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝑁‘(𝑇𝑥)) ∈ ℝ ∧ 0 ≤ (𝑁‘(𝑇𝑥)))) ∧ (𝑁𝑦) ≤ 1) → ((𝑁‘(𝑇𝑥)) · (𝑁𝑦)) ≤ ((𝑁‘(𝑇𝑥)) · 1))
7564, 68, 72, 73, 74syl31anc 1320 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑋) ∧ (𝑦𝑋 ∧ (𝑁𝑦) ≤ 1)) → ((𝑁‘(𝑇𝑥)) · (𝑁𝑦)) ≤ ((𝑁‘(𝑇𝑥)) · 1))
7661recnd 9823 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑋) ∧ (𝑦𝑋 ∧ (𝑁𝑦) ≤ 1)) → (𝑁‘(𝑇𝑥)) ∈ ℂ)
7776mulid1d 9812 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑋) ∧ (𝑦𝑋 ∧ (𝑁𝑦) ≤ 1)) → ((𝑁‘(𝑇𝑥)) · 1) = (𝑁‘(𝑇𝑥)))
7875, 77breqtrd 4507 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑋) ∧ (𝑦𝑋 ∧ (𝑁𝑦) ≤ 1)) → ((𝑁‘(𝑇𝑥)) · (𝑁𝑦)) ≤ (𝑁‘(𝑇𝑥)))
7960, 65, 61, 67, 78letrd 9945 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑋) ∧ (𝑦𝑋 ∧ (𝑁𝑦) ≤ 1)) → (abs‘((𝑇𝑥)𝑃𝑦)) ≤ (𝑁‘(𝑇𝑥)))
8055, 79eqbrtrd 4503 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ (𝑦𝑋 ∧ (𝑁𝑦) ≤ 1)) → (abs‘((𝐹𝑦)‘𝑥)) ≤ (𝑁‘(𝑇𝑥)))
8135, 80sylan2b 490 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑦 ∈ {𝑧𝑋 ∣ (𝑁𝑧) ≤ 1}) → (abs‘((𝐹𝑦)‘𝑥)) ≤ (𝑁‘(𝑇𝑥)))
82 fveq1 5986 . . . . . . . . . . . . . 14 ((𝐹𝑦) = 𝑤 → ((𝐹𝑦)‘𝑥) = (𝑤𝑥))
8382fveq2d 5991 . . . . . . . . . . . . 13 ((𝐹𝑦) = 𝑤 → (abs‘((𝐹𝑦)‘𝑥)) = (abs‘(𝑤𝑥)))
8483breq1d 4491 . . . . . . . . . . . 12 ((𝐹𝑦) = 𝑤 → ((abs‘((𝐹𝑦)‘𝑥)) ≤ (𝑁‘(𝑇𝑥)) ↔ (abs‘(𝑤𝑥)) ≤ (𝑁‘(𝑇𝑥))))
8581, 84syl5ibcom 233 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑦 ∈ {𝑧𝑋 ∣ (𝑁𝑧) ≤ 1}) → ((𝐹𝑦) = 𝑤 → (abs‘(𝑤𝑥)) ≤ (𝑁‘(𝑇𝑥))))
8685rexlimdva 2917 . . . . . . . . . 10 ((𝜑𝑥𝑋) → (∃𝑦 ∈ {𝑧𝑋 ∣ (𝑁𝑧) ≤ 1} (𝐹𝑦) = 𝑤 → (abs‘(𝑤𝑥)) ≤ (𝑁‘(𝑇𝑥))))
8732, 86syld 45 . . . . . . . . 9 ((𝜑𝑥𝑋) → (𝑤𝐾 → (abs‘(𝑤𝑥)) ≤ (𝑁‘(𝑇𝑥))))
8887ralrimiv 2852 . . . . . . . 8 ((𝜑𝑥𝑋) → ∀𝑤𝐾 (abs‘(𝑤𝑥)) ≤ (𝑁‘(𝑇𝑥)))
89 breq2 4485 . . . . . . . . . 10 (𝑧 = (𝑁‘(𝑇𝑥)) → ((abs‘(𝑤𝑥)) ≤ 𝑧 ↔ (abs‘(𝑤𝑥)) ≤ (𝑁‘(𝑇𝑥))))
9089ralbidv 2873 . . . . . . . . 9 (𝑧 = (𝑁‘(𝑇𝑥)) → (∀𝑤𝐾 (abs‘(𝑤𝑥)) ≤ 𝑧 ↔ ∀𝑤𝐾 (abs‘(𝑤𝑥)) ≤ (𝑁‘(𝑇𝑥))))
9190rspcev 3186 . . . . . . . 8 (((𝑁‘(𝑇𝑥)) ∈ ℝ ∧ ∀𝑤𝐾 (abs‘(𝑤𝑥)) ≤ (𝑁‘(𝑇𝑥))) → ∃𝑧 ∈ ℝ ∀𝑤𝐾 (abs‘(𝑤𝑥)) ≤ 𝑧)
9212, 88, 91syl2anc 690 . . . . . . 7 ((𝜑𝑥𝑋) → ∃𝑧 ∈ ℝ ∀𝑤𝐾 (abs‘(𝑤𝑥)) ≤ 𝑧)
9392ralrimiva 2853 . . . . . 6 (𝜑 → ∀𝑥𝑋𝑧 ∈ ℝ ∀𝑤𝐾 (abs‘(𝑤𝑥)) ≤ 𝑧)
94 imassrn 5287 . . . . . . . . 9 (𝐹 “ {𝑧𝑋 ∣ (𝑁𝑧) ≤ 1}) ⊆ ran 𝐹
9528, 94eqsstri 3502 . . . . . . . 8 𝐾 ⊆ ran 𝐹
96 frn 5851 . . . . . . . . 9 (𝐹:𝑋⟶(𝑈 BLnOp 𝑊) → ran 𝐹 ⊆ (𝑈 BLnOp 𝑊))
9723, 96syl 17 . . . . . . . 8 (𝜑 → ran 𝐹 ⊆ (𝑈 BLnOp 𝑊))
9895, 97syl5ss 3483 . . . . . . 7 (𝜑𝐾 ⊆ (𝑈 BLnOp 𝑊))
99 hlobn 26916 . . . . . . . . 9 (𝑈 ∈ CHilOLD𝑈 ∈ CBan)
1002, 99ax-mp 5 . . . . . . . 8 𝑈 ∈ CBan
10117cnnv 26684 . . . . . . . 8 𝑊 ∈ NrmCVec
10217cnnvnm 26689 . . . . . . . . 9 abs = (normCV𝑊)
103 eqid 2514 . . . . . . . . 9 (𝑈 normOpOLD 𝑊) = (𝑈 normOpOLD 𝑊)
1044, 102, 103ubth 26891 . . . . . . . 8 ((𝑈 ∈ CBan ∧ 𝑊 ∈ NrmCVec ∧ 𝐾 ⊆ (𝑈 BLnOp 𝑊)) → (∀𝑥𝑋𝑧 ∈ ℝ ∀𝑤𝐾 (abs‘(𝑤𝑥)) ≤ 𝑧 ↔ ∃𝑦 ∈ ℝ ∀𝑤𝐾 ((𝑈 normOpOLD 𝑊)‘𝑤) ≤ 𝑦))
105100, 101, 104mp3an12 1405 . . . . . . 7 (𝐾 ⊆ (𝑈 BLnOp 𝑊) → (∀𝑥𝑋𝑧 ∈ ℝ ∀𝑤𝐾 (abs‘(𝑤𝑥)) ≤ 𝑧 ↔ ∃𝑦 ∈ ℝ ∀𝑤𝐾 ((𝑈 normOpOLD 𝑊)‘𝑤) ≤ 𝑦))
10698, 105syl 17 . . . . . 6 (𝜑 → (∀𝑥𝑋𝑧 ∈ ℝ ∀𝑤𝐾 (abs‘(𝑤𝑥)) ≤ 𝑧 ↔ ∃𝑦 ∈ ℝ ∀𝑤𝐾 ((𝑈 normOpOLD 𝑊)‘𝑤) ≤ 𝑦))
10793, 106mpbid 220 . . . . 5 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑤𝐾 ((𝑈 normOpOLD 𝑊)‘𝑤) ≤ 𝑦)
108 simpr 475 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ (𝑁𝑥) ≤ 1)) → (𝑥𝑋 ∧ (𝑁𝑥) ≤ 1))
109 fveq2 5987 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑥 → (𝑁𝑧) = (𝑁𝑥))
110109breq1d 4491 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥 → ((𝑁𝑧) ≤ 1 ↔ (𝑁𝑥) ≤ 1))
111110elrab 3235 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑧𝑋 ∣ (𝑁𝑧) ≤ 1} ↔ (𝑥𝑋 ∧ (𝑁𝑥) ≤ 1))
112108, 111sylibr 222 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ (𝑁𝑥) ≤ 1)) → 𝑥 ∈ {𝑧𝑋 ∣ (𝑁𝑧) ≤ 1})
11322, 21dmmptd 5822 . . . . . . . . . . . . . . . . 17 (𝜑 → dom 𝐹 = 𝑋)
114113eleq2d 2577 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥 ∈ dom 𝐹𝑥𝑋))
115114biimpar 500 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑋) → 𝑥 ∈ dom 𝐹)
116 funfvima 6273 . . . . . . . . . . . . . . . 16 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (𝑥 ∈ {𝑧𝑋 ∣ (𝑁𝑧) ≤ 1} → (𝐹𝑥) ∈ (𝐹 “ {𝑧𝑋 ∣ (𝑁𝑧) ≤ 1})))
11725, 116sylan 486 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ dom 𝐹) → (𝑥 ∈ {𝑧𝑋 ∣ (𝑁𝑧) ≤ 1} → (𝐹𝑥) ∈ (𝐹 “ {𝑧𝑋 ∣ (𝑁𝑧) ≤ 1})))
118115, 117syldan 485 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → (𝑥 ∈ {𝑧𝑋 ∣ (𝑁𝑧) ≤ 1} → (𝐹𝑥) ∈ (𝐹 “ {𝑧𝑋 ∣ (𝑁𝑧) ≤ 1})))
119118ad2ant2r 778 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ (𝑁𝑥) ≤ 1)) → (𝑥 ∈ {𝑧𝑋 ∣ (𝑁𝑧) ≤ 1} → (𝐹𝑥) ∈ (𝐹 “ {𝑧𝑋 ∣ (𝑁𝑧) ≤ 1})))
120112, 119mpd 15 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ (𝑁𝑥) ≤ 1)) → (𝐹𝑥) ∈ (𝐹 “ {𝑧𝑋 ∣ (𝑁𝑧) ≤ 1}))
121120, 28syl6eleqr 2603 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ (𝑁𝑥) ≤ 1)) → (𝐹𝑥) ∈ 𝐾)
122 fveq2 5987 . . . . . . . . . . . . 13 (𝑤 = (𝐹𝑥) → ((𝑈 normOpOLD 𝑊)‘𝑤) = ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)))
123122breq1d 4491 . . . . . . . . . . . 12 (𝑤 = (𝐹𝑥) → (((𝑈 normOpOLD 𝑊)‘𝑤) ≤ 𝑦 ↔ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦))
124123rspcv 3182 . . . . . . . . . . 11 ((𝐹𝑥) ∈ 𝐾 → (∀𝑤𝐾 ((𝑈 normOpOLD 𝑊)‘𝑤) ≤ 𝑦 → ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦))
125121, 124syl 17 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ (𝑁𝑥) ≤ 1)) → (∀𝑤𝐾 ((𝑈 normOpOLD 𝑊)‘𝑤) ≤ 𝑦 → ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦))
12612ad2ant2r 778 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → (𝑁‘(𝑇𝑥)) ∈ ℝ)
127126, 126remulcld 9825 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → ((𝑁‘(𝑇𝑥)) · (𝑁‘(𝑇𝑥))) ∈ ℝ)
12823ffvelrnda 6151 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥𝑋) → (𝐹𝑥) ∈ (𝑈 BLnOp 𝑊))
12917cnnvba 26686 . . . . . . . . . . . . . . . . . . . 20 ℂ = (BaseSet‘𝑊)
1304, 129, 103, 18nmblore 26803 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ (𝐹𝑥) ∈ (𝑈 BLnOp 𝑊)) → ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ∈ ℝ)
1313, 101, 130mp3an12 1405 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑥) ∈ (𝑈 BLnOp 𝑊) → ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ∈ ℝ)
132128, 131syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝑋) → ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ∈ ℝ)
133132ad2ant2r 778 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ∈ ℝ)
134133, 126remulcld 9825 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → (((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) · (𝑁‘(𝑇𝑥))) ∈ ℝ)
135 simplr 787 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → 𝑦 ∈ ℝ)
136135, 126remulcld 9825 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → (𝑦 · (𝑁‘(𝑇𝑥))) ∈ ℝ)
137 fveq2 5987 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = 𝑥 → (𝑇𝑧) = (𝑇𝑥))
138137oveq2d 6442 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 = 𝑥 → (𝑤𝑃(𝑇𝑧)) = (𝑤𝑃(𝑇𝑥)))
139138mpteq2dv 4571 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = 𝑥 → (𝑤𝑋 ↦ (𝑤𝑃(𝑇𝑧))) = (𝑤𝑋 ↦ (𝑤𝑃(𝑇𝑥))))
14039mptex 6267 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤𝑋 ↦ (𝑤𝑃(𝑇𝑥))) ∈ V
141139, 22, 140fvmpt 6075 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥𝑋 → (𝐹𝑥) = (𝑤𝑋 ↦ (𝑤𝑃(𝑇𝑥))))
142141adantl 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥𝑋) → (𝐹𝑥) = (𝑤𝑋 ↦ (𝑤𝑃(𝑇𝑥))))
143142fveq1d 5989 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥𝑋) → ((𝐹𝑥)‘(𝑇𝑥)) = ((𝑤𝑋 ↦ (𝑤𝑃(𝑇𝑥)))‘(𝑇𝑥)))
144 oveq1 6433 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = (𝑇𝑥) → (𝑤𝑃(𝑇𝑥)) = ((𝑇𝑥)𝑃(𝑇𝑥)))
145 eqid 2514 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤𝑋 ↦ (𝑤𝑃(𝑇𝑥))) = (𝑤𝑋 ↦ (𝑤𝑃(𝑇𝑥)))
146 ovex 6454 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑇𝑥)𝑃(𝑇𝑥)) ∈ V
147144, 145, 146fvmpt 6075 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑇𝑥) ∈ 𝑋 → ((𝑤𝑋 ↦ (𝑤𝑃(𝑇𝑥)))‘(𝑇𝑥)) = ((𝑇𝑥)𝑃(𝑇𝑥)))
1489, 147syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥𝑋) → ((𝑤𝑋 ↦ (𝑤𝑃(𝑇𝑥)))‘(𝑇𝑥)) = ((𝑇𝑥)𝑃(𝑇𝑥)))
149143, 148eqtrd 2548 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥𝑋) → ((𝐹𝑥)‘(𝑇𝑥)) = ((𝑇𝑥)𝑃(𝑇𝑥)))
150149ad2ant2r 778 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → ((𝐹𝑥)‘(𝑇𝑥)) = ((𝑇𝑥)𝑃(𝑇𝑥)))
1519ad2ant2r 778 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → (𝑇𝑥) ∈ 𝑋)
1524, 10, 14ipidsq 26725 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 ∈ NrmCVec ∧ (𝑇𝑥) ∈ 𝑋) → ((𝑇𝑥)𝑃(𝑇𝑥)) = ((𝑁‘(𝑇𝑥))↑2))
1533, 151, 152sylancr 693 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → ((𝑇𝑥)𝑃(𝑇𝑥)) = ((𝑁‘(𝑇𝑥))↑2))
154150, 153eqtrd 2548 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → ((𝐹𝑥)‘(𝑇𝑥)) = ((𝑁‘(𝑇𝑥))↑2))
155154fveq2d 5991 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → (abs‘((𝐹𝑥)‘(𝑇𝑥))) = (abs‘((𝑁‘(𝑇𝑥))↑2)))
156 resqcl 12661 . . . . . . . . . . . . . . . . . . 19 ((𝑁‘(𝑇𝑥)) ∈ ℝ → ((𝑁‘(𝑇𝑥))↑2) ∈ ℝ)
157 sqge0 12670 . . . . . . . . . . . . . . . . . . 19 ((𝑁‘(𝑇𝑥)) ∈ ℝ → 0 ≤ ((𝑁‘(𝑇𝑥))↑2))
158156, 157absidd 13868 . . . . . . . . . . . . . . . . . 18 ((𝑁‘(𝑇𝑥)) ∈ ℝ → (abs‘((𝑁‘(𝑇𝑥))↑2)) = ((𝑁‘(𝑇𝑥))↑2))
159126, 158syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → (abs‘((𝑁‘(𝑇𝑥))↑2)) = ((𝑁‘(𝑇𝑥))↑2))
160126recnd 9823 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → (𝑁‘(𝑇𝑥)) ∈ ℂ)
161160sqvald 12735 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → ((𝑁‘(𝑇𝑥))↑2) = ((𝑁‘(𝑇𝑥)) · (𝑁‘(𝑇𝑥))))
162155, 159, 1613eqtrd 2552 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → (abs‘((𝐹𝑥)‘(𝑇𝑥))) = ((𝑁‘(𝑇𝑥)) · (𝑁‘(𝑇𝑥))))
163128ad2ant2r 778 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → (𝐹𝑥) ∈ (𝑈 BLnOp 𝑊))
1644, 10, 102, 103, 18, 3, 101nmblolbi 26817 . . . . . . . . . . . . . . . . 17 (((𝐹𝑥) ∈ (𝑈 BLnOp 𝑊) ∧ (𝑇𝑥) ∈ 𝑋) → (abs‘((𝐹𝑥)‘(𝑇𝑥))) ≤ (((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) · (𝑁‘(𝑇𝑥))))
165163, 151, 164syl2anc 690 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → (abs‘((𝐹𝑥)‘(𝑇𝑥))) ≤ (((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) · (𝑁‘(𝑇𝑥))))
166162, 165eqbrtrrd 4505 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → ((𝑁‘(𝑇𝑥)) · (𝑁‘(𝑇𝑥))) ≤ (((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) · (𝑁‘(𝑇𝑥))))
1673, 151, 69sylancr 693 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → 0 ≤ (𝑁‘(𝑇𝑥)))
168 simprr 791 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)
169133, 135, 126, 167, 168lemul1ad 10713 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → (((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) · (𝑁‘(𝑇𝑥))) ≤ (𝑦 · (𝑁‘(𝑇𝑥))))
170127, 134, 136, 166, 169letrd 9945 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → ((𝑁‘(𝑇𝑥)) · (𝑁‘(𝑇𝑥))) ≤ (𝑦 · (𝑁‘(𝑇𝑥))))
171 lemul1 10624 . . . . . . . . . . . . . . . . . 18 (((𝑁‘(𝑇𝑥)) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ ((𝑁‘(𝑇𝑥)) ∈ ℝ ∧ 0 < (𝑁‘(𝑇𝑥)))) → ((𝑁‘(𝑇𝑥)) ≤ 𝑦 ↔ ((𝑁‘(𝑇𝑥)) · (𝑁‘(𝑇𝑥))) ≤ (𝑦 · (𝑁‘(𝑇𝑥)))))
172171biimprd 236 . . . . . . . . . . . . . . . . 17 (((𝑁‘(𝑇𝑥)) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ ((𝑁‘(𝑇𝑥)) ∈ ℝ ∧ 0 < (𝑁‘(𝑇𝑥)))) → (((𝑁‘(𝑇𝑥)) · (𝑁‘(𝑇𝑥))) ≤ (𝑦 · (𝑁‘(𝑇𝑥))) → (𝑁‘(𝑇𝑥)) ≤ 𝑦))
1731723expia 1258 . . . . . . . . . . . . . . . 16 (((𝑁‘(𝑇𝑥)) ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((𝑁‘(𝑇𝑥)) ∈ ℝ ∧ 0 < (𝑁‘(𝑇𝑥))) → (((𝑁‘(𝑇𝑥)) · (𝑁‘(𝑇𝑥))) ≤ (𝑦 · (𝑁‘(𝑇𝑥))) → (𝑁‘(𝑇𝑥)) ≤ 𝑦)))
174173expdimp 451 . . . . . . . . . . . . . . 15 ((((𝑁‘(𝑇𝑥)) ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑁‘(𝑇𝑥)) ∈ ℝ) → (0 < (𝑁‘(𝑇𝑥)) → (((𝑁‘(𝑇𝑥)) · (𝑁‘(𝑇𝑥))) ≤ (𝑦 · (𝑁‘(𝑇𝑥))) → (𝑁‘(𝑇𝑥)) ≤ 𝑦)))
175126, 135, 126, 174syl21anc 1316 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → (0 < (𝑁‘(𝑇𝑥)) → (((𝑁‘(𝑇𝑥)) · (𝑁‘(𝑇𝑥))) ≤ (𝑦 · (𝑁‘(𝑇𝑥))) → (𝑁‘(𝑇𝑥)) ≤ 𝑦)))
176170, 175mpid 42 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → (0 < (𝑁‘(𝑇𝑥)) → (𝑁‘(𝑇𝑥)) ≤ 𝑦))
177 0red 9796 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → 0 ∈ ℝ)
1784, 129, 18blof 26802 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ (𝐹𝑥) ∈ (𝑈 BLnOp 𝑊)) → (𝐹𝑥):𝑋⟶ℂ)
1793, 101, 178mp3an12 1405 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑥) ∈ (𝑈 BLnOp 𝑊) → (𝐹𝑥):𝑋⟶ℂ)
180128, 179syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝑋) → (𝐹𝑥):𝑋⟶ℂ)
181180ad2ant2r 778 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → (𝐹𝑥):𝑋⟶ℂ)
1824, 129, 103nmooge0 26784 . . . . . . . . . . . . . . . . 17 ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ (𝐹𝑥):𝑋⟶ℂ) → 0 ≤ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)))
1833, 101, 182mp3an12 1405 . . . . . . . . . . . . . . . 16 ((𝐹𝑥):𝑋⟶ℂ → 0 ≤ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)))
184181, 183syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → 0 ≤ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)))
185177, 133, 135, 184, 168letrd 9945 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → 0 ≤ 𝑦)
186 breq1 4484 . . . . . . . . . . . . . 14 (0 = (𝑁‘(𝑇𝑥)) → (0 ≤ 𝑦 ↔ (𝑁‘(𝑇𝑥)) ≤ 𝑦))
187185, 186syl5ibcom 233 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → (0 = (𝑁‘(𝑇𝑥)) → (𝑁‘(𝑇𝑥)) ≤ 𝑦))
188 0re 9795 . . . . . . . . . . . . . . 15 0 ∈ ℝ
189 leloe 9874 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ ∧ (𝑁‘(𝑇𝑥)) ∈ ℝ) → (0 ≤ (𝑁‘(𝑇𝑥)) ↔ (0 < (𝑁‘(𝑇𝑥)) ∨ 0 = (𝑁‘(𝑇𝑥)))))
190188, 126, 189sylancr 693 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → (0 ≤ (𝑁‘(𝑇𝑥)) ↔ (0 < (𝑁‘(𝑇𝑥)) ∨ 0 = (𝑁‘(𝑇𝑥)))))
191167, 190mpbid 220 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → (0 < (𝑁‘(𝑇𝑥)) ∨ 0 = (𝑁‘(𝑇𝑥))))
192176, 187, 191mpjaod 394 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ ((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦)) → (𝑁‘(𝑇𝑥)) ≤ 𝑦)
193192expr 640 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝑋) → (((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦 → (𝑁‘(𝑇𝑥)) ≤ 𝑦))
194193adantrr 748 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ (𝑁𝑥) ≤ 1)) → (((𝑈 normOpOLD 𝑊)‘(𝐹𝑥)) ≤ 𝑦 → (𝑁‘(𝑇𝑥)) ≤ 𝑦))
195125, 194syld 45 . . . . . . . . 9 (((𝜑𝑦 ∈ ℝ) ∧ (𝑥𝑋 ∧ (𝑁𝑥) ≤ 1)) → (∀𝑤𝐾 ((𝑈 normOpOLD 𝑊)‘𝑤) ≤ 𝑦 → (𝑁‘(𝑇𝑥)) ≤ 𝑦))
196195expr 640 . . . . . . . 8 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝑋) → ((𝑁𝑥) ≤ 1 → (∀𝑤𝐾 ((𝑈 normOpOLD 𝑊)‘𝑤) ≤ 𝑦 → (𝑁‘(𝑇𝑥)) ≤ 𝑦)))
197196com23 83 . . . . . . 7 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝑋) → (∀𝑤𝐾 ((𝑈 normOpOLD 𝑊)‘𝑤) ≤ 𝑦 → ((𝑁𝑥) ≤ 1 → (𝑁‘(𝑇𝑥)) ≤ 𝑦)))
198197ralrimdva 2856 . . . . . 6 ((𝜑𝑦 ∈ ℝ) → (∀𝑤𝐾 ((𝑈 normOpOLD 𝑊)‘𝑤) ≤ 𝑦 → ∀𝑥𝑋 ((𝑁𝑥) ≤ 1 → (𝑁‘(𝑇𝑥)) ≤ 𝑦)))
199198reximdva 2904 . . . . 5 (𝜑 → (∃𝑦 ∈ ℝ ∀𝑤𝐾 ((𝑈 normOpOLD 𝑊)‘𝑤) ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑥𝑋 ((𝑁𝑥) ≤ 1 → (𝑁‘(𝑇𝑥)) ≤ 𝑦)))
200107, 199mpd 15 . . . 4 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥𝑋 ((𝑁𝑥) ≤ 1 → (𝑁‘(𝑇𝑥)) ≤ 𝑦))
201 eqid 2514 . . . . . 6 (𝑈 normOpOLD 𝑈) = (𝑈 normOpOLD 𝑈)
2024, 4, 10, 10, 201, 3, 3nmobndi 26792 . . . . 5 (𝑇:𝑋𝑋 → (((𝑈 normOpOLD 𝑈)‘𝑇) ∈ ℝ ↔ ∃𝑦 ∈ ℝ ∀𝑥𝑋 ((𝑁𝑥) ≤ 1 → (𝑁‘(𝑇𝑥)) ≤ 𝑦)))
2038, 202syl 17 . . . 4 (𝜑 → (((𝑈 normOpOLD 𝑈)‘𝑇) ∈ ℝ ↔ ∃𝑦 ∈ ℝ ∀𝑥𝑋 ((𝑁𝑥) ≤ 1 → (𝑁‘(𝑇𝑥)) ≤ 𝑦)))
204200, 203mpbird 245 . . 3 (𝜑 → ((𝑈 normOpOLD 𝑈)‘𝑇) ∈ ℝ)
205 ltpnf 11701 . . 3 (((𝑈 normOpOLD 𝑈)‘𝑇) ∈ ℝ → ((𝑈 normOpOLD 𝑈)‘𝑇) < +∞)
206204, 205syl 17 . 2 (𝜑 → ((𝑈 normOpOLD 𝑈)‘𝑇) < +∞)
207 htth.4 . . . 4 𝐵 = (𝑈 BLnOp 𝑈)
208201, 5, 207isblo 26799 . . 3 ((𝑈 ∈ NrmCVec ∧ 𝑈 ∈ NrmCVec) → (𝑇𝐵 ↔ (𝑇𝐿 ∧ ((𝑈 normOpOLD 𝑈)‘𝑇) < +∞)))
2093, 3, 208mp2an 703 . 2 (𝑇𝐵 ↔ (𝑇𝐿 ∧ ((𝑈 normOpOLD 𝑈)‘𝑇) < +∞))
2101, 206, 209sylanbrc 694 1 (𝜑𝑇𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wo 381  wa 382  w3a 1030   = wceq 1474  wcel 1938  wral 2800  wrex 2801  {crab 2804  wss 3444  cop 4034   class class class wbr 4481  cmpt 4541  dom cdm 4932  ran crn 4933  cima 4935  Fun wfun 5683  wf 5685  cfv 5689  (class class class)co 6426  cc 9689  cr 9690  0cc0 9691  1c1 9692   + caddc 9694   · cmul 9696  +∞cpnf 9826   < clt 9829  cle 9830  2c2 10825  cexp 12590  abscabs 13681  NrmCVeccnv 26579  BaseSetcba 26581  normCVcnmcv 26585  ·𝑖OLDcdip 26712   LnOp clno 26757   normOpOLD cnmoo 26758   BLnOp cblo 26759  CPreHilOLDccphlo 26829  CBanccbn 26880  CHilOLDchlo 26913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-rep 4597  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6723  ax-inf2 8297  ax-dc 9027  ax-cnex 9747  ax-resscn 9748  ax-1cn 9749  ax-icn 9750  ax-addcl 9751  ax-addrcl 9752  ax-mulcl 9753  ax-mulrcl 9754  ax-mulcom 9755  ax-addass 9756  ax-mulass 9757  ax-distr 9758  ax-i2m1 9759  ax-1ne0 9760  ax-1rid 9761  ax-rnegex 9762  ax-rrecex 9763  ax-cnre 9764  ax-pre-lttri 9765  ax-pre-lttrn 9766  ax-pre-ltadd 9767  ax-pre-mulgt0 9768  ax-pre-sup 9769  ax-addf 9770  ax-mulf 9771
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-nel 2687  df-ral 2805  df-rex 2806  df-reu 2807  df-rmo 2808  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-int 4309  df-iun 4355  df-iin 4356  df-br 4482  df-opab 4542  df-mpt 4543  df-tr 4579  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-fr 4891  df-se 4892  df-we 4893  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-pred 5487  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-isom 5698  df-riota 6388  df-ov 6429  df-oprab 6430  df-mpt2 6431  df-of 6671  df-om 6834  df-1st 6934  df-2nd 6935  df-supp 7058  df-wrecs 7169  df-recs 7231  df-rdg 7269  df-1o 7323  df-2o 7324  df-oadd 7327  df-er 7505  df-map 7622  df-pm 7623  df-ixp 7671  df-en 7718  df-dom 7719  df-sdom 7720  df-fin 7721  df-fsupp 8035  df-fi 8076  df-sup 8107  df-inf 8108  df-oi 8174  df-card 8524  df-cda 8749  df-pnf 9831  df-mnf 9832  df-xr 9833  df-ltxr 9834  df-le 9835  df-sub 10019  df-neg 10020  df-div 10434  df-nn 10776  df-2 10834  df-3 10835  df-4 10836  df-5 10837  df-6 10838  df-7 10839  df-8 10840  df-9 10841  df-n0 11048  df-z 11119  df-dec 11234  df-uz 11428  df-q 11531  df-rp 11575  df-xneg 11688  df-xadd 11689  df-xmul 11690  df-ioo 11919  df-ico 11921  df-icc 11922  df-fz 12066  df-fzo 12203  df-seq 12532  df-exp 12591  df-hash 12848  df-cj 13546  df-re 13547  df-im 13548  df-sqrt 13682  df-abs 13683  df-clim 13933  df-sum 14134  df-struct 15581  df-ndx 15582  df-slot 15583  df-base 15584  df-sets 15585  df-ress 15586  df-plusg 15665  df-mulr 15666  df-starv 15667  df-sca 15668  df-vsca 15669  df-ip 15670  df-tset 15671  df-ple 15672  df-ds 15675  df-unif 15676  df-hom 15677  df-cco 15678  df-rest 15790  df-topn 15791  df-0g 15809  df-gsum 15810  df-topgen 15811  df-pt 15812  df-prds 15815  df-xrs 15869  df-qtop 15875  df-imas 15876  df-xps 15879  df-mre 15961  df-mrc 15962  df-acs 15964  df-mgm 16957  df-sgrp 16999  df-mnd 17010  df-submnd 17051  df-mulg 17256  df-cntz 17465  df-cmn 17926  df-psmet 19463  df-xmet 19464  df-met 19465  df-bl 19466  df-mopn 19467  df-fbas 19468  df-fg 19469  df-cnfld 19472  df-top 20424  df-bases 20425  df-topon 20426  df-topsp 20427  df-cld 20536  df-ntr 20537  df-cls 20538  df-nei 20615  df-cn 20744  df-cnp 20745  df-lm 20746  df-t1 20831  df-haus 20832  df-cmp 20903  df-tx 21078  df-hmeo 21271  df-fil 21363  df-fm 21455  df-flim 21456  df-flf 21457  df-fcls 21458  df-xms 21837  df-ms 21838  df-tms 21839  df-cncf 22412  df-cfil 22725  df-cau 22726  df-cmet 22727  df-grpo 26469  df-gid 26470  df-ginv 26471  df-gdiv 26472  df-ablo 26524  df-vc 26539  df-nv 26587  df-va 26590  df-ba 26591  df-sm 26592  df-0v 26593  df-vs 26594  df-nmcv 26595  df-ims 26596  df-dip 26713  df-lno 26761  df-nmoo 26762  df-blo 26763  df-0o 26764  df-ph 26830  df-cbn 26881  df-hlo 26914
This theorem is referenced by:  htth  26947
  Copyright terms: Public domain W3C validator