Metamath Proof Explorer

Theorem shmulcl

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

Ref Expression
Assertion shmulcl ⊢ H ∈ S ℋ ∧ A ∈ ℂ ∧ 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 simprd ⊢ H ∈ S ℋ → ∀ x ∈ ℂ ∀ 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 ∈ ℂ ∧ B ∈ H → ∀ x ∈ ℂ ∀ y ∈ H x ⋅ ℎ y ∈ H → A ⋅ ℎ B ∈ H
9 3 8 syl5com ⊢ H ∈ S ℋ → A ∈ ℂ ∧ B ∈ H → A ⋅ ℎ B ∈ H
10 9 3impib ⊢ H ∈ S ℋ ∧ A ∈ ℂ ∧ B ∈ H → A ⋅ ℎ B ∈ H