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

Metamath Proof Explorer

Theorem atpsubclN

Description: A point (singleton of an atom) is a closed projective subspace. (Contributed by NM, 25-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 1psubcl.a 
|- A = ( Atoms ` K )
1psubcl.c 
|- C = ( PSubCl ` K )
Assertion atpsubclN 
|- ( ( K e. HL /\ Q e. A ) -> { Q } e. C )

Proof

Step Hyp Ref Expression
1 1psubcl.a 
 |-  A = ( Atoms ` K )
2 1psubcl.c 
 |-  C = ( PSubCl ` K )
3 snssi 
 |-  ( Q e. A -> { Q } C_ A )
4 3 adantl 
 |-  ( ( K e. HL /\ Q e. A ) -> { Q } C_ A )
5 eqid 
 |-  ( _|_P ` K ) = ( _|_P ` K )
6 1 5 2polatN 
 |-  ( ( K e. HL /\ Q e. A ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` { Q } ) ) = { Q } )
7 1 5 2 ispsubclN 
 |-  ( K e. HL -> ( { Q } e. C <-> ( { Q } C_ A /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` { Q } ) ) = { Q } ) ) )
8 7 adantr 
 |-  ( ( K e. HL /\ Q e. A ) -> ( { Q } e. C <-> ( { Q } C_ A /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` { Q } ) ) = { Q } ) ) )
9 4 6 8 mpbir2and 
 |-  ( ( K e. HL /\ Q e. A ) -> { Q } e. C )