Metamath Proof Explorer


Theorem nvop

Description: A complex inner product space in terms of ordered pair components. (Contributed by NM, 11-Sep-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nvop.2 G=+vU
nvop.4 S=𝑠OLDU
nvop.6 N=normCVU
Assertion nvop UNrmCVecU=GSN

Proof

Step Hyp Ref Expression
1 nvop.2 G=+vU
2 nvop.4 S=𝑠OLDU
3 nvop.6 N=normCVU
4 nvrel RelNrmCVec
5 1st2nd RelNrmCVecUNrmCVecU=1stU2ndU
6 4 5 mpan UNrmCVecU=1stU2ndU
7 3 nmcvfval N=2ndU
8 7 opeq2i 1stUN=1stU2ndU
9 eqid 1stU=1stU
10 9 1 2 nvvop UNrmCVec1stU=GS
11 10 opeq1d UNrmCVec1stUN=GSN
12 8 11 eqtr3id UNrmCVec1stU2ndU=GSN
13 6 12 eqtrd UNrmCVecU=GSN