Metamath Proof Explorer

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}↔\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}↔\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}$