Metamath Proof Explorer

Theorem shsubcl

Description: Closure of vector subtraction in a subspace of a Hilbert space. (Contributed by NM, 18-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion shsubcl ⊢ H ∈ S ℋ ∧ A ∈ H ∧ B ∈ H → A - ℎ B ∈ H

Proof

Step Hyp Ref Expression
1 shss ⊢ H ∈ S ℋ → H ⊆ ℋ
2 1 sseld ⊢ H ∈ S ℋ → A ∈ H → A ∈ ℋ
3 1 sseld ⊢ H ∈ S ℋ → B ∈ H → B ∈ ℋ
4 2 3 anim12d ⊢ H ∈ S ℋ → A ∈ H ∧ B ∈ H → A ∈ ℋ ∧ B ∈ ℋ
5 4 3impib ⊢ H ∈ S ℋ ∧ A ∈ H ∧ B ∈ H → A ∈ ℋ ∧ B ∈ ℋ
6 hvsubval ⊢ A ∈ ℋ ∧ B ∈ ℋ → A - ℎ B = A + ℎ -1 ⋅ ℎ B
7 5 6 syl ⊢ H ∈ S ℋ ∧ A ∈ H ∧ B ∈ H → A - ℎ B = A + ℎ -1 ⋅ ℎ B
8 neg1cn ⊢ − 1 ∈ ℂ
9 shmulcl ⊢ H ∈ S ℋ ∧ − 1 ∈ ℂ ∧ B ∈ H → -1 ⋅ ℎ B ∈ H
10 8 9 mp3an2 ⊢ H ∈ S ℋ ∧ B ∈ H → -1 ⋅ ℎ B ∈ H
11 10 3adant2 ⊢ H ∈ S ℋ ∧ A ∈ H ∧ B ∈ H → -1 ⋅ ℎ B ∈ H
12 shaddcl ⊢ H ∈ S ℋ ∧ A ∈ H ∧ -1 ⋅ ℎ B ∈ H → A + ℎ -1 ⋅ ℎ B ∈ H
13 11 12 syld3an3 ⊢ H ∈ S ℋ ∧ A ∈ H ∧ B ∈ H → A + ℎ -1 ⋅ ℎ B ∈ H
14 7 13 eqeltrd ⊢ H ∈ S ℋ ∧ A ∈ H ∧ B ∈ H → A - ℎ B ∈ H