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

Theorem shmulcl 27261
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 27252 . . . . 5 (𝐻S ↔ ((𝐻 ⊆ ℋ ∧ 0𝐻) ∧ (∀𝑥𝐻𝑦𝐻 (𝑥 + 𝑦) ∈ 𝐻 ∧ ∀𝑥 ∈ ℂ ∀𝑦𝐻 (𝑥 · 𝑦) ∈ 𝐻)))
21simprbi 478 . . . 4 (𝐻S → (∀𝑥𝐻𝑦𝐻 (𝑥 + 𝑦) ∈ 𝐻 ∧ ∀𝑥 ∈ ℂ ∀𝑦𝐻 (𝑥 · 𝑦) ∈ 𝐻))
32simprd 477 . . 3 (𝐻S → ∀𝑥 ∈ ℂ ∀𝑦𝐻 (𝑥 · 𝑦) ∈ 𝐻)
4 oveq1 6530 . . . . 5 (𝑥 = 𝐴 → (𝑥 · 𝑦) = (𝐴 · 𝑦))
54eleq1d 2667 . . . 4 (𝑥 = 𝐴 → ((𝑥 · 𝑦) ∈ 𝐻 ↔ (𝐴 · 𝑦) ∈ 𝐻))
6 oveq2 6531 . . . . 5 (𝑦 = 𝐵 → (𝐴 · 𝑦) = (𝐴 · 𝐵))
76eleq1d 2667 . . . 4 (𝑦 = 𝐵 → ((𝐴 · 𝑦) ∈ 𝐻 ↔ (𝐴 · 𝐵) ∈ 𝐻))
85, 7rspc2v 3288 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵𝐻) → (∀𝑥 ∈ ℂ ∀𝑦𝐻 (𝑥 · 𝑦) ∈ 𝐻 → (𝐴 · 𝐵) ∈ 𝐻))
93, 8syl5com 31 . 2 (𝐻S → ((𝐴 ∈ ℂ ∧ 𝐵𝐻) → (𝐴 · 𝐵) ∈ 𝐻))
1093impib 1253 1 ((𝐻S𝐴 ∈ ℂ ∧ 𝐵𝐻) → (𝐴 · 𝐵) ∈ 𝐻)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030   = wceq 1474  wcel 1975  wral 2891  wss 3535  (class class class)co 6523  cc 9786  chil 26962   + cva 26963   · csm 26964  0c0v 26967   S csh 26971
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pr 4824  ax-hilex 27042  ax-hfvadd 27043  ax-hfvmul 27048
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ral 2896  df-rex 2897  df-rab 2900  df-v 3170  df-sbc 3398  df-csb 3495  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-op 4127  df-uni 4363  df-iun 4447  df-br 4574  df-opab 4634  df-id 4939  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-fv 5794  df-ov 6526  df-sh 27250
This theorem is referenced by:  shsubcl  27263  norm1exi  27293  hhssabloilem  27304  hhssnv  27307  shsel3  27360  shscli  27362  shintcli  27374  pjhthlem1  27436  h1de2bi  27599  h1de2ctlem  27600  spansni  27602  spansnmul  27609  spansnss  27616  spanunsni  27624  h1datomi  27626  pjmulii  27722  mayete3i  27773  imaelshi  28103  strlem1  28295  cdj1i  28478  cdj3lem1  28479
  Copyright terms: Public domain W3C validator