Metamath Proof Explorer

Theorem ipval3

Description: Expansion of the inner product value ipval . (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses dipfval.1 
|- X = ( BaseSet ` U )
dipfval.2 
|- G = ( +v ` U )
dipfval.4 
|- S = ( .sOLD ` U )
dipfval.6 
|- N = ( normCV ` U )
dipfval.7 
|- P = ( .iOLD ` U )
ipval3.3 
|- M = ( -v ` U )
Assertion ipval3 
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) = ( ( ( ( ( N ` ( A G B ) ) ^ 2 ) - ( ( N ` ( A M B ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A M ( _i S B ) ) ) ^ 2 ) ) ) ) / 4 ) )

Proof

Step Hyp Ref Expression
1 dipfval.1 
 |-  X = ( BaseSet ` U )
2 dipfval.2 
 |-  G = ( +v ` U )
3 dipfval.4 
 |-  S = ( .sOLD ` U )
4 dipfval.6 
 |-  N = ( normCV ` U )
5 dipfval.7 
 |-  P = ( .iOLD ` U )
6 ipval3.3 
 |-  M = ( -v ` U )
7 1 2 3 4 5 ipval2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) = ( ( ( ( ( N ` ( A G B ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) ) / 4 ) )
8 1 2 3 6 nvmval 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A M B ) = ( A G ( -u 1 S B ) ) )
9 8 fveq2d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A M B ) ) = ( N ` ( A G ( -u 1 S B ) ) ) )
10 9 oveq1d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N ` ( A M B ) ) ^ 2 ) = ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) )
11 10 oveq2d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( N ` ( A G B ) ) ^ 2 ) - ( ( N ` ( A M B ) ) ^ 2 ) ) = ( ( ( N ` ( A G B ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) )
12 ax-icn 
 |-  _i e. CC
13 1 3 nvscl 
 |-  ( ( U e. NrmCVec /\ _i e. CC /\ B e. X ) -> ( _i S B ) e. X )
14 12 13 mp3an2 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( _i S B ) e. X )
15 14 3adant2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( _i S B ) e. X )
16 1 2 3 6 nvmval 
 |-  ( ( U e. NrmCVec /\ A e. X /\ ( _i S B ) e. X ) -> ( A M ( _i S B ) ) = ( A G ( -u 1 S ( _i S B ) ) ) )
17 15 16 syld3an3 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A M ( _i S B ) ) = ( A G ( -u 1 S ( _i S B ) ) ) )
18 12 mulm1i 
 |-  ( -u 1 x. _i ) = -u _i
19 18 oveq1i 
 |-  ( ( -u 1 x. _i ) S B ) = ( -u _i S B )
20 neg1cn 
 |-  -u 1 e. CC
21 1 3 nvsass 
 |-  ( ( U e. NrmCVec /\ ( -u 1 e. CC /\ _i e. CC /\ B e. X ) ) -> ( ( -u 1 x. _i ) S B ) = ( -u 1 S ( _i S B ) ) )
22 20 21 mp3anr1 
 |-  ( ( U e. NrmCVec /\ ( _i e. CC /\ B e. X ) ) -> ( ( -u 1 x. _i ) S B ) = ( -u 1 S ( _i S B ) ) )
23 12 22 mpanr1 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( ( -u 1 x. _i ) S B ) = ( -u 1 S ( _i S B ) ) )
24 19 23 syl5reqr 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( -u 1 S ( _i S B ) ) = ( -u _i S B ) )
25 24 3adant2 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( -u 1 S ( _i S B ) ) = ( -u _i S B ) )
26 25 oveq2d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G ( -u 1 S ( _i S B ) ) ) = ( A G ( -u _i S B ) ) )
27 17 26 eqtrd 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A M ( _i S B ) ) = ( A G ( -u _i S B ) ) )
28 27 fveq2d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A M ( _i S B ) ) ) = ( N ` ( A G ( -u _i S B ) ) ) )
29 28 oveq1d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N ` ( A M ( _i S B ) ) ) ^ 2 ) = ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) )
30 29 oveq2d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A M ( _i S B ) ) ) ^ 2 ) ) = ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) )
31 30 oveq2d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A M ( _i S B ) ) ) ^ 2 ) ) ) = ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) )
32 11 31 oveq12d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( ( N ` ( A G B ) ) ^ 2 ) - ( ( N ` ( A M B ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A M ( _i S B ) ) ) ^ 2 ) ) ) ) = ( ( ( ( N ` ( A G B ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) ) )
33 32 oveq1d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( ( ( N ` ( A G B ) ) ^ 2 ) - ( ( N ` ( A M B ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A M ( _i S B ) ) ) ^ 2 ) ) ) ) / 4 ) = ( ( ( ( ( N ` ( A G B ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) ) / 4 ) )
34 7 33 eqtr4d 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A P B ) = ( ( ( ( ( N ` ( A G B ) ) ^ 2 ) - ( ( N ` ( A M B ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A M ( _i S B ) ) ) ^ 2 ) ) ) ) / 4 ) )