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 )