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

Theorem shmulcl 26857
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 26848 . . . . 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 465 . . . 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 464 . . 3  |-  ( H  e.  SH  ->  A. x  e.  CC  A. y  e.  H  ( x  .h  y )  e.  H
)
4 oveq1 6309 . . . . 5  |-  ( x  =  A  ->  (
x  .h  y )  =  ( A  .h  y ) )
54eleq1d 2491 . . . 4  |-  ( x  =  A  ->  (
( x  .h  y
)  e.  H  <->  ( A  .h  y )  e.  H
) )
6 oveq2 6310 . . . . 5  |-  ( y  =  B  ->  ( A  .h  y )  =  ( A  .h  B ) )
76eleq1d 2491 . . . 4  |-  ( y  =  B  ->  (
( A  .h  y
)  e.  H  <->  ( A  .h  B )  e.  H
) )
85, 7rspc2v 3191 . . 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 31 . 2  |-  ( H  e.  SH  ->  (
( A  e.  CC  /\  B  e.  H )  ->  ( A  .h  B )  e.  H
) )
1093impib 1203 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 370    /\ w3a 982    = wceq 1437    e. wcel 1868   A.wral 2775    C_ wss 3436  (class class class)co 6302   CCcc 9538   ~Hchil 26558    +h cva 26559    .h csm 26560   0hc0v 26563   SHcsh 26567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pr 4657  ax-hilex 26638  ax-hfvadd 26639  ax-hfvmul 26644
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-id 4765  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-fv 5606  df-ov 6305  df-sh 26846
This theorem is referenced by:  shsubcl  26859  norm1exi  26889  hhssabloi  26899  hhssnv  26901  shsel3  26954  shscli  26956  shintcli  26968  pjhthlem1  27030  h1de2bi  27193  h1de2ctlem  27194  spansni  27196  spansnmul  27203  spansnss  27210  spanunsni  27218  h1datomi  27220  pjmulii  27316  mayete3i  27367  imaelshi  27697  strlem1  27889  cdj1i  28072  cdj3lem1  28073
  Copyright terms: Public domain W3C validator