Metamath Proof Explorer


Theorem nmoleub

Description: The operator norm, defined as an infimum of upper bounds, can also be defined as a supremum of norms of F ( x ) away from zero. (Contributed by Mario Carneiro, 18-Oct-2015)

Ref Expression
Hypotheses nmofval.1 𝑁 = ( 𝑆 normOp 𝑇 )
nmoi.2 𝑉 = ( Base ‘ 𝑆 )
nmoi.3 𝐿 = ( norm ‘ 𝑆 )
nmoi.4 𝑀 = ( norm ‘ 𝑇 )
nmoi2.z 0 = ( 0g𝑆 )
nmoleub.1 ( 𝜑𝑆 ∈ NrmGrp )
nmoleub.2 ( 𝜑𝑇 ∈ NrmGrp )
nmoleub.3 ( 𝜑𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
nmoleub.4 ( 𝜑𝐴 ∈ ℝ* )
nmoleub.5 ( 𝜑 → 0 ≤ 𝐴 )
Assertion nmoleub ( 𝜑 → ( ( 𝑁𝐹 ) ≤ 𝐴 ↔ ∀ 𝑥𝑉 ( 𝑥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 nmoleub.1 ( 𝜑𝑆 ∈ NrmGrp )
7 nmoleub.2 ( 𝜑𝑇 ∈ NrmGrp )
8 nmoleub.3 ( 𝜑𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
9 nmoleub.4 ( 𝜑𝐴 ∈ ℝ* )
10 nmoleub.5 ( 𝜑 → 0 ≤ 𝐴 )
11 7 ad2antrr ( ( ( 𝜑 ∧ ( 𝑁𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥𝑉𝑥0 ) ) → 𝑇 ∈ NrmGrp )
12 eqid ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
13 2 12 ghmf ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
14 8 13 syl ( 𝜑𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
15 14 ad2antrr ( ( ( 𝜑 ∧ ( 𝑁𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥𝑉𝑥0 ) ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
16 simprl ( ( ( 𝜑 ∧ ( 𝑁𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥𝑉𝑥0 ) ) → 𝑥𝑉 )
17 ffvelrn ( ( 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) ∧ 𝑥𝑉 ) → ( 𝐹𝑥 ) ∈ ( Base ‘ 𝑇 ) )
18 15 16 17 syl2anc ( ( ( 𝜑 ∧ ( 𝑁𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥𝑉𝑥0 ) ) → ( 𝐹𝑥 ) ∈ ( Base ‘ 𝑇 ) )
19 12 4 nmcl ( ( 𝑇 ∈ NrmGrp ∧ ( 𝐹𝑥 ) ∈ ( Base ‘ 𝑇 ) ) → ( 𝑀 ‘ ( 𝐹𝑥 ) ) ∈ ℝ )
20 11 18 19 syl2anc ( ( ( 𝜑 ∧ ( 𝑁𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥𝑉𝑥0 ) ) → ( 𝑀 ‘ ( 𝐹𝑥 ) ) ∈ ℝ )
21 6 adantr ( ( 𝜑 ∧ ( 𝑁𝐹 ) ≤ 𝐴 ) → 𝑆 ∈ NrmGrp )
22 2 3 5 nmrpcl ( ( 𝑆 ∈ NrmGrp ∧ 𝑥𝑉𝑥0 ) → ( 𝐿𝑥 ) ∈ ℝ+ )
23 22 3expb ( ( 𝑆 ∈ NrmGrp ∧ ( 𝑥𝑉𝑥0 ) ) → ( 𝐿𝑥 ) ∈ ℝ+ )
24 21 23 sylan ( ( ( 𝜑 ∧ ( 𝑁𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥𝑉𝑥0 ) ) → ( 𝐿𝑥 ) ∈ ℝ+ )
25 20 24 rerpdivcld ( ( ( 𝜑 ∧ ( 𝑁𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥𝑉𝑥0 ) ) → ( ( 𝑀 ‘ ( 𝐹𝑥 ) ) / ( 𝐿𝑥 ) ) ∈ ℝ )
26 25 rexrd ( ( ( 𝜑 ∧ ( 𝑁𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥𝑉𝑥0 ) ) → ( ( 𝑀 ‘ ( 𝐹𝑥 ) ) / ( 𝐿𝑥 ) ) ∈ ℝ* )
27 1 nmocl ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝑁𝐹 ) ∈ ℝ* )
28 6 7 8 27 syl3anc ( 𝜑 → ( 𝑁𝐹 ) ∈ ℝ* )
29 28 ad2antrr ( ( ( 𝜑 ∧ ( 𝑁𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥𝑉𝑥0 ) ) → ( 𝑁𝐹 ) ∈ ℝ* )
30 9 ad2antrr ( ( ( 𝜑 ∧ ( 𝑁𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥𝑉𝑥0 ) ) → 𝐴 ∈ ℝ* )
31 6 7 8 3jca ( 𝜑 → ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) )
32 31 adantr ( ( 𝜑 ∧ ( 𝑁𝐹 ) ≤ 𝐴 ) → ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) )
33 1 2 3 4 5 nmoi2 ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑥𝑉𝑥0 ) ) → ( ( 𝑀 ‘ ( 𝐹𝑥 ) ) / ( 𝐿𝑥 ) ) ≤ ( 𝑁𝐹 ) )
34 32 33 sylan ( ( ( 𝜑 ∧ ( 𝑁𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥𝑉𝑥0 ) ) → ( ( 𝑀 ‘ ( 𝐹𝑥 ) ) / ( 𝐿𝑥 ) ) ≤ ( 𝑁𝐹 ) )
35 simplr ( ( ( 𝜑 ∧ ( 𝑁𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥𝑉𝑥0 ) ) → ( 𝑁𝐹 ) ≤ 𝐴 )
36 26 29 30 34 35 xrletrd ( ( ( 𝜑 ∧ ( 𝑁𝐹 ) ≤ 𝐴 ) ∧ ( 𝑥𝑉𝑥0 ) ) → ( ( 𝑀 ‘ ( 𝐹𝑥 ) ) / ( 𝐿𝑥 ) ) ≤ 𝐴 )
37 36 expr ( ( ( 𝜑 ∧ ( 𝑁𝐹 ) ≤ 𝐴 ) ∧ 𝑥𝑉 ) → ( 𝑥0 → ( ( 𝑀 ‘ ( 𝐹𝑥 ) ) / ( 𝐿𝑥 ) ) ≤ 𝐴 ) )
38 37 ralrimiva ( ( 𝜑 ∧ ( 𝑁𝐹 ) ≤ 𝐴 ) → ∀ 𝑥𝑉 ( 𝑥0 → ( ( 𝑀 ‘ ( 𝐹𝑥 ) ) / ( 𝐿𝑥 ) ) ≤ 𝐴 ) )
39 0le0 0 ≤ 0
40 simpllr ( ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) ∧ 𝑥 = 0 ) → 𝐴 ∈ ℝ )
41 40 recnd ( ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) ∧ 𝑥 = 0 ) → 𝐴 ∈ ℂ )
42 41 mul01d ( ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) ∧ 𝑥 = 0 ) → ( 𝐴 · 0 ) = 0 )
43 39 42 breqtrrid ( ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) ∧ 𝑥 = 0 ) → 0 ≤ ( 𝐴 · 0 ) )
44 fveq2 ( 𝑥 = 0 → ( 𝐹𝑥 ) = ( 𝐹0 ) )
45 8 ad2antrr ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
46 eqid ( 0g𝑇 ) = ( 0g𝑇 )
47 5 46 ghmid ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝐹0 ) = ( 0g𝑇 ) )
48 45 47 syl ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) → ( 𝐹0 ) = ( 0g𝑇 ) )
49 44 48 sylan9eqr ( ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) ∧ 𝑥 = 0 ) → ( 𝐹𝑥 ) = ( 0g𝑇 ) )
50 49 fveq2d ( ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) ∧ 𝑥 = 0 ) → ( 𝑀 ‘ ( 𝐹𝑥 ) ) = ( 𝑀 ‘ ( 0g𝑇 ) ) )
51 7 ad3antrrr ( ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) ∧ 𝑥 = 0 ) → 𝑇 ∈ NrmGrp )
52 4 46 nm0 ( 𝑇 ∈ NrmGrp → ( 𝑀 ‘ ( 0g𝑇 ) ) = 0 )
53 51 52 syl ( ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) ∧ 𝑥 = 0 ) → ( 𝑀 ‘ ( 0g𝑇 ) ) = 0 )
54 50 53 eqtrd ( ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) ∧ 𝑥 = 0 ) → ( 𝑀 ‘ ( 𝐹𝑥 ) ) = 0 )
55 fveq2 ( 𝑥 = 0 → ( 𝐿𝑥 ) = ( 𝐿0 ) )
56 6 ad2antrr ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) → 𝑆 ∈ NrmGrp )
57 3 5 nm0 ( 𝑆 ∈ NrmGrp → ( 𝐿0 ) = 0 )
58 56 57 syl ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) → ( 𝐿0 ) = 0 )
59 55 58 sylan9eqr ( ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) ∧ 𝑥 = 0 ) → ( 𝐿𝑥 ) = 0 )
60 59 oveq2d ( ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) ∧ 𝑥 = 0 ) → ( 𝐴 · ( 𝐿𝑥 ) ) = ( 𝐴 · 0 ) )
61 43 54 60 3brtr4d ( ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) ∧ 𝑥 = 0 ) → ( 𝑀 ‘ ( 𝐹𝑥 ) ) ≤ ( 𝐴 · ( 𝐿𝑥 ) ) )
62 61 a1d ( ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) ∧ 𝑥 = 0 ) → ( ( 𝑥0 → ( ( 𝑀 ‘ ( 𝐹𝑥 ) ) / ( 𝐿𝑥 ) ) ≤ 𝐴 ) → ( 𝑀 ‘ ( 𝐹𝑥 ) ) ≤ ( 𝐴 · ( 𝐿𝑥 ) ) ) )
63 simpr ( ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) ∧ 𝑥0 ) → 𝑥0 )
64 7 ad2antrr ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) → 𝑇 ∈ NrmGrp )
65 14 adantr ( ( 𝜑𝐴 ∈ ℝ ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) )
66 65 17 sylan ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) → ( 𝐹𝑥 ) ∈ ( Base ‘ 𝑇 ) )
67 64 66 19 syl2anc ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) → ( 𝑀 ‘ ( 𝐹𝑥 ) ) ∈ ℝ )
68 67 adantr ( ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) ∧ 𝑥0 ) → ( 𝑀 ‘ ( 𝐹𝑥 ) ) ∈ ℝ )
69 simpllr ( ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) ∧ 𝑥0 ) → 𝐴 ∈ ℝ )
70 6 adantr ( ( 𝜑𝐴 ∈ ℝ ) → 𝑆 ∈ NrmGrp )
71 22 3expa ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑥𝑉 ) ∧ 𝑥0 ) → ( 𝐿𝑥 ) ∈ ℝ+ )
72 70 71 sylanl1 ( ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) ∧ 𝑥0 ) → ( 𝐿𝑥 ) ∈ ℝ+ )
73 68 69 72 ledivmul2d ( ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) ∧ 𝑥0 ) → ( ( ( 𝑀 ‘ ( 𝐹𝑥 ) ) / ( 𝐿𝑥 ) ) ≤ 𝐴 ↔ ( 𝑀 ‘ ( 𝐹𝑥 ) ) ≤ ( 𝐴 · ( 𝐿𝑥 ) ) ) )
74 73 biimpd ( ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) ∧ 𝑥0 ) → ( ( ( 𝑀 ‘ ( 𝐹𝑥 ) ) / ( 𝐿𝑥 ) ) ≤ 𝐴 → ( 𝑀 ‘ ( 𝐹𝑥 ) ) ≤ ( 𝐴 · ( 𝐿𝑥 ) ) ) )
75 63 74 embantd ( ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) ∧ 𝑥0 ) → ( ( 𝑥0 → ( ( 𝑀 ‘ ( 𝐹𝑥 ) ) / ( 𝐿𝑥 ) ) ≤ 𝐴 ) → ( 𝑀 ‘ ( 𝐹𝑥 ) ) ≤ ( 𝐴 · ( 𝐿𝑥 ) ) ) )
76 62 75 pm2.61dane ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ 𝑥𝑉 ) → ( ( 𝑥0 → ( ( 𝑀 ‘ ( 𝐹𝑥 ) ) / ( 𝐿𝑥 ) ) ≤ 𝐴 ) → ( 𝑀 ‘ ( 𝐹𝑥 ) ) ≤ ( 𝐴 · ( 𝐿𝑥 ) ) ) )
77 76 ralimdva ( ( 𝜑𝐴 ∈ ℝ ) → ( ∀ 𝑥𝑉 ( 𝑥0 → ( ( 𝑀 ‘ ( 𝐹𝑥 ) ) / ( 𝐿𝑥 ) ) ≤ 𝐴 ) → ∀ 𝑥𝑉 ( 𝑀 ‘ ( 𝐹𝑥 ) ) ≤ ( 𝐴 · ( 𝐿𝑥 ) ) ) )
78 7 adantr ( ( 𝜑𝐴 ∈ ℝ ) → 𝑇 ∈ NrmGrp )
79 8 adantr ( ( 𝜑𝐴 ∈ ℝ ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
80 simpr ( ( 𝜑𝐴 ∈ ℝ ) → 𝐴 ∈ ℝ )
81 10 adantr ( ( 𝜑𝐴 ∈ ℝ ) → 0 ≤ 𝐴 )
82 1 2 3 4 nmolb ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ∀ 𝑥𝑉 ( 𝑀 ‘ ( 𝐹𝑥 ) ) ≤ ( 𝐴 · ( 𝐿𝑥 ) ) → ( 𝑁𝐹 ) ≤ 𝐴 ) )
83 70 78 79 80 81 82 syl311anc ( ( 𝜑𝐴 ∈ ℝ ) → ( ∀ 𝑥𝑉 ( 𝑀 ‘ ( 𝐹𝑥 ) ) ≤ ( 𝐴 · ( 𝐿𝑥 ) ) → ( 𝑁𝐹 ) ≤ 𝐴 ) )
84 77 83 syld ( ( 𝜑𝐴 ∈ ℝ ) → ( ∀ 𝑥𝑉 ( 𝑥0 → ( ( 𝑀 ‘ ( 𝐹𝑥 ) ) / ( 𝐿𝑥 ) ) ≤ 𝐴 ) → ( 𝑁𝐹 ) ≤ 𝐴 ) )
85 84 imp ( ( ( 𝜑𝐴 ∈ ℝ ) ∧ ∀ 𝑥𝑉 ( 𝑥0 → ( ( 𝑀 ‘ ( 𝐹𝑥 ) ) / ( 𝐿𝑥 ) ) ≤ 𝐴 ) ) → ( 𝑁𝐹 ) ≤ 𝐴 )
86 85 an32s ( ( ( 𝜑 ∧ ∀ 𝑥𝑉 ( 𝑥0 → ( ( 𝑀 ‘ ( 𝐹𝑥 ) ) / ( 𝐿𝑥 ) ) ≤ 𝐴 ) ) ∧ 𝐴 ∈ ℝ ) → ( 𝑁𝐹 ) ≤ 𝐴 )
87 28 ad2antrr ( ( ( 𝜑 ∧ ∀ 𝑥𝑉 ( 𝑥0 → ( ( 𝑀 ‘ ( 𝐹𝑥 ) ) / ( 𝐿𝑥 ) ) ≤ 𝐴 ) ) ∧ 𝐴 = +∞ ) → ( 𝑁𝐹 ) ∈ ℝ* )
88 pnfge ( ( 𝑁𝐹 ) ∈ ℝ* → ( 𝑁𝐹 ) ≤ +∞ )
89 87 88 syl ( ( ( 𝜑 ∧ ∀ 𝑥𝑉 ( 𝑥0 → ( ( 𝑀 ‘ ( 𝐹𝑥 ) ) / ( 𝐿𝑥 ) ) ≤ 𝐴 ) ) ∧ 𝐴 = +∞ ) → ( 𝑁𝐹 ) ≤ +∞ )
90 simpr ( ( ( 𝜑 ∧ ∀ 𝑥𝑉 ( 𝑥0 → ( ( 𝑀 ‘ ( 𝐹𝑥 ) ) / ( 𝐿𝑥 ) ) ≤ 𝐴 ) ) ∧ 𝐴 = +∞ ) → 𝐴 = +∞ )
91 89 90 breqtrrd ( ( ( 𝜑 ∧ ∀ 𝑥𝑉 ( 𝑥0 → ( ( 𝑀 ‘ ( 𝐹𝑥 ) ) / ( 𝐿𝑥 ) ) ≤ 𝐴 ) ) ∧ 𝐴 = +∞ ) → ( 𝑁𝐹 ) ≤ 𝐴 )
92 ge0nemnf ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) → 𝐴 ≠ -∞ )
93 9 10 92 syl2anc ( 𝜑𝐴 ≠ -∞ )
94 9 93 jca ( 𝜑 → ( 𝐴 ∈ ℝ*𝐴 ≠ -∞ ) )
95 xrnemnf ( ( 𝐴 ∈ ℝ*𝐴 ≠ -∞ ) ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) )
96 94 95 sylib ( 𝜑 → ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) )
97 96 adantr ( ( 𝜑 ∧ ∀ 𝑥𝑉 ( 𝑥0 → ( ( 𝑀 ‘ ( 𝐹𝑥 ) ) / ( 𝐿𝑥 ) ) ≤ 𝐴 ) ) → ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ) )
98 86 91 97 mpjaodan ( ( 𝜑 ∧ ∀ 𝑥𝑉 ( 𝑥0 → ( ( 𝑀 ‘ ( 𝐹𝑥 ) ) / ( 𝐿𝑥 ) ) ≤ 𝐴 ) ) → ( 𝑁𝐹 ) ≤ 𝐴 )
99 38 98 impbida ( 𝜑 → ( ( 𝑁𝐹 ) ≤ 𝐴 ↔ ∀ 𝑥𝑉 ( 𝑥0 → ( ( 𝑀 ‘ ( 𝐹𝑥 ) ) / ( 𝐿𝑥 ) ) ≤ 𝐴 ) ) )