Metamath Proof Explorer

Theorem shless

Description: Subset implies subset of subspace sum. (Contributed by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ssrexv ⊢ A ⊆ B → ∃ y ∈ A ∃ z ∈ C x = y + ℎ z → ∃ y ∈ B ∃ z ∈ C x = y + ℎ z
2 1 adantl ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → ∃ y ∈ A ∃ z ∈ C x = y + ℎ z → ∃ y ∈ B ∃ z ∈ C x = y + ℎ z
3 simpl1 ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → A ∈ S ℋ
4 simpl3 ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → C ∈ S ℋ
5 shsel ⊢ A ∈ S ℋ ∧ C ∈ S ℋ → x ∈ A + ℋ C ↔ ∃ y ∈ A ∃ z ∈ C x = y + ℎ z
6 3 4 5 syl2anc ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → x ∈ A + ℋ C ↔ ∃ y ∈ A ∃ z ∈ C x = y + ℎ z
7 simpl2 ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → B ∈ S ℋ
8 shsel ⊢ B ∈ S ℋ ∧ C ∈ S ℋ → x ∈ B + ℋ C ↔ ∃ y ∈ B ∃ z ∈ C x = y + ℎ z
9 7 4 8 syl2anc ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → x ∈ B + ℋ C ↔ ∃ y ∈ B ∃ z ∈ C x = y + ℎ z
10 2 6 9 3imtr4d ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → x ∈ A + ℋ C → x ∈ B + ℋ C
11 10 ssrdv ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ S ℋ ∧ A ⊆ B → A + ℋ C ⊆ B + ℋ C