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}}_{\mathscr{H}}\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}}_{\mathscr{H}}\to H\subseteq \mathscr{H}$$
2	1	sseld	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}\to \left(A\in H\to A\in \mathscr{H}\right)$$
3	1	sseld	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}\to \left(B\in H\to B\in \mathscr{H}\right)$$
4	2 3	anim12d	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}\to \left(\left(A\in H\wedge B\in H\right)\to \left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\right)$$
5	4	3impib	$$⊢\left(H\in {\mathbf{S}}_{\mathscr{H}}\wedge A\in H\wedge B\in H\right)\to \left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)$$
6		hvsubval	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to A{-}_{ℎ}B=A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)$$
7	5 6	syl	$$⊢\left(H\in {\mathbf{S}}_{\mathscr{H}}\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}}_{\mathscr{H}}\wedge -1\in ℂ\wedge B\in H\right)\to -1{\cdot }_{ℎ}B\in H$$
10	8 9	mp3an2	$$⊢\left(H\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in H\right)\to -1{\cdot }_{ℎ}B\in H$$
11	10	3adant2	$$⊢\left(H\in {\mathbf{S}}_{\mathscr{H}}\wedge A\in H\wedge B\in H\right)\to -1{\cdot }_{ℎ}B\in H$$
12		shaddcl	$$⊢\left(H\in {\mathbf{S}}_{\mathscr{H}}\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}}_{\mathscr{H}}\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}}_{\mathscr{H}}\wedge A\in H\wedge B\in H\right)\to A{-}_{ℎ}B\in H$$