lsslvec

Description: A vector subspace is a vector space. (Contributed by NM, 14-Mar-2015)

Step	Hyp	Ref	Expression
1		lsslvec.x	$⊢ X = W ↾_{𝑠} U$
2		lsslvec.s	$⊢ S = LSubSp (W)$
3		lveclmod	$⊢ W \in LVec \to W \in LMod$
4	1 2	lsslmod	$⊢ (W \in LMod \land U \in S) \to X \in LMod$
5	3 4	sylan	$⊢ (W \in LVec \land U \in S) \to X \in LMod$
6		eqid	$⊢ Scalar (W) = Scalar (W)$
7	1 6	resssca	$⊢ U \in S \to Scalar (W) = Scalar (X)$
8	7	adantl	$⊢ (W \in LVec \land U \in S) \to Scalar (W) = Scalar (X)$
9	6	lvecdrng	$⊢ W \in LVec \to Scalar (W) \in DivRing$
10	9	adantr	$⊢ (W \in LVec \land U \in S) \to Scalar (W) \in DivRing$
11	8 10	eqeltrrd	$⊢ (W \in LVec \land U \in S) \to Scalar (X) \in DivRing$
12		eqid	$⊢ Scalar (X) = Scalar (X)$
13	12	islvec	$⊢ X \in LVec \leftrightarrow (X \in LMod \land Scalar (X) \in DivRing)$
14	5 11 13	sylanbrc	$⊢ (W \in LVec \land U \in S) \to X \in LVec$

Metamath Proof Explorer