Theorem lssset

Description: The set of all (not necessarily closed) linear subspaces of a left module or left vector space. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 15-Jul-2014)

	Ref	Expression
Hypotheses	lssset.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	lssset.b	$$⊢B={\mathrm{Base}}_F$$
	lssset.v	$$⊢V={\mathrm{Base}}_W$$
	lssset.p	$$⊢\underset{\dot{}}{+}={+}_W$$
	lssset.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	lssset.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
Assertion	lssset	$$⊢W\in X\to S=\left\{s\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\forall x\in B\forall a\in s\forall b\in s\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in s\right\}$$

Proof

Step	Hyp	Ref	Expression
1		lssset.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		lssset.b	$$⊢B={\mathrm{Base}}_F$$
3		lssset.v	$$⊢V={\mathrm{Base}}_W$$
4		lssset.p	$$⊢\underset{\dot{}}{+}={+}_W$$
5		lssset.t	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
6		lssset.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
7		elex	$$⊢W\in X\to W\in \mathrm{V}$$
8		fveq2	$$⊢w=W\to {\mathrm{Base}}_w={\mathrm{Base}}_W$$
9	8 3	syl6eqr	$$⊢w=W\to {\mathrm{Base}}_w=V$$
10	9	pweqd	$$⊢w=W\to 𝒫{\mathrm{Base}}_w=𝒫V$$
11	10	difeq1d	$$⊢w=W\to 𝒫{\mathrm{Base}}_w\setminus \left\{\varnothing \right\}=𝒫V\setminus \left\{\varnothing \right\}$$
12		fveq2	$$⊢w=W\to \mathrm{Scalar}\left(w\right)=\mathrm{Scalar}\left(W\right)$$
13	12 1	syl6eqr	$$⊢w=W\to \mathrm{Scalar}\left(w\right)=F$$
14	13	fveq2d	$$⊢w=W\to {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}={\mathrm{Base}}_F$$
15	14 2	syl6eqr	$$⊢w=W\to {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}=B$$
16		fveq2	$$⊢w=W\to {\cdot }_w={\cdot }_W$$
17	16 5	syl6eqr	$$⊢w=W\to {\cdot }_w=\underset{\dot{}}{·}$$
18	17	oveqd	$$⊢w=W\to x{\cdot }_{w}a=x\underset{\dot{}}{·}a$$
19	18	oveq1d	$$⊢w=W\to \left(x{\cdot }_{w}a\right){+}_{w}b=\left(x\underset{\dot{}}{·}a\right){+}_{w}b$$
20		fveq2	$$⊢w=W\to {+}_w={+}_W$$
21	20 4	syl6eqr	$$⊢w=W\to {+}_w=\underset{\dot{}}{+}$$
22	21	oveqd	$$⊢w=W\to \left(x\underset{\dot{}}{·}a\right){+}_{w}b=\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b$$
23	19 22	eqtrd	$$⊢w=W\to \left(x{\cdot }_{w}a\right){+}_{w}b=\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b$$
24	23	eleq1d	$$⊢w=W\to \left(\left(x{\cdot }_{w}a\right){+}_{w}b\in s\leftrightarrow \left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in s\right)$$
25	24	2ralbidv	$$⊢w=W\to \left(\forall a\in s\forall b\in s\left(x{\cdot }_{w}a\right){+}_{w}b\in s\leftrightarrow \forall a\in s\forall b\in s\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in s\right)$$
26	15 25	raleqbidv	$$⊢w=W\to \left(\forall x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}\forall a\in s\forall b\in s\left(x{\cdot }_{w}a\right){+}_{w}b\in s\leftrightarrow \forall x\in B\forall a\in s\forall b\in s\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in s\right)$$
27	11 26	rabeqbidv	$$⊢w=W\to \left\{s\in \left(𝒫{\mathrm{Base}}_w\setminus \left\{\varnothing \right\}\right)|\forall x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}\forall a\in s\forall b\in s\left(x{\cdot }_{w}a\right){+}_{w}b\in s\right\}=\left\{s\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\forall x\in B\forall a\in s\forall b\in s\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in s\right\}$$
28		df-lss	$$⊢\mathrm{LSubSp}=\left(w\in \mathrm{V}⟼\left\{s\in \left(𝒫{\mathrm{Base}}_w\setminus \left\{\varnothing \right\}\right)|\forall x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(w\right)}\forall a\in s\forall b\in s\left(x{\cdot }_{w}a\right){+}_{w}b\in s\right\}\right)$$
29	3	fvexi	$$⊢V\in \mathrm{V}$$
30	29	pwex	$$⊢𝒫V\in \mathrm{V}$$
31	30	difexi	$$⊢𝒫V\setminus \left\{\varnothing \right\}\in \mathrm{V}$$
32	31	rabex	$$⊢\left\{s\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\forall x\in B\forall a\in s\forall b\in s\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in s\right\}\in \mathrm{V}$$
33	27 28 32	fvmpt	$$⊢W\in \mathrm{V}\to \mathrm{LSubSp}\left(W\right)=\left\{s\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\forall x\in B\forall a\in s\forall b\in s\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in s\right\}$$
34	7 33	syl	$$⊢W\in X\to \mathrm{LSubSp}\left(W\right)=\left\{s\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\forall x\in B\forall a\in s\forall b\in s\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in s\right\}$$
35	6 34	syl5eq	$$⊢W\in X\to S=\left\{s\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)|\forall x\in B\forall a\in s\forall b\in s\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in s\right\}$$