Metamath Proof Explorer

Theorem sumspansn

Description: The sum of two vectors belong to the span of one of them iff the other vector also belongs. (Contributed by NM, 1-Nov-2005) (New usage is discouraged.)

Ref Expression
Assertion sumspansn ⊢ A ∈ ℋ ∧ B ∈ ℋ → A + ℎ B ∈ span ⁡ A ↔ B ∈ span ⁡ A

Proof

Step Hyp Ref Expression
1 spansnsh ⊢ A ∈ ℋ → span ⁡ A ∈ S ℋ
2 1 adantr ⊢ A ∈ ℋ ∧ A + ℎ B ∈ span ⁡ A → span ⁡ A ∈ S ℋ
3 simpr ⊢ A ∈ ℋ ∧ A + ℎ B ∈ span ⁡ A → A + ℎ B ∈ span ⁡ A
4 spansnid ⊢ A ∈ ℋ → A ∈ span ⁡ A
5 4 adantr ⊢ A ∈ ℋ ∧ A + ℎ B ∈ span ⁡ A → A ∈ span ⁡ A
6 shsubcl ⊢ span ⁡ A ∈ S ℋ ∧ A + ℎ B ∈ span ⁡ A ∧ A ∈ span ⁡ A → A + ℎ B - ℎ A ∈ span ⁡ A
7 2 3 5 6 syl3anc ⊢ A ∈ ℋ ∧ A + ℎ B ∈ span ⁡ A → A + ℎ B - ℎ A ∈ span ⁡ A
8 7 ex ⊢ A ∈ ℋ → A + ℎ B ∈ span ⁡ A → A + ℎ B - ℎ A ∈ span ⁡ A
9 8 adantr ⊢ A ∈ ℋ ∧ B ∈ ℋ → A + ℎ B ∈ span ⁡ A → A + ℎ B - ℎ A ∈ span ⁡ A
10 hvpncan2 ⊢ A ∈ ℋ ∧ B ∈ ℋ → A + ℎ B - ℎ A = B
11 10 eleq1d ⊢ A ∈ ℋ ∧ B ∈ ℋ → A + ℎ B - ℎ A ∈ span ⁡ A ↔ B ∈ span ⁡ A
12 9 11 sylibd ⊢ A ∈ ℋ ∧ B ∈ ℋ → A + ℎ B ∈ span ⁡ A → B ∈ span ⁡ A
13 shaddcl ⊢ span ⁡ A ∈ S ℋ ∧ A ∈ span ⁡ A ∧ B ∈ span ⁡ A → A + ℎ B ∈ span ⁡ A
14 13 3expia ⊢ span ⁡ A ∈ S ℋ ∧ A ∈ span ⁡ A → B ∈ span ⁡ A → A + ℎ B ∈ span ⁡ A
15 1 4 14 syl2anc ⊢ A ∈ ℋ → B ∈ span ⁡ A → A + ℎ B ∈ span ⁡ A
16 15 adantr ⊢ A ∈ ℋ ∧ B ∈ ℋ → B ∈ span ⁡ A → A + ℎ B ∈ span ⁡ A
17 12 16 impbid ⊢ A ∈ ℋ ∧ B ∈ ℋ → A + ℎ B ∈ span ⁡ A ↔ B ∈ span ⁡ A