Theorem nmop0

Description: The norm of the zero operator is zero. (Contributed by NM, 8-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	nmop0	|- ( normop ` 0hop ) = 0

Proof

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