Theorem pmapidclN

Description: Projective map of the LUB of a closed subspace. (Contributed by NM, 3-Feb-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pmapidcl.u	|- U = ( lub ` K )
	pmapidcl.m	|- M = ( pmap ` K )
	pmapidcl.c	|- C = ( PSubCl ` K )
Assertion	pmapidclN	|- ( ( K e. HL /\ X e. C ) -> ( M ` ( U ` X ) ) = X )

Proof

Step	Hyp	Ref	Expression
1		pmapidcl.u	|- U = ( lub ` K )
2		pmapidcl.m	|- M = ( pmap ` K )
3		pmapidcl.c	|- C = ( PSubCl ` K )
4		eqid	|- ( Atoms ` K ) = ( Atoms ` K )
5	4 3	psubclssatN	|- ( ( K e. HL /\ X e. C ) -> X C_ ( Atoms ` K ) )
6		eqid	|- ( _|_P ` K ) = ( _|_P ` K )
7	1 4 2 6	2polvalN	|- ( ( K e. HL /\ X C_ ( Atoms ` K ) ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = ( M ` ( U ` X ) ) )
8	5 7	syldan	|- ( ( K e. HL /\ X e. C ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = ( M ` ( U ` X ) ) )
9	6 3	psubcli2N	|- ( ( K e. HL /\ X e. C ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X )
10	8 9	eqtr3d	|- ( ( K e. HL /\ X e. C ) -> ( M ` ( U ` X ) ) = X )