Metamath Proof Explorer

Theorem spanpr

Description: The span of a pair of vectors. (Contributed by NM, 9-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion spanpr ⊢ A ∈ ℋ ∧ B ∈ ℋ → span ⁡ A + ℎ B ⊆ span ⁡ A B

Proof

Step Hyp Ref Expression
1 spansnsh ⊢ A ∈ ℋ → span ⁡ A ∈ S ℋ
2 spansnsh ⊢ B ∈ ℋ → span ⁡ B ∈ S ℋ
3 shscl ⊢ span ⁡ A ∈ S ℋ ∧ span ⁡ B ∈ S ℋ → span ⁡ A + ℋ span ⁡ B ∈ S ℋ
4 1 2 3 syl2an ⊢ A ∈ ℋ ∧ B ∈ ℋ → span ⁡ A + ℋ span ⁡ B ∈ S ℋ
5 4 adantr ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ x ∈ span ⁡ A + ℎ B → span ⁡ A + ℋ span ⁡ B ∈ S ℋ
6 1 2 anim12i ⊢ A ∈ ℋ ∧ B ∈ ℋ → span ⁡ A ∈ S ℋ ∧ span ⁡ B ∈ S ℋ
7 spansnid ⊢ A ∈ ℋ → A ∈ span ⁡ A
8 spansnid ⊢ B ∈ ℋ → B ∈ span ⁡ B
9 7 8 anim12i ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ∈ span ⁡ A ∧ B ∈ span ⁡ B
10 shsva ⊢ span ⁡ A ∈ S ℋ ∧ span ⁡ B ∈ S ℋ → A ∈ span ⁡ A ∧ B ∈ span ⁡ B → A + ℎ B ∈ span ⁡ A + ℋ span ⁡ B
11 6 9 10 sylc ⊢ A ∈ ℋ ∧ B ∈ ℋ → A + ℎ B ∈ span ⁡ A + ℋ span ⁡ B
12 11 adantr ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ x ∈ span ⁡ A + ℎ B → A + ℎ B ∈ span ⁡ A + ℋ span ⁡ B
13 simpr ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ x ∈ span ⁡ A + ℎ B → x ∈ span ⁡ A + ℎ B
14 elspansn3 ⊢ span ⁡ A + ℋ span ⁡ B ∈ S ℋ ∧ A + ℎ B ∈ span ⁡ A + ℋ span ⁡ B ∧ x ∈ span ⁡ A + ℎ B → x ∈ span ⁡ A + ℋ span ⁡ B
15 5 12 13 14 syl3anc ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ x ∈ span ⁡ A + ℎ B → x ∈ span ⁡ A + ℋ span ⁡ B
16 15 ex ⊢ A ∈ ℋ ∧ B ∈ ℋ → x ∈ span ⁡ A + ℎ B → x ∈ span ⁡ A + ℋ span ⁡ B
17 16 ssrdv ⊢ A ∈ ℋ ∧ B ∈ ℋ → span ⁡ A + ℎ B ⊆ span ⁡ A + ℋ span ⁡ B
18 df-pr ⊢ A B = A ∪ B
19 18 fveq2i ⊢ span ⁡ A B = span ⁡ A ∪ B
20 snssi ⊢ A ∈ ℋ → A ⊆ ℋ
21 snssi ⊢ B ∈ ℋ → B ⊆ ℋ
22 spanun ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → span ⁡ A ∪ B = span ⁡ A + ℋ span ⁡ B
23 20 21 22 syl2an ⊢ A ∈ ℋ ∧ B ∈ ℋ → span ⁡ A ∪ B = span ⁡ A + ℋ span ⁡ B
24 19 23 eqtr2id ⊢ A ∈ ℋ ∧ B ∈ ℋ → span ⁡ A + ℋ span ⁡ B = span ⁡ A B
25 17 24 sseqtrd ⊢ A ∈ ℋ ∧ B ∈ ℋ → span ⁡ A + ℎ B ⊆ span ⁡ A B