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	|- ( ( A e. SH /\ B e. SH ) -> ( A +H B ) C_ ~H )

Proof

Step	Hyp	Ref	Expression
1		shsval	|- ( ( A e. SH /\ B e. SH ) -> ( A +H B ) = ( +h " ( A X. B ) ) )
2		imassrn	|- ( +h " ( A X. B ) ) C_ ran +h
3		ax-hfvadd	|- +h : ( ~H X. ~H ) --> ~H
4		frn	|- ( +h : ( ~H X. ~H ) --> ~H -> ran +h C_ ~H )
5	3 4	ax-mp	|- ran +h C_ ~H
6	2 5	sstri	|- ( +h " ( A X. B ) ) C_ ~H
7	1 6	eqsstrdi	|- ( ( A e. SH /\ B e. SH ) -> ( A +H B ) C_ ~H )