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 ffvelrnda 
 |-  ( ( ( 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 ffvelrnda 
 |-  ( ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) /\ a e. ( 0 ..^ 3 ) ) -> ( n ` a ) e. NN )
49 40 48 ffvelrnd 
 |-  ( ( ( 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 ffvelrnd 
 |-  ( ( 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 1ex 
 |-  1 e. _V
76 75 tpid2 
 |-  1 e. { 0 , 1 , 2 }
77 76 58 eleqtrri 
 |-  1 e. ( 0 ..^ 3 )
78 77 a1i 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> 1 e. ( 0 ..^ 3 ) )
79 47 78 ffvelrnd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( n ` 1 ) e. NN )
80 2 ffnd 
 |-  ( ph -> K Fn NN )
81 eqidd 
 |-  ( ( ph /\ ( n ` 1 ) e. NN ) -> ( Lam ` ( n ` 1 ) ) = ( Lam ` ( n ` 1 ) ) )
82 eqidd 
 |-  ( ( ph /\ ( n ` 1 ) e. NN ) -> ( K ` ( n ` 1 ) ) = ( K ` ( n ` 1 ) ) )
83 64 80 16 16 17 81 82 ofval 
 |-  ( ( ph /\ ( n ` 1 ) e. NN ) -> ( ( Lam oF x. K ) ` ( n ` 1 ) ) = ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) )
84 55 79 83 syl2anc 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( ( Lam oF x. K ) ` ( n ` 1 ) ) = ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) )
85 74 84 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 ) ) ) )
86 s3fv2 
 |-  ( ( Lam oF x. K ) e. _V -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 2 ) = ( Lam oF x. K ) )
87 71 86 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 ) )
88 87 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 ) ) )
89 2ex 
 |-  2 e. _V
90 89 tpid3 
 |-  2 e. { 0 , 1 , 2 }
91 90 58 eleqtrri 
 |-  2 e. ( 0 ..^ 3 )
92 91 a1i 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> 2 e. ( 0 ..^ 3 ) )
93 47 92 ffvelrnd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( n ` 2 ) e. NN )
94 eqidd 
 |-  ( ( ph /\ ( n ` 2 ) e. NN ) -> ( Lam ` ( n ` 2 ) ) = ( Lam ` ( n ` 2 ) ) )
95 eqidd 
 |-  ( ( ph /\ ( n ` 2 ) e. NN ) -> ( K ` ( n ` 2 ) ) = ( K ` ( n ` 2 ) ) )
96 64 80 16 16 17 94 95 ofval 
 |-  ( ( ph /\ ( n ` 2 ) e. NN ) -> ( ( Lam oF x. K ) ` ( n ` 2 ) ) = ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) )
97 55 93 96 syl2anc 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( ( Lam oF x. K ) ` ( n ` 2 ) ) = ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) )
98 88 97 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 ) ) ) )
99 85 98 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 ) ) ) ) )
100 70 99 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 ) ) ) ) ) )
101 50 100 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 ) ) ) ) ) )
102 101 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 ) ) ) ) ) )
103 nfv 
 |-  F/ a ( ph /\ x e. ( 0 (,) 1 ) )
104 nfcv 
 |-  F/_ a ( ( ( Lam oF x. H ) vts N ) ` x )
105 fzofi 
 |-  ( 1 ..^ 3 ) e. Fin
106 105 a1i 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( 1 ..^ 3 ) e. Fin )
107 56 a1i 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> 0 e. _V )
108 eqid 
 |-  0 = 0
109 108 orci 
 |-  ( 0 = 0 \/ 0 = 3 )
110 0elfz 
 |-  ( 3 e. NN0 -> 0 e. ( 0 ... 3 ) )
111 elfznelfzob 
 |-  ( 0 e. ( 0 ... 3 ) -> ( -. 0 e. ( 1 ..^ 3 ) <-> ( 0 = 0 \/ 0 = 3 ) ) )
112 44 110 111 mp2b 
 |-  ( -. 0 e. ( 1 ..^ 3 ) <-> ( 0 = 0 \/ 0 = 3 ) )
113 109 112 mpbir 
 |-  -. 0 e. ( 1 ..^ 3 )
114 113 a1i 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> -. 0 e. ( 1 ..^ 3 ) )
115 3 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ a e. ( 1 ..^ 3 ) ) -> N e. NN0 )
116 ioossre 
 |-  ( 0 (,) 1 ) C_ RR
117 ax-resscn 
 |-  RR C_ CC
118 116 117 sstri 
 |-  ( 0 (,) 1 ) C_ CC
119 118 a1i 
 |-  ( ph -> ( 0 (,) 1 ) C_ CC )
120 119 sselda 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> x e. CC )
121 120 adantr 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ a e. ( 1 ..^ 3 ) ) -> x e. CC )
122 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 ) )
123 fzo0ss1 
 |-  ( 1 ..^ 3 ) C_ ( 0 ..^ 3 )
124 123 a1i 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( 1 ..^ 3 ) C_ ( 0 ..^ 3 ) )
125 124 sselda 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ a e. ( 1 ..^ 3 ) ) -> a e. ( 0 ..^ 3 ) )
126 122 125 ffvelrnd 
 |-  ( ( ( 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 ) )
127 126 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 )
128 115 121 127 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 )
129 51 52 ax-mp 
 |-  ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 0 ) = ( Lam oF x. H )
130 28 129 eqtrdi 
 |-  ( a = 0 -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) = ( Lam oF x. H ) )
131 130 oveq1d 
 |-  ( a = 0 -> ( ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) vts N ) = ( ( Lam oF x. H ) vts N ) )
132 131 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 ) )
133 3 adantr 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> N e. NN0 )
134 18 adantr 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( Lam oF x. H ) : NN --> CC )
135 133 120 134 vtscl 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( ( ( Lam oF x. H ) vts N ) ` x ) e. CC )
136 103 104 106 107 114 128 132 135 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 ) ) )
137 uncom 
 |-  ( ( 1 ..^ 3 ) u. { 0 } ) = ( { 0 } u. ( 1 ..^ 3 ) )
138 fzo0sn0fzo1 
 |-  ( 3 e. NN -> ( 0 ..^ 3 ) = ( { 0 } u. ( 1 ..^ 3 ) ) )
139 4 138 ax-mp 
 |-  ( 0 ..^ 3 ) = ( { 0 } u. ( 1 ..^ 3 ) )
140 137 139 eqtr4i 
 |-  ( ( 1 ..^ 3 ) u. { 0 } ) = ( 0 ..^ 3 )
141 140 a1i 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( ( 1 ..^ 3 ) u. { 0 } ) = ( 0 ..^ 3 ) )
142 141 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 ) )
143 fzo13pr 
 |-  ( 1 ..^ 3 ) = { 1 , 2 }
144 143 eleq2i 
 |-  ( a e. ( 1 ..^ 3 ) <-> a e. { 1 , 2 } )
145 vex 
 |-  a e. _V
146 145 elpr 
 |-  ( a e. { 1 , 2 } <-> ( a = 1 \/ a = 2 ) )
147 144 146 bitri 
 |-  ( a e. ( 1 ..^ 3 ) <-> ( a = 1 \/ a = 2 ) )
148 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 ) )
149 71 72 mp1i 
 |-  ( ( ph /\ a = 1 ) -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 1 ) = ( Lam oF x. K ) )
150 148 149 eqtrd 
 |-  ( ( ph /\ a = 1 ) -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) = ( Lam oF x. K ) )
151 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 ) )
152 71 86 mp1i 
 |-  ( ( ph /\ a = 2 ) -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` 2 ) = ( Lam oF x. K ) )
153 151 152 eqtrd 
 |-  ( ( ph /\ a = 2 ) -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) = ( Lam oF x. K ) )
154 150 153 jaodan 
 |-  ( ( ph /\ ( a = 1 \/ a = 2 ) ) -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) = ( Lam oF x. K ) )
155 147 154 sylan2b 
 |-  ( ( ph /\ a e. ( 1 ..^ 3 ) ) -> ( <" ( Lam oF x. H ) ( Lam oF x. K ) ( Lam oF x. K ) "> ` a ) = ( Lam oF x. K ) )
156 155 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 ) )
157 156 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 ) )
158 157 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 ) )
159 158 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 ) )
160 22 adantr 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( Lam oF x. K ) : NN --> CC )
161 133 120 160 vtscl 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( ( ( Lam oF x. K ) vts N ) ` x ) e. CC )
162 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 ) ) ) )
163 106 161 162 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 ) ) ) )
164 nnuz 
 |-  NN = ( ZZ>= ` 1 )
165 4 164 eleqtri 
 |-  3 e. ( ZZ>= ` 1 )
166 hashfzo 
 |-  ( 3 e. ( ZZ>= ` 1 ) -> ( # ` ( 1 ..^ 3 ) ) = ( 3 - 1 ) )
167 165 166 ax-mp 
 |-  ( # ` ( 1 ..^ 3 ) ) = ( 3 - 1 )
168 3m1e2 
 |-  ( 3 - 1 ) = 2
169 167 168 eqtri 
 |-  ( # ` ( 1 ..^ 3 ) ) = 2
170 169 a1i 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( # ` ( 1 ..^ 3 ) ) = 2 )
171 170 oveq2d 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( ( ( ( Lam oF x. K ) vts N ) ` x ) ^ ( # ` ( 1 ..^ 3 ) ) ) = ( ( ( ( Lam oF x. K ) vts N ) ` x ) ^ 2 ) )
172 159 163 171 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 ) )
173 172 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 ) ) )
174 161 sqcld 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( ( ( ( Lam oF x. K ) vts N ) ` x ) ^ 2 ) e. CC )
175 135 174 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 ) ) )
176 173 175 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 ) ) )
177 136 142 176 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 ) ) )
178 177 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 ) ) ) ) )
179 178 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 )
180 27 102 179 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 )