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ℋ ( 𝐴 ⊆ 𝑥 → 𝐵 ∈ 𝑥 ) ) ) |
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ℋ ( 𝐴 ⊆ 𝑥 → 𝐵 ∈ 𝑥 ) ) ) |