Metamath Proof Explorer

Theorem nmoi2

Description: The operator norm is a bound on the growth of a vector under the action of the operator. (Contributed by Mario Carneiro, 19-Oct-2015)

Ref Expression
Hypotheses nmofval.1 
|- N = ( S normOp T )
nmoi.2 
|- V = ( Base ` S )
nmoi.3 
|- L = ( norm ` S )
nmoi.4 
|- M = ( norm ` T )
nmoi2.z 
|- .0. = ( 0g ` S )
Assertion nmoi2 
|- ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( ( M ` ( F ` X ) ) / ( L ` X ) ) <_ ( N ` F ) )

Proof

Step Hyp Ref Expression
1 nmofval.1 
 |-  N = ( S normOp T )
2 nmoi.2 
 |-  V = ( Base ` S )
3 nmoi.3 
 |-  L = ( norm ` S )
4 nmoi.4 
 |-  M = ( norm ` T )
5 nmoi2.z 
 |-  .0. = ( 0g ` S )
6 simpl2 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> T e. NrmGrp )
7 simpl3 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> F e. ( S GrpHom T ) )
8 eqid 
 |-  ( Base ` T ) = ( Base ` T )
9 2 8 ghmf 
 |-  ( F e. ( S GrpHom T ) -> F : V --> ( Base ` T ) )
10 7 9 syl 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> F : V --> ( Base ` T ) )
11 simprl 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> X e. V )
12 10 11 ffvelrnd 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( F ` X ) e. ( Base ` T ) )
13 8 4 nmcl 
 |-  ( ( T e. NrmGrp /\ ( F ` X ) e. ( Base ` T ) ) -> ( M ` ( F ` X ) ) e. RR )
14 6 12 13 syl2anc 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( M ` ( F ` X ) ) e. RR )
15 14 rexrd 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( M ` ( F ` X ) ) e. RR* )
16 1 nmocl 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( N ` F ) e. RR* )
17 16 adantr 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( N ` F ) e. RR* )
18 2 3 5 nmrpcl 
 |-  ( ( S e. NrmGrp /\ X e. V /\ X =/= .0. ) -> ( L ` X ) e. RR+ )
19 18 3expb 
 |-  ( ( S e. NrmGrp /\ ( X e. V /\ X =/= .0. ) ) -> ( L ` X ) e. RR+ )
20 19 3ad2antl1 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( L ` X ) e. RR+ )
21 20 rpxrd 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( L ` X ) e. RR* )
22 17 21 xmulcld 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( ( N ` F ) *e ( L ` X ) ) e. RR* )
23 20 rpreccld 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( 1 / ( L ` X ) ) e. RR+ )
24 23 rpxrd 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( 1 / ( L ` X ) ) e. RR* )
25 23 rpge0d 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> 0 <_ ( 1 / ( L ` X ) ) )
26 24 25 jca 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( ( 1 / ( L ` X ) ) e. RR* /\ 0 <_ ( 1 / ( L ` X ) ) ) )
27 1 2 3 4 nmoix 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ X e. V ) -> ( M ` ( F ` X ) ) <_ ( ( N ` F ) *e ( L ` X ) ) )
28 27 adantrr 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( M ` ( F ` X ) ) <_ ( ( N ` F ) *e ( L ` X ) ) )
29 xlemul1a 
 |-  ( ( ( ( M ` ( F ` X ) ) e. RR* /\ ( ( N ` F ) *e ( L ` X ) ) e. RR* /\ ( ( 1 / ( L ` X ) ) e. RR* /\ 0 <_ ( 1 / ( L ` X ) ) ) ) /\ ( M ` ( F ` X ) ) <_ ( ( N ` F ) *e ( L ` X ) ) ) -> ( ( M ` ( F ` X ) ) *e ( 1 / ( L ` X ) ) ) <_ ( ( ( N ` F ) *e ( L ` X ) ) *e ( 1 / ( L ` X ) ) ) )
30 15 22 26 28 29 syl31anc 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( ( M ` ( F ` X ) ) *e ( 1 / ( L ` X ) ) ) <_ ( ( ( N ` F ) *e ( L ` X ) ) *e ( 1 / ( L ` X ) ) ) )
31 23 rpred 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( 1 / ( L ` X ) ) e. RR )
32 rexmul 
 |-  ( ( ( M ` ( F ` X ) ) e. RR /\ ( 1 / ( L ` X ) ) e. RR ) -> ( ( M ` ( F ` X ) ) *e ( 1 / ( L ` X ) ) ) = ( ( M ` ( F ` X ) ) x. ( 1 / ( L ` X ) ) ) )
33 14 31 32 syl2anc 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( ( M ` ( F ` X ) ) *e ( 1 / ( L ` X ) ) ) = ( ( M ` ( F ` X ) ) x. ( 1 / ( L ` X ) ) ) )
34 14 recnd 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( M ` ( F ` X ) ) e. CC )
35 20 rpcnd 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( L ` X ) e. CC )
36 20 rpne0d 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( L ` X ) =/= 0 )
37 34 35 36 divrecd 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( ( M ` ( F ` X ) ) / ( L ` X ) ) = ( ( M ` ( F ` X ) ) x. ( 1 / ( L ` X ) ) ) )
38 33 37 eqtr4d 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( ( M ` ( F ` X ) ) *e ( 1 / ( L ` X ) ) ) = ( ( M ` ( F ` X ) ) / ( L ` X ) ) )
39 xmulass 
 |-  ( ( ( N ` F ) e. RR* /\ ( L ` X ) e. RR* /\ ( 1 / ( L ` X ) ) e. RR* ) -> ( ( ( N ` F ) *e ( L ` X ) ) *e ( 1 / ( L ` X ) ) ) = ( ( N ` F ) *e ( ( L ` X ) *e ( 1 / ( L ` X ) ) ) ) )
40 17 21 24 39 syl3anc 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( ( ( N ` F ) *e ( L ` X ) ) *e ( 1 / ( L ` X ) ) ) = ( ( N ` F ) *e ( ( L ` X ) *e ( 1 / ( L ` X ) ) ) ) )
41 20 rpred 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( L ` X ) e. RR )
42 rexmul 
 |-  ( ( ( L ` X ) e. RR /\ ( 1 / ( L ` X ) ) e. RR ) -> ( ( L ` X ) *e ( 1 / ( L ` X ) ) ) = ( ( L ` X ) x. ( 1 / ( L ` X ) ) ) )
43 41 31 42 syl2anc 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( ( L ` X ) *e ( 1 / ( L ` X ) ) ) = ( ( L ` X ) x. ( 1 / ( L ` X ) ) ) )
44 35 36 recidd 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( ( L ` X ) x. ( 1 / ( L ` X ) ) ) = 1 )
45 43 44 eqtrd 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( ( L ` X ) *e ( 1 / ( L ` X ) ) ) = 1 )
46 45 oveq2d 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( ( N ` F ) *e ( ( L ` X ) *e ( 1 / ( L ` X ) ) ) ) = ( ( N ` F ) *e 1 ) )
47 xmulid1 
 |-  ( ( N ` F ) e. RR* -> ( ( N ` F ) *e 1 ) = ( N ` F ) )
48 17 47 syl 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( ( N ` F ) *e 1 ) = ( N ` F ) )
49 40 46 48 3eqtrd 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( ( ( N ` F ) *e ( L ` X ) ) *e ( 1 / ( L ` X ) ) ) = ( N ` F ) )
50 30 38 49 3brtr3d 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( X e. V /\ X =/= .0. ) ) -> ( ( M ` ( F ` X ) ) / ( L ` X ) ) <_ ( N ` F ) )