Metamath Proof Explorer

Theorem nmolb2d

Description: Any upper bound on the values of a linear operator at nonzero vectors translates to an upper bound on the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015)

Ref Expression
Hypotheses nmofval.1 
|- N = ( S normOp T )
nmofval.2 
|- V = ( Base ` S )
nmofval.3 
|- L = ( norm ` S )
nmofval.4 
|- M = ( norm ` T )
nmolb2d.z 
|- .0. = ( 0g ` S )
nmolb2d.1 
|- ( ph -> S e. NrmGrp )
nmolb2d.2 
|- ( ph -> T e. NrmGrp )
nmolb2d.3 
|- ( ph -> F e. ( S GrpHom T ) )
nmolb2d.4 
|- ( ph -> A e. RR )
nmolb2d.5 
|- ( ph -> 0 <_ A )
nmolb2d.6 
|- ( ( ph /\ ( x e. V /\ x =/= .0. ) ) -> ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) )
Assertion nmolb2d 
|- ( ph -> ( N ` F ) <_ A )

Proof

Step Hyp Ref Expression
1 nmofval.1 
 |-  N = ( S normOp T )
2 nmofval.2 
 |-  V = ( Base ` S )
3 nmofval.3 
 |-  L = ( norm ` S )
4 nmofval.4 
 |-  M = ( norm ` T )
5 nmolb2d.z 
 |-  .0. = ( 0g ` S )
6 nmolb2d.1 
 |-  ( ph -> S e. NrmGrp )
7 nmolb2d.2 
 |-  ( ph -> T e. NrmGrp )
8 nmolb2d.3 
 |-  ( ph -> F e. ( S GrpHom T ) )
9 nmolb2d.4 
 |-  ( ph -> A e. RR )
10 nmolb2d.5 
 |-  ( ph -> 0 <_ A )
11 nmolb2d.6 
 |-  ( ( ph /\ ( x e. V /\ x =/= .0. ) ) -> ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) )
12 2fveq3 
 |-  ( x = .0. -> ( M ` ( F ` x ) ) = ( M ` ( F ` .0. ) ) )
13 fveq2 
 |-  ( x = .0. -> ( L ` x ) = ( L ` .0. ) )
14 13 oveq2d 
 |-  ( x = .0. -> ( A x. ( L ` x ) ) = ( A x. ( L ` .0. ) ) )
15 12 14 breq12d 
 |-  ( x = .0. -> ( ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) <-> ( M ` ( F ` .0. ) ) <_ ( A x. ( L ` .0. ) ) ) )
16 11 anassrs 
 |-  ( ( ( ph /\ x e. V ) /\ x =/= .0. ) -> ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) )
17 0le0 
 |-  0 <_ 0
18 9 recnd 
 |-  ( ph -> A e. CC )
19 18 mul01d 
 |-  ( ph -> ( A x. 0 ) = 0 )
20 17 19 breqtrrid 
 |-  ( ph -> 0 <_ ( A x. 0 ) )
21 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
22 5 21 ghmid 
 |-  ( F e. ( S GrpHom T ) -> ( F ` .0. ) = ( 0g ` T ) )
23 8 22 syl 
 |-  ( ph -> ( F ` .0. ) = ( 0g ` T ) )
24 23 fveq2d 
 |-  ( ph -> ( M ` ( F ` .0. ) ) = ( M ` ( 0g ` T ) ) )
25 4 21 nm0 
 |-  ( T e. NrmGrp -> ( M ` ( 0g ` T ) ) = 0 )
26 7 25 syl 
 |-  ( ph -> ( M ` ( 0g ` T ) ) = 0 )
27 24 26 eqtrd 
 |-  ( ph -> ( M ` ( F ` .0. ) ) = 0 )
28 3 5 nm0 
 |-  ( S e. NrmGrp -> ( L ` .0. ) = 0 )
29 6 28 syl 
 |-  ( ph -> ( L ` .0. ) = 0 )
30 29 oveq2d 
 |-  ( ph -> ( A x. ( L ` .0. ) ) = ( A x. 0 ) )
31 20 27 30 3brtr4d 
 |-  ( ph -> ( M ` ( F ` .0. ) ) <_ ( A x. ( L ` .0. ) ) )
32 31 adantr 
 |-  ( ( ph /\ x e. V ) -> ( M ` ( F ` .0. ) ) <_ ( A x. ( L ` .0. ) ) )
33 15 16 32 pm2.61ne 
 |-  ( ( ph /\ x e. V ) -> ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) )
34 33 ralrimiva 
 |-  ( ph -> A. x e. V ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) )
35 1 2 3 4 nmolb 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ A e. RR /\ 0 <_ A ) -> ( A. x e. V ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) -> ( N ` F ) <_ A ) )
36 6 7 8 9 10 35 syl311anc 
 |-  ( ph -> ( A. x e. V ( M ` ( F ` x ) ) <_ ( A x. ( L ` x ) ) -> ( N ` F ) <_ A ) )
37 34 36 mpd 
 |-  ( ph -> ( N ` F ) <_ A )