This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 >. )