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

Metamath Proof Explorer

Theorem pointpsubN

Description: A point (singleton of an atom) is a projective subspace. Remark below Definition 15.1 of MaedaMaeda p. 61. (Contributed by NM, 13-Oct-2011) (New usage is discouraged.)

Ref Expression
Hypotheses pointpsub.p 
|- P = ( Points ` K )
pointpsub.s 
|- S = ( PSubSp ` K )
Assertion pointpsubN 
|- ( ( K e. AtLat /\ X e. P ) -> X e. S )

Proof

Step Hyp Ref Expression
1 pointpsub.p 
 |-  P = ( Points ` K )
2 pointpsub.s 
 |-  S = ( PSubSp ` K )
3 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
4 3 1 ispointN 
 |-  ( K e. AtLat -> ( X e. P <-> E. q e. ( Atoms ` K ) X = { q } ) )
5 3 2 snatpsubN 
 |-  ( ( K e. AtLat /\ q e. ( Atoms ` K ) ) -> { q } e. S )
6 5 ex 
 |-  ( K e. AtLat -> ( q e. ( Atoms ` K ) -> { q } e. S ) )
7 eleq1a 
 |-  ( { q } e. S -> ( X = { q } -> X e. S ) )
8 6 7 syl6 
 |-  ( K e. AtLat -> ( q e. ( Atoms ` K ) -> ( X = { q } -> X e. S ) ) )
9 8 rexlimdv 
 |-  ( K e. AtLat -> ( E. q e. ( Atoms ` K ) X = { q } -> X e. S ) )
10 4 9 sylbid 
 |-  ( K e. AtLat -> ( X e. P -> X e. S ) )
11 10 imp 
 |-  ( ( K e. AtLat /\ X e. P ) -> X e. S )