This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem shsub2

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

Ref Expression
Assertion shsub2 ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → A ⊆ B + ℋ A

Proof

Step Hyp Ref Expression
1 shsub1 ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → A ⊆ A + ℋ B
2 shscom ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → A + ℋ B = B + ℋ A
3 1 2 sseqtrd ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → A ⊆ B + ℋ A