# 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 ${⊢}\left({H}\in {\mathbf{S}}_{ℋ}\wedge {A}\in {H}\wedge {B}\in {H}\right)\to {A}{-}_{ℎ}{B}\in {H}$

### Proof

Step Hyp Ref Expression
1 shss ${⊢}{H}\in {\mathbf{S}}_{ℋ}\to {H}\subseteq ℋ$
2 1 sseld ${⊢}{H}\in {\mathbf{S}}_{ℋ}\to \left({A}\in {H}\to {A}\in ℋ\right)$
3 1 sseld ${⊢}{H}\in {\mathbf{S}}_{ℋ}\to \left({B}\in {H}\to {B}\in ℋ\right)$
4 2 3 anim12d ${⊢}{H}\in {\mathbf{S}}_{ℋ}\to \left(\left({A}\in {H}\wedge {B}\in {H}\right)\to \left({A}\in ℋ\wedge {B}\in ℋ\right)\right)$
5 4 3impib ${⊢}\left({H}\in {\mathbf{S}}_{ℋ}\wedge {A}\in {H}\wedge {B}\in {H}\right)\to \left({A}\in ℋ\wedge {B}\in ℋ\right)$
6 hvsubval ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {A}{-}_{ℎ}{B}={A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)$
7 5 6 syl ${⊢}\left({H}\in {\mathbf{S}}_{ℋ}\wedge {A}\in {H}\wedge {B}\in {H}\right)\to {A}{-}_{ℎ}{B}={A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)$
8 neg1cn ${⊢}-1\in ℂ$
9 shmulcl ${⊢}\left({H}\in {\mathbf{S}}_{ℋ}\wedge -1\in ℂ\wedge {B}\in {H}\right)\to -1{\cdot }_{ℎ}{B}\in {H}$
10 8 9 mp3an2 ${⊢}\left({H}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {H}\right)\to -1{\cdot }_{ℎ}{B}\in {H}$
11 10 3adant2 ${⊢}\left({H}\in {\mathbf{S}}_{ℋ}\wedge {A}\in {H}\wedge {B}\in {H}\right)\to -1{\cdot }_{ℎ}{B}\in {H}$
12 shaddcl ${⊢}\left({H}\in {\mathbf{S}}_{ℋ}\wedge {A}\in {H}\wedge -1{\cdot }_{ℎ}{B}\in {H}\right)\to {A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)\in {H}$
13 11 12 syld3an3 ${⊢}\left({H}\in {\mathbf{S}}_{ℋ}\wedge {A}\in {H}\wedge {B}\in {H}\right)\to {A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)\in {H}$
14 7 13 eqeltrd ${⊢}\left({H}\in {\mathbf{S}}_{ℋ}\wedge {A}\in {H}\wedge {B}\in {H}\right)\to {A}{-}_{ℎ}{B}\in {H}$