Theorem atpsubclN

Description: A point (singleton of an atom) 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	atpsubclN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ) → { 𝑄 } ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		1psubcl.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		1psubcl.c	⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
3		snssi	⊢ ( 𝑄 ∈ 𝐴 → { 𝑄 } ⊆ 𝐴 )
4	3	adantl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ) → { 𝑄 } ⊆ 𝐴 )
5		eqid	⊢ ( ⊥𝑃 ‘ 𝐾 ) = ( ⊥𝑃 ‘ 𝐾 )
6	1 5	2polatN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ) → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝑄 } ) ) = { 𝑄 } )
7	1 5 2	ispsubclN	⊢ ( 𝐾 ∈ HL → ( { 𝑄 } ∈ 𝐶 ↔ ( { 𝑄 } ⊆ 𝐴 ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝑄 } ) ) = { 𝑄 } ) ) )
8	7	adantr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ) → ( { 𝑄 } ∈ 𝐶 ↔ ( { 𝑄 } ⊆ 𝐴 ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ { 𝑄 } ) ) = { 𝑄 } ) ) )
9	4 6 8	mpbir2and	⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ) → { 𝑄 } ∈ 𝐶 )