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	$$⊢N=S\mathrm{normOp}T$$
	nmofval.2	$$⊢V={\mathrm{Base}}_S$$
	nmofval.3	$$⊢L=\mathrm{norm}\left(S\right)$$
	nmofval.4	$$⊢M=\mathrm{norm}\left(T\right)$$
	nmolb2d.z	$$⊢\underset{\dot{}}{0}=0_S$$
	nmolb2d.1	$$⊢\phi \to S\in \mathrm{NrmGrp}$$
	nmolb2d.2	$$⊢\phi \to T\in \mathrm{NrmGrp}$$
	nmolb2d.3	$$⊢\phi \to F\in \left(S\mathrm{GrpHom}T\right)$$
	nmolb2d.4	$$⊢\phi \to A\in ℝ$$
	nmolb2d.5	$$⊢\phi \to 0\le A$$
	nmolb2d.6	$$⊢\left(\phi \wedge \left(x\in V\wedge x\ne \underset{\dot{}}{0}\right)\right)\to M\left(F\left(x\right)\right)\le AL\left(x\right)$$
Assertion	nmolb2d	$$⊢\phi \to N\left(F\right)\le A$$

Proof

Step	Hyp	Ref	Expression
1		nmofval.1	$$⊢N=S\mathrm{normOp}T$$
2		nmofval.2	$$⊢V={\mathrm{Base}}_S$$
3		nmofval.3	$$⊢L=\mathrm{norm}\left(S\right)$$
4		nmofval.4	$$⊢M=\mathrm{norm}\left(T\right)$$
5		nmolb2d.z	$$⊢\underset{\dot{}}{0}=0_S$$
6		nmolb2d.1	$$⊢\phi \to S\in \mathrm{NrmGrp}$$
7		nmolb2d.2	$$⊢\phi \to T\in \mathrm{NrmGrp}$$
8		nmolb2d.3	$$⊢\phi \to F\in \left(S\mathrm{GrpHom}T\right)$$
9		nmolb2d.4	$$⊢\phi \to A\in ℝ$$
10		nmolb2d.5	$$⊢\phi \to 0\le A$$
11		nmolb2d.6	$$⊢\left(\phi \wedge \left(x\in V\wedge x\ne \underset{\dot{}}{0}\right)\right)\to M\left(F\left(x\right)\right)\le AL\left(x\right)$$
12		2fveq3	$$⊢x=\underset{\dot{}}{0}\to M\left(F\left(x\right)\right)=M\left(F\left(\underset{\dot{}}{0}\right)\right)$$
13		fveq2	$$⊢x=\underset{\dot{}}{0}\to L\left(x\right)=L\left(\underset{\dot{}}{0}\right)$$
14	13	oveq2d	$$⊢x=\underset{\dot{}}{0}\to AL\left(x\right)=AL\left(\underset{\dot{}}{0}\right)$$
15	12 14	breq12d	$$⊢x=\underset{\dot{}}{0}\to \left(M\left(F\left(x\right)\right)\le AL\left(x\right)\leftrightarrow M\left(F\left(\underset{\dot{}}{0}\right)\right)\le AL\left(\underset{\dot{}}{0}\right)\right)$$
16	11	anassrs	$$⊢\left(\left(\phi \wedge x\in V\right)\wedge x\ne \underset{\dot{}}{0}\right)\to M\left(F\left(x\right)\right)\le AL\left(x\right)$$
17		0le0	$$⊢0\le 0$$
18	9	recnd	$$⊢\phi \to A\in ℂ$$
19	18	mul01d	$$⊢\phi \to A\cdot 0=0$$
20	17 19	breqtrrid	$$⊢\phi \to 0\le A\cdot 0$$
21		eqid	$$⊢0_T=0_T$$
22	5 21	ghmid	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to F\left(\underset{\dot{}}{0}\right)=0_T$$
23	8 22	syl	$$⊢\phi \to F\left(\underset{\dot{}}{0}\right)=0_T$$
24	23	fveq2d	$$⊢\phi \to M\left(F\left(\underset{\dot{}}{0}\right)\right)=M\left(0_T\right)$$
25	4 21	nm0	$$⊢T\in \mathrm{NrmGrp}\to M\left(0_T\right)=0$$
26	7 25	syl	$$⊢\phi \to M\left(0_T\right)=0$$
27	24 26	eqtrd	$$⊢\phi \to M\left(F\left(\underset{\dot{}}{0}\right)\right)=0$$
28	3 5	nm0	$$⊢S\in \mathrm{NrmGrp}\to L\left(\underset{\dot{}}{0}\right)=0$$
29	6 28	syl	$$⊢\phi \to L\left(\underset{\dot{}}{0}\right)=0$$
30	29	oveq2d	$$⊢\phi \to AL\left(\underset{\dot{}}{0}\right)=A\cdot 0$$
31	20 27 30	3brtr4d	$$⊢\phi \to M\left(F\left(\underset{\dot{}}{0}\right)\right)\le AL\left(\underset{\dot{}}{0}\right)$$
32	31	adantr	$$⊢\left(\phi \wedge x\in V\right)\to M\left(F\left(\underset{\dot{}}{0}\right)\right)\le AL\left(\underset{\dot{}}{0}\right)$$
33	15 16 32	pm2.61ne	$$⊢\left(\phi \wedge x\in V\right)\to M\left(F\left(x\right)\right)\le AL\left(x\right)$$
34	33	ralrimiva	$$⊢\phi \to \forall x\in VM\left(F\left(x\right)\right)\le AL\left(x\right)$$
35	1 2 3 4	nmolb	$$⊢\left(\left(S\in \mathrm{NrmGrp}\wedge T\in \mathrm{NrmGrp}\wedge F\in \left(S\mathrm{GrpHom}T\right)\right)\wedge A\in ℝ\wedge 0\le A\right)\to \left(\forall x\in VM\left(F\left(x\right)\right)\le AL\left(x\right)\to N\left(F\right)\le A\right)$$
36	6 7 8 9 10 35	syl311anc	$$⊢\phi \to \left(\forall x\in VM\left(F\left(x\right)\right)\le AL\left(x\right)\to N\left(F\right)\le A\right)$$
37	34 36	mpd	$$⊢\phi \to N\left(F\right)\le A$$