blo3i

Description: Properties that determine a bounded linear operator. (Contributed by NM, 13-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	isblo3i.1	$⊢ X = BaseSet (U)$
	isblo3i.m	$⊢ M = {norm}_{CV} (U)$
	isblo3i.n	$⊢ N = {norm}_{CV} (W)$
	isblo3i.4	$⊢ L = U LnOp W$
	isblo3i.5	$⊢ B = U BLnOp W$
	isblo3i.u	$⊢ U \in NrmCVec$
	isblo3i.w	$⊢ W \in NrmCVec$
Assertion	blo3i	$⊢ (T \in L \land A \in ℝ \land \forall y \in X N (T (y)) \leq A M (y)) \to T \in B$

Step	Hyp	Ref	Expression
1		isblo3i.1	$⊢ X = BaseSet (U)$
2		isblo3i.m	$⊢ M = {norm}_{CV} (U)$
3		isblo3i.n	$⊢ N = {norm}_{CV} (W)$
4		isblo3i.4	$⊢ L = U LnOp W$
5		isblo3i.5	$⊢ B = U BLnOp W$
6		isblo3i.u	$⊢ U \in NrmCVec$
7		isblo3i.w	$⊢ W \in NrmCVec$
8		oveq1	$⊢ x = A \to x M (y) = A M (y)$
9	8	breq2d	$⊢ x = A \to (N (T (y)) \leq x M (y) \leftrightarrow N (T (y)) \leq A M (y))$
10	9	ralbidv	$⊢ x = A \to (\forall y \in X N (T (y)) \leq x M (y) \leftrightarrow \forall y \in X N (T (y)) \leq A M (y))$
11	10	rspcev	$⊢ (A \in ℝ \land \forall y \in X N (T (y)) \leq A M (y)) \to \exists x \in ℝ \forall y \in X N (T (y)) \leq x M (y)$
12	1 2 3 4 5 6 7	isblo3i	$⊢ T \in B \leftrightarrow (T \in L \land \exists x \in ℝ \forall y \in X N (T (y)) \leq x M (y))$
13	12	biimpri	$⊢ (T \in L \land \exists x \in ℝ \forall y \in X N (T (y)) \leq x M (y)) \to T \in B$
14	11 13	sylan2	$⊢ (T \in L \land (A \in ℝ \land \forall y \in X N (T (y)) \leq A M (y))) \to T \in B$
15	14	3impb	$⊢ (T \in L \land A \in ℝ \land \forall y \in X N (T (y)) \leq A M (y)) \to T \in B$

Metamath Proof Explorer