Metamath Proof Explorer


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 ∧ 𝑄𝐴 ) → { 𝑄 } ∈ 𝐶 )