This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nmlnoubi

Description: An upper bound for the operator norm of a linear operator, using only the properties of nonzero arguments. (Contributed by NM, 1-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses nmlnoubi.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nmlnoubi.z ⊢ 𝑍 = ( 0vec ‘ 𝑈 )
nmlnoubi.k ⊢ 𝐾 = ( normCV ‘ 𝑈 )
nmlnoubi.m ⊢ 𝑀 = ( normCV ‘ 𝑊 )
nmlnoubi.3 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
nmlnoubi.7 ⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
nmlnoubi.u ⊢ 𝑈 ∈ NrmCVec
nmlnoubi.w ⊢ 𝑊 ∈ NrmCVec
Assertion nmlnoubi ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) ) → ( 𝑁 ‘ 𝑇 ) ≤ 𝐴 )

Proof

Step Hyp Ref Expression
1 nmlnoubi.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nmlnoubi.z ⊢ 𝑍 = ( 0vec ‘ 𝑈 )
3 nmlnoubi.k ⊢ 𝐾 = ( normCV ‘ 𝑈 )
4 nmlnoubi.m ⊢ 𝑀 = ( normCV ‘ 𝑊 )
5 nmlnoubi.3 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
6 nmlnoubi.7 ⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
7 nmlnoubi.u ⊢ 𝑈 ∈ NrmCVec
8 nmlnoubi.w ⊢ 𝑊 ∈ NrmCVec
9 2fveq3 ⊢ ( 𝑥 = 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ 𝑍 ) ) )
10 fveq2 ⊢ ( 𝑥 = 𝑍 → ( 𝐾 ‘ 𝑥 ) = ( 𝐾 ‘ 𝑍 ) )
11 10 oveq2d ⊢ ( 𝑥 = 𝑍 → ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) = ( 𝐴 · ( 𝐾 ‘ 𝑍 ) ) )
12 9 11 breq12d ⊢ ( 𝑥 = 𝑍 → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ↔ ( 𝑀 ‘ ( 𝑇 ‘ 𝑍 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑍 ) ) ) )
13 id ⊢ ( ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) → ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) )
14 13 imp ⊢ ( ( ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) ∧ 𝑥 ≠ 𝑍 ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) )
15 14 adantll ⊢ ( ( ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) ∧ ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ≠ 𝑍 ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) )
16 0le0 ⊢ 0 ≤ 0
17 eqid ⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
18 eqid ⊢ ( 0vec ‘ 𝑊 ) = ( 0vec ‘ 𝑊 )
19 1 17 2 18 6 lno0 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( 𝑇 ‘ 𝑍 ) = ( 0vec ‘ 𝑊 ) )
20 7 8 19 mp3an12 ⊢ ( 𝑇 ∈ 𝐿 → ( 𝑇 ‘ 𝑍 ) = ( 0vec ‘ 𝑊 ) )
21 20 fveq2d ⊢ ( 𝑇 ∈ 𝐿 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑍 ) ) = ( 𝑀 ‘ ( 0vec ‘ 𝑊 ) ) )
22 18 4 nvz0 ⊢ ( 𝑊 ∈ NrmCVec → ( 𝑀 ‘ ( 0vec ‘ 𝑊 ) ) = 0 )
23 8 22 ax-mp ⊢ ( 𝑀 ‘ ( 0vec ‘ 𝑊 ) ) = 0
24 21 23 eqtrdi ⊢ ( 𝑇 ∈ 𝐿 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑍 ) ) = 0 )
25 24 adantr ⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑍 ) ) = 0 )
26 2 3 nvz0 ⊢ ( 𝑈 ∈ NrmCVec → ( 𝐾 ‘ 𝑍 ) = 0 )
27 7 26 ax-mp ⊢ ( 𝐾 ‘ 𝑍 ) = 0
28 27 oveq2i ⊢ ( 𝐴 · ( 𝐾 ‘ 𝑍 ) ) = ( 𝐴 · 0 )
29 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
30 29 mul01d ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 0 ) = 0 )
31 28 30 eqtrid ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · ( 𝐾 ‘ 𝑍 ) ) = 0 )
32 31 ad2antrl ⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) → ( 𝐴 · ( 𝐾 ‘ 𝑍 ) ) = 0 )
33 25 32 breq12d ⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑍 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑍 ) ) ↔ 0 ≤ 0 ) )
34 16 33 mpbiri ⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑍 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑍 ) ) )
35 34 adantr ⊢ ( ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) ∧ ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑍 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑍 ) ) )
36 12 15 35 pm2.61ne ⊢ ( ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) ∧ ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) )
37 36 ex ⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) → ( ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) )
38 37 ralimdv ⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) → ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) )
39 38 3impia ⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) ) → ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) )
40 1 17 6 lnof ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
41 7 8 40 mp3an12 ⊢ ( 𝑇 ∈ 𝐿 → 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
42 1 17 3 4 5 7 8 nmoub2i ⊢ ( ( 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) → ( 𝑁 ‘ 𝑇 ) ≤ 𝐴 )
43 41 42 syl3an1 ⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) → ( 𝑁 ‘ 𝑇 ) ≤ 𝐴 )
44 39 43 syld3an3 ⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑥 ≠ 𝑍 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐾 ‘ 𝑥 ) ) ) ) → ( 𝑁 ‘ 𝑇 ) ≤ 𝐴 )