Metamath Proof Explorer


Theorem cnnvg

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

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

Proof

Step Hyp Ref Expression
1 cnnvg.6
 |-  U = <. <. + , x. >. , abs >.
2 eqid
 |-  ( +v ` U ) = ( +v ` U )
3 2 vafval
 |-  ( +v ` U ) = ( 1st ` ( 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
 |-  ( 1st ` ( 1st ` U ) ) = ( 1st ` <. + , x. >. )
13 addex
 |-  + e. _V
14 mulex
 |-  x. e. _V
15 13 14 op1st
 |-  ( 1st ` <. + , x. >. ) = +
16 3 12 15 3eqtrri
 |-  + = ( +v ` U )