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 → ( 𝑈 ‘ ∅ ) = ∅ )