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 )