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 = ( Base ` K )
	pmapsubcl.m	|- M = ( pmap ` K )
	pmapsubcl.c	|- C = ( PSubCl ` K )
Assertion	pmapsubclN	|- ( ( K e. HL /\ X e. B ) -> ( M ` X ) e. C )

Proof

Step	Hyp	Ref	Expression
1		pmapsubcl.b	|- B = ( Base ` K )
2		pmapsubcl.m	|- M = ( pmap ` K )
3		pmapsubcl.c	|- C = ( PSubCl ` K )
4		eqid	|- ( Atoms ` K ) = ( Atoms ` K )
5	1 4 2	pmapssat	|- ( ( K e. HL /\ X e. B ) -> ( M ` X ) C_ ( Atoms ` K ) )
6		eqid	|- ( _|_P ` K ) = ( _|_P ` K )
7	1 2 6	2polpmapN	|- ( ( K e. HL /\ X e. B ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( M ` X ) ) ) = ( M ` X ) )
8	4 6 3	ispsubclN	|- ( K e. HL -> ( ( M ` X ) e. C <-> ( ( M ` X ) C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( M ` X ) ) ) = ( M ` X ) ) ) )
9	8	adantr	|- ( ( K e. HL /\ X e. B ) -> ( ( M ` X ) e. C <-> ( ( M ` X ) C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( M ` X ) ) ) = ( M ` X ) ) ) )
10	5 7 9	mpbir2and	|- ( ( K e. HL /\ X e. B ) -> ( M ` X ) e. C )