Theorem 1psubclN

Description: The set of all atoms 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	1psubclN	|- ( K e. HL -> A e. C )

Proof

Step	Hyp	Ref	Expression
1		1psubcl.a	|- A = ( Atoms ` K )
2		1psubcl.c	|- C = ( PSubCl ` K )
3		ssidd	|- ( K e. HL -> A C_ A )
4		eqid	|- ( _|_P ` K ) = ( _|_P ` K )
5	1 4	pol1N	|- ( K e. HL -> ( ( _|_P ` K ) ` A ) = (/) )
6	5	fveq2d	|- ( K e. HL -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` A ) ) = ( ( _|_P ` K ) ` (/) ) )
7	1 4	pol0N	|- ( K e. HL -> ( ( _|_P ` K ) ` (/) ) = A )
8	6 7	eqtrd	|- ( K e. HL -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` A ) ) = A )
9	1 4 2	ispsubclN	|- ( K e. HL -> ( A e. C <-> ( A C_ A /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` A ) ) = A ) ) )
10	3 8 9	mpbir2and	|- ( K e. HL -> A e. C )