This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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