# 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}=\mathrm{BaseSet}\left({U}\right)$
dipfval.2 ${⊢}{G}={+}_{v}\left({U}\right)$
dipfval.4 ${⊢}{S}={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
dipfval.6 ${⊢}{N}={norm}_{CV}\left({U}\right)$
dipfval.7 ${⊢}{P}={\cdot }_{\mathrm{𝑖OLD}}\left({U}\right)$
Assertion ipval2 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{P}{B}=\frac{{{N}\left({A}{G}{B}\right)}^{2}-{{N}\left({A}{G}\left(-1{S}{B}\right)\right)}^{2}+\mathrm{i}\left({{N}\left({A}{G}\left(\mathrm{i}{S}{B}\right)\right)}^{2}-{{N}\left({A}{G}\left(\left(-\mathrm{i}\right){S}{B}\right)\right)}^{2}\right)}{4}$

### Proof

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