Metamath Proof Explorer


Theorem phop

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

Ref Expression
Hypotheses phop.2 G = + v U
phop.4 S = 𝑠OLD U
phop.6 N = norm CV U
Assertion phop U CPreHil OLD U = G S N

Proof

Step Hyp Ref Expression
1 phop.2 G = + v U
2 phop.4 S = 𝑠OLD U
3 phop.6 N = norm CV U
4 phrel Rel CPreHil OLD
5 1st2nd Rel CPreHil OLD U CPreHil OLD U = 1 st U 2 nd U
6 4 5 mpan U CPreHil OLD 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 phnv U CPreHil OLD U NrmCVec
10 eqid 1 st U = 1 st U
11 10 nvvc U NrmCVec 1 st U CVec OLD
12 vcrel Rel CVec OLD
13 1st2nd Rel CVec OLD 1 st U CVec OLD 1 st U = 1 st 1 st U 2 nd 1 st U
14 12 13 mpan 1 st U CVec OLD 1 st U = 1 st 1 st U 2 nd 1 st U
15 1 vafval G = 1 st 1 st U
16 2 smfval S = 2 nd 1 st U
17 15 16 opeq12i G S = 1 st 1 st U 2 nd 1 st U
18 14 17 eqtr4di 1 st U CVec OLD 1 st U = G S
19 9 11 18 3syl U CPreHil OLD 1 st U = G S
20 19 opeq1d U CPreHil OLD 1 st U N = G S N
21 8 20 eqtr3id U CPreHil OLD 1 st U 2 nd U = G S N
22 6 21 eqtrd U CPreHil OLD U = G S N