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 ‘ { 𝐴 } ) ) )