Metamath Proof Explorer

Theorem nmosetre

Description: The set in the supremum of the operator norm definition df-nmoo is a set of reals. (Contributed by NM, 13-Nov-2007) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	nmosetre.2	$⊢ Y = BaseSet (W)$
		nmosetre.4	$⊢ N = {norm}_{CV} (W)$
	Assertion	nmosetre	$⊢ (W \in NrmCVec \land T : X ⟶ Y) \to \{x \| \exists z \in X (M (z) \leq 1 \land x = N (T (z)))\} \subseteq ℝ$

Proof

Step	Hyp	Ref	Expression
1		nmosetre.2	$⊢ Y = BaseSet (W)$
2		nmosetre.4	$⊢ N = {norm}_{CV} (W)$
3		ffvelcdm	$⊢ (T : X ⟶ Y \land z \in X) \to T (z) \in Y$
4	1 2	nvcl	$⊢ (W \in NrmCVec \land T (z) \in Y) \to N (T (z)) \in ℝ$
5	3 4	sylan2	$⊢ (W \in NrmCVec \land (T : X ⟶ Y \land z \in X)) \to N (T (z)) \in ℝ$
6	5	anassrs	$⊢ ((W \in NrmCVec \land T : X ⟶ Y) \land z \in X) \to N (T (z)) \in ℝ$
7		eleq1	$⊢ x = N (T (z)) \to (x \in ℝ \leftrightarrow N (T (z)) \in ℝ)$
8	6 7	imbitrrid	$⊢ x = N (T (z)) \to (((W \in NrmCVec \land T : X ⟶ Y) \land z \in X) \to x \in ℝ)$
9	8	impcom	$⊢ (((W \in NrmCVec \land T : X ⟶ Y) \land z \in X) \land x = N (T (z))) \to x \in ℝ$
10	9	adantrl	$⊢ (((W \in NrmCVec \land T : X ⟶ Y) \land z \in X) \land (M (z) \leq 1 \land x = N (T (z)))) \to x \in ℝ$
11	10	rexlimdva2	$⊢ (W \in NrmCVec \land T : X ⟶ Y) \to (\exists z \in X (M (z) \leq 1 \land x = N (T (z))) \to x \in ℝ)$
12	11	abssdv	$⊢ (W \in NrmCVec \land T : X ⟶ Y) \to \{x \| \exists z \in X (M (z) \leq 1 \land x = N (T (z)))\} \subseteq ℝ$