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 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) / ( 𝐿 ‘ 𝑋 ) ) ≤ ( 𝑁 ‘ 𝐹 ) )