Theorem 00lss

Description: The empty structure has no subspaces (for use with fvco4i ). (Contributed by Stefan O'Rear, 31-Mar-2015)

	Ref	Expression
Assertion	00lss	$$⊢\varnothing =\mathrm{LSubSp}\left(\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		noel	$$⊢\neg a\in \varnothing$$
2		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
3		eqid	$$⊢\mathrm{LSubSp}\left(\varnothing \right)=\mathrm{LSubSp}\left(\varnothing \right)$$
4	2 3	lssss	$$⊢a\in \mathrm{LSubSp}\left(\varnothing \right)\to a\subseteq \varnothing$$
5		ss0	$$⊢a\subseteq \varnothing \to a=\varnothing$$
6	4 5	syl	$$⊢a\in \mathrm{LSubSp}\left(\varnothing \right)\to a=\varnothing$$
7	3	lssn0	$$⊢a\in \mathrm{LSubSp}\left(\varnothing \right)\to a\ne \varnothing$$
8	7	neneqd	$$⊢a\in \mathrm{LSubSp}\left(\varnothing \right)\to \neg a=\varnothing$$
9	6 8	pm2.65i	$$⊢\neg a\in \mathrm{LSubSp}\left(\varnothing \right)$$
10	1 9	2false	$$⊢a\in \varnothing \leftrightarrow a\in \mathrm{LSubSp}\left(\varnothing \right)$$
11	10	eqriv	$$⊢\varnothing =\mathrm{LSubSp}\left(\varnothing \right)$$