Theorem shsva

Description: Vector sum belongs to subspace sum. (Contributed by NM, 15-Dec-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	shsva	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) → ( 𝐶 +ℎ 𝐷 ) ∈ ( 𝐴 +ℋ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝐶 +ℎ 𝐷 ) = ( 𝐶 +ℎ 𝐷 )
2		rspceov	⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ ( 𝐶 +ℎ 𝐷 ) = ( 𝐶 +ℎ 𝐷 ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐶 +ℎ 𝐷 ) = ( 𝑥 +ℎ 𝑦 ) )
3	1 2	mp3an3	⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐶 +ℎ 𝐷 ) = ( 𝑥 +ℎ 𝑦 ) )
4		shsel	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( ( 𝐶 +ℎ 𝐷 ) ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐶 +ℎ 𝐷 ) = ( 𝑥 +ℎ 𝑦 ) ) )
5	3 4	imbitrrid	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) → ( 𝐶 +ℎ 𝐷 ) ∈ ( 𝐴 +ℋ 𝐵 ) ) )