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

Metamath Proof Explorer

Theorem shsel1

Description: A subspace sum contains a member of one of its subspaces. (Contributed by NM, 15-Dec-2004) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 shel ⊢ A ∈ S ℋ ∧ C ∈ A → C ∈ ℋ
2 ax-hvaddid ⊢ C ∈ ℋ → C + ℎ 0 ℎ = C
3 1 2 syl ⊢ A ∈ S ℋ ∧ C ∈ A → C + ℎ 0 ℎ = C
4 3 adantlr ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ A → C + ℎ 0 ℎ = C
5 sh0 ⊢ B ∈ S ℋ → 0 ℎ ∈ B
6 5 adantl ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → 0 ℎ ∈ B
7 shsva ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → C ∈ A ∧ 0 ℎ ∈ B → C + ℎ 0 ℎ ∈ A + ℋ B
8 6 7 mpan2d ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → C ∈ A → C + ℎ 0 ℎ ∈ A + ℋ B
9 8 imp ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ A → C + ℎ 0 ℎ ∈ A + ℋ B
10 4 9 eqeltrrd ⊢ A ∈ S ℋ ∧ B ∈ S ℋ ∧ C ∈ A → C ∈ A + ℋ B
11 10 ex ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → C ∈ A → C ∈ A + ℋ B