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	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 +ℋ 𝐵 ) ⊆ ℋ )

Proof

Step	Hyp	Ref	Expression
1		shsval	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 +ℋ 𝐵 ) = ( +ℎ “ ( 𝐴 × 𝐵 ) ) )
2		imassrn	⊢ ( +ℎ “ ( 𝐴 × 𝐵 ) ) ⊆ ran +ℎ
3		ax-hfvadd	⊢ +ℎ : ( ℋ × ℋ ) ⟶ ℋ
4		frn	⊢ ( +ℎ : ( ℋ × ℋ ) ⟶ ℋ → ran +ℎ ⊆ ℋ )
5	3 4	ax-mp	⊢ ran +ℎ ⊆ ℋ
6	2 5	sstri	⊢ ( +ℎ “ ( 𝐴 × 𝐵 ) ) ⊆ ℋ
7	1 6	eqsstrdi	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 +ℋ 𝐵 ) ⊆ ℋ )