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

Metamath Proof Explorer

Theorem pcl0N

Description: The projective subspace closure of the empty subspace. (Contributed by NM, 12-Sep-2013) (New usage is discouraged.)

Ref Expression
Hypothesis pcl0.c ⊢ U = PCl ⁡ K
Assertion pcl0N ⊢ K ∈ HL → U ⁡ ∅ = ∅

Proof

Step Hyp Ref Expression
1 pcl0.c ⊢ U = PCl ⁡ K
2 0ss ⊢ ∅ ⊆ Atoms ⁡ K
3 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
4 eqid ⊢ ⊥ 𝑃 ⁡ K = ⊥ 𝑃 ⁡ K
5 3 4 1 pclss2polN ⊢ K ∈ HL ∧ ∅ ⊆ Atoms ⁡ K → U ⁡ ∅ ⊆ ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ ∅
6 2 5 mpan2 ⊢ K ∈ HL → U ⁡ ∅ ⊆ ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ ∅
7 4 2pol0N ⊢ K ∈ HL → ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ ∅ = ∅
8 6 7 sseqtrd ⊢ K ∈ HL → U ⁡ ∅ ⊆ ∅
9 ss0 ⊢ U ⁡ ∅ ⊆ ∅ → U ⁡ ∅ = ∅
10 8 9 syl ⊢ K ∈ HL → U ⁡ ∅ = ∅