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	$$⊢\underset{\dot{}}{\perp }={\perp }_{𝑃}\left(K\right)$$
Assertion	2pol0N	$$⊢K\in \mathrm{HL}\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(\varnothing \right)\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		2pol0.o	$$⊢\underset{\dot{}}{\perp }={\perp }_{𝑃}\left(K\right)$$
2		eqid	$$⊢\mathrm{Atoms}\left(K\right)=\mathrm{Atoms}\left(K\right)$$
3	2 1	pol0N	$$⊢K\in \mathrm{HL}\to \underset{\dot{}}{\perp }\left(\varnothing \right)=\mathrm{Atoms}\left(K\right)$$
4	3	fveq2d	$$⊢K\in \mathrm{HL}\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(\varnothing \right)\right)=\underset{\dot{}}{\perp }\left(\mathrm{Atoms}\left(K\right)\right)$$
5	2 1	pol1N	$$⊢K\in \mathrm{HL}\to \underset{\dot{}}{\perp }\left(\mathrm{Atoms}\left(K\right)\right)=\varnothing$$
6	4 5	eqtrd	$$⊢K\in \mathrm{HL}\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(\varnothing \right)\right)=\varnothing$$