Description: Functionality of th scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | vciOLD.1 | |- G = ( 1st ` W ) |
|
| vciOLD.2 | |- S = ( 2nd ` W ) |
||
| vciOLD.3 | |- X = ran G |
||
| Assertion | vcsm | |- ( W e. CVecOLD -> S : ( CC X. X ) --> X ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vciOLD.1 | |- G = ( 1st ` W ) |
|
| 2 | vciOLD.2 | |- S = ( 2nd ` W ) |
|
| 3 | vciOLD.3 | |- X = ran G |
|
| 4 | 1 2 3 | vciOLD | |- ( W e. CVecOLD -> ( G e. AbelOp /\ S : ( CC X. X ) --> X /\ A. x e. X ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) ) ) |
| 5 | 4 | simp2d | |- ( W e. CVecOLD -> S : ( CC X. X ) --> X ) |