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

Metamath Proof Explorer

Theorem shscl

Description: Closure of subspace sum. (Contributed by NM, 15-Dec-2004) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ A = if A ∈ S ℋ A ℋ → A + ℋ B = if A ∈ S ℋ A ℋ + ℋ B
2 1 eleq1d ⊢ A = if A ∈ S ℋ A ℋ → A + ℋ B ∈ S ℋ ↔ if A ∈ S ℋ A ℋ + ℋ B ∈ S ℋ
3 oveq2 ⊢ B = if B ∈ S ℋ B ℋ → if A ∈ S ℋ A ℋ + ℋ B = if A ∈ S ℋ A ℋ + ℋ if B ∈ S ℋ B ℋ
4 3 eleq1d ⊢ B = if B ∈ S ℋ B ℋ → if A ∈ S ℋ A ℋ + ℋ B ∈ S ℋ ↔ if A ∈ S ℋ A ℋ + ℋ if B ∈ S ℋ B ℋ ∈ S ℋ
5 helsh ⊢ ℋ ∈ S ℋ
6 5 elimel ⊢ if A ∈ S ℋ A ℋ ∈ S ℋ
7 5 elimel ⊢ if B ∈ S ℋ B ℋ ∈ S ℋ
8 6 7 shscli ⊢ if A ∈ S ℋ A ℋ + ℋ if B ∈ S ℋ B ℋ ∈ S ℋ
9 2 4 8 dedth2h ⊢ A ∈ S ℋ ∧ B ∈ S ℋ → A + ℋ B ∈ S ℋ