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

Definition df-shs 26091
Description: Define subspace sum in  SH. See shsval 26095, shsval2i 26170, and shsval3i 26171 for its value. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.)
Assertion
Ref Expression
df-shs  |-  +H  =  ( x  e.  SH ,  y  e.  SH  |->  (  +h  " ( x  X.  y ) ) )
Distinct variable group:    x, y

Detailed syntax breakdown of Definition df-shs
StepHypRef Expression
1 cph 25713 . 2  class  +H
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 csh 25710 . . 3  class  SH
5 cva 25702 . . . 4  class  +h
62cv 1380 . . . . 5  class  x
73cv 1380 . . . . 5  class  y
86, 7cxp 4983 . . . 4  class  ( x  X.  y )
95, 8cima 4988 . . 3  class  (  +h  " ( x  X.  y ) )
102, 3, 4, 4, 9cmpt2 6279 . 2  class  ( x  e.  SH ,  y  e.  SH  |->  (  +h  " ( x  X.  y ) ) )
111, 10wceq 1381 1  wff  +H  =  ( x  e.  SH ,  y  e.  SH  |->  (  +h  " ( x  X.  y ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  shsval  26095
  Copyright terms: Public domain W3C validator