# Metamath Proof Explorer

## Theorem 4ipval2

Description: Four times the inner product value ipval3 , useful for simplifying certain proofs. (Contributed by NM, 10-Apr-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 )`
Assertion 4ipval2
`|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( 4 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 ) ) ) ) )`

### 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 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 ) )`
7 6 oveq2d
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( 4 x. ( A P B ) ) = ( 4 x. ( ( ( ( ( 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 simp1
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> U e. NrmCVec )`
9 1 2 nvgcl
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G B ) e. X )`
10 1 4 nvcl
` |-  ( ( U e. NrmCVec /\ ( A G B ) e. X ) -> ( N ` ( A G B ) ) e. RR )`
11 8 9 10 syl2anc
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A G B ) ) e. RR )`
12 11 recnd
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A G B ) ) e. CC )`
13 12 sqcld
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N ` ( A G B ) ) ^ 2 ) e. CC )`
14 neg1cn
` |-  -u 1 e. CC`
15 1 3 nvscl
` |-  ( ( U e. NrmCVec /\ -u 1 e. CC /\ B e. X ) -> ( -u 1 S B ) e. X )`
16 14 15 mp3an2
` |-  ( ( U e. NrmCVec /\ B e. X ) -> ( -u 1 S B ) e. X )`
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( -u 1 S B ) e. X )`
18 1 2 nvgcl
` |-  ( ( U e. NrmCVec /\ A e. X /\ ( -u 1 S B ) e. X ) -> ( A G ( -u 1 S B ) ) e. X )`
19 17 18 syld3an3
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G ( -u 1 S B ) ) e. X )`
20 1 4 nvcl
` |-  ( ( U e. NrmCVec /\ ( A G ( -u 1 S B ) ) e. X ) -> ( N ` ( A G ( -u 1 S B ) ) ) e. RR )`
21 8 19 20 syl2anc
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A G ( -u 1 S B ) ) ) e. RR )`
22 21 recnd
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A G ( -u 1 S B ) ) ) e. CC )`
23 22 sqcld
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) e. CC )`
24 13 23 subcld
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( N ` ( A G B ) ) ^ 2 ) - ( ( N ` ( A G ( -u 1 S B ) ) ) ^ 2 ) ) e. CC )`
25 ax-icn
` |-  _i e. CC`
26 1 3 nvscl
` |-  ( ( U e. NrmCVec /\ _i e. CC /\ B e. X ) -> ( _i S B ) e. X )`
27 25 26 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 )`
29 1 2 nvgcl
` |-  ( ( U e. NrmCVec /\ A e. X /\ ( _i S B ) e. X ) -> ( A G ( _i S B ) ) e. X )`
30 28 29 syld3an3
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G ( _i S B ) ) e. X )`
31 1 4 nvcl
` |-  ( ( U e. NrmCVec /\ ( A G ( _i S B ) ) e. X ) -> ( N ` ( A G ( _i S B ) ) ) e. RR )`
32 8 30 31 syl2anc
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A G ( _i S B ) ) ) e. RR )`
33 32 recnd
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A G ( _i S B ) ) ) e. CC )`
34 33 sqcld
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) e. CC )`
35 negicn
` |-  -u _i e. CC`
36 1 3 nvscl
` |-  ( ( U e. NrmCVec /\ -u _i e. CC /\ B e. X ) -> ( -u _i S B ) e. X )`
37 35 36 mp3an2
` |-  ( ( U e. NrmCVec /\ B e. X ) -> ( -u _i S B ) e. X )`
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( -u _i S B ) e. X )`
39 1 2 nvgcl
` |-  ( ( U e. NrmCVec /\ A e. X /\ ( -u _i S B ) e. X ) -> ( A G ( -u _i S B ) ) e. X )`
40 38 39 syld3an3
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G ( -u _i S B ) ) e. X )`
41 1 4 nvcl
` |-  ( ( U e. NrmCVec /\ ( A G ( -u _i S B ) ) e. X ) -> ( N ` ( A G ( -u _i S B ) ) ) e. RR )`
42 8 40 41 syl2anc
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A G ( -u _i S B ) ) ) e. RR )`
43 42 recnd
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A G ( -u _i S B ) ) ) e. CC )`
44 43 sqcld
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) e. CC )`
45 34 44 subcld
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) e. CC )`
46 mulcl
` |-  ( ( _i e. CC /\ ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) e. CC ) -> ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) e. CC )`
47 25 45 46 sylancr
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( _i x. ( ( ( N ` ( A G ( _i S B ) ) ) ^ 2 ) - ( ( N ` ( A G ( -u _i S B ) ) ) ^ 2 ) ) ) e. CC )`
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( ( 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 ) ) ) ) e. CC )`
` |-  4 e. CC`
` |-  4 =/= 0`
` |-  ( ( ( ( ( ( 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 ) ) ) ) e. CC /\ 4 e. CC /\ 4 =/= 0 ) -> ( 4 x. ( ( ( ( ( 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 ) ) = ( ( ( ( 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 ) ) ) ) )`
` |-  ( ( ( ( ( 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 ) ) ) ) e. CC -> ( 4 x. ( ( ( ( ( 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 ) ) = ( ( ( ( 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 ) ) ) ) )`
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( 4 x. ( ( ( ( ( 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 ) ) = ( ( ( ( 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 ) ) ) ) )`
` |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( 4 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 ) ) ) ) )`