Metamath Proof Explorer

Theorem shsvs

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

Ref Expression
Assertion shsvs ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → C ∈ A ∧ D ∈ B → C - ℎ D ∈ A + ℋ B

Proof

Step Hyp Ref Expression
1 shscl ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → A + ℋ B ∈ S ℋ
2 1 a1d ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → C ∈ A ∧ D ∈ B → A + ℋ B ∈ S ℋ
3 shsel1 ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → C ∈ A → C ∈ A + ℋ B
4 3 adantrd ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → C ∈ A ∧ D ∈ B → C ∈ A + ℋ B
5 shsel2 ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → D ∈ B → D ∈ A + ℋ B
6 5 adantld ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → C ∈ A ∧ D ∈ B → D ∈ A + ℋ B
7 2 4 6 3jcad ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → C ∈ A ∧ D ∈ B → A + ℋ B ∈ S ℋ ∧ C ∈ A + ℋ B ∧ D ∈ A + ℋ B
8 shsubcl ⊢ A + ℋ B ∈ S ℋ ∧ C ∈ A + ℋ B ∧ D ∈ A + ℋ B → C - ℎ D ∈ A + ℋ B
9 7 8 syl6 ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → C ∈ A ∧ D ∈ B → C - ℎ D ∈ A + ℋ B