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 ${⊢}\left({H}\in {\mathbf{S}}_{ℋ}\wedge {A}\in ℂ\wedge {B}\in {H}\right)\to {A}{\cdot }_{ℎ}{B}\in {H}$

Proof

Step Hyp Ref Expression
1 issh2 ${⊢}{H}\in {\mathbf{S}}_{ℋ}↔\left(\left({H}\subseteq ℋ\wedge {0}_{ℎ}\in {H}\right)\wedge \left(\forall {x}\in {H}\phantom{\rule{.4em}{0ex}}\forall {y}\in {H}\phantom{\rule{.4em}{0ex}}{x}{+}_{ℎ}{y}\in {H}\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {H}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{ℎ}{y}\in {H}\right)\right)$
2 1 simprbi ${⊢}{H}\in {\mathbf{S}}_{ℋ}\to \left(\forall {x}\in {H}\phantom{\rule{.4em}{0ex}}\forall {y}\in {H}\phantom{\rule{.4em}{0ex}}{x}{+}_{ℎ}{y}\in {H}\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {H}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{ℎ}{y}\in {H}\right)$
3 2 simprd ${⊢}{H}\in {\mathbf{S}}_{ℋ}\to \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {H}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{ℎ}{y}\in {H}$
4 oveq1 ${⊢}{x}={A}\to {x}{\cdot }_{ℎ}{y}={A}{\cdot }_{ℎ}{y}$
5 4 eleq1d ${⊢}{x}={A}\to \left({x}{\cdot }_{ℎ}{y}\in {H}↔{A}{\cdot }_{ℎ}{y}\in {H}\right)$
6 oveq2 ${⊢}{y}={B}\to {A}{\cdot }_{ℎ}{y}={A}{\cdot }_{ℎ}{B}$
7 6 eleq1d ${⊢}{y}={B}\to \left({A}{\cdot }_{ℎ}{y}\in {H}↔{A}{\cdot }_{ℎ}{B}\in {H}\right)$
8 5 7 rspc2v ${⊢}\left({A}\in ℂ\wedge {B}\in {H}\right)\to \left(\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {H}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{ℎ}{y}\in {H}\to {A}{\cdot }_{ℎ}{B}\in {H}\right)$
9 3 8 syl5com ${⊢}{H}\in {\mathbf{S}}_{ℋ}\to \left(\left({A}\in ℂ\wedge {B}\in {H}\right)\to {A}{\cdot }_{ℎ}{B}\in {H}\right)$
10 9 3impib ${⊢}\left({H}\in {\mathbf{S}}_{ℋ}\wedge {A}\in ℂ\wedge {B}\in {H}\right)\to {A}{\cdot }_{ℎ}{B}\in {H}$