Theorem pcl0N

Description: The projective subspace closure of the empty subspace. (Contributed by NM, 12-Sep-2013) (New usage is discouraged.)

	Ref	Expression
Hypothesis	pcl0.c	$$⊢U=\mathrm{PCl}\left(K\right)$$
Assertion	pcl0N	$$⊢K\in \mathrm{HL}\to U\left(\varnothing \right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		pcl0.c	$$⊢U=\mathrm{PCl}\left(K\right)$$
2		0ss	$$⊢\varnothing \subseteq \mathrm{Atoms}\left(K\right)$$
3		eqid	$$⊢\mathrm{Atoms}\left(K\right)=\mathrm{Atoms}\left(K\right)$$
4		eqid	$$⊢{\perp }_{𝑃}\left(K\right)={\perp }_{𝑃}\left(K\right)$$
5	3 4 1	pclss2polN	$$⊢\left(K\in \mathrm{HL}\wedge \varnothing \subseteq \mathrm{Atoms}\left(K\right)\right)\to U\left(\varnothing \right)\subseteq {\perp }_{𝑃}\left(K\right)\left({\perp }_{𝑃}\left(K\right)\left(\varnothing \right)\right)$$
6	2 5	mpan2	$$⊢K\in \mathrm{HL}\to U\left(\varnothing \right)\subseteq {\perp }_{𝑃}\left(K\right)\left({\perp }_{𝑃}\left(K\right)\left(\varnothing \right)\right)$$
7	4	2pol0N	$$⊢K\in \mathrm{HL}\to {\perp }_{𝑃}\left(K\right)\left({\perp }_{𝑃}\left(K\right)\left(\varnothing \right)\right)=\varnothing$$
8	6 7	sseqtrd	$$⊢K\in \mathrm{HL}\to U\left(\varnothing \right)\subseteq \varnothing$$
9		ss0	$$⊢U\left(\varnothing \right)\subseteq \varnothing \to U\left(\varnothing \right)=\varnothing$$
10	8 9	syl	$$⊢K\in \mathrm{HL}\to U\left(\varnothing \right)=\varnothing$$