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	\|- T e. LinFn
	nmcfnex.2	\|- T e. ContFn
Assertion	nmcfnexi	\|- ( normfn ` T ) e. RR

Proof

Step	Hyp	Ref	Expression
1		nmcfnex.1	\|- T e. LinFn
2		nmcfnex.2	\|- T e. ContFn
3		ax-hv0cl	\|- 0h e. ~H
4		1rp	\|- 1 e. RR+
5		cnfnc	\|- ( ( T e. ContFn /\ 0h e. ~H /\ 1 e. RR+ ) -> E. y e. RR+ A. z e. ~H ( ( normh ` ( z -h 0h ) ) < y -> ( abs ` ( ( T ` z ) - ( T ` 0h ) ) ) < 1 ) )
6	2 3 4 5	mp3an	\|- E. y e. RR+ A. z e. ~H ( ( normh ` ( z -h 0h ) ) < y -> ( abs ` ( ( T ` z ) - ( T ` 0h ) ) ) < 1 )
7		hvsub0	\|- ( z e. ~H -> ( z -h 0h ) = z )
8	7	fveq2d	\|- ( z e. ~H -> ( normh ` ( z -h 0h ) ) = ( normh ` z ) )
9	8	breq1d	\|- ( z e. ~H -> ( ( normh ` ( z -h 0h ) ) < y <-> ( normh ` z ) < y ) )
10	1	lnfn0i	\|- ( T ` 0h ) = 0
11	10	oveq2i	\|- ( ( T ` z ) - ( T ` 0h ) ) = ( ( T ` z ) - 0 )
12	1	lnfnfi	\|- T : ~H --> CC
13	12	ffvelcdmi	\|- ( z e. ~H -> ( T ` z ) e. CC )
14	13	subid1d	\|- ( z e. ~H -> ( ( T ` z ) - 0 ) = ( T ` z ) )
15	11 14	eqtrid	\|- ( z e. ~H -> ( ( T ` z ) - ( T ` 0h ) ) = ( T ` z ) )
16	15	fveq2d	\|- ( z e. ~H -> ( abs ` ( ( T ` z ) - ( T ` 0h ) ) ) = ( abs ` ( T ` z ) ) )
17	16	breq1d	\|- ( z e. ~H -> ( ( abs ` ( ( T ` z ) - ( T ` 0h ) ) ) < 1 <-> ( abs ` ( T ` z ) ) < 1 ) )
18	9 17	imbi12d	\|- ( z e. ~H -> ( ( ( normh ` ( z -h 0h ) ) < y -> ( abs ` ( ( T ` z ) - ( T ` 0h ) ) ) < 1 ) <-> ( ( normh ` z ) < y -> ( abs ` ( T ` z ) ) < 1 ) ) )
19	18	ralbiia	\|- ( A. z e. ~H ( ( normh ` ( z -h 0h ) ) < y -> ( abs ` ( ( T ` z ) - ( T ` 0h ) ) ) < 1 ) <-> A. z e. ~H ( ( normh ` z ) < y -> ( abs ` ( T ` z ) ) < 1 ) )
20	19	rexbii	\|- ( E. y e. RR+ A. z e. ~H ( ( normh ` ( z -h 0h ) ) < y -> ( abs ` ( ( T ` z ) - ( T ` 0h ) ) ) < 1 ) <-> E. y e. RR+ A. z e. ~H ( ( normh ` z ) < y -> ( abs ` ( T ` z ) ) < 1 ) )
21	6 20	mpbi	\|- E. y e. RR+ A. z e. ~H ( ( normh ` z ) < y -> ( abs ` ( T ` z ) ) < 1 )
22		nmfnval	\|- ( T : ~H --> CC -> ( normfn ` T ) = sup ( { m \| E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( abs ` ( T ` x ) ) ) } , RR* , < ) )
23	12 22	ax-mp	\|- ( normfn ` T ) = sup ( { m \| E. x e. ~H ( ( normh ` x ) <_ 1 /\ m = ( abs ` ( T ` x ) ) ) } , RR* , < )
24	12	ffvelcdmi	\|- ( x e. ~H -> ( T ` x ) e. CC )
25	24	abscld	\|- ( x e. ~H -> ( abs ` ( T ` x ) ) e. RR )
26	10	fveq2i	\|- ( abs ` ( T ` 0h ) ) = ( abs ` 0 )
27		abs0	\|- ( abs ` 0 ) = 0
28	26 27	eqtri	\|- ( abs ` ( T ` 0h ) ) = 0
29		rpcn	\|- ( ( y / 2 ) e. RR+ -> ( y / 2 ) e. CC )
30	1	lnfnmuli	\|- ( ( ( y / 2 ) e. CC /\ x e. ~H ) -> ( T ` ( ( y / 2 ) .h x ) ) = ( ( y / 2 ) x. ( T ` x ) ) )
31	29 30	sylan	\|- ( ( ( y / 2 ) e. RR+ /\ x e. ~H ) -> ( T ` ( ( y / 2 ) .h x ) ) = ( ( y / 2 ) x. ( T ` x ) ) )
32	31	fveq2d	\|- ( ( ( y / 2 ) e. RR+ /\ x e. ~H ) -> ( abs ` ( T ` ( ( y / 2 ) .h x ) ) ) = ( abs ` ( ( y / 2 ) x. ( T ` x ) ) ) )
33		absmul	\|- ( ( ( y / 2 ) e. CC /\ ( T ` x ) e. CC ) -> ( abs ` ( ( y / 2 ) x. ( T ` x ) ) ) = ( ( abs ` ( y / 2 ) ) x. ( abs ` ( T ` x ) ) ) )
34	29 24 33	syl2an	\|- ( ( ( y / 2 ) e. RR+ /\ x e. ~H ) -> ( abs ` ( ( y / 2 ) x. ( T ` x ) ) ) = ( ( abs ` ( y / 2 ) ) x. ( abs ` ( T ` x ) ) ) )
35		rpre	\|- ( ( y / 2 ) e. RR+ -> ( y / 2 ) e. RR )
36		rpge0	\|- ( ( y / 2 ) e. RR+ -> 0 <_ ( y / 2 ) )
37	35 36	absidd	\|- ( ( y / 2 ) e. RR+ -> ( abs ` ( y / 2 ) ) = ( y / 2 ) )
38	37	adantr	\|- ( ( ( y / 2 ) e. RR+ /\ x e. ~H ) -> ( abs ` ( y / 2 ) ) = ( y / 2 ) )
39	38	oveq1d	\|- ( ( ( y / 2 ) e. RR+ /\ x e. ~H ) -> ( ( abs ` ( y / 2 ) ) x. ( abs ` ( T ` x ) ) ) = ( ( y / 2 ) x. ( abs ` ( T ` x ) ) ) )
40	32 34 39	3eqtrrd	\|- ( ( ( y / 2 ) e. RR+ /\ x e. ~H ) -> ( ( y / 2 ) x. ( abs ` ( T ` x ) ) ) = ( abs ` ( T ` ( ( y / 2 ) .h x ) ) ) )
41	21 23 25 28 40	nmcexi	\|- ( normfn ` T ) e. RR

Metamath Proof Explorer

Theorem nmcfnexi

Proof