# 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 )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 ) )`