Metamath Proof Explorer

Theorem esumcst

Description: The extended sum of a constant. (Contributed by Thierry Arnoux, 3-Mar-2017) (Revised by Thierry Arnoux, 5-Jul-2017)

Ref Expression
Hypotheses esumcst.1 
|- F/_ k A
esumcst.2 
|- F/_ k B
Assertion esumcst 
|- ( ( A e. V /\ B e. ( 0 [,] +oo ) ) -> sum* k e. A B = ( ( # ` A ) *e B ) )

Proof

Step Hyp Ref Expression
1 esumcst.1 
 |-  F/_ k A
2 esumcst.2 
 |-  F/_ k B
3 1 nfel1 
 |-  F/ k A e. V
4 2 nfel1 
 |-  F/ k B e. ( 0 [,] +oo )
5 3 4 nfan 
 |-  F/ k ( A e. V /\ B e. ( 0 [,] +oo ) )
6 simpl 
 |-  ( ( A e. V /\ B e. ( 0 [,] +oo ) ) -> A e. V )
7 simplr 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ k e. A ) -> B e. ( 0 [,] +oo ) )
8 xrge0tmd 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. TopMnd
9 tmdmnd 
 |-  ( ( RR*s |`s ( 0 [,] +oo ) ) e. TopMnd -> ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd )
10 8 9 ax-mp 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd
11 10 a1i 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ x e. ( ~P A i^i Fin ) ) -> ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd )
12 inss2 
 |-  ( ~P A i^i Fin ) C_ Fin
13 simpr 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ x e. ( ~P A i^i Fin ) ) -> x e. ( ~P A i^i Fin ) )
14 12 13 sseldi 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ x e. ( ~P A i^i Fin ) ) -> x e. Fin )
15 simplr 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ x e. ( ~P A i^i Fin ) ) -> B e. ( 0 [,] +oo ) )
16 xrge0base 
 |-  ( 0 [,] +oo ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) )
17 eqid 
 |-  ( .g ` ( RR*s |`s ( 0 [,] +oo ) ) ) = ( .g ` ( RR*s |`s ( 0 [,] +oo ) ) )
18 2 16 17 gsumconstf 
 |-  ( ( ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd /\ x e. Fin /\ B e. ( 0 [,] +oo ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) = ( ( # ` x ) ( .g ` ( RR*s |`s ( 0 [,] +oo ) ) ) B ) )
19 11 14 15 18 syl3anc 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ x e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) = ( ( # ` x ) ( .g ` ( RR*s |`s ( 0 [,] +oo ) ) ) B ) )
20 hashcl 
 |-  ( x e. Fin -> ( # ` x ) e. NN0 )
21 14 20 syl 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ x e. ( ~P A i^i Fin ) ) -> ( # ` x ) e. NN0 )
22 xrge0mulgnn0 
 |-  ( ( ( # ` x ) e. NN0 /\ B e. ( 0 [,] +oo ) ) -> ( ( # ` x ) ( .g ` ( RR*s |`s ( 0 [,] +oo ) ) ) B ) = ( ( # ` x ) *e B ) )
23 21 15 22 syl2anc 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ x e. ( ~P A i^i Fin ) ) -> ( ( # ` x ) ( .g ` ( RR*s |`s ( 0 [,] +oo ) ) ) B ) = ( ( # ` x ) *e B ) )
24 19 23 eqtrd 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ x e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> B ) ) = ( ( # ` x ) *e B ) )
25 5 1 6 7 24 esumval 
 |-  ( ( A e. V /\ B e. ( 0 [,] +oo ) ) -> sum* k e. A B = sup ( ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) , RR* , < ) )
26 nn0ssre 
 |-  NN0 C_ RR
27 ressxr 
 |-  RR C_ RR*
28 26 27 sstri 
 |-  NN0 C_ RR*
29 pnfxr 
 |-  +oo e. RR*
30 snssi 
 |-  ( +oo e. RR* -> { +oo } C_ RR* )
31 29 30 ax-mp 
 |-  { +oo } C_ RR*
32 28 31 unssi 
 |-  ( NN0 u. { +oo } ) C_ RR*
33 hashf 
 |-  # : _V --> ( NN0 u. { +oo } )
34 vex 
 |-  x e. _V
35 ffvelrn 
 |-  ( ( # : _V --> ( NN0 u. { +oo } ) /\ x e. _V ) -> ( # ` x ) e. ( NN0 u. { +oo } ) )
36 33 34 35 mp2an 
 |-  ( # ` x ) e. ( NN0 u. { +oo } )
37 32 36 sselii 
 |-  ( # ` x ) e. RR*
38 37 a1i 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ x e. ( ~P A i^i Fin ) ) -> ( # ` x ) e. RR* )
39 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
40 simpr 
 |-  ( ( A e. V /\ B e. ( 0 [,] +oo ) ) -> B e. ( 0 [,] +oo ) )
41 39 40 sseldi 
 |-  ( ( A e. V /\ B e. ( 0 [,] +oo ) ) -> B e. RR* )
42 41 adantr 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ x e. ( ~P A i^i Fin ) ) -> B e. RR* )
43 38 42 xmulcld 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ x e. ( ~P A i^i Fin ) ) -> ( ( # ` x ) *e B ) e. RR* )
44 43 fmpttd 
 |-  ( ( A e. V /\ B e. ( 0 [,] +oo ) ) -> ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) : ( ~P A i^i Fin ) --> RR* )
45 44 frnd 
 |-  ( ( A e. V /\ B e. ( 0 [,] +oo ) ) -> ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) C_ RR* )
46 hashxrcl 
 |-  ( A e. V -> ( # ` A ) e. RR* )
47 46 adantr 
 |-  ( ( A e. V /\ B e. ( 0 [,] +oo ) ) -> ( # ` A ) e. RR* )
48 47 41 xmulcld 
 |-  ( ( A e. V /\ B e. ( 0 [,] +oo ) ) -> ( ( # ` A ) *e B ) e. RR* )
49 vex 
 |-  y e. _V
50 eqid 
 |-  ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) = ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) )
51 50 elrnmpt 
 |-  ( y e. _V -> ( y e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) <-> E. x e. ( ~P A i^i Fin ) y = ( ( # ` x ) *e B ) ) )
52 49 51 ax-mp 
 |-  ( y e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) <-> E. x e. ( ~P A i^i Fin ) y = ( ( # ` x ) *e B ) )
53 52 biimpi 
 |-  ( y e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) -> E. x e. ( ~P A i^i Fin ) y = ( ( # ` x ) *e B ) )
54 47 adantr 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ x e. ( ~P A i^i Fin ) ) -> ( # ` A ) e. RR* )
55 0xr 
 |-  0 e. RR*
56 55 a1i 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ x e. ( ~P A i^i Fin ) ) -> 0 e. RR* )
57 29 a1i 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ x e. ( ~P A i^i Fin ) ) -> +oo e. RR* )
58 iccgelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ B e. ( 0 [,] +oo ) ) -> 0 <_ B )
59 56 57 15 58 syl3anc 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ x e. ( ~P A i^i Fin ) ) -> 0 <_ B )
60 42 59 jca 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ x e. ( ~P A i^i Fin ) ) -> ( B e. RR* /\ 0 <_ B ) )
61 6 adantr 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ x e. ( ~P A i^i Fin ) ) -> A e. V )
62 inss1 
 |-  ( ~P A i^i Fin ) C_ ~P A
63 62 sseli 
 |-  ( x e. ( ~P A i^i Fin ) -> x e. ~P A )
64 elpwi 
 |-  ( x e. ~P A -> x C_ A )
65 13 63 64 3syl 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ x e. ( ~P A i^i Fin ) ) -> x C_ A )
66 ssdomg 
 |-  ( A e. V -> ( x C_ A -> x ~<_ A ) )
67 61 65 66 sylc 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ x e. ( ~P A i^i Fin ) ) -> x ~<_ A )
68 hashdomi 
 |-  ( x ~<_ A -> ( # ` x ) <_ ( # ` A ) )
69 67 68 syl 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ x e. ( ~P A i^i Fin ) ) -> ( # ` x ) <_ ( # ` A ) )
70 xlemul1a 
 |-  ( ( ( ( # ` x ) e. RR* /\ ( # ` A ) e. RR* /\ ( B e. RR* /\ 0 <_ B ) ) /\ ( # ` x ) <_ ( # ` A ) ) -> ( ( # ` x ) *e B ) <_ ( ( # ` A ) *e B ) )
71 38 54 60 69 70 syl31anc 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ x e. ( ~P A i^i Fin ) ) -> ( ( # ` x ) *e B ) <_ ( ( # ` A ) *e B ) )
72 71 ralrimiva 
 |-  ( ( A e. V /\ B e. ( 0 [,] +oo ) ) -> A. x e. ( ~P A i^i Fin ) ( ( # ` x ) *e B ) <_ ( ( # ` A ) *e B ) )
73 r19.29r 
 |-  ( ( E. x e. ( ~P A i^i Fin ) y = ( ( # ` x ) *e B ) /\ A. x e. ( ~P A i^i Fin ) ( ( # ` x ) *e B ) <_ ( ( # ` A ) *e B ) ) -> E. x e. ( ~P A i^i Fin ) ( y = ( ( # ` x ) *e B ) /\ ( ( # ` x ) *e B ) <_ ( ( # ` A ) *e B ) ) )
74 53 72 73 syl2anr 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) ) -> E. x e. ( ~P A i^i Fin ) ( y = ( ( # ` x ) *e B ) /\ ( ( # ` x ) *e B ) <_ ( ( # ` A ) *e B ) ) )
75 simpl 
 |-  ( ( y = ( ( # ` x ) *e B ) /\ ( ( # ` x ) *e B ) <_ ( ( # ` A ) *e B ) ) -> y = ( ( # ` x ) *e B ) )
76 simpr 
 |-  ( ( y = ( ( # ` x ) *e B ) /\ ( ( # ` x ) *e B ) <_ ( ( # ` A ) *e B ) ) -> ( ( # ` x ) *e B ) <_ ( ( # ` A ) *e B ) )
77 75 76 eqbrtrd 
 |-  ( ( y = ( ( # ` x ) *e B ) /\ ( ( # ` x ) *e B ) <_ ( ( # ` A ) *e B ) ) -> y <_ ( ( # ` A ) *e B ) )
78 77 rexlimivw 
 |-  ( E. x e. ( ~P A i^i Fin ) ( y = ( ( # ` x ) *e B ) /\ ( ( # ` x ) *e B ) <_ ( ( # ` A ) *e B ) ) -> y <_ ( ( # ` A ) *e B ) )
79 74 78 syl 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) ) -> y <_ ( ( # ` A ) *e B ) )
80 79 ralrimiva 
 |-  ( ( A e. V /\ B e. ( 0 [,] +oo ) ) -> A. y e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) y <_ ( ( # ` A ) *e B ) )
81 pwidg 
 |-  ( A e. Fin -> A e. ~P A )
82 81 ancri 
 |-  ( A e. Fin -> ( A e. ~P A /\ A e. Fin ) )
83 elin 
 |-  ( A e. ( ~P A i^i Fin ) <-> ( A e. ~P A /\ A e. Fin ) )
84 82 83 sylibr 
 |-  ( A e. Fin -> A e. ( ~P A i^i Fin ) )
85 eqid 
 |-  ( ( # ` A ) *e B ) = ( ( # ` A ) *e B )
86 fveq2 
 |-  ( x = A -> ( # ` x ) = ( # ` A ) )
87 86 oveq1d 
 |-  ( x = A -> ( ( # ` x ) *e B ) = ( ( # ` A ) *e B ) )
88 87 rspceeqv 
 |-  ( ( A e. ( ~P A i^i Fin ) /\ ( ( # ` A ) *e B ) = ( ( # ` A ) *e B ) ) -> E. x e. ( ~P A i^i Fin ) ( ( # ` A ) *e B ) = ( ( # ` x ) *e B ) )
89 85 88 mpan2 
 |-  ( A e. ( ~P A i^i Fin ) -> E. x e. ( ~P A i^i Fin ) ( ( # ` A ) *e B ) = ( ( # ` x ) *e B ) )
90 ovex 
 |-  ( ( # ` A ) *e B ) e. _V
91 50 elrnmpt 
 |-  ( ( ( # ` A ) *e B ) e. _V -> ( ( ( # ` A ) *e B ) e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) <-> E. x e. ( ~P A i^i Fin ) ( ( # ` A ) *e B ) = ( ( # ` x ) *e B ) ) )
92 90 91 ax-mp 
 |-  ( ( ( # ` A ) *e B ) e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) <-> E. x e. ( ~P A i^i Fin ) ( ( # ` A ) *e B ) = ( ( # ` x ) *e B ) )
93 89 92 sylibr 
 |-  ( A e. ( ~P A i^i Fin ) -> ( ( # ` A ) *e B ) e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) )
94 84 93 syl 
 |-  ( A e. Fin -> ( ( # ` A ) *e B ) e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) )
95 94 adantl 
 |-  ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ A e. Fin ) -> ( ( # ` A ) *e B ) e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) )
96 simplr 
 |-  ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ A e. Fin ) -> y < ( ( # ` A ) *e B ) )
97 breq2 
 |-  ( z = ( ( # ` A ) *e B ) -> ( y < z <-> y < ( ( # ` A ) *e B ) ) )
98 97 rspcev 
 |-  ( ( ( ( # ` A ) *e B ) e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) /\ y < ( ( # ` A ) *e B ) ) -> E. z e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) y < z )
99 95 96 98 syl2anc 
 |-  ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ A e. Fin ) -> E. z e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) y < z )
100 0elpw 
 |-  (/) e. ~P A
101 0fin 
 |-  (/) e. Fin
102 elin 
 |-  ( (/) e. ( ~P A i^i Fin ) <-> ( (/) e. ~P A /\ (/) e. Fin ) )
103 100 101 102 mpbir2an 
 |-  (/) e. ( ~P A i^i Fin )
104 103 a1i 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B = 0 ) -> (/) e. ( ~P A i^i Fin ) )
105 simpr 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B = 0 ) -> B = 0 )
106 105 oveq2d 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B = 0 ) -> ( ( # ` (/) ) *e B ) = ( ( # ` (/) ) *e 0 ) )
107 hash0 
 |-  ( # ` (/) ) = 0
108 107 55 eqeltri 
 |-  ( # ` (/) ) e. RR*
109 xmul01 
 |-  ( ( # ` (/) ) e. RR* -> ( ( # ` (/) ) *e 0 ) = 0 )
110 108 109 ax-mp 
 |-  ( ( # ` (/) ) *e 0 ) = 0
111 106 110 eqtr2di 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B = 0 ) -> 0 = ( ( # ` (/) ) *e B ) )
112 fveq2 
 |-  ( x = (/) -> ( # ` x ) = ( # ` (/) ) )
113 112 oveq1d 
 |-  ( x = (/) -> ( ( # ` x ) *e B ) = ( ( # ` (/) ) *e B ) )
114 113 rspceeqv 
 |-  ( ( (/) e. ( ~P A i^i Fin ) /\ 0 = ( ( # ` (/) ) *e B ) ) -> E. x e. ( ~P A i^i Fin ) 0 = ( ( # ` x ) *e B ) )
115 104 111 114 syl2anc 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B = 0 ) -> E. x e. ( ~P A i^i Fin ) 0 = ( ( # ` x ) *e B ) )
116 ovex 
 |-  ( ( # ` x ) *e B ) e. _V
117 50 116 elrnmpti 
 |-  ( 0 e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) <-> E. x e. ( ~P A i^i Fin ) 0 = ( ( # ` x ) *e B ) )
118 115 117 sylibr 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B = 0 ) -> 0 e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) )
119 simpllr 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B = 0 ) -> y < ( ( # ` A ) *e B ) )
120 105 oveq2d 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B = 0 ) -> ( ( # ` A ) *e B ) = ( ( # ` A ) *e 0 ) )
121 47 ad4antr 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B = 0 ) -> ( # ` A ) e. RR* )
122 xmul01 
 |-  ( ( # ` A ) e. RR* -> ( ( # ` A ) *e 0 ) = 0 )
123 121 122 syl 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B = 0 ) -> ( ( # ` A ) *e 0 ) = 0 )
124 120 123 eqtrd 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B = 0 ) -> ( ( # ` A ) *e B ) = 0 )
125 119 124 breqtrd 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B = 0 ) -> y < 0 )
126 breq2 
 |-  ( z = 0 -> ( y < z <-> y < 0 ) )
127 126 rspcev 
 |-  ( ( 0 e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) /\ y < 0 ) -> E. z e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) y < z )
128 118 125 127 syl2anc 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B = 0 ) -> E. z e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) y < z )
129 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) /\ n e. NN ) /\ ( y / B ) < n ) /\ a e. ~P A ) /\ ( # ` a ) = n ) -> a e. ~P A )
130 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) /\ n e. NN ) /\ ( y / B ) < n ) /\ a e. ~P A ) /\ ( # ` a ) = n ) -> ( # ` a ) = n )
131 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) /\ n e. NN ) /\ ( y / B ) < n ) /\ a e. ~P A ) /\ ( # ` a ) = n ) -> n e. NN )
132 130 131 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) /\ n e. NN ) /\ ( y / B ) < n ) /\ a e. ~P A ) /\ ( # ` a ) = n ) -> ( # ` a ) e. NN )
133 nnnn0 
 |-  ( ( # ` a ) e. NN -> ( # ` a ) e. NN0 )
134 vex 
 |-  a e. _V
135 hashclb 
 |-  ( a e. _V -> ( a e. Fin <-> ( # ` a ) e. NN0 ) )
136 134 135 ax-mp 
 |-  ( a e. Fin <-> ( # ` a ) e. NN0 )
137 133 136 sylibr 
 |-  ( ( # ` a ) e. NN -> a e. Fin )
138 132 137 syl 
 |-  ( ( ( ( ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) /\ n e. NN ) /\ ( y / B ) < n ) /\ a e. ~P A ) /\ ( # ` a ) = n ) -> a e. Fin )
139 129 138 elind 
 |-  ( ( ( ( ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) /\ n e. NN ) /\ ( y / B ) < n ) /\ a e. ~P A ) /\ ( # ` a ) = n ) -> a e. ( ~P A i^i Fin ) )
140 eqidd 
 |-  ( ( ( ( ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) /\ n e. NN ) /\ ( y / B ) < n ) /\ a e. ~P A ) /\ ( # ` a ) = n ) -> ( ( # ` a ) *e B ) = ( ( # ` a ) *e B ) )
141 fveq2 
 |-  ( x = a -> ( # ` x ) = ( # ` a ) )
142 141 oveq1d 
 |-  ( x = a -> ( ( # ` x ) *e B ) = ( ( # ` a ) *e B ) )
143 142 rspceeqv 
 |-  ( ( a e. ( ~P A i^i Fin ) /\ ( ( # ` a ) *e B ) = ( ( # ` a ) *e B ) ) -> E. x e. ( ~P A i^i Fin ) ( ( # ` a ) *e B ) = ( ( # ` x ) *e B ) )
144 139 140 143 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) /\ n e. NN ) /\ ( y / B ) < n ) /\ a e. ~P A ) /\ ( # ` a ) = n ) -> E. x e. ( ~P A i^i Fin ) ( ( # ` a ) *e B ) = ( ( # ` x ) *e B ) )
145 50 116 elrnmpti 
 |-  ( ( ( # ` a ) *e B ) e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) <-> E. x e. ( ~P A i^i Fin ) ( ( # ` a ) *e B ) = ( ( # ` x ) *e B ) )
146 144 145 sylibr 
 |-  ( ( ( ( ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) /\ n e. NN ) /\ ( y / B ) < n ) /\ a e. ~P A ) /\ ( # ` a ) = n ) -> ( ( # ` a ) *e B ) e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) )
147 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) /\ n e. NN ) /\ ( y / B ) < n ) /\ a e. ~P A ) /\ ( # ` a ) = n ) -> ( y / B ) < n )
148 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) /\ n e. NN ) /\ ( y / B ) < n ) /\ a e. ~P A ) /\ ( # ` a ) = n ) -> y e. RR )
149 131 nnred 
 |-  ( ( ( ( ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) /\ n e. NN ) /\ ( y / B ) < n ) /\ a e. ~P A ) /\ ( # ` a ) = n ) -> n e. RR )
150 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) /\ n e. NN ) /\ ( y / B ) < n ) /\ a e. ~P A ) /\ ( # ` a ) = n ) -> B e. RR+ )
151 148 149 150 ltdivmul2d 
 |-  ( ( ( ( ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) /\ n e. NN ) /\ ( y / B ) < n ) /\ a e. ~P A ) /\ ( # ` a ) = n ) -> ( ( y / B ) < n <-> y < ( n x. B ) ) )
152 147 151 mpbid 
 |-  ( ( ( ( ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) /\ n e. NN ) /\ ( y / B ) < n ) /\ a e. ~P A ) /\ ( # ` a ) = n ) -> y < ( n x. B ) )
153 130 oveq1d 
 |-  ( ( ( ( ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) /\ n e. NN ) /\ ( y / B ) < n ) /\ a e. ~P A ) /\ ( # ` a ) = n ) -> ( ( # ` a ) *e B ) = ( n *e B ) )
154 150 rpred 
 |-  ( ( ( ( ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) /\ n e. NN ) /\ ( y / B ) < n ) /\ a e. ~P A ) /\ ( # ` a ) = n ) -> B e. RR )
155 rexmul 
 |-  ( ( n e. RR /\ B e. RR ) -> ( n *e B ) = ( n x. B ) )
156 149 154 155 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) /\ n e. NN ) /\ ( y / B ) < n ) /\ a e. ~P A ) /\ ( # ` a ) = n ) -> ( n *e B ) = ( n x. B ) )
157 153 156 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) /\ n e. NN ) /\ ( y / B ) < n ) /\ a e. ~P A ) /\ ( # ` a ) = n ) -> ( ( # ` a ) *e B ) = ( n x. B ) )
158 152 157 breqtrrd 
 |-  ( ( ( ( ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) /\ n e. NN ) /\ ( y / B ) < n ) /\ a e. ~P A ) /\ ( # ` a ) = n ) -> y < ( ( # ` a ) *e B ) )
159 breq2 
 |-  ( z = ( ( # ` a ) *e B ) -> ( y < z <-> y < ( ( # ` a ) *e B ) ) )
160 159 rspcev 
 |-  ( ( ( ( # ` a ) *e B ) e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) /\ y < ( ( # ` a ) *e B ) ) -> E. z e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) y < z )
161 146 158 160 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) /\ n e. NN ) /\ ( y / B ) < n ) /\ a e. ~P A ) /\ ( # ` a ) = n ) -> E. z e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) y < z )
162 161 rexlimdva2 
 |-  ( ( ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) /\ n e. NN ) /\ ( y / B ) < n ) -> ( E. a e. ~P A ( # ` a ) = n -> E. z e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) y < z ) )
163 162 impr 
 |-  ( ( ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) /\ n e. NN ) /\ ( ( y / B ) < n /\ E. a e. ~P A ( # ` a ) = n ) ) -> E. z e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) y < z )
164 simp-4r 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) -> y e. RR )
165 simpr 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) -> B e. RR+ )
166 164 165 rerpdivcld 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) -> ( y / B ) e. RR )
167 arch 
 |-  ( ( y / B ) e. RR -> E. n e. NN ( y / B ) < n )
168 166 167 syl 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) -> E. n e. NN ( y / B ) < n )
169 ishashinf 
 |-  ( -. A e. Fin -> A. n e. NN E. a e. ~P A ( # ` a ) = n )
170 169 ad2antlr 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) -> A. n e. NN E. a e. ~P A ( # ` a ) = n )
171 r19.29r 
 |-  ( ( E. n e. NN ( y / B ) < n /\ A. n e. NN E. a e. ~P A ( # ` a ) = n ) -> E. n e. NN ( ( y / B ) < n /\ E. a e. ~P A ( # ` a ) = n ) )
172 168 170 171 syl2anc 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) -> E. n e. NN ( ( y / B ) < n /\ E. a e. ~P A ( # ` a ) = n ) )
173 163 172 r19.29a 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B e. RR+ ) -> E. z e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) y < z )
174 nfielex 
 |-  ( -. A e. Fin -> E. l l e. A )
175 174 adantr 
 |-  ( ( -. A e. Fin /\ B = +oo ) -> E. l l e. A )
176 snelpwi 
 |-  ( l e. A -> { l } e. ~P A )
177 snfi 
 |-  { l } e. Fin
178 176 177 jctir 
 |-  ( l e. A -> ( { l } e. ~P A /\ { l } e. Fin ) )
179 elin 
 |-  ( { l } e. ( ~P A i^i Fin ) <-> ( { l } e. ~P A /\ { l } e. Fin ) )
180 178 179 sylibr 
 |-  ( l e. A -> { l } e. ( ~P A i^i Fin ) )
181 180 adantl 
 |-  ( ( ( -. A e. Fin /\ B = +oo ) /\ l e. A ) -> { l } e. ( ~P A i^i Fin ) )
182 simplr 
 |-  ( ( ( -. A e. Fin /\ B = +oo ) /\ l e. A ) -> B = +oo )
183 182 oveq2d 
 |-  ( ( ( -. A e. Fin /\ B = +oo ) /\ l e. A ) -> ( ( # ` { l } ) *e B ) = ( ( # ` { l } ) *e +oo ) )
184 hashsng 
 |-  ( l e. A -> ( # ` { l } ) = 1 )
185 1re 
 |-  1 e. RR
186 27 185 sselii 
 |-  1 e. RR*
187 184 186 eqeltrdi 
 |-  ( l e. A -> ( # ` { l } ) e. RR* )
188 0lt1 
 |-  0 < 1
189 188 184 breqtrrid 
 |-  ( l e. A -> 0 < ( # ` { l } ) )
190 xmulpnf1 
 |-  ( ( ( # ` { l } ) e. RR* /\ 0 < ( # ` { l } ) ) -> ( ( # ` { l } ) *e +oo ) = +oo )
191 187 189 190 syl2anc 
 |-  ( l e. A -> ( ( # ` { l } ) *e +oo ) = +oo )
192 191 adantl 
 |-  ( ( ( -. A e. Fin /\ B = +oo ) /\ l e. A ) -> ( ( # ` { l } ) *e +oo ) = +oo )
193 183 192 eqtr2d 
 |-  ( ( ( -. A e. Fin /\ B = +oo ) /\ l e. A ) -> +oo = ( ( # ` { l } ) *e B ) )
194 fveq2 
 |-  ( x = { l } -> ( # ` x ) = ( # ` { l } ) )
195 194 oveq1d 
 |-  ( x = { l } -> ( ( # ` x ) *e B ) = ( ( # ` { l } ) *e B ) )
196 195 rspceeqv 
 |-  ( ( { l } e. ( ~P A i^i Fin ) /\ +oo = ( ( # ` { l } ) *e B ) ) -> E. x e. ( ~P A i^i Fin ) +oo = ( ( # ` x ) *e B ) )
197 181 193 196 syl2anc 
 |-  ( ( ( -. A e. Fin /\ B = +oo ) /\ l e. A ) -> E. x e. ( ~P A i^i Fin ) +oo = ( ( # ` x ) *e B ) )
198 175 197 exlimddv 
 |-  ( ( -. A e. Fin /\ B = +oo ) -> E. x e. ( ~P A i^i Fin ) +oo = ( ( # ` x ) *e B ) )
199 198 adantll 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B = +oo ) -> E. x e. ( ~P A i^i Fin ) +oo = ( ( # ` x ) *e B ) )
200 50 116 elrnmpti 
 |-  ( +oo e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) <-> E. x e. ( ~P A i^i Fin ) +oo = ( ( # ` x ) *e B ) )
201 199 200 sylibr 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B = +oo ) -> +oo e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) )
202 simp-4r 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B = +oo ) -> y e. RR )
203 ltpnf 
 |-  ( y e. RR -> y < +oo )
204 202 203 syl 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B = +oo ) -> y < +oo )
205 breq2 
 |-  ( z = +oo -> ( y < z <-> y < +oo ) )
206 205 rspcev 
 |-  ( ( +oo e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) /\ y < +oo ) -> E. z e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) y < z )
207 201 204 206 syl2anc 
 |-  ( ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) /\ B = +oo ) -> E. z e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) y < z )
208 simp-4r 
 |-  ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) -> B e. ( 0 [,] +oo ) )
209 elxrge02 
 |-  ( B e. ( 0 [,] +oo ) <-> ( B = 0 \/ B e. RR+ \/ B = +oo ) )
210 208 209 sylib 
 |-  ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) -> ( B = 0 \/ B e. RR+ \/ B = +oo ) )
211 128 173 207 210 mpjao3dan 
 |-  ( ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) /\ -. A e. Fin ) -> E. z e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) y < z )
212 99 211 pm2.61dan 
 |-  ( ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) /\ y < ( ( # ` A ) *e B ) ) -> E. z e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) y < z )
213 212 ex 
 |-  ( ( ( A e. V /\ B e. ( 0 [,] +oo ) ) /\ y e. RR ) -> ( y < ( ( # ` A ) *e B ) -> E. z e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) y < z ) )
214 213 ralrimiva 
 |-  ( ( A e. V /\ B e. ( 0 [,] +oo ) ) -> A. y e. RR ( y < ( ( # ` A ) *e B ) -> E. z e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) y < z ) )
215 supxr2 
 |-  ( ( ( ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) C_ RR* /\ ( ( # ` A ) *e B ) e. RR* ) /\ ( A. y e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) y <_ ( ( # ` A ) *e B ) /\ A. y e. RR ( y < ( ( # ` A ) *e B ) -> E. z e. ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) y < z ) ) ) -> sup ( ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) , RR* , < ) = ( ( # ` A ) *e B ) )
216 45 48 80 214 215 syl22anc 
 |-  ( ( A e. V /\ B e. ( 0 [,] +oo ) ) -> sup ( ran ( x e. ( ~P A i^i Fin ) |-> ( ( # ` x ) *e B ) ) , RR* , < ) = ( ( # ` A ) *e B ) )
217 25 216 eqtrd 
 |-  ( ( A e. V /\ B e. ( 0 [,] +oo ) ) -> sum* k e. A B = ( ( # ` A ) *e B ) )