This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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