Description: The closed subspace closure of the empty set. (Contributed by NM, 12-Sep-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | 2pol0.o | |- ._|_ = ( _|_P ` K ) |
|
Assertion | 2pol0N | |- ( K e. HL -> ( ._|_ ` ( ._|_ ` (/) ) ) = (/) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2pol0.o | |- ._|_ = ( _|_P ` K ) |
|
2 | eqid | |- ( Atoms ` K ) = ( Atoms ` K ) |
|
3 | 2 1 | pol0N | |- ( K e. HL -> ( ._|_ ` (/) ) = ( Atoms ` K ) ) |
4 | 3 | fveq2d | |- ( K e. HL -> ( ._|_ ` ( ._|_ ` (/) ) ) = ( ._|_ ` ( Atoms ` K ) ) ) |
5 | 2 1 | pol1N | |- ( K e. HL -> ( ._|_ ` ( Atoms ` K ) ) = (/) ) |
6 | 4 5 | eqtrd | |- ( K e. HL -> ( ._|_ ` ( ._|_ ` (/) ) ) = (/) ) |