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

Metamath Proof Explorer

Theorem nmolb2d

Description: Any upper bound on the values of a linear operator at nonzero vectors translates to an upper bound on the operator norm. (Contributed by Mario Carneiro, 18-Oct-2015)

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

Proof

Step Hyp Ref Expression
1 nmofval.1 ⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
2 nmofval.2 ⊢ 𝑉 = ( Base ‘ 𝑆 )
3 nmofval.3 ⊢ 𝐿 = ( norm ‘ 𝑆 )
4 nmofval.4 ⊢ 𝑀 = ( norm ‘ 𝑇 )
5 nmolb2d.z ⊢ 0 = ( 0g ‘ 𝑆 )
6 nmolb2d.1 ⊢ ( 𝜑 → 𝑆 ∈ NrmGrp )
7 nmolb2d.2 ⊢ ( 𝜑 → 𝑇 ∈ NrmGrp )
8 nmolb2d.3 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
9 nmolb2d.4 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
10 nmolb2d.5 ⊢ ( 𝜑 → 0 ≤ 𝐴 )
11 nmolb2d.6 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) )
12 2fveq3 ⊢ ( 𝑥 = 0 → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 𝐹 ‘ 0 ) ) )
13 fveq2 ⊢ ( 𝑥 = 0 → ( 𝐿 ‘ 𝑥 ) = ( 𝐿 ‘ 0 ) )
14 13 oveq2d ⊢ ( 𝑥 = 0 → ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) = ( 𝐴 · ( 𝐿 ‘ 0 ) ) )
15 12 14 breq12d ⊢ ( 𝑥 = 0 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) ↔ ( 𝑀 ‘ ( 𝐹 ‘ 0 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 0 ) ) ) )
16 11 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑥 ≠ 0 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) )
17 0le0 ⊢ 0 ≤ 0
18 9 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
19 18 mul01d ⊢ ( 𝜑 → ( 𝐴 · 0 ) = 0 )
20 17 19 breqtrrid ⊢ ( 𝜑 → 0 ≤ ( 𝐴 · 0 ) )
21 eqid ⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 )
22 5 21 ghmid ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑇 ) )
23 8 22 syl ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑇 ) )
24 23 fveq2d ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐹 ‘ 0 ) ) = ( 𝑀 ‘ ( 0g ‘ 𝑇 ) ) )
25 4 21 nm0 ⊢ ( 𝑇 ∈ NrmGrp → ( 𝑀 ‘ ( 0g ‘ 𝑇 ) ) = 0 )
26 7 25 syl ⊢ ( 𝜑 → ( 𝑀 ‘ ( 0g ‘ 𝑇 ) ) = 0 )
27 24 26 eqtrd ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐹 ‘ 0 ) ) = 0 )
28 3 5 nm0 ⊢ ( 𝑆 ∈ NrmGrp → ( 𝐿 ‘ 0 ) = 0 )
29 6 28 syl ⊢ ( 𝜑 → ( 𝐿 ‘ 0 ) = 0 )
30 29 oveq2d ⊢ ( 𝜑 → ( 𝐴 · ( 𝐿 ‘ 0 ) ) = ( 𝐴 · 0 ) )
31 20 27 30 3brtr4d ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐹 ‘ 0 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 0 ) ) )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝑀 ‘ ( 𝐹 ‘ 0 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 0 ) ) )
33 15 16 32 pm2.61ne ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) )
34 33 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) )
35 1 2 3 4 nmolb ⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) )
36 6 7 8 9 10 35 syl311anc ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑉 ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( 𝐿 ‘ 𝑥 ) ) → ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ) )
37 34 36 mpd ⊢ ( 𝜑 → ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 )