This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cncvcOLD

Description: Obsolete version of cncvs . The set of complex numbers is a complex vector space. The vector operation is + , and the scalar product is x. . (Contributed by NM, 5-Nov-2006) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion cncvcOLD 
|- <. + , x. >. e. CVecOLD

Proof

Step Hyp Ref Expression
1 cnaddabloOLD 
 |-  + e. AbelOp
2 ax-addf 
 |-  + : ( CC X. CC ) --> CC
3 2 fdmi 
 |-  dom + = ( CC X. CC )
4 ax-mulf 
 |-  x. : ( CC X. CC ) --> CC
5 mullid 
 |-  ( x e. CC -> ( 1 x. x ) = x )
6 adddi 
 |-  ( ( y e. CC /\ x e. CC /\ z e. CC ) -> ( y x. ( x + z ) ) = ( ( y x. x ) + ( y x. z ) ) )
7 adddir 
 |-  ( ( y e. CC /\ z e. CC /\ x e. CC ) -> ( ( y + z ) x. x ) = ( ( y x. x ) + ( z x. x ) ) )
8 mulass 
 |-  ( ( y e. CC /\ z e. CC /\ x e. CC ) -> ( ( y x. z ) x. x ) = ( y x. ( z x. x ) ) )
9 eqid 
 |-  <. + , x. >. = <. + , x. >.
10 1 3 4 5 6 7 8 9 isvciOLD 
 |-  <. + , x. >. e. CVecOLD