Metamath Proof Explorer

Theorem shaddcl

Description: Closure of vector addition in a subspace of a Hilbert space. (Contributed by NM, 13-Sep-1999) (New usage is discouraged.)

Ref Expression
Assertion shaddcl ⊢ H ∈ S ℋ ∧ A ∈ H ∧ B ∈ H → A + ℎ B ∈ H

Proof

Step Hyp Ref Expression
1 issh2 ⊢ H ∈ S ℋ ↔ H ⊆ ℋ ∧ 0 ℎ ∈ H ∧ ∀ x ∈ H ∀ y ∈ H x + ℎ y ∈ H ∧ ∀ x ∈ ℂ ∀ y ∈ H x ⋅ ℎ y ∈ H
2 1 simprbi ⊢ H ∈ S ℋ → ∀ x ∈ H ∀ y ∈ H x + ℎ y ∈ H ∧ ∀ x ∈ ℂ ∀ y ∈ H x ⋅ ℎ y ∈ H
3 2 simpld ⊢ H ∈ S ℋ → ∀ x ∈ H ∀ y ∈ H x + ℎ y ∈ H
4 oveq1 ⊢ x = A → x + ℎ y = A + ℎ y
5 4 eleq1d ⊢ x = A → x + ℎ y ∈ H ↔ A + ℎ y ∈ H
6 oveq2 ⊢ y = B → A + ℎ y = A + ℎ B
7 6 eleq1d ⊢ y = B → A + ℎ y ∈ H ↔ A + ℎ B ∈ H
8 5 7 rspc2v ⊢ A ∈ H ∧ B ∈ H → ∀ x ∈ H ∀ y ∈ H x + ℎ y ∈ H → A + ℎ B ∈ H
9 3 8 syl5com ⊢ H ∈ S ℋ → A ∈ H ∧ B ∈ H → A + ℎ B ∈ H
10 9 3impib ⊢ H ∈ S ℋ ∧ A ∈ H ∧ B ∈ H → A + ℎ B ∈ H