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

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 1psubcl.a ⊢ A = Atoms ⁡ K
2 1psubcl.c ⊢ C = PSubCl ⁡ K
3 ssidd ⊢ K ∈ HL → A ⊆ A
4 eqid ⊢ ⊥ 𝑃 ⁡ K = ⊥ 𝑃 ⁡ K
5 1 4 pol1N ⊢ K ∈ HL → ⊥ 𝑃 ⁡ K ⁡ A = ∅
6 5 fveq2d ⊢ K ∈ HL → ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ A = ⊥ 𝑃 ⁡ K ⁡ ∅
7 1 4 pol0N ⊢ K ∈ HL → ⊥ 𝑃 ⁡ K ⁡ ∅ = A
8 6 7 eqtrd ⊢ K ∈ HL → ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ A = A
9 1 4 2 ispsubclN ⊢ K ∈ HL → A ∈ C ↔ A ⊆ A ∧ ⊥ 𝑃 ⁡ K ⁡ ⊥ 𝑃 ⁡ K ⁡ A = A
10 3 8 9 mpbir2and ⊢ K ∈ HL → A ∈ C