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	⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
Assertion	0psubclN	⊢ ( 𝐾 ∈ HL → ∅ ∈ 𝐶 )

Proof

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