Theorem shsub1

Description: Subspace sum is an upper bound of its arguments. (Contributed by NM, 14-Dec-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	shsub1	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → 𝐴 ⊆ ( 𝐴 +ℋ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		shsel1	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ) )
2	1	ssrdv	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → 𝐴 ⊆ ( 𝐴 +ℋ 𝐵 ) )