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 B V
Assertion elspani A B span A x S A x B x

Proof

Step Hyp Ref Expression
1 elspan.1 B V
2 spanval A span A = x S | A x
3 2 eleq2d A B span A B x S | A x
4 1 elintrab B x S | A x x S A x B x
5 3 4 bitrdi A B span A x S A x B x