Theorem 1psubclN

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

	Ref	Expression
Hypotheses	1psubcl.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	1psubcl.c	⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
Assertion	1psubclN	⊢ ( 𝐾 ∈ HL → 𝐴 ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		1psubcl.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		1psubcl.c	⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
3		ssidd	⊢ ( 𝐾 ∈ HL → 𝐴 ⊆ 𝐴 )
4		eqid	⊢ ( ⊥𝑃 ‘ 𝐾 ) = ( ⊥𝑃 ‘ 𝐾 )
5	1 4	pol1N	⊢ ( 𝐾 ∈ HL → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝐴 ) = ∅ )
6	5	fveq2d	⊢ ( 𝐾 ∈ HL → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝐴 ) ) = ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ∅ ) )
7	1 4	pol0N	⊢ ( 𝐾 ∈ HL → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ∅ ) = 𝐴 )
8	6 7	eqtrd	⊢ ( 𝐾 ∈ HL → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝐴 ) ) = 𝐴 )
9	1 4 2	ispsubclN	⊢ ( 𝐾 ∈ HL → ( 𝐴 ∈ 𝐶 ↔ ( 𝐴 ⊆ 𝐴 ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝐴 ) ) = 𝐴 ) ) )
10	3 8 9	mpbir2and	⊢ ( 𝐾 ∈ HL → 𝐴 ∈ 𝐶 )