Metamath Proof Explorer

Theorem dipcl

Description: An inner product is a complex number. (Contributed by NM, 1-Feb-2007) (Revised by Mario Carneiro, 5-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses ipcl.1 
|- X = ( BaseSet ` U )
ipcl.7 
|- P = ( .iOLD ` U )
Assertion dipcl 
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) e. 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 /\ A e. X /\ B e. X ) -> ( A P B ) = ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) B ) ) ) ^ 2 ) ) / 4 ) )
7 fzfid 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( 1 ... 4 ) e. Fin )
8 ax-icn 
 |-  _i e. CC
9 elfznn 
 |-  ( k e. ( 1 ... 4 ) -> k e. NN )
10 9 nnnn0d 
 |-  ( k e. ( 1 ... 4 ) -> k e. NN0 )
11 expcl 
 |-  ( ( _i e. CC /\ k e. NN0 ) -> ( _i ^ k ) e. CC )
12 8 10 11 sylancr 
 |-  ( k e. ( 1 ... 4 ) -> ( _i ^ k ) e. CC )
13 12 adantl 
 |-  ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ k e. ( 1 ... 4 ) ) -> ( _i ^ k ) e. CC )
14 1 3 4 5 2 ipval2lem4 
 |-  ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ ( _i ^ k ) e. CC ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) B ) ) ) ^ 2 ) e. CC )
15 12 14 sylan2 
 |-  ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ k e. ( 1 ... 4 ) ) -> ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) B ) ) ) ^ 2 ) e. CC )
16 13 15 mulcld 
 |-  ( ( ( U e. NrmCVec /\ A e. X /\ B e. X ) /\ k e. ( 1 ... 4 ) ) -> ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) B ) ) ) ^ 2 ) ) e. CC )
17 7 16 fsumcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) B ) ) ) ^ 2 ) ) e. CC )
18 4cn 
 |-  4 e. CC
19 4ne0 
 |-  4 =/= 0
20 divcl 
 |-  ( ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) B ) ) ) ^ 2 ) ) e. CC /\ 4 e. CC /\ 4 =/= 0 ) -> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) B ) ) ) ^ 2 ) ) / 4 ) e. CC )
21 18 19 20 mp3an23 
 |-  ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) B ) ) ) ^ 2 ) ) e. CC -> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) B ) ) ) ^ 2 ) ) / 4 ) e. CC )
22 17 21 syl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( ( normCV ` U ) ` ( A ( +v ` U ) ( ( _i ^ k ) ( .sOLD ` U ) B ) ) ) ^ 2 ) ) / 4 ) e. CC )
23 6 22 eqeltrd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) e. CC )