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	⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝐻 ) → ( 𝐴 ·ℎ 𝐵 ) ∈ 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		issh2	⊢ ( 𝐻 ∈ Sℋ ↔ ( ( 𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻 ) ∧ ( ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 +ℎ 𝑦 ) ∈ 𝐻 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ℎ 𝑦 ) ∈ 𝐻 ) ) )
2	1	simprbi	⊢ ( 𝐻 ∈ Sℋ → ( ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 +ℎ 𝑦 ) ∈ 𝐻 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ℎ 𝑦 ) ∈ 𝐻 ) )
3	2	simprd	⊢ ( 𝐻 ∈ Sℋ → ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ℎ 𝑦 ) ∈ 𝐻 )
4		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ·ℎ 𝑦 ) = ( 𝐴 ·ℎ 𝑦 ) )
5	4	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ·ℎ 𝑦 ) ∈ 𝐻 ↔ ( 𝐴 ·ℎ 𝑦 ) ∈ 𝐻 ) )
6		oveq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 ·ℎ 𝑦 ) = ( 𝐴 ·ℎ 𝐵 ) )
7	6	eleq1d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ·ℎ 𝑦 ) ∈ 𝐻 ↔ ( 𝐴 ·ℎ 𝐵 ) ∈ 𝐻 ) )
8	5 7	rspc2v	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝐻 ) → ( ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ℎ 𝑦 ) ∈ 𝐻 → ( 𝐴 ·ℎ 𝐵 ) ∈ 𝐻 ) )
9	3 8	syl5com	⊢ ( 𝐻 ∈ Sℋ → ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝐻 ) → ( 𝐴 ·ℎ 𝐵 ) ∈ 𝐻 ) )
10	9	3impib	⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝐻 ) → ( 𝐴 ·ℎ 𝐵 ) ∈ 𝐻 )