Description: The empty set is a closed projective subspace. (Contributed by NM, 25-Jan-2012) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | 0psubcl.c | |- C = ( PSubCl ` K ) |
|
| Assertion | 0psubclN | |- ( K e. HL -> (/) e. C ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0psubcl.c | |- C = ( PSubCl ` K ) |
|
| 2 | 0ss | |- (/) C_ ( Atoms ` K ) |
|
| 3 | 2 | a1i | |- ( K e. HL -> (/) C_ ( Atoms ` K ) ) |
| 4 | eqid | |- ( _|_P ` K ) = ( _|_P ` K ) |
|
| 5 | 4 | 2pol0N | |- ( K e. HL -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` (/) ) ) = (/) ) |
| 6 | eqid | |- ( Atoms ` K ) = ( Atoms ` K ) |
|
| 7 | 6 4 1 | ispsubclN | |- ( K e. HL -> ( (/) e. C <-> ( (/) C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` (/) ) ) = (/) ) ) ) |
| 8 | 3 5 7 | mpbir2and | |- ( K e. HL -> (/) e. C ) |