Metamath Proof Explorer


Theorem nvvop

Description: The vector space component of a normed complex vector space is an ordered pair of the underlying group and a scalar product. (Contributed by NM, 28-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses nvvop.1 W = 1 st U
nvvop.2 G = + v U
nvvop.4 S = 𝑠OLD U
Assertion nvvop U NrmCVec W = G S

Proof

Step Hyp Ref Expression
1 nvvop.1 W = 1 st U
2 nvvop.2 G = + v U
3 nvvop.4 S = 𝑠OLD U
4 vcrel Rel CVec OLD
5 nvss NrmCVec CVec OLD × V
6 eqid norm CV U = norm CV U
7 1 6 nvop2 U NrmCVec U = W norm CV U
8 7 eleq1d U NrmCVec U NrmCVec W norm CV U NrmCVec
9 8 ibi U NrmCVec W norm CV U NrmCVec
10 5 9 sseldi U NrmCVec W norm CV U CVec OLD × V
11 opelxp1 W norm CV U CVec OLD × V W CVec OLD
12 10 11 syl U NrmCVec W CVec OLD
13 1st2nd Rel CVec OLD W CVec OLD W = 1 st W 2 nd W
14 4 12 13 sylancr U NrmCVec W = 1 st W 2 nd W
15 2 vafval G = 1 st 1 st U
16 1 fveq2i 1 st W = 1 st 1 st U
17 15 16 eqtr4i G = 1 st W
18 3 smfval S = 2 nd 1 st U
19 1 fveq2i 2 nd W = 2 nd 1 st U
20 18 19 eqtr4i S = 2 nd W
21 17 20 opeq12i G S = 1 st W 2 nd W
22 14 21 eqtr4di U NrmCVec W = G S