This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )