Metamath Proof Explorer

Theorem nmoleub2a

Description: The operator norm is the supremum of the value of a linear operator in the closed unit ball. (Contributed by Mario Carneiro, 19-Oct-2015)

Ref Expression
Hypotheses nmoleub2.n ${⊢}{N}={S}\mathrm{normOp}{T}$
nmoleub2.v ${⊢}{V}={\mathrm{Base}}_{{S}}$
nmoleub2.l ${⊢}{L}=\mathrm{norm}\left({S}\right)$
nmoleub2.m ${⊢}{M}=\mathrm{norm}\left({T}\right)$
nmoleub2.g ${⊢}{G}=\mathrm{Scalar}\left({S}\right)$
nmoleub2.w ${⊢}{K}={\mathrm{Base}}_{{G}}$
nmoleub2.s ${⊢}{\phi }\to {S}\in \left(\mathrm{NrmMod}\cap \mathrm{CMod}\right)$
nmoleub2.t ${⊢}{\phi }\to {T}\in \left(\mathrm{NrmMod}\cap \mathrm{CMod}\right)$
nmoleub2.f ${⊢}{\phi }\to {F}\in \left({S}\mathrm{LMHom}{T}\right)$
nmoleub2.a ${⊢}{\phi }\to {A}\in {ℝ}^{*}$
nmoleub2.r ${⊢}{\phi }\to {R}\in {ℝ}^{+}$
nmoleub2a.5 ${⊢}{\phi }\to ℚ\subseteq {K}$
Assertion nmoleub2a ${⊢}{\phi }\to \left({N}\left({F}\right)\le {A}↔\forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right)\le {R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)$

Proof

Step Hyp Ref Expression
1 nmoleub2.n ${⊢}{N}={S}\mathrm{normOp}{T}$
2 nmoleub2.v ${⊢}{V}={\mathrm{Base}}_{{S}}$
3 nmoleub2.l ${⊢}{L}=\mathrm{norm}\left({S}\right)$
4 nmoleub2.m ${⊢}{M}=\mathrm{norm}\left({T}\right)$
5 nmoleub2.g ${⊢}{G}=\mathrm{Scalar}\left({S}\right)$
6 nmoleub2.w ${⊢}{K}={\mathrm{Base}}_{{G}}$
7 nmoleub2.s ${⊢}{\phi }\to {S}\in \left(\mathrm{NrmMod}\cap \mathrm{CMod}\right)$
8 nmoleub2.t ${⊢}{\phi }\to {T}\in \left(\mathrm{NrmMod}\cap \mathrm{CMod}\right)$
9 nmoleub2.f ${⊢}{\phi }\to {F}\in \left({S}\mathrm{LMHom}{T}\right)$
10 nmoleub2.a ${⊢}{\phi }\to {A}\in {ℝ}^{*}$
11 nmoleub2.r ${⊢}{\phi }\to {R}\in {ℝ}^{+}$
12 nmoleub2a.5 ${⊢}{\phi }\to ℚ\subseteq {K}$
13 idd ${⊢}\left({L}\left({x}\right)\in ℝ\wedge {R}\in ℝ\right)\to \left({L}\left({x}\right)\le {R}\to {L}\left({x}\right)\le {R}\right)$
14 ltle ${⊢}\left({L}\left({x}\right)\in ℝ\wedge {R}\in ℝ\right)\to \left({L}\left({x}\right)<{R}\to {L}\left({x}\right)\le {R}\right)$
15 1 2 3 4 5 6 7 8 9 10 11 12 13 14 nmoleub2lem2 ${⊢}{\phi }\to \left({N}\left({F}\right)\le {A}↔\forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left({L}\left({x}\right)\le {R}\to \frac{{M}\left({F}\left({x}\right)\right)}{{R}}\le {A}\right)\right)$