Theorem 0psubclN

Description: The empty set is a closed projective subspace. (Contributed by NM, 25-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypothesis	0psubcl.c	$$⊢C=\mathrm{PSubCl}\left(K\right)$$
Assertion	0psubclN	$$⊢K\in \mathrm{HL}\to \varnothing \in C$$

Proof

Step	Hyp	Ref	Expression
1		0psubcl.c	$$⊢C=\mathrm{PSubCl}\left(K\right)$$
2		0ss	$$⊢\varnothing \subseteq \mathrm{Atoms}\left(K\right)$$
3	2	a1i	$$⊢K\in \mathrm{HL}\to \varnothing \subseteq \mathrm{Atoms}\left(K\right)$$
4		eqid	$$⊢{\perp }_{𝑃}\left(K\right)={\perp }_{𝑃}\left(K\right)$$
5	4	2pol0N	$$⊢K\in \mathrm{HL}\to {\perp }_{𝑃}\left(K\right)\left({\perp }_{𝑃}\left(K\right)\left(\varnothing \right)\right)=\varnothing$$
6		eqid	$$⊢\mathrm{Atoms}\left(K\right)=\mathrm{Atoms}\left(K\right)$$
7	6 4 1	ispsubclN	$$⊢K\in \mathrm{HL}\to \left(\varnothing \in C\leftrightarrow \left(\varnothing \subseteq \mathrm{Atoms}\left(K\right)\wedge {\perp }_{𝑃}\left(K\right)\left({\perp }_{𝑃}\left(K\right)\left(\varnothing \right)\right)=\varnothing \right)\right)$$
8	3 5 7	mpbir2and	$$⊢K\in \mathrm{HL}\to \varnothing \in C$$