Metamath Proof Explorer

Theorem elspancl

Description: A member of a span is a vector. (Contributed by NM, 17-Dec-2004) (New usage is discouraged.)

Ref Expression
Assertion elspancl 
|- ( ( A C_ ~H /\ B e. ( span ` A ) ) -> B e. ~H )

Proof

Step Hyp Ref Expression
1 spancl 
 |-  ( A C_ ~H -> ( span ` A ) e. SH )
2 shel 
 |-  ( ( ( span ` A ) e. SH /\ B e. ( span ` A ) ) -> B e. ~H )
3 1 2 sylan 
 |-  ( ( A C_ ~H /\ B e. ( span ` A ) ) -> B e. ~H )