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