lssnvc

Description: A subspace of a normed vector space is a normed vector space. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	lssnlm.x	$⊢ X = W ↾_{𝑠} U$
	lssnlm.s	$⊢ S = LSubSp (W)$
Assertion	lssnvc	$⊢ (W \in NrmVec \land U \in S) \to X \in NrmVec$

Step	Hyp	Ref	Expression
1		lssnlm.x	$⊢ X = W ↾_{𝑠} U$
2		lssnlm.s	$⊢ S = LSubSp (W)$
3		nvcnlm	$⊢ W \in NrmVec \to W \in NrmMod$
4	1 2	lssnlm	$⊢ (W \in NrmMod \land U \in S) \to X \in NrmMod$
5	3 4	sylan	$⊢ (W \in NrmVec \land U \in S) \to X \in NrmMod$
6		eqid	$⊢ Scalar (W) = Scalar (W)$
7	1 6	resssca	$⊢ U \in S \to Scalar (W) = Scalar (X)$
8	7	adantl	$⊢ (W \in NrmVec \land U \in S) \to Scalar (W) = Scalar (X)$
9		nvclvec	$⊢ W \in NrmVec \to W \in LVec$
10	6	lvecdrng	$⊢ W \in LVec \to Scalar (W) \in DivRing$
11	9 10	syl	$⊢ W \in NrmVec \to Scalar (W) \in DivRing$
12	11	adantr	$⊢ (W \in NrmVec \land U \in S) \to Scalar (W) \in DivRing$
13	8 12	eqeltrrd	$⊢ (W \in NrmVec \land U \in S) \to Scalar (X) \in DivRing$
14		eqid	$⊢ Scalar (X) = Scalar (X)$
15	14	isnvc2	$⊢ X \in NrmVec \leftrightarrow (X \in NrmMod \land Scalar (X) \in DivRing)$
16	5 13 15	sylanbrc	$⊢ (W \in NrmVec \land U \in S) \to X \in NrmVec$

Metamath Proof Explorer