Theorem nmfn0

Description: The norm of the identically zero functional is zero. (Contributed by NM, 25-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	nmfn0	|- ( normfn ` ( ~H X. { 0 } ) ) = 0

Proof

Step	Hyp	Ref	Expression
1		0lnfn	|- ( ~H X. { 0 } ) e. LinFn
2		lnfnf	|- ( ( ~H X. { 0 } ) e. LinFn -> ( ~H X. { 0 } ) : ~H --> CC )
3		nmfnval	|- ( ( ~H X. { 0 } ) : ~H --> CC -> ( normfn ` ( ~H X. { 0 } ) ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( ( ~H X. { 0 } ) ` y ) ) ) } , RR* , < ) )
4	1 2 3	mp2b	|- ( normfn ` ( ~H X. { 0 } ) ) = sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( ( ~H X. { 0 } ) ` y ) ) ) } , RR* , < )
5		c0ex	|- 0 e. _V
6	5	fvconst2	|- ( y e. ~H -> ( ( ~H X. { 0 } ) ` y ) = 0 )
7	6	fveq2d	|- ( y e. ~H -> ( abs ` ( ( ~H X. { 0 } ) ` y ) ) = ( abs ` 0 ) )
8		abs0	|- ( abs ` 0 ) = 0
9	7 8	eqtrdi	|- ( y e. ~H -> ( abs ` ( ( ~H X. { 0 } ) ` y ) ) = 0 )
10	9	eqeq2d	|- ( y e. ~H -> ( x = ( abs ` ( ( ~H X. { 0 } ) ` y ) ) <-> x = 0 ) )
11	10	anbi2d	|- ( y e. ~H -> ( ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( ( ~H X. { 0 } ) ` y ) ) ) <-> ( ( normh ` y ) <_ 1 /\ x = 0 ) ) )
12	11	rexbiia	|- ( E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( ( ~H X. { 0 } ) ` y ) ) ) <-> E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = 0 ) )
13		ax-hv0cl	|- 0h e. ~H
14		0le1	|- 0 <_ 1
15		fveq2	|- ( y = 0h -> ( normh ` y ) = ( normh ` 0h ) )
16		norm0	|- ( normh ` 0h ) = 0
17	15 16	eqtrdi	|- ( y = 0h -> ( normh ` y ) = 0 )
18	17	breq1d	|- ( y = 0h -> ( ( normh ` y ) <_ 1 <-> 0 <_ 1 ) )
19	18	rspcev	|- ( ( 0h e. ~H /\ 0 <_ 1 ) -> E. y e. ~H ( normh ` y ) <_ 1 )
20	13 14 19	mp2an	|- E. y e. ~H ( normh ` y ) <_ 1
21		r19.41v	|- ( E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = 0 ) <-> ( E. y e. ~H ( normh ` y ) <_ 1 /\ x = 0 ) )
22	20 21	mpbiran	|- ( E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = 0 ) <-> x = 0 )
23	12 22	bitri	|- ( E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( ( ~H X. { 0 } ) ` y ) ) ) <-> x = 0 )
24	23	abbii	|- { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( ( ~H X. { 0 } ) ` y ) ) ) } = { x | x = 0 }
25		df-sn	|- { 0 } = { x | x = 0 }
26	24 25	eqtr4i	|- { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( ( ~H X. { 0 } ) ` y ) ) ) } = { 0 }
27	26	supeq1i	|- sup ( { x | E. y e. ~H ( ( normh ` y ) <_ 1 /\ x = ( abs ` ( ( ~H X. { 0 } ) ` y ) ) ) } , RR* , < ) = sup ( { 0 } , RR* , < )
28		xrltso	|- < Or RR*
29		0xr	|- 0 e. RR*
30		supsn	|- ( ( < Or RR* /\ 0 e. RR* ) -> sup ( { 0 } , RR* , < ) = 0 )
31	28 29 30	mp2an	|- sup ( { 0 } , RR* , < ) = 0
32	4 27 31	3eqtri	|- ( normfn ` ( ~H X. { 0 } ) ) = 0