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ℋ )