Metamath Proof Explorer

Theorem pcl0bN

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

Ref Expression
Hypotheses pcl0b.a 
|- A = ( Atoms ` K )
pcl0b.c 
|- U = ( PCl ` K )
Assertion pcl0bN 
|- ( ( K e. HL /\ P C_ A ) -> ( ( U ` P ) = (/) <-> P = (/) ) )

Proof

Step Hyp Ref Expression
1 pcl0b.a 
 |-  A = ( Atoms ` K )
2 pcl0b.c 
 |-  U = ( PCl ` K )
3 1 2 pclssidN 
 |-  ( ( K e. HL /\ P C_ A ) -> P C_ ( U ` P ) )
4 eqimss 
 |-  ( ( U ` P ) = (/) -> ( U ` P ) C_ (/) )
5 3 4 sylan9ss 
 |-  ( ( ( K e. HL /\ P C_ A ) /\ ( U ` P ) = (/) ) -> P C_ (/) )
6 ss0 
 |-  ( P C_ (/) -> P = (/) )
7 5 6 syl 
 |-  ( ( ( K e. HL /\ P C_ A ) /\ ( U ` P ) = (/) ) -> P = (/) )
8 fveq2 
 |-  ( P = (/) -> ( U ` P ) = ( U ` (/) ) )
9 2 pcl0N 
 |-  ( K e. HL -> ( U ` (/) ) = (/) )
10 8 9 sylan9eqr 
 |-  ( ( K e. HL /\ P = (/) ) -> ( U ` P ) = (/) )
11 10 adantlr 
 |-  ( ( ( K e. HL /\ P C_ A ) /\ P = (/) ) -> ( U ` P ) = (/) )
12 7 11 impbida 
 |-  ( ( K e. HL /\ P C_ A ) -> ( ( U ` P ) = (/) <-> P = (/) ) )