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 𝑁 = ( 𝑆 normOp 𝑇 )
nmoi.2 𝑉 = ( Base ‘ 𝑆 )
nmoi.3 𝐿 = ( norm ‘ 𝑆 )
nmoi.4 𝑀 = ( norm ‘ 𝑇 )
nmoi2.z 0 = ( 0g𝑆 )
Assertion nmoi2 ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( ( 𝑀 ‘ ( 𝐹𝑋 ) ) / ( 𝐿𝑋 ) ) ≤ ( 𝑁𝐹 ) )

Proof

Step Hyp Ref Expression
1 nmofval.1 𝑁 = ( 𝑆 normOp 𝑇 )
2 nmoi.2 𝑉 = ( Base ‘ 𝑆 )
3 nmoi.3 𝐿 = ( norm ‘ 𝑆 )
4 nmoi.4 𝑀 = ( norm ‘ 𝑇 )
5 nmoi2.z 0 = ( 0g𝑆 )
6 simpl2 ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → 𝑇 ∈ NrmGrp )
7 simpl3 ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
8 eqid ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
9 2 8 ghmf ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
10 7 9 syl ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
11 simprl ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → 𝑋𝑉 )
12 10 11 ffvelrnd ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( 𝐹𝑋 ) ∈ ( Base ‘ 𝑇 ) )
13 8 4 nmcl ( ( 𝑇 ∈ NrmGrp ∧ ( 𝐹𝑋 ) ∈ ( Base ‘ 𝑇 ) ) → ( 𝑀 ‘ ( 𝐹𝑋 ) ) ∈ ℝ )
14 6 12 13 syl2anc ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( 𝑀 ‘ ( 𝐹𝑋 ) ) ∈ ℝ )
15 14 rexrd ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( 𝑀 ‘ ( 𝐹𝑋 ) ) ∈ ℝ* )
16 1 nmocl ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝑁𝐹 ) ∈ ℝ* )
17 16 adantr ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( 𝑁𝐹 ) ∈ ℝ* )
18 2 3 5 nmrpcl ( ( 𝑆 ∈ NrmGrp ∧ 𝑋𝑉𝑋0 ) → ( 𝐿𝑋 ) ∈ ℝ+ )
19 18 3expb ( ( 𝑆 ∈ NrmGrp ∧ ( 𝑋𝑉𝑋0 ) ) → ( 𝐿𝑋 ) ∈ ℝ+ )
20 19 3ad2antl1 ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( 𝐿𝑋 ) ∈ ℝ+ )
21 20 rpxrd ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( 𝐿𝑋 ) ∈ ℝ* )
22 17 21 xmulcld ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( ( 𝑁𝐹 ) ·e ( 𝐿𝑋 ) ) ∈ ℝ* )
23 20 rpreccld ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( 1 / ( 𝐿𝑋 ) ) ∈ ℝ+ )
24 23 rpxrd ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( 1 / ( 𝐿𝑋 ) ) ∈ ℝ* )
25 23 rpge0d ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → 0 ≤ ( 1 / ( 𝐿𝑋 ) ) )
26 24 25 jca ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( ( 1 / ( 𝐿𝑋 ) ) ∈ ℝ* ∧ 0 ≤ ( 1 / ( 𝐿𝑋 ) ) ) )
27 1 2 3 4 nmoix ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋𝑉 ) → ( 𝑀 ‘ ( 𝐹𝑋 ) ) ≤ ( ( 𝑁𝐹 ) ·e ( 𝐿𝑋 ) ) )
28 27 adantrr ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( 𝑀 ‘ ( 𝐹𝑋 ) ) ≤ ( ( 𝑁𝐹 ) ·e ( 𝐿𝑋 ) ) )
29 xlemul1a ( ( ( ( 𝑀 ‘ ( 𝐹𝑋 ) ) ∈ ℝ* ∧ ( ( 𝑁𝐹 ) ·e ( 𝐿𝑋 ) ) ∈ ℝ* ∧ ( ( 1 / ( 𝐿𝑋 ) ) ∈ ℝ* ∧ 0 ≤ ( 1 / ( 𝐿𝑋 ) ) ) ) ∧ ( 𝑀 ‘ ( 𝐹𝑋 ) ) ≤ ( ( 𝑁𝐹 ) ·e ( 𝐿𝑋 ) ) ) → ( ( 𝑀 ‘ ( 𝐹𝑋 ) ) ·e ( 1 / ( 𝐿𝑋 ) ) ) ≤ ( ( ( 𝑁𝐹 ) ·e ( 𝐿𝑋 ) ) ·e ( 1 / ( 𝐿𝑋 ) ) ) )
30 15 22 26 28 29 syl31anc ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( ( 𝑀 ‘ ( 𝐹𝑋 ) ) ·e ( 1 / ( 𝐿𝑋 ) ) ) ≤ ( ( ( 𝑁𝐹 ) ·e ( 𝐿𝑋 ) ) ·e ( 1 / ( 𝐿𝑋 ) ) ) )
31 23 rpred ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( 1 / ( 𝐿𝑋 ) ) ∈ ℝ )
32 rexmul ( ( ( 𝑀 ‘ ( 𝐹𝑋 ) ) ∈ ℝ ∧ ( 1 / ( 𝐿𝑋 ) ) ∈ ℝ ) → ( ( 𝑀 ‘ ( 𝐹𝑋 ) ) ·e ( 1 / ( 𝐿𝑋 ) ) ) = ( ( 𝑀 ‘ ( 𝐹𝑋 ) ) · ( 1 / ( 𝐿𝑋 ) ) ) )
33 14 31 32 syl2anc ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( ( 𝑀 ‘ ( 𝐹𝑋 ) ) ·e ( 1 / ( 𝐿𝑋 ) ) ) = ( ( 𝑀 ‘ ( 𝐹𝑋 ) ) · ( 1 / ( 𝐿𝑋 ) ) ) )
34 14 recnd ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( 𝑀 ‘ ( 𝐹𝑋 ) ) ∈ ℂ )
35 20 rpcnd ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( 𝐿𝑋 ) ∈ ℂ )
36 20 rpne0d ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( 𝐿𝑋 ) ≠ 0 )
37 34 35 36 divrecd ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( ( 𝑀 ‘ ( 𝐹𝑋 ) ) / ( 𝐿𝑋 ) ) = ( ( 𝑀 ‘ ( 𝐹𝑋 ) ) · ( 1 / ( 𝐿𝑋 ) ) ) )
38 33 37 eqtr4d ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( ( 𝑀 ‘ ( 𝐹𝑋 ) ) ·e ( 1 / ( 𝐿𝑋 ) ) ) = ( ( 𝑀 ‘ ( 𝐹𝑋 ) ) / ( 𝐿𝑋 ) ) )
39 xmulass ( ( ( 𝑁𝐹 ) ∈ ℝ* ∧ ( 𝐿𝑋 ) ∈ ℝ* ∧ ( 1 / ( 𝐿𝑋 ) ) ∈ ℝ* ) → ( ( ( 𝑁𝐹 ) ·e ( 𝐿𝑋 ) ) ·e ( 1 / ( 𝐿𝑋 ) ) ) = ( ( 𝑁𝐹 ) ·e ( ( 𝐿𝑋 ) ·e ( 1 / ( 𝐿𝑋 ) ) ) ) )
40 17 21 24 39 syl3anc ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( ( ( 𝑁𝐹 ) ·e ( 𝐿𝑋 ) ) ·e ( 1 / ( 𝐿𝑋 ) ) ) = ( ( 𝑁𝐹 ) ·e ( ( 𝐿𝑋 ) ·e ( 1 / ( 𝐿𝑋 ) ) ) ) )
41 20 rpred ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( 𝐿𝑋 ) ∈ ℝ )
42 rexmul ( ( ( 𝐿𝑋 ) ∈ ℝ ∧ ( 1 / ( 𝐿𝑋 ) ) ∈ ℝ ) → ( ( 𝐿𝑋 ) ·e ( 1 / ( 𝐿𝑋 ) ) ) = ( ( 𝐿𝑋 ) · ( 1 / ( 𝐿𝑋 ) ) ) )
43 41 31 42 syl2anc ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( ( 𝐿𝑋 ) ·e ( 1 / ( 𝐿𝑋 ) ) ) = ( ( 𝐿𝑋 ) · ( 1 / ( 𝐿𝑋 ) ) ) )
44 35 36 recidd ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( ( 𝐿𝑋 ) · ( 1 / ( 𝐿𝑋 ) ) ) = 1 )
45 43 44 eqtrd ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( ( 𝐿𝑋 ) ·e ( 1 / ( 𝐿𝑋 ) ) ) = 1 )
46 45 oveq2d ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( ( 𝑁𝐹 ) ·e ( ( 𝐿𝑋 ) ·e ( 1 / ( 𝐿𝑋 ) ) ) ) = ( ( 𝑁𝐹 ) ·e 1 ) )
47 xmulid1 ( ( 𝑁𝐹 ) ∈ ℝ* → ( ( 𝑁𝐹 ) ·e 1 ) = ( 𝑁𝐹 ) )
48 17 47 syl ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( ( 𝑁𝐹 ) ·e 1 ) = ( 𝑁𝐹 ) )
49 40 46 48 3eqtrd ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( ( ( 𝑁𝐹 ) ·e ( 𝐿𝑋 ) ) ·e ( 1 / ( 𝐿𝑋 ) ) ) = ( 𝑁𝐹 ) )
50 30 38 49 3brtr3d ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋𝑉𝑋0 ) ) → ( ( 𝑀 ‘ ( 𝐹𝑋 ) ) / ( 𝐿𝑋 ) ) ≤ ( 𝑁𝐹 ) )