Theorem pcl0N

Description: The projective subspace closure of the empty subspace. (Contributed by NM, 12-Sep-2013) (New usage is discouraged.)

	Ref	Expression
Hypothesis	pcl0.c	|- U = ( PCl ` K )
Assertion	pcl0N	|- ( K e. HL -> ( U ` (/) ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		pcl0.c	|- U = ( PCl ` K )
2		0ss	|- (/) C_ ( Atoms ` K )
3		eqid	|- ( Atoms ` K ) = ( Atoms ` K )
4		eqid	|- ( _|_P ` K ) = ( _|_P ` K )
5	3 4 1	pclss2polN	|- ( ( K e. HL /\ (/) C_ ( Atoms ` K ) ) -> ( U ` (/) ) C_ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` (/) ) ) )
6	2 5	mpan2	|- ( K e. HL -> ( U ` (/) ) C_ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` (/) ) ) )
7	4	2pol0N	|- ( K e. HL -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` (/) ) ) = (/) )
8	6 7	sseqtrd	|- ( K e. HL -> ( U ` (/) ) C_ (/) )
9		ss0	|- ( ( U ` (/) ) C_ (/) -> ( U ` (/) ) = (/) )
10	8 9	syl	|- ( K e. HL -> ( U ` (/) ) = (/) )