Theorem shaddcl

Description: Closure of vector addition in a subspace of a Hilbert space. (Contributed by NM, 13-Sep-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	shaddcl	$$⊢\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		issh2	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}\leftrightarrow \left(\left(H\subseteq \mathscr{H}\wedge 0_{ℎ}\in H\right)\wedge \left(\forall x\in H\forall y\in Hx{+}_{ℎ}y\in H\wedge \forall x\in ℂ\forall y\in Hx{\cdot }_{ℎ}y\in H\right)\right)$$
2	1	simprbi	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}\to \left(\forall x\in H\forall y\in Hx{+}_{ℎ}y\in H\wedge \forall x\in ℂ\forall y\in Hx{\cdot }_{ℎ}y\in H\right)$$
3	2	simpld	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}\to \forall x\in H\forall y\in Hx{+}_{ℎ}y\in H$$
4		oveq1	$$⊢x=A\to x{+}_{ℎ}y=A{+}_{ℎ}y$$
5	4	eleq1d	$$⊢x=A\to \left(x{+}_{ℎ}y\in H\leftrightarrow A{+}_{ℎ}y\in H\right)$$
6		oveq2	$$⊢y=B\to A{+}_{ℎ}y=A{+}_{ℎ}B$$
7	6	eleq1d	$$⊢y=B\to \left(A{+}_{ℎ}y\in H\leftrightarrow A{+}_{ℎ}B\in H\right)$$
8	5 7	rspc2v	$$⊢\left(A\in H\wedge B\in H\right)\to \left(\forall x\in H\forall y\in Hx{+}_{ℎ}y\in H\to A{+}_{ℎ}B\in H\right)$$
9	3 8	syl5com	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}\to \left(\left(A\in H\wedge B\in H\right)\to A{+}_{ℎ}B\in H\right)$$
10	9	3impib	$$⊢\left(H\in {\mathbf{S}}_{\mathscr{H}}\wedge A\in H\wedge B\in H\right)\to A{+}_{ℎ}B\in H$$