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

Metamath Proof Explorer

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 ` (/) ) = (/) )