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 ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
1psubcl.c ⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
Assertion 1psubclN ( 𝐾 ∈ HL → 𝐴 ∈ 𝐶 )

Proof

Step Hyp Ref Expression
1 1psubcl.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 1psubcl.c ⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
3 ssidd ⊢ ( 𝐾 ∈ HL → 𝐴 ⊆ 𝐴 )
4 eqid ⊢ ( ⊥𝑃 ‘ 𝐾 ) = ( ⊥𝑃 ‘ 𝐾 )
5 1 4 pol1N ⊢ ( 𝐾 ∈ HL → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝐴 ) = ∅ )
6 5 fveq2d ⊢ ( 𝐾 ∈ HL → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝐴 ) ) = ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ∅ ) )
7 1 4 pol0N ⊢ ( 𝐾 ∈ HL → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ∅ ) = 𝐴 )
8 6 7 eqtrd ⊢ ( 𝐾 ∈ HL → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝐴 ) ) = 𝐴 )
9 1 4 2 ispsubclN ⊢ ( 𝐾 ∈ HL → ( 𝐴 ∈ 𝐶 ↔ ( 𝐴 ⊆ 𝐴 ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝐴 ) ) = 𝐴 ) ) )
10 3 8 9 mpbir2and ⊢ ( 𝐾 ∈ HL → 𝐴 ∈ 𝐶 )