Metamath Proof Explorer


Theorem 2pol0N

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

Proof

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