Theorem 1psubclN

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

	Ref	Expression
Hypotheses	1psubcl.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	1psubcl.c	$$⊢C=\mathrm{PSubCl}\left(K\right)$$
Assertion	1psubclN	$$⊢K\in \mathrm{HL}\to A\in C$$

Proof

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