Theorem islssd

Description: Properties that determine a subspace of a left module or left vector space. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 8-Jan-2015)

	Ref	Expression
Hypotheses	islssd.f	$$⊢\phi \to F=\mathrm{Scalar}\left(W\right)$$
	islssd.b	$$⊢\phi \to B={\mathrm{Base}}_F$$
	islssd.v	$$⊢\phi \to V={\mathrm{Base}}_W$$
	islssd.p	$$⊢\phi \to \underset{\dot{}}{+}={+}_W$$
	islssd.t	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_W$$
	islssd.s	$$⊢\phi \to S=\mathrm{LSubSp}\left(W\right)$$
	islssd.u	$$⊢\phi \to U\subseteq V$$
	islssd.z	$$⊢\phi \to U\ne \varnothing$$
	islssd.c	$$⊢\left(\phi \wedge \left(x\in B\wedge a\in U\wedge b\in U\right)\right)\to \left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in U$$
Assertion	islssd	$$⊢\phi \to U\in S$$

Proof

Step	Hyp	Ref	Expression
1		islssd.f	$$⊢\phi \to F=\mathrm{Scalar}\left(W\right)$$
2		islssd.b	$$⊢\phi \to B={\mathrm{Base}}_F$$
3		islssd.v	$$⊢\phi \to V={\mathrm{Base}}_W$$
4		islssd.p	$$⊢\phi \to \underset{\dot{}}{+}={+}_W$$
5		islssd.t	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_W$$
6		islssd.s	$$⊢\phi \to S=\mathrm{LSubSp}\left(W\right)$$
7		islssd.u	$$⊢\phi \to U\subseteq V$$
8		islssd.z	$$⊢\phi \to U\ne \varnothing$$
9		islssd.c	$$⊢\left(\phi \wedge \left(x\in B\wedge a\in U\wedge b\in U\right)\right)\to \left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in U$$
10	7 3	sseqtrd	$$⊢\phi \to U\subseteq {\mathrm{Base}}_W$$
11	9	3exp2	$$⊢\phi \to \left(x\in B\to \left(a\in U\to \left(b\in U\to \left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in U\right)\right)\right)$$
12	11	imp43	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge \left(a\in U\wedge b\in U\right)\right)\to \left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in U$$
13	12	ralrimivva	$$⊢\left(\phi \wedge x\in B\right)\to \forall a\in U\forall b\in U\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in U$$
14	13	ex	$$⊢\phi \to \left(x\in B\to \forall a\in U\forall b\in U\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in U\right)$$
15	1	fveq2d	$$⊢\phi \to {\mathrm{Base}}_F={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
16	2 15	eqtrd	$$⊢\phi \to B={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
17	16	eleq2d	$$⊢\phi \to \left(x\in B\leftrightarrow x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\right)$$
18	4	oveqd	$$⊢\phi \to \left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b=\left(x\underset{\dot{}}{·}a\right){+}_{W}b$$
19	5	oveqd	$$⊢\phi \to x\underset{\dot{}}{·}a=x{\cdot }_{W}a$$
20	19	oveq1d	$$⊢\phi \to \left(x\underset{\dot{}}{·}a\right){+}_{W}b=\left(x{\cdot }_{W}a\right){+}_{W}b$$
21	18 20	eqtrd	$$⊢\phi \to \left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b=\left(x{\cdot }_{W}a\right){+}_{W}b$$
22	21	eleq1d	$$⊢\phi \to \left(\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in U\leftrightarrow \left(x{\cdot }_{W}a\right){+}_{W}b\in U\right)$$
23	22	2ralbidv	$$⊢\phi \to \left(\forall a\in U\forall b\in U\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in U\leftrightarrow \forall a\in U\forall b\in U\left(x{\cdot }_{W}a\right){+}_{W}b\in U\right)$$
24	14 17 23	3imtr3d	$$⊢\phi \to \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\to \forall a\in U\forall b\in U\left(x{\cdot }_{W}a\right){+}_{W}b\in U\right)$$
25	24	ralrimiv	$$⊢\phi \to \forall x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\forall a\in U\forall b\in U\left(x{\cdot }_{W}a\right){+}_{W}b\in U$$
26		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
27		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
28		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
29		eqid	$$⊢{+}_W={+}_W$$
30		eqid	$$⊢{\cdot }_W={\cdot }_W$$
31		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
32	26 27 28 29 30 31	islss	$$⊢U\in \mathrm{LSubSp}\left(W\right)\leftrightarrow \left(U\subseteq {\mathrm{Base}}_W\wedge U\ne \varnothing \wedge \forall x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\forall a\in U\forall b\in U\left(x{\cdot }_{W}a\right){+}_{W}b\in U\right)$$
33	10 8 25 32	syl3anbrc	$$⊢\phi \to U\in \mathrm{LSubSp}\left(W\right)$$
34	33 6	eleqtrrd	$$⊢\phi \to U\in S$$