This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0psubclN

Description: The empty set is a closed projective subspace. (Contributed by NM, 25-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypothesis 0psubcl.c ⊢ C = PSubCl ⁡ K
Assertion 0psubclN ⊢ K ∈ HL → ∅ ∈ C

Proof

Step Hyp Ref Expression
1 0psubcl.c ⊢ C = PSubCl ⁡ K
2 0ss ⊢ ∅ ⊆ Atoms ⁡ K
3 2 a1i ⊢ K ∈ HL → ∅ ⊆ Atoms ⁡ K
4 eqid ⊢ ⊥ 𝑃 ⁡ K = ⊥ 𝑃 ⁡ K
5 4 2pol0N ⊢ K ∈ HL → ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ ∅ = ∅
6 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
7 6 4 1 ispsubclN ⊢ K ∈ HL → ∅ ∈ C ↔ ∅ ⊆ Atoms ⁡ K ∧ ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ ∅ = ∅
8 3 5 7 mpbir2and ⊢ K ∈ HL → ∅ ∈ C