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

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 ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) ↔ 𝐵 ∈ ( span ‘ { 𝐴 } ) ) )

Proof

Step Hyp Ref Expression
1 spansnsh ⊢ ( 𝐴 ∈ ℋ → ( span ‘ { 𝐴 } ) ∈ Sℋ )
2 1 adantr ⊢ ( ( 𝐴 ∈ ℋ ∧ ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) ) → ( span ‘ { 𝐴 } ) ∈ Sℋ )
3 simpr ⊢ ( ( 𝐴 ∈ ℋ ∧ ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) ) → ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) )
4 spansnid ⊢ ( 𝐴 ∈ ℋ → 𝐴 ∈ ( span ‘ { 𝐴 } ) )
5 4 adantr ⊢ ( ( 𝐴 ∈ ℋ ∧ ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) ) → 𝐴 ∈ ( span ‘ { 𝐴 } ) )
6 shsubcl ⊢ ( ( ( span ‘ { 𝐴 } ) ∈ Sℋ ∧ ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) ∧ 𝐴 ∈ ( span ‘ { 𝐴 } ) ) → ( ( 𝐴 +ℎ 𝐵 ) −ℎ 𝐴 ) ∈ ( span ‘ { 𝐴 } ) )
7 2 3 5 6 syl3anc ⊢ ( ( 𝐴 ∈ ℋ ∧ ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) ) → ( ( 𝐴 +ℎ 𝐵 ) −ℎ 𝐴 ) ∈ ( span ‘ { 𝐴 } ) )
8 7 ex ⊢ ( 𝐴 ∈ ℋ → ( ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) → ( ( 𝐴 +ℎ 𝐵 ) −ℎ 𝐴 ) ∈ ( span ‘ { 𝐴 } ) ) )
9 8 adantr ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) → ( ( 𝐴 +ℎ 𝐵 ) −ℎ 𝐴 ) ∈ ( span ‘ { 𝐴 } ) ) )
10 hvpncan2 ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 +ℎ 𝐵 ) −ℎ 𝐴 ) = 𝐵 )
11 10 eleq1d ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( 𝐴 +ℎ 𝐵 ) −ℎ 𝐴 ) ∈ ( span ‘ { 𝐴 } ) ↔ 𝐵 ∈ ( span ‘ { 𝐴 } ) ) )
12 9 11 sylibd ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) → 𝐵 ∈ ( span ‘ { 𝐴 } ) ) )
13 shaddcl ⊢ ( ( ( span ‘ { 𝐴 } ) ∈ Sℋ ∧ 𝐴 ∈ ( span ‘ { 𝐴 } ) ∧ 𝐵 ∈ ( span ‘ { 𝐴 } ) ) → ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) )
14 13 3expia ⊢ ( ( ( span ‘ { 𝐴 } ) ∈ Sℋ ∧ 𝐴 ∈ ( span ‘ { 𝐴 } ) ) → ( 𝐵 ∈ ( span ‘ { 𝐴 } ) → ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) ) )
15 1 4 14 syl2anc ⊢ ( 𝐴 ∈ ℋ → ( 𝐵 ∈ ( span ‘ { 𝐴 } ) → ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) ) )
16 15 adantr ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐵 ∈ ( span ‘ { 𝐴 } ) → ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) ) )
17 12 16 impbid ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 +ℎ 𝐵 ) ∈ ( span ‘ { 𝐴 } ) ↔ 𝐵 ∈ ( span ‘ { 𝐴 } ) ) )