Theorem islss

Description: The predicate "is 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	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	islss	$$⊢U\in S\leftrightarrow \left(U\subseteq V\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)$$

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		elfvex	$$⊢U\in \mathrm{LSubSp}\left(W\right)\to W\in \mathrm{V}$$
8	7 6	eleq2s	$$⊢U\in S\to W\in \mathrm{V}$$
9		fvprc	$$⊢\neg W\in \mathrm{V}\to {\mathrm{Base}}_W=\varnothing$$
10	3 9	eqtrid	$$⊢\neg W\in \mathrm{V}\to V=\varnothing$$
11	10	sseq2d	$$⊢\neg W\in \mathrm{V}\to \left(U\subseteq V\leftrightarrow U\subseteq \varnothing \right)$$
12	11	biimpcd	$$⊢U\subseteq V\to \left(\neg W\in \mathrm{V}\to U\subseteq \varnothing \right)$$
13		ss0	$$⊢U\subseteq \varnothing \to U=\varnothing$$
14	12 13	syl6	$$⊢U\subseteq V\to \left(\neg W\in \mathrm{V}\to U=\varnothing \right)$$
15	14	necon1ad	$$⊢U\subseteq V\to \left(U\ne \varnothing \to W\in \mathrm{V}\right)$$
16	15	imp	$$⊢\left(U\subseteq V\wedge U\ne \varnothing \right)\to W\in \mathrm{V}$$
17	16	3adant3	$$⊢\left(U\subseteq V\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)\to W\in \mathrm{V}$$
18	1 2 3 4 5 6	lssset	$$⊢W\in \mathrm{V}\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\}$$
19	18	eleq2d	$$⊢W\in \mathrm{V}\to \left(U\in S\leftrightarrow U\in \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\}\right)$$
20		eldifsn	$$⊢U\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)\leftrightarrow \left(U\in 𝒫V\wedge U\ne \varnothing \right)$$
21	3	fvexi	$$⊢V\in \mathrm{V}$$
22	21	elpw2	$$⊢U\in 𝒫V\leftrightarrow U\subseteq V$$
23	22	anbi1i	$$⊢\left(U\in 𝒫V\wedge U\ne \varnothing \right)\leftrightarrow \left(U\subseteq V\wedge U\ne \varnothing \right)$$
24	20 23	bitri	$$⊢U\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)\leftrightarrow \left(U\subseteq V\wedge U\ne \varnothing \right)$$
25	24	anbi1i	$$⊢\left(U\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)\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)\leftrightarrow \left(\left(U\subseteq V\wedge U\ne \varnothing \right)\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)$$
26		eleq2	$$⊢s=U\to \left(\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in s\leftrightarrow \left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in U\right)$$
27	26	raleqbi1dv	$$⊢s=U\to \left(\forall b\in s\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in s\leftrightarrow \forall b\in U\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in U\right)$$
28	27	raleqbi1dv	$$⊢s=U\to \left(\forall a\in s\forall b\in s\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in s\leftrightarrow \forall a\in U\forall b\in U\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in U\right)$$
29	28	ralbidv	$$⊢s=U\to \left(\forall x\in B\forall a\in s\forall b\in s\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in s\leftrightarrow \forall x\in B\forall a\in U\forall b\in U\left(x\underset{\dot{}}{·}a\right)\underset{\dot{}}{+}b\in U\right)$$
30	29	elrab	$$⊢U\in \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\}\leftrightarrow \left(U\in \left(𝒫V\setminus \left\{\varnothing \right\}\right)\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)$$
31		df-3an	$$⊢\left(U\subseteq V\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)\leftrightarrow \left(\left(U\subseteq V\wedge U\ne \varnothing \right)\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)$$
32	25 30 31	3bitr4i	$$⊢U\in \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\}\leftrightarrow \left(U\subseteq V\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)$$
33	19 32	bitrdi	$$⊢W\in \mathrm{V}\to \left(U\in S\leftrightarrow \left(U\subseteq V\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)\right)$$
34	8 17 33	pm5.21nii	$$⊢U\in S\leftrightarrow \left(U\subseteq V\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)$$