asplss

Description: The algebraic span of a set of vectors is a vector subspace. (Contributed by Mario Carneiro, 7-Jan-2015)

	Ref	Expression
Hypotheses	aspval.a	$⊢ A = AlgSpan (W)$
	aspval.v	$⊢ V = {Base}_{W}$
	aspval.l	$⊢ L = LSubSp (W)$
Assertion	asplss	$⊢ (W \in AssAlg \land S \subseteq V) \to A (S) \in L$

Step	Hyp	Ref	Expression
1		aspval.a	$⊢ A = AlgSpan (W)$
2		aspval.v	$⊢ V = {Base}_{W}$
3		aspval.l	$⊢ L = LSubSp (W)$
4	1 2 3	aspval	$⊢ (W \in AssAlg \land S \subseteq V) \to A (S) = ⋂ \{t \in (SubRing (W) \cap L) \| S \subseteq t\}$
5		assalmod	$⊢ W \in AssAlg \to W \in LMod$
6	5	adantr	$⊢ (W \in AssAlg \land S \subseteq V) \to W \in LMod$
7		ssrab2	$⊢ \{t \in (SubRing (W) \cap L) \| S \subseteq t\} \subseteq SubRing (W) \cap L$
8		inss2	$⊢ SubRing (W) \cap L \subseteq L$
9	7 8	sstri	$⊢ \{t \in (SubRing (W) \cap L) \| S \subseteq t\} \subseteq L$
10	9	a1i	$⊢ (W \in AssAlg \land S \subseteq V) \to \{t \in (SubRing (W) \cap L) \| S \subseteq t\} \subseteq L$
11		fvex	$⊢ A (S) \in V$
12	4 11	eqeltrrdi	$⊢ (W \in AssAlg \land S \subseteq V) \to ⋂ \{t \in (SubRing (W) \cap L) \| S \subseteq t\} \in V$
13		intex	$⊢ \{t \in (SubRing (W) \cap L) \| S \subseteq t\} \neq \emptyset \leftrightarrow ⋂ \{t \in (SubRing (W) \cap L) \| S \subseteq t\} \in V$
14	12 13	sylibr	$⊢ (W \in AssAlg \land S \subseteq V) \to \{t \in (SubRing (W) \cap L) \| S \subseteq t\} \neq \emptyset$
15	3	lssintcl	$⊢ (W \in LMod \land \{t \in (SubRing (W) \cap L) \| S \subseteq t\} \subseteq L \land \{t \in (SubRing (W) \cap L) \| S \subseteq t\} \neq \emptyset) \to ⋂ \{t \in (SubRing (W) \cap L) \| S \subseteq t\} \in L$
16	6 10 14 15	syl3anc	$⊢ (W \in AssAlg \land S \subseteq V) \to ⋂ \{t \in (SubRing (W) \cap L) \| S \subseteq t\} \in L$
17	4 16	eqeltrd	$⊢ (W \in AssAlg \land S \subseteq V) \to A (S) \in L$

Metamath Proof Explorer