Metamath Proof Explorer


Theorem elspani

Description: Membership in the span of a subset of Hilbert space. (Contributed by NM, 2-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypothesis elspan.1 𝐵 ∈ V
Assertion elspani ( 𝐴 ⊆ ℋ → ( 𝐵 ∈ ( span ‘ 𝐴 ) ↔ ∀ 𝑥S ( 𝐴𝑥𝐵𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 elspan.1 𝐵 ∈ V
2 spanval ( 𝐴 ⊆ ℋ → ( span ‘ 𝐴 ) = { 𝑥S𝐴𝑥 } )
3 2 eleq2d ( 𝐴 ⊆ ℋ → ( 𝐵 ∈ ( span ‘ 𝐴 ) ↔ 𝐵 { 𝑥S𝐴𝑥 } ) )
4 1 elintrab ( 𝐵 { 𝑥S𝐴𝑥 } ↔ ∀ 𝑥S ( 𝐴𝑥𝐵𝑥 ) )
5 3 4 bitrdi ( 𝐴 ⊆ ℋ → ( 𝐵 ∈ ( span ‘ 𝐴 ) ↔ ∀ 𝑥S ( 𝐴𝑥𝐵𝑥 ) ) )