Metamath Proof Explorer

Theorem nmoleub2b

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

		Ref	Expression
	Hypotheses	nmoleub2.n	$⊢ N = S normOp T$
		nmoleub2.v	$⊢ V = {Base}_{S}$
		nmoleub2.l	$⊢ L = norm (S)$
		nmoleub2.m	$⊢ M = norm (T)$
		nmoleub2.g	$⊢ G = Scalar (S)$
		nmoleub2.w	$⊢ K = {Base}_{G}$
		nmoleub2.s	$⊢ φ \to S \in (NrmMod \cap CMod)$
		nmoleub2.t	$⊢ φ \to T \in (NrmMod \cap CMod)$
		nmoleub2.f	$⊢ φ \to F \in (S LMHom T)$
		nmoleub2.a	$⊢ φ \to A \in ℝ^{*}$
		nmoleub2.r	$⊢ φ \to R \in ℝ^{+}$
		nmoleub2a.5	$⊢ φ \to ℚ \subseteq K$
	Assertion	nmoleub2b	$⊢ φ \to (N (F) \leq A \leftrightarrow \forall x \in V (L (x) < R \to \frac{M (F (x))}{R} \leq A))$

Proof

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