This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elspansn3

Description: A member of the span of the singleton of a vector is a member of a subspace containing the vector. (Contributed by NM, 16-Dec-2004) (New usage is discouraged.)

Ref Expression
Assertion elspansn3 ⊢ A ∈ S ℋ ∧ B ∈ A ∧ C ∈ span ⁡ B → C ∈ A

Proof

Step Hyp Ref Expression
1 spansnss ⊢ A ∈ S ℋ ∧ B ∈ A → span ⁡ B ⊆ A
2 1 sseld ⊢ A ∈ S ℋ ∧ B ∈ A → C ∈ span ⁡ B → C ∈ A
3 2 3impia ⊢ A ∈ S ℋ ∧ B ∈ A ∧ C ∈ span ⁡ B → C ∈ A