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

Theorem shmulcl 26004
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  |-  ( ( H  e.  SH  /\  A  e.  CC  /\  B  e.  H )  ->  ( A  .h  B )  e.  H )

Proof of Theorem shmulcl
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 issh2 25995 . . . . 5  |-  ( H  e.  SH  <->  ( ( H  C_  ~H  /\  0h  e.  H )  /\  ( A. x  e.  H  A. y  e.  H  ( x  +h  y
)  e.  H  /\  A. x  e.  CC  A. y  e.  H  (
x  .h  y )  e.  H ) ) )
21simprbi 464 . . . 4  |-  ( H  e.  SH  ->  ( A. x  e.  H  A. y  e.  H  ( x  +h  y
)  e.  H  /\  A. x  e.  CC  A. y  e.  H  (
x  .h  y )  e.  H ) )
32simprd 463 . . 3  |-  ( H  e.  SH  ->  A. x  e.  CC  A. y  e.  H  ( x  .h  y )  e.  H
)
4 oveq1 6285 . . . . 5  |-  ( x  =  A  ->  (
x  .h  y )  =  ( A  .h  y ) )
54eleq1d 2510 . . . 4  |-  ( x  =  A  ->  (
( x  .h  y
)  e.  H  <->  ( A  .h  y )  e.  H
) )
6 oveq2 6286 . . . . 5  |-  ( y  =  B  ->  ( A  .h  y )  =  ( A  .h  B ) )
76eleq1d 2510 . . . 4  |-  ( y  =  B  ->  (
( A  .h  y
)  e.  H  <->  ( A  .h  B )  e.  H
) )
85, 7rspc2v 3203 . . 3  |-  ( ( A  e.  CC  /\  B  e.  H )  ->  ( A. x  e.  CC  A. y  e.  H  ( x  .h  y )  e.  H  ->  ( A  .h  B
)  e.  H ) )
93, 8syl5com 30 . 2  |-  ( H  e.  SH  ->  (
( A  e.  CC  /\  B  e.  H )  ->  ( A  .h  B )  e.  H
) )
1093impib 1193 1  |-  ( ( H  e.  SH  /\  A  e.  CC  /\  B  e.  H )  ->  ( A  .h  B )  e.  H )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 972    = wceq 1381    e. wcel 1802   A.wral 2791    C_ wss 3459  (class class class)co 6278   CCcc 9490   ~Hchil 25705    +h cva 25706    .h csm 25707   0hc0v 25710   SHcsh 25714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4555  ax-nul 4563  ax-pr 4673  ax-hilex 25785  ax-hfvadd 25786  ax-hfvmul 25791
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3419  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-nul 3769  df-if 3924  df-pw 3996  df-sn 4012  df-pr 4014  df-op 4018  df-uni 4232  df-iun 4314  df-br 4435  df-opab 4493  df-id 4782  df-xp 4992  df-rel 4993  df-cnv 4994  df-co 4995  df-dm 4996  df-rn 4997  df-res 4998  df-ima 4999  df-iota 5538  df-fun 5577  df-fn 5578  df-f 5579  df-fv 5583  df-ov 6281  df-sh 25993
This theorem is referenced by:  shsubcl  26007  norm1exi  26037  hhssabloi  26047  hhssnv  26049  shsel3  26102  shscli  26104  shintcli  26116  pjhthlem1  26178  h1de2bi  26341  h1de2ctlem  26342  spansni  26344  spansnmul  26351  spansnss  26358  spanunsni  26366  h1datomi  26368  pjmulii  26464  mayete3i  26515  imaelshi  26846  strlem1  27038  cdj1i  27221  cdj3lem1  27222
  Copyright terms: Public domain W3C validator