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 ⊢ A = Atoms ⁡ K
1psubcl.c ⊢ C = PSubCl ⁡ K
Assertion atpsubclN ⊢ K ∈ HL ∧ Q ∈ A → Q ∈ C

Proof

Step Hyp Ref Expression
1 1psubcl.a ⊢ A = Atoms ⁡ K
2 1psubcl.c ⊢ C = PSubCl ⁡ K
3 snssi ⊢ Q ∈ A → Q ⊆ A
4 3 adantl ⊢ K ∈ HL ∧ Q ∈ A → Q ⊆ A
5 eqid ⊢ ⊥ 𝑃 ⁡ K = ⊥ 𝑃 ⁡ K
6 1 5 2polatN ⊢ K ∈ HL ∧ Q ∈ A → ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ Q = Q
7 1 5 2 ispsubclN ⊢ K ∈ HL → Q ∈ C ↔ Q ⊆ A ∧ ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ Q = Q
8 7 adantr ⊢ K ∈ HL ∧ Q ∈ A → Q ∈ C ↔ Q ⊆ A ∧ ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ Q = Q
9 4 6 8 mpbir2and ⊢ K ∈ HL ∧ Q ∈ A → Q ∈ C