HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  cnlnadjlem2 Structured version   Visualization version   GIF version

Theorem cnlnadjlem2 29318
Description: Lemma for cnlnadji 29326. 𝐺 is a continuous linear functional. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
Hypotheses
Ref Expression
cnlnadjlem.1 𝑇 ∈ LinOp
cnlnadjlem.2 𝑇 ∈ ContOp
cnlnadjlem.3 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑦))
Assertion
Ref Expression
cnlnadjlem2 (𝑦 ∈ ℋ → (𝐺 ∈ LinFn ∧ 𝐺 ∈ ContFn))
Distinct variable group:   𝑦,𝑔,𝑇
Allowed substitution hints:   𝐺(𝑦,𝑔)

Proof of Theorem cnlnadjlem2
Dummy variables 𝑤 𝑧 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnlnadjlem.1 . . . . . . . 8 𝑇 ∈ LinOp
21lnopfi 29219 . . . . . . 7 𝑇: ℋ⟶ ℋ
32ffvelrni 6548 . . . . . 6 (𝑔 ∈ ℋ → (𝑇𝑔) ∈ ℋ)
4 hicl 28328 . . . . . 6 (((𝑇𝑔) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇𝑔) ·ih 𝑦) ∈ ℂ)
53, 4sylan 575 . . . . 5 ((𝑔 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇𝑔) ·ih 𝑦) ∈ ℂ)
65ancoms 450 . . . 4 ((𝑦 ∈ ℋ ∧ 𝑔 ∈ ℋ) → ((𝑇𝑔) ·ih 𝑦) ∈ ℂ)
7 cnlnadjlem.3 . . . 4 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑦))
86, 7fmptd 6574 . . 3 (𝑦 ∈ ℋ → 𝐺: ℋ⟶ℂ)
9 hvmulcl 28261 . . . . . . 7 ((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ) → (𝑥 · 𝑤) ∈ ℋ)
101lnopaddi 29221 . . . . . . . . . . . 12 (((𝑥 · 𝑤) ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑇‘((𝑥 · 𝑤) + 𝑧)) = ((𝑇‘(𝑥 · 𝑤)) + (𝑇𝑧)))
11103adant3 1162 . . . . . . . . . . 11 (((𝑥 · 𝑤) ∈ ℋ ∧ 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑇‘((𝑥 · 𝑤) + 𝑧)) = ((𝑇‘(𝑥 · 𝑤)) + (𝑇𝑧)))
1211oveq1d 6857 . . . . . . . . . 10 (((𝑥 · 𝑤) ∈ ℋ ∧ 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇‘((𝑥 · 𝑤) + 𝑧)) ·ih 𝑦) = (((𝑇‘(𝑥 · 𝑤)) + (𝑇𝑧)) ·ih 𝑦))
132ffvelrni 6548 . . . . . . . . . . 11 ((𝑥 · 𝑤) ∈ ℋ → (𝑇‘(𝑥 · 𝑤)) ∈ ℋ)
142ffvelrni 6548 . . . . . . . . . . 11 (𝑧 ∈ ℋ → (𝑇𝑧) ∈ ℋ)
15 id 22 . . . . . . . . . . 11 (𝑦 ∈ ℋ → 𝑦 ∈ ℋ)
16 ax-his2 28331 . . . . . . . . . . 11 (((𝑇‘(𝑥 · 𝑤)) ∈ ℋ ∧ (𝑇𝑧) ∈ ℋ ∧ 𝑦 ∈ ℋ) → (((𝑇‘(𝑥 · 𝑤)) + (𝑇𝑧)) ·ih 𝑦) = (((𝑇‘(𝑥 · 𝑤)) ·ih 𝑦) + ((𝑇𝑧) ·ih 𝑦)))
1713, 14, 15, 16syl3an 1199 . . . . . . . . . 10 (((𝑥 · 𝑤) ∈ ℋ ∧ 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (((𝑇‘(𝑥 · 𝑤)) + (𝑇𝑧)) ·ih 𝑦) = (((𝑇‘(𝑥 · 𝑤)) ·ih 𝑦) + ((𝑇𝑧) ·ih 𝑦)))
1812, 17eqtrd 2799 . . . . . . . . 9 (((𝑥 · 𝑤) ∈ ℋ ∧ 𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇‘((𝑥 · 𝑤) + 𝑧)) ·ih 𝑦) = (((𝑇‘(𝑥 · 𝑤)) ·ih 𝑦) + ((𝑇𝑧) ·ih 𝑦)))
19183comr 1155 . . . . . . . 8 ((𝑦 ∈ ℋ ∧ (𝑥 · 𝑤) ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑇‘((𝑥 · 𝑤) + 𝑧)) ·ih 𝑦) = (((𝑇‘(𝑥 · 𝑤)) ·ih 𝑦) + ((𝑇𝑧) ·ih 𝑦)))
20193expa 1147 . . . . . . 7 (((𝑦 ∈ ℋ ∧ (𝑥 · 𝑤) ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑇‘((𝑥 · 𝑤) + 𝑧)) ·ih 𝑦) = (((𝑇‘(𝑥 · 𝑤)) ·ih 𝑦) + ((𝑇𝑧) ·ih 𝑦)))
219, 20sylanl2 671 . . . . . 6 (((𝑦 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) → ((𝑇‘((𝑥 · 𝑤) + 𝑧)) ·ih 𝑦) = (((𝑇‘(𝑥 · 𝑤)) ·ih 𝑦) + ((𝑇𝑧) ·ih 𝑦)))
22 hvaddcl 28260 . . . . . . . . 9 (((𝑥 · 𝑤) ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑥 · 𝑤) + 𝑧) ∈ ℋ)
239, 22sylan 575 . . . . . . . 8 (((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑥 · 𝑤) + 𝑧) ∈ ℋ)
24 cnlnadjlem.2 . . . . . . . . 9 𝑇 ∈ ContOp
251, 24, 7cnlnadjlem1 29317 . . . . . . . 8 (((𝑥 · 𝑤) + 𝑧) ∈ ℋ → (𝐺‘((𝑥 · 𝑤) + 𝑧)) = ((𝑇‘((𝑥 · 𝑤) + 𝑧)) ·ih 𝑦))
2623, 25syl 17 . . . . . . 7 (((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → (𝐺‘((𝑥 · 𝑤) + 𝑧)) = ((𝑇‘((𝑥 · 𝑤) + 𝑧)) ·ih 𝑦))
2726adantll 705 . . . . . 6 (((𝑦 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) → (𝐺‘((𝑥 · 𝑤) + 𝑧)) = ((𝑇‘((𝑥 · 𝑤) + 𝑧)) ·ih 𝑦))
282ffvelrni 6548 . . . . . . . . . . 11 (𝑤 ∈ ℋ → (𝑇𝑤) ∈ ℋ)
29 ax-his3 28332 . . . . . . . . . . 11 ((𝑥 ∈ ℂ ∧ (𝑇𝑤) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑥 · (𝑇𝑤)) ·ih 𝑦) = (𝑥 · ((𝑇𝑤) ·ih 𝑦)))
3028, 29syl3an2 1203 . . . . . . . . . 10 ((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑥 · (𝑇𝑤)) ·ih 𝑦) = (𝑥 · ((𝑇𝑤) ·ih 𝑦)))
31303comr 1155 . . . . . . . . 9 ((𝑦 ∈ ℋ ∧ 𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ) → ((𝑥 · (𝑇𝑤)) ·ih 𝑦) = (𝑥 · ((𝑇𝑤) ·ih 𝑦)))
32313expb 1149 . . . . . . . 8 ((𝑦 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ)) → ((𝑥 · (𝑇𝑤)) ·ih 𝑦) = (𝑥 · ((𝑇𝑤) ·ih 𝑦)))
331lnopmuli 29222 . . . . . . . . . 10 ((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ) → (𝑇‘(𝑥 · 𝑤)) = (𝑥 · (𝑇𝑤)))
3433oveq1d 6857 . . . . . . . . 9 ((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ) → ((𝑇‘(𝑥 · 𝑤)) ·ih 𝑦) = ((𝑥 · (𝑇𝑤)) ·ih 𝑦))
3534adantl 473 . . . . . . . 8 ((𝑦 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ)) → ((𝑇‘(𝑥 · 𝑤)) ·ih 𝑦) = ((𝑥 · (𝑇𝑤)) ·ih 𝑦))
361, 24, 7cnlnadjlem1 29317 . . . . . . . . . 10 (𝑤 ∈ ℋ → (𝐺𝑤) = ((𝑇𝑤) ·ih 𝑦))
3736oveq2d 6858 . . . . . . . . 9 (𝑤 ∈ ℋ → (𝑥 · (𝐺𝑤)) = (𝑥 · ((𝑇𝑤) ·ih 𝑦)))
3837ad2antll 720 . . . . . . . 8 ((𝑦 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ)) → (𝑥 · (𝐺𝑤)) = (𝑥 · ((𝑇𝑤) ·ih 𝑦)))
3932, 35, 383eqtr4rd 2810 . . . . . . 7 ((𝑦 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ)) → (𝑥 · (𝐺𝑤)) = ((𝑇‘(𝑥 · 𝑤)) ·ih 𝑦))
401, 24, 7cnlnadjlem1 29317 . . . . . . 7 (𝑧 ∈ ℋ → (𝐺𝑧) = ((𝑇𝑧) ·ih 𝑦))
4139, 40oveqan12d 6861 . . . . . 6 (((𝑦 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) → ((𝑥 · (𝐺𝑤)) + (𝐺𝑧)) = (((𝑇‘(𝑥 · 𝑤)) ·ih 𝑦) + ((𝑇𝑧) ·ih 𝑦)))
4221, 27, 413eqtr4d 2809 . . . . 5 (((𝑦 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ)) ∧ 𝑧 ∈ ℋ) → (𝐺‘((𝑥 · 𝑤) + 𝑧)) = ((𝑥 · (𝐺𝑤)) + (𝐺𝑧)))
4342ralrimiva 3113 . . . 4 ((𝑦 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑤 ∈ ℋ)) → ∀𝑧 ∈ ℋ (𝐺‘((𝑥 · 𝑤) + 𝑧)) = ((𝑥 · (𝐺𝑤)) + (𝐺𝑧)))
4443ralrimivva 3118 . . 3 (𝑦 ∈ ℋ → ∀𝑥 ∈ ℂ ∀𝑤 ∈ ℋ ∀𝑧 ∈ ℋ (𝐺‘((𝑥 · 𝑤) + 𝑧)) = ((𝑥 · (𝐺𝑤)) + (𝐺𝑧)))
45 ellnfn 29133 . . 3 (𝐺 ∈ LinFn ↔ (𝐺: ℋ⟶ℂ ∧ ∀𝑥 ∈ ℂ ∀𝑤 ∈ ℋ ∀𝑧 ∈ ℋ (𝐺‘((𝑥 · 𝑤) + 𝑧)) = ((𝑥 · (𝐺𝑤)) + (𝐺𝑧))))
468, 44, 45sylanbrc 578 . 2 (𝑦 ∈ ℋ → 𝐺 ∈ LinFn)
471, 24nmcopexi 29277 . . . . 5 (normop𝑇) ∈ ℝ
48 normcl 28373 . . . . 5 (𝑦 ∈ ℋ → (norm𝑦) ∈ ℝ)
49 remulcl 10274 . . . . 5 (((normop𝑇) ∈ ℝ ∧ (norm𝑦) ∈ ℝ) → ((normop𝑇) · (norm𝑦)) ∈ ℝ)
5047, 48, 49sylancr 581 . . . 4 (𝑦 ∈ ℋ → ((normop𝑇) · (norm𝑦)) ∈ ℝ)
5140adantr 472 . . . . . . . . . 10 ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝐺𝑧) = ((𝑇𝑧) ·ih 𝑦))
52 hicl 28328 . . . . . . . . . . 11 (((𝑇𝑧) ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇𝑧) ·ih 𝑦) ∈ ℂ)
5314, 52sylan 575 . . . . . . . . . 10 ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((𝑇𝑧) ·ih 𝑦) ∈ ℂ)
5451, 53eqeltrd 2844 . . . . . . . . 9 ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝐺𝑧) ∈ ℂ)
5554abscld 14462 . . . . . . . 8 ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (abs‘(𝐺𝑧)) ∈ ℝ)
56 normcl 28373 . . . . . . . . . 10 ((𝑇𝑧) ∈ ℋ → (norm‘(𝑇𝑧)) ∈ ℝ)
5714, 56syl 17 . . . . . . . . 9 (𝑧 ∈ ℋ → (norm‘(𝑇𝑧)) ∈ ℝ)
58 remulcl 10274 . . . . . . . . 9 (((norm‘(𝑇𝑧)) ∈ ℝ ∧ (norm𝑦) ∈ ℝ) → ((norm‘(𝑇𝑧)) · (norm𝑦)) ∈ ℝ)
5957, 48, 58syl2an 589 . . . . . . . 8 ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((norm‘(𝑇𝑧)) · (norm𝑦)) ∈ ℝ)
60 normcl 28373 . . . . . . . . . 10 (𝑧 ∈ ℋ → (norm𝑧) ∈ ℝ)
61 remulcl 10274 . . . . . . . . . 10 (((normop𝑇) ∈ ℝ ∧ (norm𝑧) ∈ ℝ) → ((normop𝑇) · (norm𝑧)) ∈ ℝ)
6247, 60, 61sylancr 581 . . . . . . . . 9 (𝑧 ∈ ℋ → ((normop𝑇) · (norm𝑧)) ∈ ℝ)
63 remulcl 10274 . . . . . . . . 9 ((((normop𝑇) · (norm𝑧)) ∈ ℝ ∧ (norm𝑦) ∈ ℝ) → (((normop𝑇) · (norm𝑧)) · (norm𝑦)) ∈ ℝ)
6462, 48, 63syl2an 589 . . . . . . . 8 ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (((normop𝑇) · (norm𝑧)) · (norm𝑦)) ∈ ℝ)
6551fveq2d 6379 . . . . . . . . 9 ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (abs‘(𝐺𝑧)) = (abs‘((𝑇𝑧) ·ih 𝑦)))
66 bcs 28429 . . . . . . . . . 10 (((𝑇𝑧) ∈ ℋ ∧ 𝑦 ∈ ℋ) → (abs‘((𝑇𝑧) ·ih 𝑦)) ≤ ((norm‘(𝑇𝑧)) · (norm𝑦)))
6714, 66sylan 575 . . . . . . . . 9 ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (abs‘((𝑇𝑧) ·ih 𝑦)) ≤ ((norm‘(𝑇𝑧)) · (norm𝑦)))
6865, 67eqbrtrd 4831 . . . . . . . 8 ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (abs‘(𝐺𝑧)) ≤ ((norm‘(𝑇𝑧)) · (norm𝑦)))
6957adantr 472 . . . . . . . . 9 ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (norm‘(𝑇𝑧)) ∈ ℝ)
7062adantr 472 . . . . . . . . 9 ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((normop𝑇) · (norm𝑧)) ∈ ℝ)
71 normge0 28374 . . . . . . . . . . 11 (𝑦 ∈ ℋ → 0 ≤ (norm𝑦))
7248, 71jca 507 . . . . . . . . . 10 (𝑦 ∈ ℋ → ((norm𝑦) ∈ ℝ ∧ 0 ≤ (norm𝑦)))
7372adantl 473 . . . . . . . . 9 ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((norm𝑦) ∈ ℝ ∧ 0 ≤ (norm𝑦)))
741, 24nmcoplbi 29278 . . . . . . . . . 10 (𝑧 ∈ ℋ → (norm‘(𝑇𝑧)) ≤ ((normop𝑇) · (norm𝑧)))
7574adantr 472 . . . . . . . . 9 ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (norm‘(𝑇𝑧)) ≤ ((normop𝑇) · (norm𝑧)))
76 lemul1a 11131 . . . . . . . . 9 ((((norm‘(𝑇𝑧)) ∈ ℝ ∧ ((normop𝑇) · (norm𝑧)) ∈ ℝ ∧ ((norm𝑦) ∈ ℝ ∧ 0 ≤ (norm𝑦))) ∧ (norm‘(𝑇𝑧)) ≤ ((normop𝑇) · (norm𝑧))) → ((norm‘(𝑇𝑧)) · (norm𝑦)) ≤ (((normop𝑇) · (norm𝑧)) · (norm𝑦)))
7769, 70, 73, 75, 76syl31anc 1492 . . . . . . . 8 ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → ((norm‘(𝑇𝑧)) · (norm𝑦)) ≤ (((normop𝑇) · (norm𝑧)) · (norm𝑦)))
7855, 59, 64, 68, 77letrd 10448 . . . . . . 7 ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (abs‘(𝐺𝑧)) ≤ (((normop𝑇) · (norm𝑧)) · (norm𝑦)))
7960recnd 10322 . . . . . . . 8 (𝑧 ∈ ℋ → (norm𝑧) ∈ ℂ)
8048recnd 10322 . . . . . . . 8 (𝑦 ∈ ℋ → (norm𝑦) ∈ ℂ)
8147recni 10308 . . . . . . . . 9 (normop𝑇) ∈ ℂ
82 mul32 10457 . . . . . . . . 9 (((normop𝑇) ∈ ℂ ∧ (norm𝑧) ∈ ℂ ∧ (norm𝑦) ∈ ℂ) → (((normop𝑇) · (norm𝑧)) · (norm𝑦)) = (((normop𝑇) · (norm𝑦)) · (norm𝑧)))
8381, 82mp3an1 1572 . . . . . . . 8 (((norm𝑧) ∈ ℂ ∧ (norm𝑦) ∈ ℂ) → (((normop𝑇) · (norm𝑧)) · (norm𝑦)) = (((normop𝑇) · (norm𝑦)) · (norm𝑧)))
8479, 80, 83syl2an 589 . . . . . . 7 ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (((normop𝑇) · (norm𝑧)) · (norm𝑦)) = (((normop𝑇) · (norm𝑦)) · (norm𝑧)))
8578, 84breqtrd 4835 . . . . . 6 ((𝑧 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (abs‘(𝐺𝑧)) ≤ (((normop𝑇) · (norm𝑦)) · (norm𝑧)))
8685ancoms 450 . . . . 5 ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (abs‘(𝐺𝑧)) ≤ (((normop𝑇) · (norm𝑦)) · (norm𝑧)))
8786ralrimiva 3113 . . . 4 (𝑦 ∈ ℋ → ∀𝑧 ∈ ℋ (abs‘(𝐺𝑧)) ≤ (((normop𝑇) · (norm𝑦)) · (norm𝑧)))
88 oveq1 6849 . . . . . . 7 (𝑥 = ((normop𝑇) · (norm𝑦)) → (𝑥 · (norm𝑧)) = (((normop𝑇) · (norm𝑦)) · (norm𝑧)))
8988breq2d 4821 . . . . . 6 (𝑥 = ((normop𝑇) · (norm𝑦)) → ((abs‘(𝐺𝑧)) ≤ (𝑥 · (norm𝑧)) ↔ (abs‘(𝐺𝑧)) ≤ (((normop𝑇) · (norm𝑦)) · (norm𝑧))))
9089ralbidv 3133 . . . . 5 (𝑥 = ((normop𝑇) · (norm𝑦)) → (∀𝑧 ∈ ℋ (abs‘(𝐺𝑧)) ≤ (𝑥 · (norm𝑧)) ↔ ∀𝑧 ∈ ℋ (abs‘(𝐺𝑧)) ≤ (((normop𝑇) · (norm𝑦)) · (norm𝑧))))
9190rspcev 3461 . . . 4 ((((normop𝑇) · (norm𝑦)) ∈ ℝ ∧ ∀𝑧 ∈ ℋ (abs‘(𝐺𝑧)) ≤ (((normop𝑇) · (norm𝑦)) · (norm𝑧))) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ℋ (abs‘(𝐺𝑧)) ≤ (𝑥 · (norm𝑧)))
9250, 87, 91syl2anc 579 . . 3 (𝑦 ∈ ℋ → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ℋ (abs‘(𝐺𝑧)) ≤ (𝑥 · (norm𝑧)))
93 lnfncon 29306 . . . 4 (𝐺 ∈ LinFn → (𝐺 ∈ ContFn ↔ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ℋ (abs‘(𝐺𝑧)) ≤ (𝑥 · (norm𝑧))))
9446, 93syl 17 . . 3 (𝑦 ∈ ℋ → (𝐺 ∈ ContFn ↔ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ℋ (abs‘(𝐺𝑧)) ≤ (𝑥 · (norm𝑧))))
9592, 94mpbird 248 . 2 (𝑦 ∈ ℋ → 𝐺 ∈ ContFn)
9646, 95jca 507 1 (𝑦 ∈ ℋ → (𝐺 ∈ LinFn ∧ 𝐺 ∈ ContFn))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wral 3055  wrex 3056   class class class wbr 4809  cmpt 4888  wf 6064  cfv 6068  (class class class)co 6842  cc 10187  cr 10188  0cc0 10189   + caddc 10192   · cmul 10194  cle 10329  abscabs 14261  chba 28167   + cva 28168   · csm 28169   ·ih csp 28170  normcno 28171  normopcnop 28193  ContOpccop 28194  LinOpclo 28195  ContFnccnfn 28201  LinFnclf 28202
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267  ax-addf 10268  ax-mulf 10269  ax-hilex 28247  ax-hfvadd 28248  ax-hvcom 28249  ax-hvass 28250  ax-hv0cl 28251  ax-hvaddid 28252  ax-hfvmul 28253  ax-hvmulid 28254  ax-hvmulass 28255  ax-hvdistr1 28256  ax-hvdistr2 28257  ax-hvmul0 28258  ax-hfi 28327  ax-his1 28330  ax-his2 28331  ax-his3 28332  ax-his4 28333
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-iin 4679  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-of 7095  df-om 7264  df-1st 7366  df-2nd 7367  df-supp 7498  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-er 7947  df-map 8062  df-ixp 8114  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-fsupp 8483  df-fi 8524  df-sup 8555  df-inf 8556  df-oi 8622  df-card 9016  df-cda 9243  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-z 11625  df-dec 11741  df-uz 11887  df-q 11990  df-rp 12029  df-xneg 12146  df-xadd 12147  df-xmul 12148  df-ioo 12381  df-icc 12384  df-fz 12534  df-fzo 12674  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14126  df-re 14127  df-im 14128  df-sqrt 14262  df-abs 14263  df-clim 14506  df-sum 14704  df-struct 16134  df-ndx 16135  df-slot 16136  df-base 16138  df-sets 16139  df-ress 16140  df-plusg 16229  df-mulr 16230  df-starv 16231  df-sca 16232  df-vsca 16233  df-ip 16234  df-tset 16235  df-ple 16236  df-ds 16238  df-unif 16239  df-hom 16240  df-cco 16241  df-rest 16351  df-topn 16352  df-0g 16370  df-gsum 16371  df-topgen 16372  df-pt 16373  df-prds 16376  df-xrs 16430  df-qtop 16435  df-imas 16436  df-xps 16438  df-mre 16514  df-mrc 16515  df-acs 16517  df-mgm 17510  df-sgrp 17552  df-mnd 17563  df-submnd 17604  df-mulg 17810  df-cntz 18015  df-cmn 18461  df-psmet 20011  df-xmet 20012  df-met 20013  df-bl 20014  df-mopn 20015  df-cnfld 20020  df-top 20978  df-topon 20995  df-topsp 21017  df-bases 21030  df-cld 21103  df-ntr 21104  df-cls 21105  df-cn 21311  df-cnp 21312  df-t1 21398  df-haus 21399  df-tx 21645  df-hmeo 21838  df-xms 22404  df-ms 22405  df-tms 22406  df-grpo 27739  df-gid 27740  df-ginv 27741  df-gdiv 27742  df-ablo 27791  df-vc 27805  df-nv 27838  df-va 27841  df-ba 27842  df-sm 27843  df-0v 27844  df-vs 27845  df-nmcv 27846  df-ims 27847  df-dip 27947  df-ph 28059  df-hnorm 28216  df-hba 28217  df-hvsub 28219  df-nmop 29089  df-cnop 29090  df-lnop 29091  df-nmfn 29095  df-cnfn 29097  df-lnfn 29098
This theorem is referenced by:  cnlnadjlem3  29319  cnlnadjlem5  29321
  Copyright terms: Public domain W3C validator