Metamath Proof Explorer


Theorem spansnch

Description: The span of a Hilbert space singleton belongs to the Hilbert lattice. (Contributed by NM, 9-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion spansnch ( 𝐴 ∈ ℋ → ( span ‘ { 𝐴 } ) ∈ C )

Proof

Step Hyp Ref Expression
1 spansn ( 𝐴 ∈ ℋ → ( span ‘ { 𝐴 } ) = ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) )
2 snssi ( 𝐴 ∈ ℋ → { 𝐴 } ⊆ ℋ )
3 occl ( { 𝐴 } ⊆ ℋ → ( ⊥ ‘ { 𝐴 } ) ∈ C )
4 choccl ( ( ⊥ ‘ { 𝐴 } ) ∈ C → ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) ∈ C )
5 2 3 4 3syl ( 𝐴 ∈ ℋ → ( ⊥ ‘ ( ⊥ ‘ { 𝐴 } ) ) ∈ C )
6 1 5 eqeltrd ( 𝐴 ∈ ℋ → ( span ‘ { 𝐴 } ) ∈ C )