HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  shmulcl Structured version   Visualization version   GIF version

Theorem shmulcl 28599
Description: Closure of vector scalar multiplication in a subspace of a Hilbert space. (Contributed by NM, 13-Sep-1999.) (New usage is discouraged.)
Assertion
Ref Expression
shmulcl ((𝐻S𝐴 ∈ ℂ ∧ 𝐵𝐻) → (𝐴 · 𝐵) ∈ 𝐻)

Proof of Theorem shmulcl
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 issh2 28590 . . . . 5 (𝐻S ↔ ((𝐻 ⊆ ℋ ∧ 0𝐻) ∧ (∀𝑥𝐻𝑦𝐻 (𝑥 + 𝑦) ∈ 𝐻 ∧ ∀𝑥 ∈ ℂ ∀𝑦𝐻 (𝑥 · 𝑦) ∈ 𝐻)))
21simprbi 491 . . . 4 (𝐻S → (∀𝑥𝐻𝑦𝐻 (𝑥 + 𝑦) ∈ 𝐻 ∧ ∀𝑥 ∈ ℂ ∀𝑦𝐻 (𝑥 · 𝑦) ∈ 𝐻))
32simprd 490 . . 3 (𝐻S → ∀𝑥 ∈ ℂ ∀𝑦𝐻 (𝑥 · 𝑦) ∈ 𝐻)
4 oveq1 6886 . . . . 5 (𝑥 = 𝐴 → (𝑥 · 𝑦) = (𝐴 · 𝑦))
54eleq1d 2864 . . . 4 (𝑥 = 𝐴 → ((𝑥 · 𝑦) ∈ 𝐻 ↔ (𝐴 · 𝑦) ∈ 𝐻))
6 oveq2 6887 . . . . 5 (𝑦 = 𝐵 → (𝐴 · 𝑦) = (𝐴 · 𝐵))
76eleq1d 2864 . . . 4 (𝑦 = 𝐵 → ((𝐴 · 𝑦) ∈ 𝐻 ↔ (𝐴 · 𝐵) ∈ 𝐻))
85, 7rspc2v 3511 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵𝐻) → (∀𝑥 ∈ ℂ ∀𝑦𝐻 (𝑥 · 𝑦) ∈ 𝐻 → (𝐴 · 𝐵) ∈ 𝐻))
93, 8syl5com 31 . 2 (𝐻S → ((𝐴 ∈ ℂ ∧ 𝐵𝐻) → (𝐴 · 𝐵) ∈ 𝐻))
1093impib 1145 1 ((𝐻S𝐴 ∈ ℂ ∧ 𝐵𝐻) → (𝐴 · 𝐵) ∈ 𝐻)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  w3a 1108   = wceq 1653  wcel 2157  wral 3090  wss 3770  (class class class)co 6879  cc 10223  chba 28300   + cva 28301   · csm 28302  0c0v 28305   S csh 28309
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2378  ax-ext 2778  ax-sep 4976  ax-nul 4984  ax-pr 5098  ax-hilex 28380  ax-hfvadd 28381  ax-hfvmul 28386
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2592  df-eu 2610  df-clab 2787  df-cleq 2793  df-clel 2796  df-nfc 2931  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3388  df-sbc 3635  df-csb 3730  df-dif 3773  df-un 3775  df-in 3777  df-ss 3784  df-nul 4117  df-if 4279  df-pw 4352  df-sn 4370  df-pr 4372  df-op 4376  df-uni 4630  df-iun 4713  df-br 4845  df-opab 4907  df-id 5221  df-xp 5319  df-rel 5320  df-cnv 5321  df-co 5322  df-dm 5323  df-rn 5324  df-res 5325  df-ima 5326  df-iota 6065  df-fun 6104  df-fn 6105  df-f 6106  df-fv 6110  df-ov 6882  df-sh 28588
This theorem is referenced by:  shsubcl  28601  norm1exi  28631  hhssabloilem  28642  hhssnv  28645  shsel3  28698  shscli  28700  shintcli  28712  pjhthlem1  28774  h1de2bi  28937  h1de2ctlem  28938  spansni  28940  spansnmul  28947  spansnss  28954  spanunsni  28962  h1datomi  28964  pjmulii  29060  mayete3i  29111  imaelshi  29441  strlem1  29633  cdj1i  29816  cdj3lem1  29817
  Copyright terms: Public domain W3C validator