Metamath Proof Explorer

Theorem nmo0

Description: The operator norm of the zero operator. (Contributed by Mario Carneiro, 20-Oct-2015)

Ref Expression
Hypotheses nmo0.1 
|- N = ( S normOp T )
nmo0.2 
|- V = ( Base ` S )
nmo0.3 
|- .0. = ( 0g ` T )
Assertion nmo0 
|- ( ( S e. NrmGrp /\ T e. NrmGrp ) -> ( N ` ( V X. { .0. } ) ) = 0 )

Proof

Step Hyp Ref Expression
1 nmo0.1 
 |-  N = ( S normOp T )
2 nmo0.2 
 |-  V = ( Base ` S )
3 nmo0.3 
 |-  .0. = ( 0g ` T )
4 eqid 
 |-  ( norm ` S ) = ( norm ` S )
5 eqid 
 |-  ( norm ` T ) = ( norm ` T )
6 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
7 simpl 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> S e. NrmGrp )
8 simpr 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> T e. NrmGrp )
9 ngpgrp 
 |-  ( S e. NrmGrp -> S e. Grp )
10 ngpgrp 
 |-  ( T e. NrmGrp -> T e. Grp )
11 3 2 0ghm 
 |-  ( ( S e. Grp /\ T e. Grp ) -> ( V X. { .0. } ) e. ( S GrpHom T ) )
12 9 10 11 syl2an 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> ( V X. { .0. } ) e. ( S GrpHom T ) )
13 0red 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> 0 e. RR )
14 0le0 
 |-  0 <_ 0
15 14 a1i 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> 0 <_ 0 )
16 3 fvexi 
 |-  .0. e. _V
17 16 fvconst2 
 |-  ( x e. V -> ( ( V X. { .0. } ) ` x ) = .0. )
18 17 ad2antrl 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp ) /\ ( x e. V /\ x =/= ( 0g ` S ) ) ) -> ( ( V X. { .0. } ) ` x ) = .0. )
19 18 fveq2d 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp ) /\ ( x e. V /\ x =/= ( 0g ` S ) ) ) -> ( ( norm ` T ) ` ( ( V X. { .0. } ) ` x ) ) = ( ( norm ` T ) ` .0. ) )
20 5 3 nm0 
 |-  ( T e. NrmGrp -> ( ( norm ` T ) ` .0. ) = 0 )
21 20 ad2antlr 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp ) /\ ( x e. V /\ x =/= ( 0g ` S ) ) ) -> ( ( norm ` T ) ` .0. ) = 0 )
22 19 21 eqtrd 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp ) /\ ( x e. V /\ x =/= ( 0g ` S ) ) ) -> ( ( norm ` T ) ` ( ( V X. { .0. } ) ` x ) ) = 0 )
23 2 4 nmcl 
 |-  ( ( S e. NrmGrp /\ x e. V ) -> ( ( norm ` S ) ` x ) e. RR )
24 23 ad2ant2r 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp ) /\ ( x e. V /\ x =/= ( 0g ` S ) ) ) -> ( ( norm ` S ) ` x ) e. RR )
25 24 recnd 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp ) /\ ( x e. V /\ x =/= ( 0g ` S ) ) ) -> ( ( norm ` S ) ` x ) e. CC )
26 25 mul02d 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp ) /\ ( x e. V /\ x =/= ( 0g ` S ) ) ) -> ( 0 x. ( ( norm ` S ) ` x ) ) = 0 )
27 14 26 breqtrrid 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp ) /\ ( x e. V /\ x =/= ( 0g ` S ) ) ) -> 0 <_ ( 0 x. ( ( norm ` S ) ` x ) ) )
28 22 27 eqbrtrd 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp ) /\ ( x e. V /\ x =/= ( 0g ` S ) ) ) -> ( ( norm ` T ) ` ( ( V X. { .0. } ) ` x ) ) <_ ( 0 x. ( ( norm ` S ) ` x ) ) )
29 1 2 4 5 6 7 8 12 13 15 28 nmolb2d 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> ( N ` ( V X. { .0. } ) ) <_ 0 )
30 1 nmoge0 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ ( V X. { .0. } ) e. ( S GrpHom T ) ) -> 0 <_ ( N ` ( V X. { .0. } ) ) )
31 12 30 mpd3an3 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> 0 <_ ( N ` ( V X. { .0. } ) ) )
32 1 nmocl 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ ( V X. { .0. } ) e. ( S GrpHom T ) ) -> ( N ` ( V X. { .0. } ) ) e. RR* )
33 12 32 mpd3an3 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> ( N ` ( V X. { .0. } ) ) e. RR* )
34 0xr 
 |-  0 e. RR*
35 xrletri3 
 |-  ( ( ( N ` ( V X. { .0. } ) ) e. RR* /\ 0 e. RR* ) -> ( ( N ` ( V X. { .0. } ) ) = 0 <-> ( ( N ` ( V X. { .0. } ) ) <_ 0 /\ 0 <_ ( N ` ( V X. { .0. } ) ) ) ) )
36 33 34 35 sylancl 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> ( ( N ` ( V X. { .0. } ) ) = 0 <-> ( ( N ` ( V X. { .0. } ) ) <_ 0 /\ 0 <_ ( N ` ( V X. { .0. } ) ) ) ) )
37 29 31 36 mpbir2and 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> ( N ` ( V X. { .0. } ) ) = 0 )