Theorem shsss

Description: The subspace sum is a subset of Hilbert space. (Contributed by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	shsss	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to A{+}_{\mathscr{H}}B\subseteq \mathscr{H}$$

Proof

Step	Hyp	Ref	Expression
1		shsval	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to A{+}_{\mathscr{H}}B={+}_{ℎ}\left[A\times B\right]$$
2		imassrn	$$⊢{+}_{ℎ}\left[A\times B\right]\subseteq \mathrm{ran}{+}_{ℎ}$$
3		ax-hfvadd	$$⊢{+}_{ℎ}:\mathscr{H}\times \mathscr{H}⟶\mathscr{H}$$
4		frn	$$⊢{+}_{ℎ}:\mathscr{H}\times \mathscr{H}⟶\mathscr{H}\to \mathrm{ran}{+}_{ℎ}\subseteq \mathscr{H}$$
5	3 4	ax-mp	$$⊢\mathrm{ran}{+}_{ℎ}\subseteq \mathscr{H}$$
6	2 5	sstri	$$⊢{+}_{ℎ}\left[A\times B\right]\subseteq \mathscr{H}$$
7	1 6	eqsstrdi	$$⊢\left(A\in {\mathbf{S}}_{\mathscr{H}}\wedge B\in {\mathbf{S}}_{\mathscr{H}}\right)\to A{+}_{\mathscr{H}}B\subseteq \mathscr{H}$$