Metamath Proof Explorer

Theorem ipf

Description: Mapping for the inner product operation. (Contributed by NM, 28-Jan-2008) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses ipcl.1 
|- X = ( BaseSet ` U )
ipcl.7 
|- P = ( .iOLD ` U )
Assertion ipf 
|- ( U e. NrmCVec -> P : ( X X. X ) --> CC )

Proof

Step Hyp Ref Expression
1 ipcl.1 
 |-  X = ( BaseSet ` U )
2 ipcl.7 
 |-  P = ( .iOLD ` U )
3 eqid 
 |-  ( +v ` U ) = ( +v ` U )
4 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
5 eqid 
 |-  ( normCV ` U ) = ( normCV ` U )
6 1 3 4 5 2 ipval 
 |-  ( ( U e. NrmCVec /\ x e. X /\ y e. X ) -> ( x P y ) = ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( x ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) y ) ) ) ^ 2 ) ) / 4 ) )
7 1 2 dipcl 
 |-  ( ( U e. NrmCVec /\ x e. X /\ y e. X ) -> ( x P y ) e. CC )
8 6 7 eqeltrrd 
 |-  ( ( U e. NrmCVec /\ x e. X /\ y e. X ) -> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( x ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) y ) ) ) ^ 2 ) ) / 4 ) e. CC )
9 8 3expib 
 |-  ( U e. NrmCVec -> ( ( x e. X /\ y e. X ) -> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( x ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) y ) ) ) ^ 2 ) ) / 4 ) e. CC ) )
10 9 ralrimivv 
 |-  ( U e. NrmCVec -> A. x e. X A. y e. X ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( x ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) y ) ) ) ^ 2 ) ) / 4 ) e. CC )
11 eqid 
 |-  ( x e. X , y e. X |-> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( x ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) y ) ) ) ^ 2 ) ) / 4 ) ) = ( x e. X , y e. X |-> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( x ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) y ) ) ) ^ 2 ) ) / 4 ) )
12 11 fmpo 
 |-  ( A. x e. X A. y e. X ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( x ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) y ) ) ) ^ 2 ) ) / 4 ) e. CC <-> ( x e. X , y e. X |-> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( x ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) y ) ) ) ^ 2 ) ) / 4 ) ) : ( X X. X ) --> CC )
13 10 12 sylib 
 |-  ( U e. NrmCVec -> ( x e. X , y e. X |-> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( x ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) y ) ) ) ^ 2 ) ) / 4 ) ) : ( X X. X ) --> CC )
14 1 3 4 5 2 dipfval 
 |-  ( U e. NrmCVec -> P = ( x e. X , y e. X |-> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( x ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) y ) ) ) ^ 2 ) ) / 4 ) ) )
15 14 feq1d 
 |-  ( U e. NrmCVec -> ( P : ( X X. X ) --> CC <-> ( x e. X , y e. X |-> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( x ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) y ) ) ) ^ 2 ) ) / 4 ) ) : ( X X. X ) --> CC ) )
16 13 15 mpbird 
 |-  ( U e. NrmCVec -> P : ( X X. X ) --> CC )