# Metamath Proof Explorer

## Theorem shscl

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

Ref Expression
Assertion shscl ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\right)\to {A}{+}_{ℋ}{B}\in {\mathbf{S}}_{ℋ}$

### Proof

Step Hyp Ref Expression
1 oveq1 ${⊢}{A}=if\left({A}\in {\mathbf{S}}_{ℋ},{A},ℋ\right)\to {A}{+}_{ℋ}{B}=if\left({A}\in {\mathbf{S}}_{ℋ},{A},ℋ\right){+}_{ℋ}{B}$
2 1 eleq1d ${⊢}{A}=if\left({A}\in {\mathbf{S}}_{ℋ},{A},ℋ\right)\to \left({A}{+}_{ℋ}{B}\in {\mathbf{S}}_{ℋ}↔if\left({A}\in {\mathbf{S}}_{ℋ},{A},ℋ\right){+}_{ℋ}{B}\in {\mathbf{S}}_{ℋ}\right)$
3 oveq2 ${⊢}{B}=if\left({B}\in {\mathbf{S}}_{ℋ},{B},ℋ\right)\to if\left({A}\in {\mathbf{S}}_{ℋ},{A},ℋ\right){+}_{ℋ}{B}=if\left({A}\in {\mathbf{S}}_{ℋ},{A},ℋ\right){+}_{ℋ}if\left({B}\in {\mathbf{S}}_{ℋ},{B},ℋ\right)$
4 3 eleq1d ${⊢}{B}=if\left({B}\in {\mathbf{S}}_{ℋ},{B},ℋ\right)\to \left(if\left({A}\in {\mathbf{S}}_{ℋ},{A},ℋ\right){+}_{ℋ}{B}\in {\mathbf{S}}_{ℋ}↔if\left({A}\in {\mathbf{S}}_{ℋ},{A},ℋ\right){+}_{ℋ}if\left({B}\in {\mathbf{S}}_{ℋ},{B},ℋ\right)\in {\mathbf{S}}_{ℋ}\right)$
5 helsh ${⊢}ℋ\in {\mathbf{S}}_{ℋ}$
6 5 elimel ${⊢}if\left({A}\in {\mathbf{S}}_{ℋ},{A},ℋ\right)\in {\mathbf{S}}_{ℋ}$
7 5 elimel ${⊢}if\left({B}\in {\mathbf{S}}_{ℋ},{B},ℋ\right)\in {\mathbf{S}}_{ℋ}$
8 6 7 shscli ${⊢}if\left({A}\in {\mathbf{S}}_{ℋ},{A},ℋ\right){+}_{ℋ}if\left({B}\in {\mathbf{S}}_{ℋ},{B},ℋ\right)\in {\mathbf{S}}_{ℋ}$
9 2 4 8 dedth2h ${⊢}\left({A}\in {\mathbf{S}}_{ℋ}\wedge {B}\in {\mathbf{S}}_{ℋ}\right)\to {A}{+}_{ℋ}{B}\in {\mathbf{S}}_{ℋ}$