Metamath Proof Explorer

Theorem circlemethhgt

Description: The circle method, where the Vinogradov sums are weighted using the Von Mangoldt function and smoothed using functions H and K . Statement 7.49 of Helfgott p. 69. At this point there is no further constraint on the smoothing functions. (Contributed by Thierry Arnoux, 22-Dec-2021)

Ref Expression
Hypotheses circlemethhgt.h 
|- ( ph -> H : NN --> RR )
circlemethhgt.k 
|- ( ph -> K : NN --> RR )
circlemethhgt.n 
|- ( ph -> N e. NN0 )
Assertion circlemethhgt 
|- ( ph -> sum_ n e. ( NN ( repr ` 3 ) N ) ( ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) = S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. H ) vts N ) ` x ) x. ( ( ( ( Lam oF x. K ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x )

Proof

Step Hyp Ref Expression
1 circlemethhgt.h 
 |-  ( ph -> H : NN --> RR )
2 circlemethhgt.k 
 |-  ( ph -> K : NN --> RR )
3 circlemethhgt.n 
 |-  ( ph -> N e. NN0 )
4 3nn 
 |-  3 e. NN
5 4 a1i 
 |-  ( ph -> 3 e. NN )
6 s3len 
 |-  ( # ` <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ) = 3
7 6 eqcomi 
 |-  3 = ( # ` <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> )
8 7 a1i 
 |-  ( ph -> 3 = ( # ` <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ) )
9 simprl 
 |-  ( ( ph /\ ( x e. RR /\ y e. RR ) ) -> x e. RR )
10 simprr 
 |-  ( ( ph /\ ( x e. RR /\ y e. RR ) ) -> y e. RR )
11 9 10 remulcld 
 |-  ( ( ph /\ ( x e. RR /\ y e. RR ) ) -> ( x x. y ) e. RR )
12 11 recnd 
 |-  ( ( ph /\ ( x e. RR /\ y e. RR ) ) -> ( x x. y ) e. CC )
13 vmaf 
 |-  Lam : NN --> RR
14 13 a1i 
 |-  ( ph -> Lam : NN --> RR )
15 nnex 
 |-  NN e. _V
16 15 a1i 
 |-  ( ph -> NN e. _V )
17 inidm 
 |-  ( NN i^i NN ) = NN
18 12 14 1 16 16 17 off 
 |-  ( ph -> ( Lam oF x. H ) : NN --> CC )
19 cnex 
 |-  CC e. _V
20 19 15 elmap 
 |-  ( ( Lam oF x. H ) e. ( CC ^m NN ) <-> ( Lam oF x. H ) : NN --> CC )
21 18 20 sylibr 
 |-  ( ph -> ( Lam oF x. H ) e. ( CC ^m NN ) )
22 12 14 2 16 16 17 off 
 |-  ( ph -> ( Lam oF x. K ) : NN --> CC )
23 19 15 elmap 
 |-  ( ( Lam oF x. K ) e. ( CC ^m NN ) <-> ( Lam oF x. K ) : NN --> CC )
24 22 23 sylibr 
 |-  ( ph -> ( Lam oF x. K ) e. ( CC ^m NN ) )
25 21 24 24 s3cld 
 |-  ( ph -> <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> e. Word ( CC ^m NN ) )
26 8 25 wrdfd 
 |-  ( ph -> <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> : ( 0 ..^ 3 ) --> ( CC ^m NN ) )
27 3 5 26 circlemeth 
 |-  ( ph -> sum_ n e. ( NN ( repr ` 3 ) N ) prod_ a e. ( 0 ..^ 3 ) ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) ` ( n ` a ) ) = S. ( 0 (,) 1 ) ( prod_ a e. ( 0 ..^ 3 ) ( ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) vts N ) ` x ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x )
28 fveq2 
 |-  ( a = 0 -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) = ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 0 ) )
29 fveq2 
 |-  ( a = 0 -> ( n ` a ) = ( n ` 0 ) )
30 28 29 fveq12d 
 |-  ( a = 0 -> ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) ` ( n ` a ) ) = ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 0 ) ` ( n ` 0 ) ) )
31 fveq2 
 |-  ( a = 1 -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) = ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 1 ) )
32 fveq2 
 |-  ( a = 1 -> ( n ` a ) = ( n ` 1 ) )
33 31 32 fveq12d 
 |-  ( a = 1 -> ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) ` ( n ` a ) ) = ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 1 ) ` ( n ` 1 ) ) )
34 fveq2 
 |-  ( a = 2 -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) = ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 2 ) )
35 fveq2 
 |-  ( a = 2 -> ( n ` a ) = ( n ` 2 ) )
36 34 35 fveq12d 
 |-  ( a = 2 -> ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) ` ( n ` a ) ) = ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 2 ) ` ( n ` 2 ) ) )
37 26 adantr 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> : ( 0 ..^ 3 ) --> ( CC ^m NN ) )
38 37 ffvelcdmda 
 |-  ( ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) /\ a e. ( 0 ..^ 3 ) ) -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) e. ( CC ^m NN ) )
39 elmapi 
 |-  ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) e. ( CC ^m NN ) -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) : NN --> CC )
40 38 39 syl 
 |-  ( ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) /\ a e. ( 0 ..^ 3 ) ) -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) : NN --> CC )
41 ssidd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> NN C_ NN )
42 3 nn0zd 
 |-  ( ph -> N e. ZZ )
43 42 adantr 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> N e. ZZ )
44 3nn0 
 |-  3 e. NN0
45 44 a1i 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> 3 e. NN0 )
46 simpr 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> n e. ( NN ( repr ` 3 ) N ) )
47 41 43 45 46 reprf 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> n : ( 0 ..^ 3 ) --> NN )
48 47 ffvelcdmda 
 |-  ( ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) /\ a e. ( 0 ..^ 3 ) ) -> ( n ` a ) e. NN )
49 40 48 ffvelcdmd 
 |-  ( ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) /\ a e. ( 0 ..^ 3 ) ) -> ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) ` ( n ` a ) ) e. CC )
50 30 33 36 49 prodfzo03 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> prod_ a e. ( 0 ..^ 3 ) ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) ` ( n ` a ) ) = ( ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 0 ) ` ( n ` 0 ) ) x. ( ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 1 ) ` ( n ` 1 ) ) x. ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 2 ) ` ( n ` 2 ) ) ) ) )
51 ovex 
 |-  ( Lam oF x. H ) e. _V
52 s3fv0 
 |-  ( ( Lam oF x. H ) e. _V -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 0 ) = ( Lam oF x. H ) )
53 51 52 mp1i 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 0 ) = ( Lam oF x. H ) )
54 53 fveq1d 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 0 ) ` ( n ` 0 ) ) = ( ( Lam oF x. H ) ` ( n ` 0 ) ) )
55 simpl 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ph )
56 c0ex 
 |-  0 e. _V
57 56 tpid1 
 |-  0 e. { 0 , 1 , 2 }
58 fzo0to3tp 
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
59 57 58 eleqtrri 
 |-  0 e. ( 0 ..^ 3 )
60 59 a1i 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> 0 e. ( 0 ..^ 3 ) )
61 47 60 ffvelcdmd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( n ` 0 ) e. NN )
62 ffn 
 |-  ( Lam : NN --> RR -> Lam Fn NN )
63 13 62 ax-mp 
 |-  Lam Fn NN
64 63 a1i 
 |-  ( ph -> Lam Fn NN )
65 1 ffnd 
 |-  ( ph -> H Fn NN )
66 eqidd 
 |-  ( ( ph /\ ( n ` 0 ) e. NN ) -> ( Lam ` ( n ` 0 ) ) = ( Lam ` ( n ` 0 ) ) )
67 eqidd 
 |-  ( ( ph /\ ( n ` 0 ) e. NN ) -> ( H ` ( n ` 0 ) ) = ( H ` ( n ` 0 ) ) )
68 64 65 16 16 17 66 67 ofval 
 |-  ( ( ph /\ ( n ` 0 ) e. NN ) -> ( ( Lam oF x. H ) ` ( n ` 0 ) ) = ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) )
69 55 61 68 syl2anc 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( ( Lam oF x. H ) ` ( n ` 0 ) ) = ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) )
70 54 69 eqtrd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 0 ) ` ( n ` 0 ) ) = ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) )
71 ovex 
 |-  ( Lam oF x. K ) e. _V
72 s3fv1 
 |-  ( ( Lam oF x. K ) e. _V -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 1 ) = ( Lam oF x. K ) )
73 71 72 mp1i 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 1 ) = ( Lam oF x. K ) )
74 73 fveq1d 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 1 ) ` ( n ` 1 ) ) = ( ( Lam oF x. K ) ` ( n ` 1 ) ) )
75 1eltp012 
 |-  1 e. { 0 , 1 , 2 }
76 75 58 eleqtrri 
 |-  1 e. ( 0 ..^ 3 )
77 76 a1i 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> 1 e. ( 0 ..^ 3 ) )
78 47 77 ffvelcdmd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( n ` 1 ) e. NN )
79 2 ffnd 
 |-  ( ph -> K Fn NN )
80 eqidd 
 |-  ( ( ph /\ ( n ` 1 ) e. NN ) -> ( Lam ` ( n ` 1 ) ) = ( Lam ` ( n ` 1 ) ) )
81 eqidd 
 |-  ( ( ph /\ ( n ` 1 ) e. NN ) -> ( K ` ( n ` 1 ) ) = ( K ` ( n ` 1 ) ) )
82 64 79 16 16 17 80 81 ofval 
 |-  ( ( ph /\ ( n ` 1 ) e. NN ) -> ( ( Lam oF x. K ) ` ( n ` 1 ) ) = ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) )
83 55 78 82 syl2anc 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( ( Lam oF x. K ) ` ( n ` 1 ) ) = ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) )
84 74 83 eqtrd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 1 ) ` ( n ` 1 ) ) = ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) )
85 s3fv2 
 |-  ( ( Lam oF x. K ) e. _V -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 2 ) = ( Lam oF x. K ) )
86 71 85 mp1i 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 2 ) = ( Lam oF x. K ) )
87 86 fveq1d 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 2 ) ` ( n ` 2 ) ) = ( ( Lam oF x. K ) ` ( n ` 2 ) ) )
88 2ex 
 |-  2 e. _V
89 88 tpid3 
 |-  2 e. { 0 , 1 , 2 }
90 89 58 eleqtrri 
 |-  2 e. ( 0 ..^ 3 )
91 90 a1i 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> 2 e. ( 0 ..^ 3 ) )
92 47 91 ffvelcdmd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( n ` 2 ) e. NN )
93 eqidd 
 |-  ( ( ph /\ ( n ` 2 ) e. NN ) -> ( Lam ` ( n ` 2 ) ) = ( Lam ` ( n ` 2 ) ) )
94 eqidd 
 |-  ( ( ph /\ ( n ` 2 ) e. NN ) -> ( K ` ( n ` 2 ) ) = ( K ` ( n ` 2 ) ) )
95 64 79 16 16 17 93 94 ofval 
 |-  ( ( ph /\ ( n ` 2 ) e. NN ) -> ( ( Lam oF x. K ) ` ( n ` 2 ) ) = ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) )
96 55 92 95 syl2anc 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( ( Lam oF x. K ) ` ( n ` 2 ) ) = ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) )
97 87 96 eqtrd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 2 ) ` ( n ` 2 ) ) = ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) )
98 84 97 oveq12d 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 1 ) ` ( n ` 1 ) ) x. ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 2 ) ` ( n ` 2 ) ) ) = ( ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) )
99 70 98 oveq12d 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 0 ) ` ( n ` 0 ) ) x. ( ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 1 ) ` ( n ` 1 ) ) x. ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 2 ) ` ( n ` 2 ) ) ) ) = ( ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) )
100 50 99 eqtrd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> prod_ a e. ( 0 ..^ 3 ) ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) ` ( n ` a ) ) = ( ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) )
101 100 sumeq2dv 
 |-  ( ph -> sum_ n e. ( NN ( repr ` 3 ) N ) prod_ a e. ( 0 ..^ 3 ) ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) ` ( n ` a ) ) = sum_ n e. ( NN ( repr ` 3 ) N ) ( ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) )
102 nfv 
 |-  F/ a ( ph /\ x e. ( 0 (,) 1 ) )
103 nfcv 
 |-  F/_ a ( ( ( Lam oF x. H ) vts N ) ` x )
104 fzofi 
 |-  ( 1 ..^ 3 ) e. Fin
105 104 a1i 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( 1 ..^ 3 ) e. Fin )
106 56 a1i 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> 0 e. _V )
107 eqid 
 |-  0 = 0
108 107 orci 
 |-  ( 0 = 0 \/ 0 = 3 )
109 0elfz 
 |-  ( 3 e. NN0 -> 0 e. ( 0 ... 3 ) )
110 elfznelfzob 
 |-  ( 0 e. ( 0 ... 3 ) -> ( -. 0 e. ( 1 ..^ 3 ) <-> ( 0 = 0 \/ 0 = 3 ) ) )
111 44 109 110 mp2b 
 |-  ( -. 0 e. ( 1 ..^ 3 ) <-> ( 0 = 0 \/ 0 = 3 ) )
112 108 111 mpbir 
 |-  -. 0 e. ( 1 ..^ 3 )
113 112 a1i 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> -. 0 e. ( 1 ..^ 3 ) )
114 3 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ a e. ( 1 ..^ 3 ) ) -> N e. NN0 )
115 ioossre 
 |-  ( 0 (,) 1 ) C_ RR
116 ax-resscn 
 |-  RR C_ CC
117 115 116 sstri 
 |-  ( 0 (,) 1 ) C_ CC
118 117 a1i 
 |-  ( ph -> ( 0 (,) 1 ) C_ CC )
119 118 sselda 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> x e. CC )
120 119 adantr 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ a e. ( 1 ..^ 3 ) ) -> x e. CC )
121 26 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ a e. ( 1 ..^ 3 ) ) -> <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> : ( 0 ..^ 3 ) --> ( CC ^m NN ) )
122 fzo0ss1 
 |-  ( 1 ..^ 3 ) C_ ( 0 ..^ 3 )
123 122 a1i 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( 1 ..^ 3 ) C_ ( 0 ..^ 3 ) )
124 123 sselda 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ a e. ( 1 ..^ 3 ) ) -> a e. ( 0 ..^ 3 ) )
125 121 124 ffvelcdmd 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ a e. ( 1 ..^ 3 ) ) -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) e. ( CC ^m NN ) )
126 125 39 syl 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ a e. ( 1 ..^ 3 ) ) -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) : NN --> CC )
127 114 120 126 vtscl 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ a e. ( 1 ..^ 3 ) ) -> ( ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) vts N ) ` x ) e. CC )
128 51 52 ax-mp 
 |-  ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 0 ) = ( Lam oF x. H )
129 28 128 eqtrdi 
 |-  ( a = 0 -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) = ( Lam oF x. H ) )
130 129 oveq1d 
 |-  ( a = 0 -> ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) vts N ) = ( ( Lam oF x. H ) vts N ) )
131 130 fveq1d 
 |-  ( a = 0 -> ( ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) vts N ) ` x ) = ( ( ( Lam oF x. H ) vts N ) ` x ) )
132 3 adantr 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> N e. NN0 )
133 18 adantr 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( Lam oF x. H ) : NN --> CC )
134 132 119 133 vtscl 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( ( ( Lam oF x. H ) vts N ) ` x ) e. CC )
135 102 103 105 106 113 127 131 134 fprodsplitsn 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> prod_ a e. ( ( 1 ..^ 3 ) u. { 0 } ) ( ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) vts N ) ` x ) = ( prod_ a e. ( 1 ..^ 3 ) ( ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) vts N ) ` x ) x. ( ( ( Lam oF x. H ) vts N ) ` x ) ) )
136 uncom 
 |-  ( ( 1 ..^ 3 ) u. { 0 } ) = ( { 0 } u. ( 1 ..^ 3 ) )
137 fzo0sn0fzo1 
 |-  ( 3 e. NN -> ( 0 ..^ 3 ) = ( { 0 } u. ( 1 ..^ 3 ) ) )
138 4 137 ax-mp 
 |-  ( 0 ..^ 3 ) = ( { 0 } u. ( 1 ..^ 3 ) )
139 136 138 eqtr4i 
 |-  ( ( 1 ..^ 3 ) u. { 0 } ) = ( 0 ..^ 3 )
140 139 a1i 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( ( 1 ..^ 3 ) u. { 0 } ) = ( 0 ..^ 3 ) )
141 140 prodeq1d 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> prod_ a e. ( ( 1 ..^ 3 ) u. { 0 } ) ( ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) vts N ) ` x ) = prod_ a e. ( 0 ..^ 3 ) ( ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) vts N ) ` x ) )
142 fzo13pr 
 |-  ( 1 ..^ 3 ) = { 1 , 2 }
143 142 eleq2i 
 |-  ( a e. ( 1 ..^ 3 ) <-> a e. { 1 , 2 } )
144 vex 
 |-  a e. _V
145 144 elpr 
 |-  ( a e. { 1 , 2 } <-> ( a = 1 \/ a = 2 ) )
146 143 145 bitri 
 |-  ( a e. ( 1 ..^ 3 ) <-> ( a = 1 \/ a = 2 ) )
147 31 adantl 
 |-  ( ( ph /\ a = 1 ) -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) = ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 1 ) )
148 71 72 mp1i 
 |-  ( ( ph /\ a = 1 ) -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 1 ) = ( Lam oF x. K ) )
149 147 148 eqtrd 
 |-  ( ( ph /\ a = 1 ) -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) = ( Lam oF x. K ) )
150 34 adantl 
 |-  ( ( ph /\ a = 2 ) -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) = ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 2 ) )
151 71 85 mp1i 
 |-  ( ( ph /\ a = 2 ) -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 2 ) = ( Lam oF x. K ) )
152 150 151 eqtrd 
 |-  ( ( ph /\ a = 2 ) -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) = ( Lam oF x. K ) )
153 149 152 jaodan 
 |-  ( ( ph /\ ( a = 1 \/ a = 2 ) ) -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) = ( Lam oF x. K ) )
154 146 153 sylan2b 
 |-  ( ( ph /\ a e. ( 1 ..^ 3 ) ) -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) = ( Lam oF x. K ) )
155 154 adantlr 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ a e. ( 1 ..^ 3 ) ) -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) = ( Lam oF x. K ) )
156 155 oveq1d 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ a e. ( 1 ..^ 3 ) ) -> ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) vts N ) = ( ( Lam oF x. K ) vts N ) )
157 156 fveq1d 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ a e. ( 1 ..^ 3 ) ) -> ( ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) vts N ) ` x ) = ( ( ( Lam oF x. K ) vts N ) ` x ) )
158 157 prodeq2dv 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> prod_ a e. ( 1 ..^ 3 ) ( ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) vts N ) ` x ) = prod_ a e. ( 1 ..^ 3 ) ( ( ( Lam oF x. K ) vts N ) ` x ) )
159 22 adantr 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( Lam oF x. K ) : NN --> CC )
160 132 119 159 vtscl 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( ( ( Lam oF x. K ) vts N ) ` x ) e. CC )
161 fprodconst 
 |-  ( ( ( 1 ..^ 3 ) e. Fin /\ ( ( ( Lam oF x. K ) vts N ) ` x ) e. CC ) -> prod_ a e. ( 1 ..^ 3 ) ( ( ( Lam oF x. K ) vts N ) ` x ) = ( ( ( ( Lam oF x. K ) vts N ) ` x ) ^ ( # ` ( 1 ..^ 3 ) ) ) )
162 105 160 161 syl2anc 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> prod_ a e. ( 1 ..^ 3 ) ( ( ( Lam oF x. K ) vts N ) ` x ) = ( ( ( ( Lam oF x. K ) vts N ) ` x ) ^ ( # ` ( 1 ..^ 3 ) ) ) )
163 nnuz 
 |-  NN = ( ZZ>= ` 1 )
164 4 163 eleqtri 
 |-  3 e. ( ZZ>= ` 1 )
165 hashfzo 
 |-  ( 3 e. ( ZZ>= ` 1 ) -> ( # ` ( 1 ..^ 3 ) ) = ( 3 - 1 ) )
166 164 165 ax-mp 
 |-  ( # ` ( 1 ..^ 3 ) ) = ( 3 - 1 )
167 3m1e2 
 |-  ( 3 - 1 ) = 2
168 166 167 eqtri 
 |-  ( # ` ( 1 ..^ 3 ) ) = 2
169 168 a1i 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( # ` ( 1 ..^ 3 ) ) = 2 )
170 169 oveq2d 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( ( ( ( Lam oF x. K ) vts N ) ` x ) ^ ( # ` ( 1 ..^ 3 ) ) ) = ( ( ( ( Lam oF x. K ) vts N ) ` x ) ^ 2 ) )
171 158 162 170 3eqtrd 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> prod_ a e. ( 1 ..^ 3 ) ( ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) vts N ) ` x ) = ( ( ( ( Lam oF x. K ) vts N ) ` x ) ^ 2 ) )
172 171 oveq1d 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( prod_ a e. ( 1 ..^ 3 ) ( ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) vts N ) ` x ) x. ( ( ( Lam oF x. H ) vts N ) ` x ) ) = ( ( ( ( ( Lam oF x. K ) vts N ) ` x ) ^ 2 ) x. ( ( ( Lam oF x. H ) vts N ) ` x ) ) )
173 160 sqcld 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( ( ( ( Lam oF x. K ) vts N ) ` x ) ^ 2 ) e. CC )
174 134 173 mulcomd 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( ( ( ( Lam oF x. H ) vts N ) ` x ) x. ( ( ( ( Lam oF x. K ) vts N ) ` x ) ^ 2 ) ) = ( ( ( ( ( Lam oF x. K ) vts N ) ` x ) ^ 2 ) x. ( ( ( Lam oF x. H ) vts N ) ` x ) ) )
175 172 174 eqtr4d 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( prod_ a e. ( 1 ..^ 3 ) ( ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) vts N ) ` x ) x. ( ( ( Lam oF x. H ) vts N ) ` x ) ) = ( ( ( ( Lam oF x. H ) vts N ) ` x ) x. ( ( ( ( Lam oF x. K ) vts N ) ` x ) ^ 2 ) ) )
176 135 141 175 3eqtr3d 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> prod_ a e. ( 0 ..^ 3 ) ( ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) vts N ) ` x ) = ( ( ( ( Lam oF x. H ) vts N ) ` x ) x. ( ( ( ( Lam oF x. K ) vts N ) ` x ) ^ 2 ) ) )
177 176 oveq1d 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( prod_ a e. ( 0 ..^ 3 ) ( ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) vts N ) ` x ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) = ( ( ( ( ( Lam oF x. H ) vts N ) ` x ) x. ( ( ( ( Lam oF x. K ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) )
178 177 itgeq2dv 
 |-  ( ph -> S. ( 0 (,) 1 ) ( prod_ a e. ( 0 ..^ 3 ) ( ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) vts N ) ` x ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x = S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. H ) vts N ) ` x ) x. ( ( ( ( Lam oF x. K ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x )
179 27 101 178 3eqtr3d 
 |-  ( ph -> sum_ n e. ( NN ( repr ` 3 ) N ) ( ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) = S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. H ) vts N ) ` x ) x. ( ( ( ( Lam oF x. K ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x )