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

Metamath Proof Explorer

Theorem cnnvs

Description: The scalar product operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypothesis cnnvs.6 
|- U = <. <. + , x. >. , abs >.
Assertion cnnvs 
|- x. = ( .sOLD ` U )

Proof

Step Hyp Ref Expression
1 cnnvs.6 
 |-  U = <. <. + , x. >. , abs >.
2 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
3 2 smfval 
 |-  ( .sOLD ` U ) = ( 2nd ` ( 1st ` U ) )
4 1 fveq2i 
 |-  ( 1st ` U ) = ( 1st ` <. <. + , x. >. , abs >. )
5 opex 
 |-  <. + , x. >. e. _V
6 absf 
 |-  abs : CC --> RR
7 cnex 
 |-  CC e. _V
8 fex 
 |-  ( ( abs : CC --> RR /\ CC e. _V ) -> abs e. _V )
9 6 7 8 mp2an 
 |-  abs e. _V
10 5 9 op1st 
 |-  ( 1st ` <. <. + , x. >. , abs >. ) = <. + , x. >.
11 4 10 eqtri 
 |-  ( 1st ` U ) = <. + , x. >.
12 11 fveq2i 
 |-  ( 2nd ` ( 1st ` U ) ) = ( 2nd ` <. + , x. >. )
13 addex 
 |-  + e. _V
14 mulex 
 |-  x. e. _V
15 13 14 op2nd 
 |-  ( 2nd ` <. + , x. >. ) = x.
16 3 12 15 3eqtrri 
 |-  x. = ( .sOLD ` U )