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 )