Metamath Proof Explorer


Theorem ipval2

Description: Expansion of the inner product value ipval . (Contributed by NM, 31-Jan-2007) (Revised by Mario Carneiro, 5-May-2014) (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
Assertion 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

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 1 2 3 4 5 ipval U NrmCVec A X B X A P B = k = 1 4 i k N A G i k S B 2 4
7 ax-icn i
8 1 2 3 4 5 ipval2lem4 U NrmCVec A X B X i N A G i S B 2
9 7 8 mpan2 U NrmCVec A X B X N A G i S B 2
10 mulcl i N A G i S B 2 i N A G i S B 2
11 7 9 10 sylancr U NrmCVec A X B X i N A G i S B 2
12 neg1cn 1
13 1 2 3 4 5 ipval2lem4 U NrmCVec A X B X 1 N A G -1 S B 2
14 12 13 mpan2 U NrmCVec A X B X N A G -1 S B 2
15 11 14 subcld U NrmCVec A X B X i N A G i S B 2 N A G -1 S B 2
16 negicn i
17 1 2 3 4 5 ipval2lem4 U NrmCVec A X B X i N A G i S B 2
18 16 17 mpan2 U NrmCVec A X B X N A G i S B 2
19 mulcl i N A G i S B 2 i N A G i S B 2
20 7 18 19 sylancr U NrmCVec A X B X i N A G i S B 2
21 15 20 negsubd U NrmCVec A X B X i N A G i S B 2 - N A G -1 S B 2 + i N A G i S B 2 = i N A G i S B 2 - N A G -1 S B 2 - i N A G i S B 2
22 14 mulm1d U NrmCVec A X B X -1 N A G -1 S B 2 = N A G -1 S B 2
23 22 oveq2d U NrmCVec A X B X i N A G i S B 2 + -1 N A G -1 S B 2 = i N A G i S B 2 + N A G -1 S B 2
24 11 14 negsubd U NrmCVec A X B X i N A G i S B 2 + N A G -1 S B 2 = i N A G i S B 2 N A G -1 S B 2
25 23 24 eqtrd U NrmCVec A X B X i N A G i S B 2 + -1 N A G -1 S B 2 = i N A G i S B 2 N A G -1 S B 2
26 mulneg1 i N A G i S B 2 i N A G i S B 2 = i N A G i S B 2
27 7 18 26 sylancr U NrmCVec A X B X i N A G i S B 2 = i N A G i S B 2
28 25 27 oveq12d U NrmCVec A X B X i N A G i S B 2 + -1 N A G -1 S B 2 + i N A G i S B 2 = i N A G i S B 2 - N A G -1 S B 2 + i N A G i S B 2
29 subdi i N A G i S B 2 N A G i S B 2 i N A G i S B 2 N A G i S B 2 = i N A G i S B 2 i N A G i S B 2
30 7 29 mp3an1 N A G i S B 2 N A G i S B 2 i N A G i S B 2 N A G i S B 2 = i N A G i S B 2 i N A G i S B 2
31 9 18 30 syl2anc U NrmCVec A X B X i N A G i S B 2 N A G i S B 2 = i N A G i S B 2 i N A G i S B 2
32 31 oveq1d U NrmCVec A X B X i N A G i S B 2 N A G i S B 2 N A G -1 S B 2 = i N A G i S B 2 - i N A G i S B 2 - N A G -1 S B 2
33 11 20 14 sub32d U NrmCVec A X B X i N A G i S B 2 - i N A G i S B 2 - N A G -1 S B 2 = i N A G i S B 2 - N A G -1 S B 2 - i N A G i S B 2
34 32 33 eqtrd U NrmCVec A X B X i N A G i S B 2 N A G i S B 2 N A G -1 S B 2 = i N A G i S B 2 - N A G -1 S B 2 - i N A G i S B 2
35 21 28 34 3eqtr4d U NrmCVec A X B X i N A G i S B 2 + -1 N A G -1 S B 2 + i N A G i S B 2 = i N A G i S B 2 N A G i S B 2 N A G -1 S B 2
36 1 3 nvsid U NrmCVec B X 1 S B = B
37 36 oveq2d U NrmCVec B X A G 1 S B = A G B
38 37 fveq2d U NrmCVec B X N A G 1 S B = N A G B
39 38 oveq1d U NrmCVec B X N A G 1 S B 2 = N A G B 2
40 39 3adant2 U NrmCVec A X B X N A G 1 S B 2 = N A G B 2
41 40 oveq2d U NrmCVec A X B X 1 N A G 1 S B 2 = 1 N A G B 2
42 1 2 3 4 5 ipval2lem3 U NrmCVec A X B X N A G B 2
43 42 recnd U NrmCVec A X B X N A G B 2
44 43 mulid2d U NrmCVec A X B X 1 N A G B 2 = N A G B 2
45 41 44 eqtrd U NrmCVec A X B X 1 N A G 1 S B 2 = N A G B 2
46 35 45 oveq12d U NrmCVec A X B X i N A G i S B 2 + -1 N A G -1 S B 2 + i N A G i S B 2 + 1 N A G 1 S B 2 = i N A G i S B 2 N A G i S B 2 - N A G -1 S B 2 + N A G B 2
47 nnuz = 1
48 df-4 4 = 3 + 1
49 oveq2 k = 4 i k = i 4
50 i4 i 4 = 1
51 49 50 syl6eq k = 4 i k = 1
52 51 oveq1d k = 4 i k S B = 1 S B
53 52 oveq2d k = 4 A G i k S B = A G 1 S B
54 53 fveq2d k = 4 N A G i k S B = N A G 1 S B
55 54 oveq1d k = 4 N A G i k S B 2 = N A G 1 S B 2
56 51 55 oveq12d k = 4 i k N A G i k S B 2 = 1 N A G 1 S B 2
57 nnnn0 k k 0
58 expcl i k 0 i k
59 7 57 58 sylancr k i k
60 59 adantl U NrmCVec A X B X k i k
61 1 2 3 4 5 ipval2lem4 U NrmCVec A X B X i k N A G i k S B 2
62 59 61 sylan2 U NrmCVec A X B X k N A G i k S B 2
63 60 62 mulcld U NrmCVec A X B X k i k N A G i k S B 2
64 df-3 3 = 2 + 1
65 oveq2 k = 3 i k = i 3
66 i3 i 3 = i
67 65 66 syl6eq k = 3 i k = i
68 67 oveq1d k = 3 i k S B = i S B
69 68 oveq2d k = 3 A G i k S B = A G i S B
70 69 fveq2d k = 3 N A G i k S B = N A G i S B
71 70 oveq1d k = 3 N A G i k S B 2 = N A G i S B 2
72 67 71 oveq12d k = 3 i k N A G i k S B 2 = i N A G i S B 2
73 df-2 2 = 1 + 1
74 oveq2 k = 2 i k = i 2
75 i2 i 2 = 1
76 74 75 syl6eq k = 2 i k = 1
77 76 oveq1d k = 2 i k S B = -1 S B
78 77 oveq2d k = 2 A G i k S B = A G -1 S B
79 78 fveq2d k = 2 N A G i k S B = N A G -1 S B
80 79 oveq1d k = 2 N A G i k S B 2 = N A G -1 S B 2
81 76 80 oveq12d k = 2 i k N A G i k S B 2 = -1 N A G -1 S B 2
82 1z 1
83 oveq2 k = 1 i k = i 1
84 exp1 i i 1 = i
85 7 84 ax-mp i 1 = i
86 83 85 syl6eq k = 1 i k = i
87 86 oveq1d k = 1 i k S B = i S B
88 87 oveq2d k = 1 A G i k S B = A G i S B
89 88 fveq2d k = 1 N A G i k S B = N A G i S B
90 89 oveq1d k = 1 N A G i k S B 2 = N A G i S B 2
91 86 90 oveq12d k = 1 i k N A G i k S B 2 = i N A G i S B 2
92 91 fsum1 1 i N A G i S B 2 k = 1 1 i k N A G i k S B 2 = i N A G i S B 2
93 82 11 92 sylancr U NrmCVec A X B X k = 1 1 i k N A G i k S B 2 = i N A G i S B 2
94 1nn 1
95 93 94 jctil U NrmCVec A X B X 1 k = 1 1 i k N A G i k S B 2 = i N A G i S B 2
96 eqidd U NrmCVec A X B X i N A G i S B 2 + -1 N A G -1 S B 2 = i N A G i S B 2 + -1 N A G -1 S B 2
97 47 73 81 63 95 96 fsump1i U NrmCVec A X B X 2 k = 1 2 i k N A G i k S B 2 = i N A G i S B 2 + -1 N A G -1 S B 2
98 eqidd U NrmCVec A X B X i N A G i S B 2 + -1 N A G -1 S B 2 + i N A G i S B 2 = i N A G i S B 2 + -1 N A G -1 S B 2 + i N A G i S B 2
99 47 64 72 63 97 98 fsump1i U NrmCVec A X B X 3 k = 1 3 i k N A G i k S B 2 = i N A G i S B 2 + -1 N A G -1 S B 2 + i N A G i S B 2
100 eqidd U NrmCVec A X B X i N A G i S B 2 + -1 N A G -1 S B 2 + i N A G i S B 2 + 1 N A G 1 S B 2 = i N A G i S B 2 + -1 N A G -1 S B 2 + i N A G i S B 2 + 1 N A G 1 S B 2
101 47 48 56 63 99 100 fsump1i U NrmCVec A X B X 4 k = 1 4 i k N A G i k S B 2 = i N A G i S B 2 + -1 N A G -1 S B 2 + i N A G i S B 2 + 1 N A G 1 S B 2
102 101 simprd U NrmCVec A X B X k = 1 4 i k N A G i k S B 2 = i N A G i S B 2 + -1 N A G -1 S B 2 + i N A G i S B 2 + 1 N A G 1 S B 2
103 43 14 subcld U NrmCVec A X B X N A G B 2 N A G -1 S B 2
104 9 18 subcld U NrmCVec A X B X N A G i S B 2 N A G i S B 2
105 mulcl i N A G i S B 2 N A G i S B 2 i N A G i S B 2 N A G i S B 2
106 7 104 105 sylancr U NrmCVec A X B X i N A G i S B 2 N A G i S B 2
107 103 106 addcomd U NrmCVec A X B X 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 = i N A G i S B 2 N A G i S B 2 + N A G B 2 - N A G -1 S B 2
108 106 14 43 subadd23d U NrmCVec A X B X i N A G i S B 2 N A G i S B 2 - N A G -1 S B 2 + N A G B 2 = i N A G i S B 2 N A G i S B 2 + N A G B 2 - N A G -1 S B 2
109 107 108 eqtr4d U NrmCVec A X B X 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 = i N A G i S B 2 N A G i S B 2 - N A G -1 S B 2 + N A G B 2
110 46 102 109 3eqtr4d U NrmCVec A X B X k = 1 4 i k N A G i k 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
111 110 oveq1d U NrmCVec A X B X k = 1 4 i k N A G i k 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
112 6 111 eqtrd 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