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	⊢ ( 𝜑 → ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 )