aspsubrg

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

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

Step	Hyp	Ref	Expression
1		aspval.a	$⊢ A = AlgSpan (W)$
2		aspval.v	$⊢ V = {Base}_{W}$
3		eqid	$⊢ LSubSp (W) = LSubSp (W)$
4	1 2 3	aspval	$⊢ (W \in AssAlg \land S \subseteq V) \to A (S) = ⋂ \{t \in (SubRing (W) \cap LSubSp (W)) \| S \subseteq t\}$
5		ssrab2	$⊢ \{t \in (SubRing (W) \cap LSubSp (W)) \| S \subseteq t\} \subseteq SubRing (W) \cap LSubSp (W)$
6		inss1	$⊢ SubRing (W) \cap LSubSp (W) \subseteq SubRing (W)$
7	5 6	sstri	$⊢ \{t \in (SubRing (W) \cap LSubSp (W)) \| S \subseteq t\} \subseteq SubRing (W)$
8		fvex	$⊢ A (S) \in V$
9	4 8	eqeltrrdi	$⊢ (W \in AssAlg \land S \subseteq V) \to ⋂ \{t \in (SubRing (W) \cap LSubSp (W)) \| S \subseteq t\} \in V$
10		intex	$⊢ \{t \in (SubRing (W) \cap LSubSp (W)) \| S \subseteq t\} \neq \emptyset \leftrightarrow ⋂ \{t \in (SubRing (W) \cap LSubSp (W)) \| S \subseteq t\} \in V$
11	9 10	sylibr	$⊢ (W \in AssAlg \land S \subseteq V) \to \{t \in (SubRing (W) \cap LSubSp (W)) \| S \subseteq t\} \neq \emptyset$
12		subrgint	$⊢ (\{t \in (SubRing (W) \cap LSubSp (W)) \| S \subseteq t\} \subseteq SubRing (W) \land \{t \in (SubRing (W) \cap LSubSp (W)) \| S \subseteq t\} \neq \emptyset) \to ⋂ \{t \in (SubRing (W) \cap LSubSp (W)) \| S \subseteq t\} \in SubRing (W)$
13	7 11 12	sylancr	$⊢ (W \in AssAlg \land S \subseteq V) \to ⋂ \{t \in (SubRing (W) \cap LSubSp (W)) \| S \subseteq t\} \in SubRing (W)$
14	4 13	eqeltrd	$⊢ (W \in AssAlg \land S \subseteq V) \to A (S) \in SubRing (W)$

Metamath Proof Explorer