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 ⊢ 𝑈 = ( PCl ‘ 𝐾 )
Assertion pcl0N ( 𝐾 ∈ HL → ( 𝑈 ‘ ∅ ) = ∅ )

Proof

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