Theorem shscl

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

	Ref	Expression
Assertion	shscl	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 +ℋ 𝐵 ) ∈ Sℋ )

Proof

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