Theorem lsscl

Description: Closure property of a subspace. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 8-Jan-2015)

	Ref	Expression
Hypotheses	lsscl.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	lsscl.b	$$⊢B={\mathrm{Base}}_F$$
	lsscl.p	$$⊢\underset{\dot{}}{+}={+}_W$$
	lsscl.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	lsscl.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
Assertion	lsscl	$$⊢\left(U\in S\wedge \left(Z\in B\wedge X\in U\wedge Y\in U\right)\right)\to \left(Z\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}Y\in U$$

Proof

Step	Hyp	Ref	Expression
1		lsscl.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		lsscl.b	$$⊢B={\mathrm{Base}}_F$$
3		lsscl.p	$$⊢\underset{\dot{}}{+}={+}_W$$
4		lsscl.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
5		lsscl.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
6		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
7	1 2 6 3 4 5	islss	$$⊢U\in S\leftrightarrow \left(U\subseteq {\mathrm{Base}}_W\wedge U\ne \varnothing \wedge \forall x\in B\forall a\in U\forall b\in U\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in U\right)$$
8	7	simp3bi	$$⊢U\in S\to \forall x\in B\forall a\in U\forall b\in U\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in U$$
9		oveq1	$$⊢x=Z\to x\underset{\dot{}}{·}a=Z\underset{\dot{}}{·}a$$
10	9	oveq1d	$$⊢x=Z\to \left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b=\left(Z\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b$$
11	10	eleq1d	$$⊢x=Z\to \left(\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in U\leftrightarrow \left(Z\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in U\right)$$
12		oveq2	$$⊢a=X\to Z\underset{\dot{}}{·}a=Z\underset{\dot{}}{·}X$$
13	12	oveq1d	$$⊢a=X\to \left(Z\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b=\left(Z\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}b$$
14	13	eleq1d	$$⊢a=X\to \left(\left(Z\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in U\leftrightarrow \left(Z\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}b\in U\right)$$
15		oveq2	$$⊢b=Y\to \left(Z\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}b=\left(Z\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}Y$$
16	15	eleq1d	$$⊢b=Y\to \left(\left(Z\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}b\in U\leftrightarrow \left(Z\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}Y\in U\right)$$
17	11 14 16	rspc3v	$$⊢\left(Z\in B\wedge X\in U\wedge Y\in U\right)\to \left(\forall x\in B\forall a\in U\forall b\in U\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in U\to \left(Z\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}Y\in U\right)$$
18	8 17	mpan9	$$⊢\left(U\in S\wedge \left(Z\in B\wedge X\in U\wedge Y\in U\right)\right)\to \left(Z\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}Y\in U$$