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

Metamath Proof Explorer

Theorem spansnss

Description: The span of the singleton of an element of a subspace is included in the subspace. (Contributed by NM, 5-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion spansnss ⊢ A ∈ S ℋ ∧ B ∈ A → span ⁡ B ⊆ A

Proof

Step Hyp Ref Expression
1 shel ⊢ A ∈ S ℋ ∧ B ∈ A → B ∈ ℋ
2 elspansn ⊢ B ∈ ℋ → x ∈ span ⁡ B ↔ ∃ y ∈ ℂ x = y ⋅ ℎ B
3 1 2 syl ⊢ A ∈ S ℋ ∧ B ∈ A → x ∈ span ⁡ B ↔ ∃ y ∈ ℂ x = y ⋅ ℎ B
4 shmulcl ⊢ A ∈ S ℋ ∧ y ∈ ℂ ∧ B ∈ A → y ⋅ ℎ B ∈ A
5 eleq1a ⊢ y ⋅ ℎ B ∈ A → x = y ⋅ ℎ B → x ∈ A
6 4 5 syl ⊢ A ∈ S ℋ ∧ y ∈ ℂ ∧ B ∈ A → x = y ⋅ ℎ B → x ∈ A
7 6 3exp ⊢ A ∈ S ℋ → y ∈ ℂ → B ∈ A → x = y ⋅ ℎ B → x ∈ A
8 7 com23 ⊢ A ∈ S ℋ → B ∈ A → y ∈ ℂ → x = y ⋅ ℎ B → x ∈ A
9 8 imp ⊢ A ∈ S ℋ ∧ B ∈ A → y ∈ ℂ → x = y ⋅ ℎ B → x ∈ A
10 9 rexlimdv ⊢ A ∈ S ℋ ∧ B ∈ A → ∃ y ∈ ℂ x = y ⋅ ℎ B → x ∈ A
11 3 10 sylbid ⊢ A ∈ S ℋ ∧ B ∈ A → x ∈ span ⁡ B → x ∈ A
12 11 ssrdv ⊢ A ∈ S ℋ ∧ B ∈ A → span ⁡ B ⊆ A