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	⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
Assertion	2pol0N	⊢ ( 𝐾 ∈ HL → ( ⊥ ‘ ( ⊥ ‘ ∅ ) ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		2pol0.o	⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
2		eqid	⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
3	2 1	pol0N	⊢ ( 𝐾 ∈ HL → ( ⊥ ‘ ∅ ) = ( Atoms ‘ 𝐾 ) )
4	3	fveq2d	⊢ ( 𝐾 ∈ HL → ( ⊥ ‘ ( ⊥ ‘ ∅ ) ) = ( ⊥ ‘ ( Atoms ‘ 𝐾 ) ) )
5	2 1	pol1N	⊢ ( 𝐾 ∈ HL → ( ⊥ ‘ ( Atoms ‘ 𝐾 ) ) = ∅ )
6	4 5	eqtrd	⊢ ( 𝐾 ∈ HL → ( ⊥ ‘ ( ⊥ ‘ ∅ ) ) = ∅ )