Theorem atpsubclN

Description: A point (singleton of an atom) 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	atpsubclN	$$⊢\left(K\in \mathrm{HL}\wedge Q\in A\right)\to \left\{Q\right\}\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		snssi	$$⊢Q\in A\to \left\{Q\right\}\subseteq A$$
4	3	adantl	$$⊢\left(K\in \mathrm{HL}\wedge Q\in A\right)\to \left\{Q\right\}\subseteq A$$
5		eqid	$$⊢{\perp }_{𝑃}\left(K\right)={\perp }_{𝑃}\left(K\right)$$
6	1 5	2polatN	$$⊢\left(K\in \mathrm{HL}\wedge Q\in A\right)\to {\perp }_{𝑃}\left(K\right)\left({\perp }_{𝑃}\left(K\right)\left(\left\{Q\right\}\right)\right)=\left\{Q\right\}$$
7	1 5 2	ispsubclN	$$⊢K\in \mathrm{HL}\to \left(\left\{Q\right\}\in C\leftrightarrow \left(\left\{Q\right\}\subseteq A\wedge {\perp }_{𝑃}\left(K\right)\left({\perp }_{𝑃}\left(K\right)\left(\left\{Q\right\}\right)\right)=\left\{Q\right\}\right)\right)$$
8	7	adantr	$$⊢\left(K\in \mathrm{HL}\wedge Q\in A\right)\to \left(\left\{Q\right\}\in C\leftrightarrow \left(\left\{Q\right\}\subseteq A\wedge {\perp }_{𝑃}\left(K\right)\left({\perp }_{𝑃}\left(K\right)\left(\left\{Q\right\}\right)\right)=\left\{Q\right\}\right)\right)$$
9	4 6 8	mpbir2and	$$⊢\left(K\in \mathrm{HL}\wedge Q\in A\right)\to \left\{Q\right\}\in C$$