Theorem psubcli2N

Description: Property of a closed projective subspace. (Contributed by NM, 23-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	psubcli2.p	|- ._|_ = ( _|_P ` K )
	psubcli2.c	|- C = ( PSubCl ` K )
Assertion	psubcli2N	|- ( ( K e. D /\ X e. C ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )

Proof

Step	Hyp	Ref	Expression
1		psubcli2.p	|- ._|_ = ( _|_P ` K )
2		psubcli2.c	|- C = ( PSubCl ` K )
3		eqid	|- ( Atoms ` K ) = ( Atoms ` K )
4	3 1 2	ispsubclN	|- ( K e. D -> ( X e. C <-> ( X C_ ( Atoms ` K ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) ) )
5	4	simplbda	|- ( ( K e. D /\ X e. C ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )