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 ‘ 𝑇 ) ∈ ℝ