Theorem pmapsubclN

Description: A projective map value is a closed projective subspace. (Contributed by NM, 24-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pmapsubcl.b	$$⊢B={\mathrm{Base}}_K$$
	pmapsubcl.m	$$⊢M=\mathrm{pmap}\left(K\right)$$
	pmapsubcl.c	$$⊢C=\mathrm{PSubCl}\left(K\right)$$
Assertion	pmapsubclN	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to M\left(X\right)\in C$$

Proof

Step	Hyp	Ref	Expression
1		pmapsubcl.b	$$⊢B={\mathrm{Base}}_K$$
2		pmapsubcl.m	$$⊢M=\mathrm{pmap}\left(K\right)$$
3		pmapsubcl.c	$$⊢C=\mathrm{PSubCl}\left(K\right)$$
4		eqid	$$⊢\mathrm{Atoms}\left(K\right)=\mathrm{Atoms}\left(K\right)$$
5	1 4 2	pmapssat	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to M\left(X\right)\subseteq \mathrm{Atoms}\left(K\right)$$
6		eqid	$$⊢{\perp }_{𝑃}\left(K\right)={\perp }_{𝑃}\left(K\right)$$
7	1 2 6	2polpmapN	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to {\perp }_{𝑃}\left(K\right)\left({\perp }_{𝑃}\left(K\right)\left(M\left(X\right)\right)\right)=M\left(X\right)$$
8	4 6 3	ispsubclN	$$⊢K\in \mathrm{HL}\to \left(M\left(X\right)\in C\leftrightarrow \left(M\left(X\right)\subseteq \mathrm{Atoms}\left(K\right)\wedge {\perp }_{𝑃}\left(K\right)\left({\perp }_{𝑃}\left(K\right)\left(M\left(X\right)\right)\right)=M\left(X\right)\right)\right)$$
9	8	adantr	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to \left(M\left(X\right)\in C\leftrightarrow \left(M\left(X\right)\subseteq \mathrm{Atoms}\left(K\right)\wedge {\perp }_{𝑃}\left(K\right)\left({\perp }_{𝑃}\left(K\right)\left(M\left(X\right)\right)\right)=M\left(X\right)\right)\right)$$
10	5 7 9	mpbir2and	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to M\left(X\right)\in C$$