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	$⊢ N = S normOp T$
	nmofval.2	$⊢ V = {Base}_{S}$
	nmofval.3	$⊢ L = norm (S)$
	nmofval.4	$⊢ M = norm (T)$
Assertion	nmolb	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land A \in ℝ \land 0 \leq A) \to (\forall x \in V M (F (x)) \leq A L (x) \to N (F) \leq A)$

Proof

Step	Hyp	Ref	Expression
1		nmofval.1	$⊢ N = S normOp T$
2		nmofval.2	$⊢ V = {Base}_{S}$
3		nmofval.3	$⊢ L = norm (S)$
4		nmofval.4	$⊢ M = norm (T)$
5		elrege0	$⊢ A \in [0, +∞) \leftrightarrow (A \in ℝ \land 0 \leq A)$
6	1 2 3 4	nmoval	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to N (F) = sup (\{r \in [0, +∞) \| \forall x \in V M (F (x)) \leq r L (x)\} ℝ^{*} <)$
7		ssrab2	$⊢ \{r \in [0, +∞) \| \forall x \in V M (F (x)) \leq r L (x)\} \subseteq [0, +∞)$
8		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
9	7 8	sstri	$⊢ \{r \in [0, +∞) \| \forall x \in V M (F (x)) \leq r L (x)\} \subseteq ℝ^{*}$
10		infxrcl	$⊢ \{r \in [0, +∞) \| \forall x \in V M (F (x)) \leq r L (x)\} \subseteq ℝ^{} \to sup (\{r \in [0, +∞) \| \forall x \in V M (F (x)) \leq r L (x)\} ℝ^{} <) \in ℝ^{*}$
11	9 10	mp1i	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to sup (\{r \in [0, +∞) \| \forall x \in V M (F (x)) \leq r L (x)\} ℝ^{} <) \in ℝ^{}$
12	6 11	eqeltrd	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to N (F) \in ℝ^{*}$
13	12	xrleidd	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to N (F) \leq N (F)$
14	1 2 3 4	nmogelb	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land N (F) \in ℝ^{*}) \to (N (F) \leq N (F) \leftrightarrow \forall r \in [0, +∞) (\forall x \in V M (F (x)) \leq r L (x) \to N (F) \leq r))$
15	12 14	mpdan	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to (N (F) \leq N (F) \leftrightarrow \forall r \in [0, +∞) (\forall x \in V M (F (x)) \leq r L (x) \to N (F) \leq r))$
16	13 15	mpbid	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to \forall r \in [0, +∞) (\forall x \in V M (F (x)) \leq r L (x) \to N (F) \leq r)$
17		oveq1	$⊢ r = A \to r L (x) = A L (x)$
18	17	breq2d	$⊢ r = A \to (M (F (x)) \leq r L (x) \leftrightarrow M (F (x)) \leq A L (x))$
19	18	ralbidv	$⊢ r = A \to (\forall x \in V M (F (x)) \leq r L (x) \leftrightarrow \forall x \in V M (F (x)) \leq A L (x))$
20		breq2	$⊢ r = A \to (N (F) \leq r \leftrightarrow N (F) \leq A)$
21	19 20	imbi12d	$⊢ r = A \to ((\forall x \in V M (F (x)) \leq r L (x) \to N (F) \leq r) \leftrightarrow (\forall x \in V M (F (x)) \leq A L (x) \to N (F) \leq A))$
22	21	rspccv	$⊢ \forall r \in [0, +∞) (\forall x \in V M (F (x)) \leq r L (x) \to N (F) \leq r) \to (A \in [0, +∞) \to (\forall x \in V M (F (x)) \leq A L (x) \to N (F) \leq A))$
23	16 22	syl	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to (A \in [0, +∞) \to (\forall x \in V M (F (x)) \leq A L (x) \to N (F) \leq A))$
24	5 23	biimtrrid	$⊢ (S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \to ((A \in ℝ \land 0 \leq A) \to (\forall x \in V M (F (x)) \leq A L (x) \to N (F) \leq A))$
25	24	3impib	$⊢ ((S \in NrmGrp \land T \in NrmGrp \land F \in (S GrpHom T)) \land A \in ℝ \land 0 \leq A) \to (\forall x \in V M (F (x)) \leq A L (x) \to N (F) \leq A)$

Metamath Proof Explorer

Theorem nmolb

Proof