Metamath Proof Explorer

Theorem nmoge0

Description: The operator norm of an operator is nonnegative. (Contributed by Mario Carneiro, 18-Oct-2015)

Ref Expression
Hypothesis nmofval.1 
|- N = ( S normOp T )
Assertion nmoge0 
|- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> 0 <_ ( N ` F ) )

Proof

Step Hyp Ref Expression
1 nmofval.1 
 |-  N = ( S normOp T )
2 elrege0 
 |-  ( r e. ( 0 [,) +oo ) <-> ( r e. RR /\ 0 <_ r ) )
3 2 simprbi 
 |-  ( r e. ( 0 [,) +oo ) -> 0 <_ r )
4 3 adantl 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ r e. ( 0 [,) +oo ) ) -> 0 <_ r )
5 4 a1d 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ r e. ( 0 [,) +oo ) ) -> ( A. x e. ( Base ` S ) ( ( norm ` T ) ` ( F ` x ) ) <_ ( r x. ( ( norm ` S ) ` x ) ) -> 0 <_ r ) )
6 5 ralrimiva 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> A. r e. ( 0 [,) +oo ) ( A. x e. ( Base ` S ) ( ( norm ` T ) ` ( F ` x ) ) <_ ( r x. ( ( norm ` S ) ` x ) ) -> 0 <_ r ) )
7 0xr 
 |-  0 e. RR*
8 eqid 
 |-  ( Base ` S ) = ( Base ` S )
9 eqid 
 |-  ( norm ` S ) = ( norm ` S )
10 eqid 
 |-  ( norm ` T ) = ( norm ` T )
11 1 8 9 10 nmogelb 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ 0 e. RR* ) -> ( 0 <_ ( N ` F ) <-> A. r e. ( 0 [,) +oo ) ( A. x e. ( Base ` S ) ( ( norm ` T ) ` ( F ` x ) ) <_ ( r x. ( ( norm ` S ) ` x ) ) -> 0 <_ r ) ) )
12 7 11 mpan2 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( 0 <_ ( N ` F ) <-> A. r e. ( 0 [,) +oo ) ( A. x e. ( Base ` S ) ( ( norm ` T ) ` ( F ` x ) ) <_ ( r x. ( ( norm ` S ) ` x ) ) -> 0 <_ r ) ) )
13 6 12 mpbird 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> 0 <_ ( N ` F ) )