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 = 𝑠OLD U
dipfval.6 N = norm CV U
dipfval.7 P = 𝑖OLD U
ipval3.3 M = - v U
Assertion ipval3 U NrmCVec A X B X A P B = N A G B 2 - N A M B 2 + i 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 = 𝑠OLD U
4 dipfval.6 N = norm CV U
5 dipfval.7 P = 𝑖OLD U
6 ipval3.3 M = - v U
7 1 2 3 4 5 ipval2 U NrmCVec A X B X A P B = N A G B 2 - N A G -1 S B 2 + i N A G i S B 2 N A G i S B 2 4
8 1 2 3 6 nvmval U NrmCVec A X B X A M B = A G -1 S B
9 8 fveq2d U NrmCVec A X B X N A M B = N A G -1 S B
10 9 oveq1d U NrmCVec A X B X N A M B 2 = N A G -1 S B 2
11 10 oveq2d U NrmCVec A X B X N A G B 2 N A M B 2 = N A G B 2 N A G -1 S B 2
12 ax-icn i
13 1 3 nvscl U NrmCVec i B X i S B X
14 12 13 mp3an2 U NrmCVec B X i S B X
15 14 3adant2 U NrmCVec A X B X i S B X
16 1 2 3 6 nvmval U NrmCVec A X i S B X A M i S B = A G -1 S i S B
17 15 16 syld3an3 U NrmCVec A X B X A M i S B = A G -1 S i S B
18 neg1cn 1
19 1 3 nvsass U NrmCVec 1 i B X -1 i S B = -1 S i S B
20 18 19 mp3anr1 U NrmCVec i B X -1 i S B = -1 S i S B
21 12 20 mpanr1 U NrmCVec B X -1 i S B = -1 S i S B
22 12 mulm1i -1 i = i
23 22 oveq1i -1 i S B = i S B
24 21 23 eqtr3di U NrmCVec B X -1 S i S B = i S B
25 24 3adant2 U NrmCVec A X B X -1 S i S B = i S B
26 25 oveq2d U NrmCVec A X B X A G -1 S i S B = A G i S B
27 17 26 eqtrd U NrmCVec A X B X A M i S B = A G i S B
28 27 fveq2d U NrmCVec A X B X N A M i S B = N A G i S B
29 28 oveq1d U NrmCVec A X B X N A M i S B 2 = N A G i S B 2
30 29 oveq2d U NrmCVec A X B 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 i S B 2
31 30 oveq2d U NrmCVec A X B X i N A G i S B 2 N A M i S B 2 = i N A G i S B 2 N A G i S B 2
32 11 31 oveq12d U NrmCVec A X B X N A G B 2 - N A M B 2 + i N A G i S B 2 N A M i S B 2 = N A G B 2 - N A G -1 S B 2 + i N A G i S B 2 N A G i S B 2
33 32 oveq1d U NrmCVec A X B X N A G B 2 - N A M B 2 + i N A G i S B 2 N A M i S B 2 4 = N A G B 2 - N A G -1 S B 2 + i N A G i S B 2 N A G i S B 2 4
34 7 33 eqtr4d U NrmCVec A X B X A P B = N A G B 2 - N A M B 2 + i N A G i S B 2 N A M i S B 2 4