Theorem psubclsubN

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

	Ref	Expression
Hypotheses	psubclsub.s	|- S = ( PSubSp ` K )
	psubclsub.c	|- C = ( PSubCl ` K )
Assertion	psubclsubN	|- ( ( K e. HL /\ X e. C ) -> X e. S )

Proof

Step	Hyp	Ref	Expression
1		psubclsub.s	|- S = ( PSubSp ` K )
2		psubclsub.c	|- C = ( PSubCl ` K )
3		eqid	|- ( _|_P ` K ) = ( _|_P ` K )
4	3 2	psubcli2N	|- ( ( K e. HL /\ X e. C ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X )
5		eqid	|- ( Atoms ` K ) = ( Atoms ` K )
6	5 3 2	psubcliN	|- ( ( K e. HL /\ X e. C ) -> ( X C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X ) )
7	6	simpld	|- ( ( K e. HL /\ X e. C ) -> X C_ ( Atoms ` K ) )
8	5 1 3	polsubN	|- ( ( K e. HL /\ X C_ ( Atoms ` K ) ) -> ( ( _|_P ` K ) ` X ) e. S )
9	7 8	syldan	|- ( ( K e. HL /\ X e. C ) -> ( ( _|_P ` K ) ` X ) e. S )
10	5 1	psubssat	|- ( ( K e. HL /\ ( ( _|_P ` K ) ` X ) e. S ) -> ( ( _|_P ` K ) ` X ) C_ ( Atoms ` K ) )
11	9 10	syldan	|- ( ( K e. HL /\ X e. C ) -> ( ( _|_P ` K ) ` X ) C_ ( Atoms ` K ) )
12	5 1 3	polsubN	|- ( ( K e. HL /\ ( ( _|_P ` K ) ` X ) C_ ( Atoms ` K ) ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) e. S )
13	11 12	syldan	|- ( ( K e. HL /\ X e. C ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) e. S )
14	4 13	eqeltrrd	|- ( ( K e. HL /\ X e. C ) -> X e. S )