Metamath Proof Explorer

Theorem nmolb

Description: Any upper bound on the values of a linear operator translates to an upper bound on the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015) (Proof shortened by AV, 26-Sep-2020)

Ref Expression
Hypotheses nmofval.1 ⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
nmofval.2 ⊢ 𝑉 = ( Base ‘ 𝑆 )
nmofval.3 ⊢ 𝐿 = ( norm ‘ 𝑆 )
nmofval.4 ⊢ 𝑀 = ( norm ‘ 𝑇 )
Assertion nmolb ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 nmofval.1 ⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
2 nmofval.2 ⊢ 𝑉 = ( Base ‘ 𝑆 )
3 nmofval.3 ⊢ 𝐿 = ( norm ‘ 𝑆 )
4 nmofval.4 ⊢ 𝑀 = ( norm ‘ 𝑇 )
5 elrege0 ⊢ ( 𝐴 ∈ ( 0 [,) +∞ ) ↔ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
6 1 2 3 4 nmoval ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝑁 ‘ 𝐹 ) = inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) )
7 ssrab2 ⊢ { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } ⊆ ( 0 [,) +∞ )
8 icossxr ⊢ ( 0 [,) +∞ ) ⊆ ℝ*
9 7 8 sstri ⊢ { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } ⊆ ℝ*
10 infxrcl ⊢ ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } ⊆ ℝ* → inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) ∈ ℝ* )
11 9 10 mp1i ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) } , ℝ* , < ) ∈ ℝ* )
12 6 11 eqeltrd ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝑁 ‘ 𝐹 ) ∈ ℝ* )
13 12 xrleidd ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝑁 ‘ 𝐹 ) ≤ ( 𝑁 ‘ 𝐹 ) )
14 1 2 3 4 nmogelb ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑁 ‘ 𝐹 ) ∈ ℝ* ) → ( ( 𝑁 ‘ 𝐹 ) ≤ ( 𝑁 ‘ 𝐹 ) ↔ ∀ 𝑟 ∈ ( 0 [,) +∞ ) ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝑟 ) ) )
15 12 14 mpdan ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( ( 𝑁 ‘ 𝐹 ) ≤ ( 𝑁 ‘ 𝐹 ) ↔ ∀ 𝑟 ∈ ( 0 [,) +∞ ) ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝑟 ) ) )
16 13 15 mpbid ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ∀ 𝑟 ∈ ( 0 [,) +∞ ) ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝑟 ) )
17 oveq1 ⊢ ( 𝑟 = 𝐴 → ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) = ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) )
18 17 breq2d ⊢ ( 𝑟 = 𝐴 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) ↔ ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ) )
19 18 ralbidv ⊢ ( 𝑟 = 𝐴 → ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ) )
20 breq2 ⊢ ( 𝑟 = 𝐴 → ( ( 𝑁 ‘ 𝐹 ) ≤ 𝑟 ↔ ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) )
21 19 20 imbi12d ⊢ ( 𝑟 = 𝐴 → ( ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝑟 ) ↔ ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ) )
22 21 rspccv ⊢ ( ∀ 𝑟 ∈ ( 0 [,) +∞ ) ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( 𝐿 ‘ 𝑥 ) ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝑟 ) → ( 𝐴 ∈ ( 0 [,) +∞ ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ) )
23 16 22 syl ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝐴 ∈ ( 0 [,) +∞ ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ) )
24 5 23 syl5bir ⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) ) )
25 24 3impib ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) )