Metamath Proof Explorer

Theorem nmblolbii

Description: A lower bound for the norm of a bounded linear operator. (Contributed by NM, 7-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmblolbi.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nmblolbi.4 ⊢ 𝐿 = ( normCV ‘ 𝑈 )
nmblolbi.5 ⊢ 𝑀 = ( normCV ‘ 𝑊 )
nmblolbi.6 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
nmblolbi.7 ⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
nmblolbi.u ⊢ 𝑈 ∈ NrmCVec
nmblolbi.w ⊢ 𝑊 ∈ NrmCVec
nmblolbii.b ⊢ 𝑇 ∈ 𝐵
Assertion nmblolbii ( 𝐴 ∈ 𝑋 → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 nmblolbi.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nmblolbi.4 ⊢ 𝐿 = ( normCV ‘ 𝑈 )
3 nmblolbi.5 ⊢ 𝑀 = ( normCV ‘ 𝑊 )
4 nmblolbi.6 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
5 nmblolbi.7 ⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
6 nmblolbi.u ⊢ 𝑈 ∈ NrmCVec
7 nmblolbi.w ⊢ 𝑊 ∈ NrmCVec
8 nmblolbii.b ⊢ 𝑇 ∈ 𝐵
9 fveq2 ⊢ ( 𝐴 = ( 0vec ‘ 𝑈 ) → ( 𝑇 ‘ 𝐴 ) = ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) )
10 9 fveq2d ⊢ ( 𝐴 = ( 0vec ‘ 𝑈 ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) )
11 fveq2 ⊢ ( 𝐴 = ( 0vec ‘ 𝑈 ) → ( 𝐿 ‘ 𝐴 ) = ( 𝐿 ‘ ( 0vec ‘ 𝑈 ) ) )
12 11 oveq2d ⊢ ( 𝐴 = ( 0vec ‘ 𝑈 ) → ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ 𝐴 ) ) = ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ ( 0vec ‘ 𝑈 ) ) ) )
13 10 12 breq12d ⊢ ( 𝐴 = ( 0vec ‘ 𝑈 ) → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ 𝐴 ) ) ↔ ( 𝑀 ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ ( 0vec ‘ 𝑈 ) ) ) ) )
14 1 2 nvcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐿 ‘ 𝐴 ) ∈ ℝ )
15 6 14 mpan ⊢ ( 𝐴 ∈ 𝑋 → ( 𝐿 ‘ 𝐴 ) ∈ ℝ )
16 15 adantr ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝐿 ‘ 𝐴 ) ∈ ℝ )
17 eqid ⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
18 1 17 2 nvz ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐿 ‘ 𝐴 ) = 0 ↔ 𝐴 = ( 0vec ‘ 𝑈 ) ) )
19 6 18 mpan ⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝐿 ‘ 𝐴 ) = 0 ↔ 𝐴 = ( 0vec ‘ 𝑈 ) ) )
20 19 necon3bid ⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝐿 ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) )
21 20 biimpar ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝐿 ‘ 𝐴 ) ≠ 0 )
22 16 21 rereccld ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 1 / ( 𝐿 ‘ 𝐴 ) ) ∈ ℝ )
23 1 17 2 nvgt0 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ≠ ( 0vec ‘ 𝑈 ) ↔ 0 < ( 𝐿 ‘ 𝐴 ) ) )
24 6 23 mpan ⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 ≠ ( 0vec ‘ 𝑈 ) ↔ 0 < ( 𝐿 ‘ 𝐴 ) ) )
25 24 biimpa ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → 0 < ( 𝐿 ‘ 𝐴 ) )
26 16 25 recgt0d ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → 0 < ( 1 / ( 𝐿 ‘ 𝐴 ) ) )
27 0re ⊢ 0 ∈ ℝ
28 ltle ⊢ ( ( 0 ∈ ℝ ∧ ( 1 / ( 𝐿 ‘ 𝐴 ) ) ∈ ℝ ) → ( 0 < ( 1 / ( 𝐿 ‘ 𝐴 ) ) → 0 ≤ ( 1 / ( 𝐿 ‘ 𝐴 ) ) ) )
29 27 22 28 sylancr ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 0 < ( 1 / ( 𝐿 ‘ 𝐴 ) ) → 0 ≤ ( 1 / ( 𝐿 ‘ 𝐴 ) ) ) )
30 26 29 mpd ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → 0 ≤ ( 1 / ( 𝐿 ‘ 𝐴 ) ) )
31 eqid ⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
32 1 31 5 blof ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
33 6 7 8 32 mp3an ⊢ 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 )
34 33 ffvelcdmi ⊢ ( 𝐴 ∈ 𝑋 → ( 𝑇 ‘ 𝐴 ) ∈ ( BaseSet ‘ 𝑊 ) )
35 34 adantr ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝑇 ‘ 𝐴 ) ∈ ( BaseSet ‘ 𝑊 ) )
36 eqid ⊢ ( ·𝑠OLD ‘ 𝑊 ) = ( ·𝑠OLD ‘ 𝑊 )
37 31 36 3 nvsge0 ⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( 1 / ( 𝐿 ‘ 𝐴 ) ) ) ∧ ( 𝑇 ‘ 𝐴 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( 𝑀 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝐴 ) ) ) = ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) · ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
38 7 37 mp3an1 ⊢ ( ( ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( 1 / ( 𝐿 ‘ 𝐴 ) ) ) ∧ ( 𝑇 ‘ 𝐴 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( 𝑀 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝐴 ) ) ) = ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) · ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
39 22 30 35 38 syl21anc ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝑀 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝐴 ) ) ) = ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) · ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
40 22 recnd ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 1 / ( 𝐿 ‘ 𝐴 ) ) ∈ ℂ )
41 simpl ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → 𝐴 ∈ 𝑋 )
42 eqid ⊢ ( 𝑈 LnOp 𝑊 ) = ( 𝑈 LnOp 𝑊 )
43 42 5 bloln ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → 𝑇 ∈ ( 𝑈 LnOp 𝑊 ) )
44 6 7 8 43 mp3an ⊢ 𝑇 ∈ ( 𝑈 LnOp 𝑊 )
45 6 7 44 3pm3.2i ⊢ ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ ( 𝑈 LnOp 𝑊 ) )
46 eqid ⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
47 1 46 36 42 lnomul ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ ( 𝑈 LnOp 𝑊 ) ) ∧ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝑇 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) = ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝐴 ) ) )
48 45 47 mpan ⊢ ( ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑇 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) = ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝐴 ) ) )
49 40 41 48 syl2anc ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝑇 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) = ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝐴 ) ) )
50 49 fveq2d ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) = ( 𝑀 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝑇 ‘ 𝐴 ) ) ) )
51 31 3 nvcl ⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 𝑇 ‘ 𝐴 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ ℝ )
52 7 34 51 sylancr ⊢ ( 𝐴 ∈ 𝑋 → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ ℝ )
53 52 adantr ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ ℝ )
54 53 recnd ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ ℂ )
55 16 recnd ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝐿 ‘ 𝐴 ) ∈ ℂ )
56 54 55 21 divrec2d ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) / ( 𝐿 ‘ 𝐴 ) ) = ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) · ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ) )
57 39 50 56 3eqtr4rd ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) / ( 𝐿 ‘ 𝐴 ) ) = ( 𝑀 ‘ ( 𝑇 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) )
58 1 46 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 1 / ( 𝐿 ‘ 𝐴 ) ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 )
59 6 58 mp3an1 ⊢ ( ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 )
60 59 ancoms ⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 1 / ( 𝐿 ‘ 𝐴 ) ) ∈ ℂ ) → ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 )
61 40 60 syldan ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 )
62 1 2 nvcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 ) → ( 𝐿 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ∈ ℝ )
63 6 61 62 sylancr ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝐿 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ∈ ℝ )
64 1 46 17 2 nv1 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝐿 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) = 1 )
65 6 64 mp3an1 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝐿 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) = 1 )
66 eqle ⊢ ( ( ( 𝐿 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ∈ ℝ ∧ ( 𝐿 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) = 1 ) → ( 𝐿 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ≤ 1 )
67 63 65 66 syl2anc ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝐿 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ≤ 1 )
68 6 7 33 3pm3.2i ⊢ ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
69 1 31 2 3 4 nmoolb ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ) ∧ ( ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 ∧ ( 𝐿 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ≤ 1 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ≤ ( 𝑁 ‘ 𝑇 ) )
70 68 69 mpan ⊢ ( ( ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 ∧ ( 𝐿 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ≤ 1 ) → ( 𝑀 ‘ ( 𝑇 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ≤ ( 𝑁 ‘ 𝑇 ) )
71 61 67 70 syl2anc ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ ( ( 1 / ( 𝐿 ‘ 𝐴 ) ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ≤ ( 𝑁 ‘ 𝑇 ) )
72 57 71 eqbrtrd ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) / ( 𝐿 ‘ 𝐴 ) ) ≤ ( 𝑁 ‘ 𝑇 ) )
73 1 31 4 5 nmblore ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑇 ) ∈ ℝ )
74 6 7 8 73 mp3an ⊢ ( 𝑁 ‘ 𝑇 ) ∈ ℝ
75 74 a1i ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝑁 ‘ 𝑇 ) ∈ ℝ )
76 ledivmul2 ⊢ ( ( ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ ℝ ∧ ( 𝑁 ‘ 𝑇 ) ∈ ℝ ∧ ( ( 𝐿 ‘ 𝐴 ) ∈ ℝ ∧ 0 < ( 𝐿 ‘ 𝐴 ) ) ) → ( ( ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) / ( 𝐿 ‘ 𝐴 ) ) ≤ ( 𝑁 ‘ 𝑇 ) ↔ ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ 𝐴 ) ) ) )
77 53 75 16 25 76 syl112anc ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( ( ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) / ( 𝐿 ‘ 𝐴 ) ) ≤ ( 𝑁 ‘ 𝑇 ) ↔ ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ 𝐴 ) ) ) )
78 72 77 mpbid ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ ( 0vec ‘ 𝑈 ) ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ 𝐴 ) ) )
79 0le0 ⊢ 0 ≤ 0
80 eqid ⊢ ( 0vec ‘ 𝑊 ) = ( 0vec ‘ 𝑊 )
81 1 31 17 80 42 lno0 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ ( 𝑈 LnOp 𝑊 ) ) → ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) = ( 0vec ‘ 𝑊 ) )
82 6 7 44 81 mp3an ⊢ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) = ( 0vec ‘ 𝑊 )
83 82 fveq2i ⊢ ( 𝑀 ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) = ( 𝑀 ‘ ( 0vec ‘ 𝑊 ) )
84 80 3 nvz0 ⊢ ( 𝑊 ∈ NrmCVec → ( 𝑀 ‘ ( 0vec ‘ 𝑊 ) ) = 0 )
85 7 84 ax-mp ⊢ ( 𝑀 ‘ ( 0vec ‘ 𝑊 ) ) = 0
86 83 85 eqtri ⊢ ( 𝑀 ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) = 0
87 17 2 nvz0 ⊢ ( 𝑈 ∈ NrmCVec → ( 𝐿 ‘ ( 0vec ‘ 𝑈 ) ) = 0 )
88 6 87 ax-mp ⊢ ( 𝐿 ‘ ( 0vec ‘ 𝑈 ) ) = 0
89 88 oveq2i ⊢ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ ( 0vec ‘ 𝑈 ) ) ) = ( ( 𝑁 ‘ 𝑇 ) · 0 )
90 74 recni ⊢ ( 𝑁 ‘ 𝑇 ) ∈ ℂ
91 90 mul01i ⊢ ( ( 𝑁 ‘ 𝑇 ) · 0 ) = 0
92 89 91 eqtri ⊢ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ ( 0vec ‘ 𝑈 ) ) ) = 0
93 79 86 92 3brtr4i ⊢ ( 𝑀 ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ ( 0vec ‘ 𝑈 ) ) )
94 93 a1i ⊢ ( 𝐴 ∈ 𝑋 → ( 𝑀 ‘ ( 𝑇 ‘ ( 0vec ‘ 𝑈 ) ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ ( 0vec ‘ 𝑈 ) ) ) )
95 13 78 94 pm2.61ne ⊢ ( 𝐴 ∈ 𝑋 → ( 𝑀 ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( 𝑁 ‘ 𝑇 ) · ( 𝐿 ‘ 𝐴 ) ) )