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 syl5eq ( 𝐴 ∈ ℝ → ( 𝐴 · ( 𝐾𝑍 ) ) = 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 ≤ 𝐴 ) ∧ ∀ 𝑥𝑋 ( 𝑥𝑍 → ( 𝑀 ‘ ( 𝑇𝑥 ) ) ≤ ( 𝐴 · ( 𝐾𝑥 ) ) ) ) → ( 𝑁𝑇 ) ≤ 𝐴 )