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 = ( .sOLD ` U )
phop.6
|- N = ( normCV ` U )
Assertion phop
|- ( U e. CPreHilOLD -> U = <. <. G , S >. , N >. )

Proof

Step Hyp Ref Expression
1 phop.2
 |-  G = ( +v ` U )
2 phop.4
 |-  S = ( .sOLD ` U )
3 phop.6
 |-  N = ( normCV ` U )
4 phrel
 |-  Rel CPreHilOLD
5 1st2nd
 |-  ( ( Rel CPreHilOLD /\ U e. CPreHilOLD ) -> U = <. ( 1st ` U ) , ( 2nd ` U ) >. )
6 4 5 mpan
 |-  ( U e. CPreHilOLD -> U = <. ( 1st ` U ) , ( 2nd ` U ) >. )
7 3 nmcvfval
 |-  N = ( 2nd ` U )
8 7 opeq2i
 |-  <. ( 1st ` U ) , N >. = <. ( 1st ` U ) , ( 2nd ` U ) >.
9 phnv
 |-  ( U e. CPreHilOLD -> U e. NrmCVec )
10 eqid
 |-  ( 1st ` U ) = ( 1st ` U )
11 10 nvvc
 |-  ( U e. NrmCVec -> ( 1st ` U ) e. CVecOLD )
12 vcrel
 |-  Rel CVecOLD
13 1st2nd
 |-  ( ( Rel CVecOLD /\ ( 1st ` U ) e. CVecOLD ) -> ( 1st ` U ) = <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. )
14 12 13 mpan
 |-  ( ( 1st ` U ) e. CVecOLD -> ( 1st ` U ) = <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. )
15 1 vafval
 |-  G = ( 1st ` ( 1st ` U ) )
16 2 smfval
 |-  S = ( 2nd ` ( 1st ` U ) )
17 15 16 opeq12i
 |-  <. G , S >. = <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >.
18 14 17 eqtr4di
 |-  ( ( 1st ` U ) e. CVecOLD -> ( 1st ` U ) = <. G , S >. )
19 9 11 18 3syl
 |-  ( U e. CPreHilOLD -> ( 1st ` U ) = <. G , S >. )
20 19 opeq1d
 |-  ( U e. CPreHilOLD -> <. ( 1st ` U ) , N >. = <. <. G , S >. , N >. )
21 8 20 eqtr3id
 |-  ( U e. CPreHilOLD -> <. ( 1st ` U ) , ( 2nd ` U ) >. = <. <. G , S >. , N >. )
22 6 21 eqtrd
 |-  ( U e. CPreHilOLD -> U = <. <. G , S >. , N >. )