Theorem lsssn0

Description: The singleton of the zero vector is a subspace. (Contributed by NM, 13-Jan-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lss0cl.z	$$⊢\underset{\dot{}}{0}=0_W$$
	lss0cl.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
Assertion	lsssn0	$$⊢W\in \mathrm{LMod}\to \left\{\underset{\dot{}}{0}\right\}\in S$$

Proof

Step	Hyp	Ref	Expression
1		lss0cl.z	$$⊢\underset{\dot{}}{0}=0_W$$
2		lss0cl.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
3		eqidd	$$⊢W\in \mathrm{LMod}\to \mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
4		eqidd	$$⊢W\in \mathrm{LMod}\to {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
5		eqidd	$$⊢W\in \mathrm{LMod}\to {\mathrm{Base}}_W={\mathrm{Base}}_W$$
6		eqidd	$$⊢W\in \mathrm{LMod}\to {+}_W={+}_W$$
7		eqidd	$$⊢W\in \mathrm{LMod}\to {\cdot }_W={\cdot }_W$$
8	2	a1i	$$⊢W\in \mathrm{LMod}\to S=\mathrm{LSubSp}\left(W\right)$$
9		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
10	9 1	lmod0vcl	$$⊢W\in \mathrm{LMod}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_W$$
11	10	snssd	$$⊢W\in \mathrm{LMod}\to \left\{\underset{\dot{}}{0}\right\}\subseteq {\mathrm{Base}}_W$$
12	1	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
13	12	snnz	$$⊢\left\{\underset{\dot{}}{0}\right\}\ne \varnothing$$
14	13	a1i	$$⊢W\in \mathrm{LMod}\to \left\{\underset{\dot{}}{0}\right\}\ne \varnothing$$
15		simpr2	$$⊢\left(W\in \mathrm{LMod}\wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge a\in \left\{\underset{\dot{}}{0}\right\}\wedge b\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\to a\in \left\{\underset{\dot{}}{0}\right\}$$
16		elsni	$$⊢a\in \left\{\underset{\dot{}}{0}\right\}\to a=\underset{\dot{}}{0}$$
17	15 16	syl	$$⊢\left(W\in \mathrm{LMod}\wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge a\in \left\{\underset{\dot{}}{0}\right\}\wedge b\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\to a=\underset{\dot{}}{0}$$
18	17	oveq2d	$$⊢\left(W\in \mathrm{LMod}\wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge a\in \left\{\underset{\dot{}}{0}\right\}\wedge b\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\to x{\cdot }_{W}a=x{\cdot }_W\underset{\dot{}}{0}$$
19		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
20		eqid	$$⊢{\cdot }_W={\cdot }_W$$
21		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
22	19 20 21 1	lmodvs0	$$⊢\left(W\in \mathrm{LMod}\wedge x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\right)\to x{\cdot }_W\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
23	22	3ad2antr1	$$⊢\left(W\in \mathrm{LMod}\wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge a\in \left\{\underset{\dot{}}{0}\right\}\wedge b\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\to x{\cdot }_W\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
24	18 23	eqtrd	$$⊢\left(W\in \mathrm{LMod}\wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge a\in \left\{\underset{\dot{}}{0}\right\}\wedge b\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\to x{\cdot }_{W}a=\underset{\dot{}}{0}$$
25		simpr3	$$⊢\left(W\in \mathrm{LMod}\wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge a\in \left\{\underset{\dot{}}{0}\right\}\wedge b\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\to b\in \left\{\underset{\dot{}}{0}\right\}$$
26		elsni	$$⊢b\in \left\{\underset{\dot{}}{0}\right\}\to b=\underset{\dot{}}{0}$$
27	25 26	syl	$$⊢\left(W\in \mathrm{LMod}\wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge a\in \left\{\underset{\dot{}}{0}\right\}\wedge b\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\to b=\underset{\dot{}}{0}$$
28	24 27	oveq12d	$$⊢\left(W\in \mathrm{LMod}\wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge a\in \left\{\underset{\dot{}}{0}\right\}\wedge b\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(x{\cdot }_{W}a\right){+}_{W}b=\underset{\dot{}}{0}{+}_W\underset{\dot{}}{0}$$
29		eqid	$$⊢{+}_W={+}_W$$
30	9 29 1	lmod0vlid	$$⊢\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{0}\in {\mathrm{Base}}_W\right)\to \underset{\dot{}}{0}{+}_W\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
31	10 30	mpdan	$$⊢W\in \mathrm{LMod}\to \underset{\dot{}}{0}{+}_W\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
32	31	adantr	$$⊢\left(W\in \mathrm{LMod}\wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge a\in \left\{\underset{\dot{}}{0}\right\}\wedge b\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \underset{\dot{}}{0}{+}_W\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
33	28 32	eqtrd	$$⊢\left(W\in \mathrm{LMod}\wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge a\in \left\{\underset{\dot{}}{0}\right\}\wedge b\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(x{\cdot }_{W}a\right){+}_{W}b=\underset{\dot{}}{0}$$
34		ovex	$$⊢\left(x{\cdot }_{W}a\right){+}_{W}b\in \mathrm{V}$$
35	34	elsn	$$⊢\left(x{\cdot }_{W}a\right){+}_{W}b\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \left(x{\cdot }_{W}a\right){+}_{W}b=\underset{\dot{}}{0}$$
36	33 35	sylibr	$$⊢\left(W\in \mathrm{LMod}\wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge a\in \left\{\underset{\dot{}}{0}\right\}\wedge b\in \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(x{\cdot }_{W}a\right){+}_{W}b\in \left\{\underset{\dot{}}{0}\right\}$$
37	3 4 5 6 7 8 11 14 36	islssd	$$⊢W\in \mathrm{LMod}\to \left\{\underset{\dot{}}{0}\right\}\in S$$