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 = + v U
nvop.4 S = 𝑠OLD U
nvop.6 N = norm CV U
Assertion nvop U NrmCVec U = G S N

Proof

Step Hyp Ref Expression
1 nvop.2 G = + v U
2 nvop.4 S = 𝑠OLD U
3 nvop.6 N = norm CV U
4 nvrel Rel NrmCVec
5 1st2nd Rel NrmCVec U NrmCVec U = 1 st U 2 nd U
6 4 5 mpan U NrmCVec U = 1 st U 2 nd U
7 3 nmcvfval N = 2 nd U
8 7 opeq2i 1 st U N = 1 st U 2 nd U
9 eqid 1 st U = 1 st U
10 9 1 2 nvvop U NrmCVec 1 st U = G S
11 10 opeq1d U NrmCVec 1 st U N = G S N
12 8 11 eqtr3id U NrmCVec 1 st U 2 nd U = G S N
13 6 12 eqtrd U NrmCVec U = G S N