Metamath Proof Explorer

Theorem nmcfnexi

Description: The norm of a continuous linear Hilbert space functional exists. Theorem 3.5(i) of Beran p. 99. (Contributed by NM, 14-Feb-2006) (Proof shortened by Mario Carneiro, 17-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nmcfnex.1 ⊢ 𝑇 ∈ LinFn
nmcfnex.2 ⊢ 𝑇 ∈ ContFn
Assertion nmcfnexi ( normfn ‘ 𝑇 ) ∈ ℝ

Proof

Step Hyp Ref Expression
1 nmcfnex.1 ⊢ 𝑇 ∈ LinFn
2 nmcfnex.2 ⊢ 𝑇 ∈ ContFn
3 ax-hv0cl ⊢ 0ℎ ∈ ℋ
4 1rp ⊢ 1 ∈ ℝ+
5 cnfnc ⊢ ( ( 𝑇 ∈ ContFn ∧ 0ℎ ∈ ℋ ∧ 1 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ ( 𝑧 −ℎ 0ℎ ) ) < 𝑦 → ( abs ‘ ( ( 𝑇 ‘ 𝑧 ) − ( 𝑇 ‘ 0ℎ ) ) ) < 1 ) )
6 2 3 4 5 mp3an ⊢ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ ( 𝑧 −ℎ 0ℎ ) ) < 𝑦 → ( abs ‘ ( ( 𝑇 ‘ 𝑧 ) − ( 𝑇 ‘ 0ℎ ) ) ) < 1 )
7 hvsub0 ⊢ ( 𝑧 ∈ ℋ → ( 𝑧 −ℎ 0ℎ ) = 𝑧 )
8 7 fveq2d ⊢ ( 𝑧 ∈ ℋ → ( normℎ ‘ ( 𝑧 −ℎ 0ℎ ) ) = ( normℎ ‘ 𝑧 ) )
9 8 breq1d ⊢ ( 𝑧 ∈ ℋ → ( ( normℎ ‘ ( 𝑧 −ℎ 0ℎ ) ) < 𝑦 ↔ ( normℎ ‘ 𝑧 ) < 𝑦 ) )
10 1 lnfn0i ⊢ ( 𝑇 ‘ 0ℎ ) = 0
11 10 oveq2i ⊢ ( ( 𝑇 ‘ 𝑧 ) − ( 𝑇 ‘ 0ℎ ) ) = ( ( 𝑇 ‘ 𝑧 ) − 0 )
12 1 lnfnfi ⊢ 𝑇 : ℋ ⟶ ℂ
13 12 ffvelcdmi ⊢ ( 𝑧 ∈ ℋ → ( 𝑇 ‘ 𝑧 ) ∈ ℂ )
14 13 subid1d ⊢ ( 𝑧 ∈ ℋ → ( ( 𝑇 ‘ 𝑧 ) − 0 ) = ( 𝑇 ‘ 𝑧 ) )
15 11 14 eqtrid ⊢ ( 𝑧 ∈ ℋ → ( ( 𝑇 ‘ 𝑧 ) − ( 𝑇 ‘ 0ℎ ) ) = ( 𝑇 ‘ 𝑧 ) )
16 15 fveq2d ⊢ ( 𝑧 ∈ ℋ → ( abs ‘ ( ( 𝑇 ‘ 𝑧 ) − ( 𝑇 ‘ 0ℎ ) ) ) = ( abs ‘ ( 𝑇 ‘ 𝑧 ) ) )
17 16 breq1d ⊢ ( 𝑧 ∈ ℋ → ( ( abs ‘ ( ( 𝑇 ‘ 𝑧 ) − ( 𝑇 ‘ 0ℎ ) ) ) < 1 ↔ ( abs ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 ) )
18 9 17 imbi12d ⊢ ( 𝑧 ∈ ℋ → ( ( ( normℎ ‘ ( 𝑧 −ℎ 0ℎ ) ) < 𝑦 → ( abs ‘ ( ( 𝑇 ‘ 𝑧 ) − ( 𝑇 ‘ 0ℎ ) ) ) < 1 ) ↔ ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( abs ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 ) ) )
19 18 ralbiia ⊢ ( ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ ( 𝑧 −ℎ 0ℎ ) ) < 𝑦 → ( abs ‘ ( ( 𝑇 ‘ 𝑧 ) − ( 𝑇 ‘ 0ℎ ) ) ) < 1 ) ↔ ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( abs ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 ) )
20 19 rexbii ⊢ ( ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ ( 𝑧 −ℎ 0ℎ ) ) < 𝑦 → ( abs ‘ ( ( 𝑇 ‘ 𝑧 ) − ( 𝑇 ‘ 0ℎ ) ) ) < 1 ) ↔ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( abs ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 ) )
21 6 20 mpbi ⊢ ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℋ ( ( normℎ ‘ 𝑧 ) < 𝑦 → ( abs ‘ ( 𝑇 ‘ 𝑧 ) ) < 1 )
22 nmfnval ⊢ ( 𝑇 : ℋ ⟶ ℂ → ( normfn ‘ 𝑇 ) = sup ( { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ* , < ) )
23 12 22 ax-mp ⊢ ( normfn ‘ 𝑇 ) = sup ( { 𝑚 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑚 = ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ* , < )
24 12 ffvelcdmi ⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) ∈ ℂ )
25 24 abscld ⊢ ( 𝑥 ∈ ℋ → ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ )
26 10 fveq2i ⊢ ( abs ‘ ( 𝑇 ‘ 0ℎ ) ) = ( abs ‘ 0 )
27 abs0 ⊢ ( abs ‘ 0 ) = 0
28 26 27 eqtri ⊢ ( abs ‘ ( 𝑇 ‘ 0ℎ ) ) = 0
29 rpcn ⊢ ( ( 𝑦 / 2 ) ∈ ℝ+ → ( 𝑦 / 2 ) ∈ ℂ )
30 1 lnfnmuli ⊢ ( ( ( 𝑦 / 2 ) ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) = ( ( 𝑦 / 2 ) · ( 𝑇 ‘ 𝑥 ) ) )
31 29 30 sylan ⊢ ( ( ( 𝑦 / 2 ) ∈ ℝ+ ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) = ( ( 𝑦 / 2 ) · ( 𝑇 ‘ 𝑥 ) ) )
32 31 fveq2d ⊢ ( ( ( 𝑦 / 2 ) ∈ ℝ+ ∧ 𝑥 ∈ ℋ ) → ( abs ‘ ( 𝑇 ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) ) = ( abs ‘ ( ( 𝑦 / 2 ) · ( 𝑇 ‘ 𝑥 ) ) ) )
33 absmul ⊢ ( ( ( 𝑦 / 2 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℂ ) → ( abs ‘ ( ( 𝑦 / 2 ) · ( 𝑇 ‘ 𝑥 ) ) ) = ( ( abs ‘ ( 𝑦 / 2 ) ) · ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
34 29 24 33 syl2an ⊢ ( ( ( 𝑦 / 2 ) ∈ ℝ+ ∧ 𝑥 ∈ ℋ ) → ( abs ‘ ( ( 𝑦 / 2 ) · ( 𝑇 ‘ 𝑥 ) ) ) = ( ( abs ‘ ( 𝑦 / 2 ) ) · ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
35 rpre ⊢ ( ( 𝑦 / 2 ) ∈ ℝ+ → ( 𝑦 / 2 ) ∈ ℝ )
36 rpge0 ⊢ ( ( 𝑦 / 2 ) ∈ ℝ+ → 0 ≤ ( 𝑦 / 2 ) )
37 35 36 absidd ⊢ ( ( 𝑦 / 2 ) ∈ ℝ+ → ( abs ‘ ( 𝑦 / 2 ) ) = ( 𝑦 / 2 ) )
38 37 adantr ⊢ ( ( ( 𝑦 / 2 ) ∈ ℝ+ ∧ 𝑥 ∈ ℋ ) → ( abs ‘ ( 𝑦 / 2 ) ) = ( 𝑦 / 2 ) )
39 38 oveq1d ⊢ ( ( ( 𝑦 / 2 ) ∈ ℝ+ ∧ 𝑥 ∈ ℋ ) → ( ( abs ‘ ( 𝑦 / 2 ) ) · ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( 𝑦 / 2 ) · ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
40 32 34 39 3eqtrrd ⊢ ( ( ( 𝑦 / 2 ) ∈ ℝ+ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑦 / 2 ) · ( abs ‘ ( 𝑇 ‘ 𝑥 ) ) ) = ( abs ‘ ( 𝑇 ‘ ( ( 𝑦 / 2 ) ·ℎ 𝑥 ) ) ) )
41 21 23 25 28 40 nmcexi ⊢ ( normfn ‘ 𝑇 ) ∈ ℝ