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