This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fsumvma

Description: Rewrite a sum over the von Mangoldt function as a sum over prime powers. (Contributed by Mario Carneiro, 15-Apr-2016)

Ref Expression
Hypotheses fsumvma.1 
|- ( x = ( p ^ k ) -> B = C )
fsumvma.2 
|- ( ph -> A e. Fin )
fsumvma.3 
|- ( ph -> A C_ NN )
fsumvma.4 
|- ( ph -> P e. Fin )
fsumvma.5 
|- ( ph -> ( ( p e. P /\ k e. K ) <-> ( ( p e. Prime /\ k e. NN ) /\ ( p ^ k ) e. A ) ) )
fsumvma.6 
|- ( ( ph /\ x e. A ) -> B e. CC )
fsumvma.7 
|- ( ( ph /\ ( x e. A /\ ( Lam ` x ) = 0 ) ) -> B = 0 )
Assertion fsumvma 
|- ( ph -> sum_ x e. A B = sum_ p e. P sum_ k e. K C )

Proof

Step Hyp Ref Expression
1 fsumvma.1 
 |-  ( x = ( p ^ k ) -> B = C )
2 fsumvma.2 
 |-  ( ph -> A e. Fin )
3 fsumvma.3 
 |-  ( ph -> A C_ NN )
4 fsumvma.4 
 |-  ( ph -> P e. Fin )
5 fsumvma.5 
 |-  ( ph -> ( ( p e. P /\ k e. K ) <-> ( ( p e. Prime /\ k e. NN ) /\ ( p ^ k ) e. A ) ) )
6 fsumvma.6 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
7 fsumvma.7 
 |-  ( ( ph /\ ( x e. A /\ ( Lam ` x ) = 0 ) ) -> B = 0 )
8 fvexd 
 |-  ( z = <. p , k >. -> ( ^ ` z ) e. _V )
9 fveq2 
 |-  ( z = <. p , k >. -> ( ^ ` z ) = ( ^ ` <. p , k >. ) )
10 df-ov 
 |-  ( p ^ k ) = ( ^ ` <. p , k >. )
11 9 10 eqtr4di 
 |-  ( z = <. p , k >. -> ( ^ ` z ) = ( p ^ k ) )
12 11 eqeq2d 
 |-  ( z = <. p , k >. -> ( x = ( ^ ` z ) <-> x = ( p ^ k ) ) )
13 12 biimpa 
 |-  ( ( z = <. p , k >. /\ x = ( ^ ` z ) ) -> x = ( p ^ k ) )
14 13 1 syl 
 |-  ( ( z = <. p , k >. /\ x = ( ^ ` z ) ) -> B = C )
15 8 14 csbied 
 |-  ( z = <. p , k >. -> [_ ( ^ ` z ) / x ]_ B = C )
16 2 adantr 
 |-  ( ( ph /\ p e. P ) -> A e. Fin )
17 5 biimpd 
 |-  ( ph -> ( ( p e. P /\ k e. K ) -> ( ( p e. Prime /\ k e. NN ) /\ ( p ^ k ) e. A ) ) )
18 17 impl 
 |-  ( ( ( ph /\ p e. P ) /\ k e. K ) -> ( ( p e. Prime /\ k e. NN ) /\ ( p ^ k ) e. A ) )
19 18 simprd 
 |-  ( ( ( ph /\ p e. P ) /\ k e. K ) -> ( p ^ k ) e. A )
20 19 ex 
 |-  ( ( ph /\ p e. P ) -> ( k e. K -> ( p ^ k ) e. A ) )
21 18 simpld 
 |-  ( ( ( ph /\ p e. P ) /\ k e. K ) -> ( p e. Prime /\ k e. NN ) )
22 21 simpld 
 |-  ( ( ( ph /\ p e. P ) /\ k e. K ) -> p e. Prime )
23 22 adantrr 
 |-  ( ( ( ph /\ p e. P ) /\ ( k e. K /\ z e. K ) ) -> p e. Prime )
24 21 simprd 
 |-  ( ( ( ph /\ p e. P ) /\ k e. K ) -> k e. NN )
25 24 adantrr 
 |-  ( ( ( ph /\ p e. P ) /\ ( k e. K /\ z e. K ) ) -> k e. NN )
26 24 ex 
 |-  ( ( ph /\ p e. P ) -> ( k e. K -> k e. NN ) )
27 26 ssrdv 
 |-  ( ( ph /\ p e. P ) -> K C_ NN )
28 27 sselda 
 |-  ( ( ( ph /\ p e. P ) /\ z e. K ) -> z e. NN )
29 28 adantrl 
 |-  ( ( ( ph /\ p e. P ) /\ ( k e. K /\ z e. K ) ) -> z e. NN )
30 eqid 
 |-  p = p
31 prmexpb 
 |-  ( ( ( p e. Prime /\ p e. Prime ) /\ ( k e. NN /\ z e. NN ) ) -> ( ( p ^ k ) = ( p ^ z ) <-> ( p = p /\ k = z ) ) )
32 31 baibd 
 |-  ( ( ( ( p e. Prime /\ p e. Prime ) /\ ( k e. NN /\ z e. NN ) ) /\ p = p ) -> ( ( p ^ k ) = ( p ^ z ) <-> k = z ) )
33 30 32 mpan2 
 |-  ( ( ( p e. Prime /\ p e. Prime ) /\ ( k e. NN /\ z e. NN ) ) -> ( ( p ^ k ) = ( p ^ z ) <-> k = z ) )
34 23 23 25 29 33 syl22anc 
 |-  ( ( ( ph /\ p e. P ) /\ ( k e. K /\ z e. K ) ) -> ( ( p ^ k ) = ( p ^ z ) <-> k = z ) )
35 34 ex 
 |-  ( ( ph /\ p e. P ) -> ( ( k e. K /\ z e. K ) -> ( ( p ^ k ) = ( p ^ z ) <-> k = z ) ) )
36 20 35 dom2lem 
 |-  ( ( ph /\ p e. P ) -> ( k e. K |-> ( p ^ k ) ) : K -1-1-> A )
37 f1fi 
 |-  ( ( A e. Fin /\ ( k e. K |-> ( p ^ k ) ) : K -1-1-> A ) -> K e. Fin )
38 16 36 37 syl2anc 
 |-  ( ( ph /\ p e. P ) -> K e. Fin )
39 1 eleq1d 
 |-  ( x = ( p ^ k ) -> ( B e. CC <-> C e. CC ) )
40 6 ralrimiva 
 |-  ( ph -> A. x e. A B e. CC )
41 40 adantr 
 |-  ( ( ph /\ ( p e. P /\ k e. K ) ) -> A. x e. A B e. CC )
42 5 simplbda 
 |-  ( ( ph /\ ( p e. P /\ k e. K ) ) -> ( p ^ k ) e. A )
43 39 41 42 rspcdva 
 |-  ( ( ph /\ ( p e. P /\ k e. K ) ) -> C e. CC )
44 15 4 38 43 fsum2d 
 |-  ( ph -> sum_ p e. P sum_ k e. K C = sum_ z e. U_ p e. P ( { p } X. K ) [_ ( ^ ` z ) / x ]_ B )
45 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
46 nfcv 
 |-  F/_ y B
47 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
48 45 46 47 cbvsum 
 |-  sum_ x e. ran ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) B = sum_ y e. ran ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) [_ y / x ]_ B
49 csbeq1 
 |-  ( y = ( ^ ` z ) -> [_ y / x ]_ B = [_ ( ^ ` z ) / x ]_ B )
50 snfi 
 |-  { p } e. Fin
51 xpfi 
 |-  ( ( { p } e. Fin /\ K e. Fin ) -> ( { p } X. K ) e. Fin )
52 50 38 51 sylancr 
 |-  ( ( ph /\ p e. P ) -> ( { p } X. K ) e. Fin )
53 52 ralrimiva 
 |-  ( ph -> A. p e. P ( { p } X. K ) e. Fin )
54 iunfi 
 |-  ( ( P e. Fin /\ A. p e. P ( { p } X. K ) e. Fin ) -> U_ p e. P ( { p } X. K ) e. Fin )
55 4 53 54 syl2anc 
 |-  ( ph -> U_ p e. P ( { p } X. K ) e. Fin )
56 fvex 
 |-  ( ^ ` a ) e. _V
57 56 2a1i 
 |-  ( ph -> ( a e. U_ p e. P ( { p } X. K ) -> ( ^ ` a ) e. _V ) )
58 eliunxp 
 |-  ( a e. U_ p e. P ( { p } X. K ) <-> E. p E. k ( a = <. p , k >. /\ ( p e. P /\ k e. K ) ) )
59 5 simprbda 
 |-  ( ( ph /\ ( p e. P /\ k e. K ) ) -> ( p e. Prime /\ k e. NN ) )
60 opelxp 
 |-  ( <. p , k >. e. ( Prime X. NN ) <-> ( p e. Prime /\ k e. NN ) )
61 59 60 sylibr 
 |-  ( ( ph /\ ( p e. P /\ k e. K ) ) -> <. p , k >. e. ( Prime X. NN ) )
62 eleq1 
 |-  ( a = <. p , k >. -> ( a e. ( Prime X. NN ) <-> <. p , k >. e. ( Prime X. NN ) ) )
63 61 62 syl5ibrcom 
 |-  ( ( ph /\ ( p e. P /\ k e. K ) ) -> ( a = <. p , k >. -> a e. ( Prime X. NN ) ) )
64 63 impancom 
 |-  ( ( ph /\ a = <. p , k >. ) -> ( ( p e. P /\ k e. K ) -> a e. ( Prime X. NN ) ) )
65 64 expimpd 
 |-  ( ph -> ( ( a = <. p , k >. /\ ( p e. P /\ k e. K ) ) -> a e. ( Prime X. NN ) ) )
66 65 exlimdvv 
 |-  ( ph -> ( E. p E. k ( a = <. p , k >. /\ ( p e. P /\ k e. K ) ) -> a e. ( Prime X. NN ) ) )
67 58 66 biimtrid 
 |-  ( ph -> ( a e. U_ p e. P ( { p } X. K ) -> a e. ( Prime X. NN ) ) )
68 67 ssrdv 
 |-  ( ph -> U_ p e. P ( { p } X. K ) C_ ( Prime X. NN ) )
69 68 sseld 
 |-  ( ph -> ( b e. U_ p e. P ( { p } X. K ) -> b e. ( Prime X. NN ) ) )
70 67 69 anim12d 
 |-  ( ph -> ( ( a e. U_ p e. P ( { p } X. K ) /\ b e. U_ p e. P ( { p } X. K ) ) -> ( a e. ( Prime X. NN ) /\ b e. ( Prime X. NN ) ) ) )
71 1st2nd2 
 |-  ( a e. ( Prime X. NN ) -> a = <. ( 1st ` a ) , ( 2nd ` a ) >. )
72 71 fveq2d 
 |-  ( a e. ( Prime X. NN ) -> ( ^ ` a ) = ( ^ ` <. ( 1st ` a ) , ( 2nd ` a ) >. ) )
73 df-ov 
 |-  ( ( 1st ` a ) ^ ( 2nd ` a ) ) = ( ^ ` <. ( 1st ` a ) , ( 2nd ` a ) >. )
74 72 73 eqtr4di 
 |-  ( a e. ( Prime X. NN ) -> ( ^ ` a ) = ( ( 1st ` a ) ^ ( 2nd ` a ) ) )
75 1st2nd2 
 |-  ( b e. ( Prime X. NN ) -> b = <. ( 1st ` b ) , ( 2nd ` b ) >. )
76 75 fveq2d 
 |-  ( b e. ( Prime X. NN ) -> ( ^ ` b ) = ( ^ ` <. ( 1st ` b ) , ( 2nd ` b ) >. ) )
77 df-ov 
 |-  ( ( 1st ` b ) ^ ( 2nd ` b ) ) = ( ^ ` <. ( 1st ` b ) , ( 2nd ` b ) >. )
78 76 77 eqtr4di 
 |-  ( b e. ( Prime X. NN ) -> ( ^ ` b ) = ( ( 1st ` b ) ^ ( 2nd ` b ) ) )
79 74 78 eqeqan12d 
 |-  ( ( a e. ( Prime X. NN ) /\ b e. ( Prime X. NN ) ) -> ( ( ^ ` a ) = ( ^ ` b ) <-> ( ( 1st ` a ) ^ ( 2nd ` a ) ) = ( ( 1st ` b ) ^ ( 2nd ` b ) ) ) )
80 xp1st 
 |-  ( a e. ( Prime X. NN ) -> ( 1st ` a ) e. Prime )
81 xp2nd 
 |-  ( a e. ( Prime X. NN ) -> ( 2nd ` a ) e. NN )
82 80 81 jca 
 |-  ( a e. ( Prime X. NN ) -> ( ( 1st ` a ) e. Prime /\ ( 2nd ` a ) e. NN ) )
83 xp1st 
 |-  ( b e. ( Prime X. NN ) -> ( 1st ` b ) e. Prime )
84 xp2nd 
 |-  ( b e. ( Prime X. NN ) -> ( 2nd ` b ) e. NN )
85 83 84 jca 
 |-  ( b e. ( Prime X. NN ) -> ( ( 1st ` b ) e. Prime /\ ( 2nd ` b ) e. NN ) )
86 prmexpb 
 |-  ( ( ( ( 1st ` a ) e. Prime /\ ( 1st ` b ) e. Prime ) /\ ( ( 2nd ` a ) e. NN /\ ( 2nd ` b ) e. NN ) ) -> ( ( ( 1st ` a ) ^ ( 2nd ` a ) ) = ( ( 1st ` b ) ^ ( 2nd ` b ) ) <-> ( ( 1st ` a ) = ( 1st ` b ) /\ ( 2nd ` a ) = ( 2nd ` b ) ) ) )
87 86 an4s 
 |-  ( ( ( ( 1st ` a ) e. Prime /\ ( 2nd ` a ) e. NN ) /\ ( ( 1st ` b ) e. Prime /\ ( 2nd ` b ) e. NN ) ) -> ( ( ( 1st ` a ) ^ ( 2nd ` a ) ) = ( ( 1st ` b ) ^ ( 2nd ` b ) ) <-> ( ( 1st ` a ) = ( 1st ` b ) /\ ( 2nd ` a ) = ( 2nd ` b ) ) ) )
88 82 85 87 syl2an 
 |-  ( ( a e. ( Prime X. NN ) /\ b e. ( Prime X. NN ) ) -> ( ( ( 1st ` a ) ^ ( 2nd ` a ) ) = ( ( 1st ` b ) ^ ( 2nd ` b ) ) <-> ( ( 1st ` a ) = ( 1st ` b ) /\ ( 2nd ` a ) = ( 2nd ` b ) ) ) )
89 xpopth 
 |-  ( ( a e. ( Prime X. NN ) /\ b e. ( Prime X. NN ) ) -> ( ( ( 1st ` a ) = ( 1st ` b ) /\ ( 2nd ` a ) = ( 2nd ` b ) ) <-> a = b ) )
90 79 88 89 3bitrd 
 |-  ( ( a e. ( Prime X. NN ) /\ b e. ( Prime X. NN ) ) -> ( ( ^ ` a ) = ( ^ ` b ) <-> a = b ) )
91 70 90 syl6 
 |-  ( ph -> ( ( a e. U_ p e. P ( { p } X. K ) /\ b e. U_ p e. P ( { p } X. K ) ) -> ( ( ^ ` a ) = ( ^ ` b ) <-> a = b ) ) )
92 57 91 dom2lem 
 |-  ( ph -> ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) : U_ p e. P ( { p } X. K ) -1-1-> _V )
93 f1f1orn 
 |-  ( ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) : U_ p e. P ( { p } X. K ) -1-1-> _V -> ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) : U_ p e. P ( { p } X. K ) -1-1-onto-> ran ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) )
94 92 93 syl 
 |-  ( ph -> ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) : U_ p e. P ( { p } X. K ) -1-1-onto-> ran ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) )
95 fveq2 
 |-  ( a = z -> ( ^ ` a ) = ( ^ ` z ) )
96 eqid 
 |-  ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) = ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) )
97 fvex 
 |-  ( ^ ` z ) e. _V
98 95 96 97 fvmpt 
 |-  ( z e. U_ p e. P ( { p } X. K ) -> ( ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) ` z ) = ( ^ ` z ) )
99 98 adantl 
 |-  ( ( ph /\ z e. U_ p e. P ( { p } X. K ) ) -> ( ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) ` z ) = ( ^ ` z ) )
100 fveq2 
 |-  ( a = <. p , k >. -> ( ^ ` a ) = ( ^ ` <. p , k >. ) )
101 100 10 eqtr4di 
 |-  ( a = <. p , k >. -> ( ^ ` a ) = ( p ^ k ) )
102 101 eleq1d 
 |-  ( a = <. p , k >. -> ( ( ^ ` a ) e. A <-> ( p ^ k ) e. A ) )
103 42 102 syl5ibrcom 
 |-  ( ( ph /\ ( p e. P /\ k e. K ) ) -> ( a = <. p , k >. -> ( ^ ` a ) e. A ) )
104 103 impancom 
 |-  ( ( ph /\ a = <. p , k >. ) -> ( ( p e. P /\ k e. K ) -> ( ^ ` a ) e. A ) )
105 104 expimpd 
 |-  ( ph -> ( ( a = <. p , k >. /\ ( p e. P /\ k e. K ) ) -> ( ^ ` a ) e. A ) )
106 105 exlimdvv 
 |-  ( ph -> ( E. p E. k ( a = <. p , k >. /\ ( p e. P /\ k e. K ) ) -> ( ^ ` a ) e. A ) )
107 58 106 biimtrid 
 |-  ( ph -> ( a e. U_ p e. P ( { p } X. K ) -> ( ^ ` a ) e. A ) )
108 107 imp 
 |-  ( ( ph /\ a e. U_ p e. P ( { p } X. K ) ) -> ( ^ ` a ) e. A )
109 108 fmpttd 
 |-  ( ph -> ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) : U_ p e. P ( { p } X. K ) --> A )
110 109 frnd 
 |-  ( ph -> ran ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) C_ A )
111 110 sselda 
 |-  ( ( ph /\ y e. ran ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) ) -> y e. A )
112 47 nfel1 
 |-  F/ x [_ y / x ]_ B e. CC
113 45 eleq1d 
 |-  ( x = y -> ( B e. CC <-> [_ y / x ]_ B e. CC ) )
114 112 113 rspc 
 |-  ( y e. A -> ( A. x e. A B e. CC -> [_ y / x ]_ B e. CC ) )
115 40 114 mpan9 
 |-  ( ( ph /\ y e. A ) -> [_ y / x ]_ B e. CC )
116 111 115 syldan 
 |-  ( ( ph /\ y e. ran ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) ) -> [_ y / x ]_ B e. CC )
117 49 55 94 99 116 fsumf1o 
 |-  ( ph -> sum_ y e. ran ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) [_ y / x ]_ B = sum_ z e. U_ p e. P ( { p } X. K ) [_ ( ^ ` z ) / x ]_ B )
118 48 117 eqtrid 
 |-  ( ph -> sum_ x e. ran ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) B = sum_ z e. U_ p e. P ( { p } X. K ) [_ ( ^ ` z ) / x ]_ B )
119 110 sselda 
 |-  ( ( ph /\ x e. ran ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) ) -> x e. A )
120 119 6 syldan 
 |-  ( ( ph /\ x e. ran ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) ) -> B e. CC )
121 eldif 
 |-  ( x e. ( A \ ran ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) ) <-> ( x e. A /\ -. x e. ran ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) ) )
122 96 56 elrnmpti 
 |-  ( x e. ran ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) <-> E. a e. U_ p e. P ( { p } X. K ) x = ( ^ ` a ) )
123 101 eqeq2d 
 |-  ( a = <. p , k >. -> ( x = ( ^ ` a ) <-> x = ( p ^ k ) ) )
124 123 rexiunxp 
 |-  ( E. a e. U_ p e. P ( { p } X. K ) x = ( ^ ` a ) <-> E. p e. P E. k e. K x = ( p ^ k ) )
125 122 124 bitri 
 |-  ( x e. ran ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) <-> E. p e. P E. k e. K x = ( p ^ k ) )
126 simpr 
 |-  ( ( ( ph /\ x e. A ) /\ x = ( p ^ k ) ) -> x = ( p ^ k ) )
127 simplr 
 |-  ( ( ( ph /\ x e. A ) /\ x = ( p ^ k ) ) -> x e. A )
128 126 127 eqeltrrd 
 |-  ( ( ( ph /\ x e. A ) /\ x = ( p ^ k ) ) -> ( p ^ k ) e. A )
129 5 rbaibd 
 |-  ( ( ph /\ ( p ^ k ) e. A ) -> ( ( p e. P /\ k e. K ) <-> ( p e. Prime /\ k e. NN ) ) )
130 129 adantlr 
 |-  ( ( ( ph /\ x e. A ) /\ ( p ^ k ) e. A ) -> ( ( p e. P /\ k e. K ) <-> ( p e. Prime /\ k e. NN ) ) )
131 128 130 syldan 
 |-  ( ( ( ph /\ x e. A ) /\ x = ( p ^ k ) ) -> ( ( p e. P /\ k e. K ) <-> ( p e. Prime /\ k e. NN ) ) )
132 131 pm5.32da 
 |-  ( ( ph /\ x e. A ) -> ( ( x = ( p ^ k ) /\ ( p e. P /\ k e. K ) ) <-> ( x = ( p ^ k ) /\ ( p e. Prime /\ k e. NN ) ) ) )
133 ancom 
 |-  ( ( ( p e. P /\ k e. K ) /\ x = ( p ^ k ) ) <-> ( x = ( p ^ k ) /\ ( p e. P /\ k e. K ) ) )
134 ancom 
 |-  ( ( ( p e. Prime /\ k e. NN ) /\ x = ( p ^ k ) ) <-> ( x = ( p ^ k ) /\ ( p e. Prime /\ k e. NN ) ) )
135 132 133 134 3bitr4g 
 |-  ( ( ph /\ x e. A ) -> ( ( ( p e. P /\ k e. K ) /\ x = ( p ^ k ) ) <-> ( ( p e. Prime /\ k e. NN ) /\ x = ( p ^ k ) ) ) )
136 135 2exbidv 
 |-  ( ( ph /\ x e. A ) -> ( E. p E. k ( ( p e. P /\ k e. K ) /\ x = ( p ^ k ) ) <-> E. p E. k ( ( p e. Prime /\ k e. NN ) /\ x = ( p ^ k ) ) ) )
137 r2ex 
 |-  ( E. p e. P E. k e. K x = ( p ^ k ) <-> E. p E. k ( ( p e. P /\ k e. K ) /\ x = ( p ^ k ) ) )
138 r2ex 
 |-  ( E. p e. Prime E. k e. NN x = ( p ^ k ) <-> E. p E. k ( ( p e. Prime /\ k e. NN ) /\ x = ( p ^ k ) ) )
139 136 137 138 3bitr4g 
 |-  ( ( ph /\ x e. A ) -> ( E. p e. P E. k e. K x = ( p ^ k ) <-> E. p e. Prime E. k e. NN x = ( p ^ k ) ) )
140 3 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. NN )
141 isppw2 
 |-  ( x e. NN -> ( ( Lam ` x ) =/= 0 <-> E. p e. Prime E. k e. NN x = ( p ^ k ) ) )
142 140 141 syl 
 |-  ( ( ph /\ x e. A ) -> ( ( Lam ` x ) =/= 0 <-> E. p e. Prime E. k e. NN x = ( p ^ k ) ) )
143 139 142 bitr4d 
 |-  ( ( ph /\ x e. A ) -> ( E. p e. P E. k e. K x = ( p ^ k ) <-> ( Lam ` x ) =/= 0 ) )
144 125 143 bitrid 
 |-  ( ( ph /\ x e. A ) -> ( x e. ran ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) <-> ( Lam ` x ) =/= 0 ) )
145 144 necon2bbid 
 |-  ( ( ph /\ x e. A ) -> ( ( Lam ` x ) = 0 <-> -. x e. ran ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) ) )
146 145 pm5.32da 
 |-  ( ph -> ( ( x e. A /\ ( Lam ` x ) = 0 ) <-> ( x e. A /\ -. x e. ran ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) ) ) )
147 7 ex 
 |-  ( ph -> ( ( x e. A /\ ( Lam ` x ) = 0 ) -> B = 0 ) )
148 146 147 sylbird 
 |-  ( ph -> ( ( x e. A /\ -. x e. ran ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) ) -> B = 0 ) )
149 121 148 biimtrid 
 |-  ( ph -> ( x e. ( A \ ran ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) ) -> B = 0 ) )
150 149 imp 
 |-  ( ( ph /\ x e. ( A \ ran ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) ) ) -> B = 0 )
151 110 120 150 2 fsumss 
 |-  ( ph -> sum_ x e. ran ( a e. U_ p e. P ( { p } X. K ) |-> ( ^ ` a ) ) B = sum_ x e. A B )
152 44 118 151 3eqtr2rd 
 |-  ( ph -> sum_ x e. A B = sum_ p e. P sum_ k e. K C )