Metamath Proof Explorer


Theorem gsumesum

Description: Relate a group sum on ` ( RR*s |``s ( 0 , +oo ) ) ` to a finite extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017) (Proof shortened by AV, 12-Dec-2019)

Ref Expression
Hypotheses gsumesum.0 𝑘 𝜑
gsumesum.1 ( 𝜑𝐴 ∈ Fin )
gsumesum.2 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
Assertion gsumesum ( 𝜑 → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) = Σ* 𝑘𝐴 𝐵 )

Proof

Step Hyp Ref Expression
1 gsumesum.0 𝑘 𝜑
2 gsumesum.1 ( 𝜑𝐴 ∈ Fin )
3 gsumesum.2 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
4 nfcv 𝑘 𝐴
5 eqidd ( ( 𝜑𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) )
6 1 4 2 3 5 esumval ( 𝜑 → Σ* 𝑘𝐴 𝐵 = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ) , ℝ* , < ) )
7 xrltso < Or ℝ*
8 7 a1i ( 𝜑 → < Or ℝ* )
9 iccssxr ( 0 [,] +∞ ) ⊆ ℝ*
10 xrge0base ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠s ( 0 [,] +∞ ) ) )
11 xrge0cmn ( ℝ*𝑠s ( 0 [,] +∞ ) ) ∈ CMnd
12 11 a1i ( 𝜑 → ( ℝ*𝑠s ( 0 [,] +∞ ) ) ∈ CMnd )
13 3 ex ( 𝜑 → ( 𝑘𝐴𝐵 ∈ ( 0 [,] +∞ ) ) )
14 1 13 ralrimi ( 𝜑 → ∀ 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) )
15 10 12 2 14 gsummptcl ( 𝜑 → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) ∈ ( 0 [,] +∞ ) )
16 9 15 sselid ( 𝜑 → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) ∈ ℝ* )
17 pwidg ( 𝐴 ∈ Fin → 𝐴 ∈ 𝒫 𝐴 )
18 2 17 syl ( 𝜑𝐴 ∈ 𝒫 𝐴 )
19 18 2 elind ( 𝜑𝐴 ∈ ( 𝒫 𝐴 ∩ Fin ) )
20 eqidd ( 𝜑 → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) )
21 mpteq1 ( 𝑥 = 𝐴 → ( 𝑘𝑥𝐵 ) = ( 𝑘𝐴𝐵 ) )
22 21 oveq2d ( 𝑥 = 𝐴 → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) )
23 22 rspceeqv ( ( 𝐴 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) ) → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) )
24 19 20 23 syl2anc ( 𝜑 → ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) )
25 eqid ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ) = ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) )
26 ovex ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ∈ V
27 25 26 elrnmpti ( ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) )
28 24 27 sylibr ( 𝜑 → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ) )
29 simpr ( ( 𝜑𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ) ) → 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ) )
30 mpteq1 ( 𝑥 = 𝑎 → ( 𝑘𝑥𝐵 ) = ( 𝑘𝑎𝐵 ) )
31 30 oveq2d ( 𝑥 = 𝑎 → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) )
32 31 cbvmptv ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ) = ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) )
33 ovex ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) ∈ V
34 32 33 elrnmpti ( 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ) ↔ ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑦 = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) )
35 29 34 sylib ( ( 𝜑𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ) ) → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑦 = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) )
36 11 a1i ( ( 𝜑𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ℝ*𝑠s ( 0 [,] +∞ ) ) ∈ CMnd )
37 inss2 ( 𝒫 𝐴 ∩ Fin ) ⊆ Fin
38 simpr ( ( 𝜑𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) )
39 37 38 sselid ( ( 𝜑𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑎 ∈ Fin )
40 nfv 𝑘 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin )
41 1 40 nfan 𝑘 ( 𝜑𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) )
42 simpll ( ( ( 𝜑𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘𝑎 ) → 𝜑 )
43 inss1 ( 𝒫 𝐴 ∩ Fin ) ⊆ 𝒫 𝐴
44 43 sseli ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑎 ∈ 𝒫 𝐴 )
45 44 elpwid ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑎𝐴 )
46 45 ad2antlr ( ( ( 𝜑𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘𝑎 ) → 𝑎𝐴 )
47 simpr ( ( ( 𝜑𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘𝑎 ) → 𝑘𝑎 )
48 46 47 sseldd ( ( ( 𝜑𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘𝑎 ) → 𝑘𝐴 )
49 42 48 3 syl2anc ( ( ( 𝜑𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘𝑎 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
50 49 ex ( ( 𝜑𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑘𝑎𝐵 ∈ ( 0 [,] +∞ ) ) )
51 41 50 ralrimi ( ( 𝜑𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ∀ 𝑘𝑎 𝐵 ∈ ( 0 [,] +∞ ) )
52 10 36 39 51 gsummptcl ( ( 𝜑𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) ∈ ( 0 [,] +∞ ) )
53 9 52 sselid ( ( 𝜑𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) ∈ ℝ* )
54 diffi ( 𝐴 ∈ Fin → ( 𝐴𝑎 ) ∈ Fin )
55 2 54 syl ( 𝜑 → ( 𝐴𝑎 ) ∈ Fin )
56 55 adantr ( ( 𝜑𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐴𝑎 ) ∈ Fin )
57 simpll ( ( ( 𝜑𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐴𝑎 ) ) → 𝜑 )
58 simpr ( ( ( 𝜑𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐴𝑎 ) ) → 𝑘 ∈ ( 𝐴𝑎 ) )
59 58 eldifad ( ( ( 𝜑𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐴𝑎 ) ) → 𝑘𝐴 )
60 57 59 3 syl2anc ( ( ( 𝜑𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐴𝑎 ) ) → 𝐵 ∈ ( 0 [,] +∞ ) )
61 60 ex ( ( 𝜑𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑘 ∈ ( 𝐴𝑎 ) → 𝐵 ∈ ( 0 [,] +∞ ) ) )
62 41 61 ralrimi ( ( 𝜑𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ∀ 𝑘 ∈ ( 𝐴𝑎 ) 𝐵 ∈ ( 0 [,] +∞ ) )
63 10 36 56 62 gsummptcl ( ( 𝜑𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝐴𝑎 ) ↦ 𝐵 ) ) ∈ ( 0 [,] +∞ ) )
64 9 63 sselid ( ( 𝜑𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝐴𝑎 ) ↦ 𝐵 ) ) ∈ ℝ* )
65 elxrge0 ( ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝐴𝑎 ) ↦ 𝐵 ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝐴𝑎 ) ↦ 𝐵 ) ) ∈ ℝ* ∧ 0 ≤ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝐴𝑎 ) ↦ 𝐵 ) ) ) )
66 65 simprbi ( ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝐴𝑎 ) ↦ 𝐵 ) ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝐴𝑎 ) ↦ 𝐵 ) ) )
67 63 66 syl ( ( 𝜑𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 0 ≤ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝐴𝑎 ) ↦ 𝐵 ) ) )
68 xraddge02 ( ( ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) ∈ ℝ* ∧ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝐴𝑎 ) ↦ 𝐵 ) ) ∈ ℝ* ) → ( 0 ≤ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝐴𝑎 ) ↦ 𝐵 ) ) → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) ≤ ( ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) +𝑒 ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝐴𝑎 ) ↦ 𝐵 ) ) ) ) )
69 68 imp ( ( ( ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) ∈ ℝ* ∧ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝐴𝑎 ) ↦ 𝐵 ) ) ∈ ℝ* ) ∧ 0 ≤ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝐴𝑎 ) ↦ 𝐵 ) ) ) → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) ≤ ( ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) +𝑒 ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝐴𝑎 ) ↦ 𝐵 ) ) ) )
70 53 64 67 69 syl21anc ( ( 𝜑𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) ≤ ( ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) +𝑒 ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝐴𝑎 ) ↦ 𝐵 ) ) ) )
71 70 adantlr ( ( ( 𝜑𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ) ) ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) ≤ ( ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) +𝑒 ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝐴𝑎 ) ↦ 𝐵 ) ) ) )
72 simpll ( ( ( 𝜑𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ) ) ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝜑 )
73 45 adantl ( ( ( 𝜑𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ) ) ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑎𝐴 )
74 xrge00 0 = ( 0g ‘ ( ℝ*𝑠s ( 0 [,] +∞ ) ) )
75 xrge0plusg +𝑒 = ( +g ‘ ( ℝ*𝑠s ( 0 [,] +∞ ) ) )
76 11 a1i ( ( 𝜑𝑎𝐴 ) → ( ℝ*𝑠s ( 0 [,] +∞ ) ) ∈ CMnd )
77 2 adantr ( ( 𝜑𝑎𝐴 ) → 𝐴 ∈ Fin )
78 eqid ( 𝑘𝐴𝐵 ) = ( 𝑘𝐴𝐵 )
79 1 3 78 fmptdf ( 𝜑 → ( 𝑘𝐴𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
80 79 adantr ( ( 𝜑𝑎𝐴 ) → ( 𝑘𝐴𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
81 78 fnmpt ( ∀ 𝑘𝐴 𝐵 ∈ ( 0 [,] +∞ ) → ( 𝑘𝐴𝐵 ) Fn 𝐴 )
82 14 81 syl ( 𝜑 → ( 𝑘𝐴𝐵 ) Fn 𝐴 )
83 c0ex 0 ∈ V
84 83 a1i ( 𝜑 → 0 ∈ V )
85 82 2 84 fndmfifsupp ( 𝜑 → ( 𝑘𝐴𝐵 ) finSupp 0 )
86 85 adantr ( ( 𝜑𝑎𝐴 ) → ( 𝑘𝐴𝐵 ) finSupp 0 )
87 disjdif ( 𝑎 ∩ ( 𝐴𝑎 ) ) = ∅
88 87 a1i ( ( 𝜑𝑎𝐴 ) → ( 𝑎 ∩ ( 𝐴𝑎 ) ) = ∅ )
89 undif ( 𝑎𝐴 ↔ ( 𝑎 ∪ ( 𝐴𝑎 ) ) = 𝐴 )
90 89 biimpi ( 𝑎𝐴 → ( 𝑎 ∪ ( 𝐴𝑎 ) ) = 𝐴 )
91 90 eqcomd ( 𝑎𝐴𝐴 = ( 𝑎 ∪ ( 𝐴𝑎 ) ) )
92 91 adantl ( ( 𝜑𝑎𝐴 ) → 𝐴 = ( 𝑎 ∪ ( 𝐴𝑎 ) ) )
93 10 74 75 76 77 80 86 88 92 gsumsplit ( ( 𝜑𝑎𝐴 ) → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) = ( ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( ( 𝑘𝐴𝐵 ) ↾ 𝑎 ) ) +𝑒 ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( ( 𝑘𝐴𝐵 ) ↾ ( 𝐴𝑎 ) ) ) ) )
94 resmpt ( 𝑎𝐴 → ( ( 𝑘𝐴𝐵 ) ↾ 𝑎 ) = ( 𝑘𝑎𝐵 ) )
95 94 oveq2d ( 𝑎𝐴 → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( ( 𝑘𝐴𝐵 ) ↾ 𝑎 ) ) = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) )
96 95 adantl ( ( 𝜑𝑎𝐴 ) → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( ( 𝑘𝐴𝐵 ) ↾ 𝑎 ) ) = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) )
97 difss ( 𝐴𝑎 ) ⊆ 𝐴
98 resmpt ( ( 𝐴𝑎 ) ⊆ 𝐴 → ( ( 𝑘𝐴𝐵 ) ↾ ( 𝐴𝑎 ) ) = ( 𝑘 ∈ ( 𝐴𝑎 ) ↦ 𝐵 ) )
99 97 98 ax-mp ( ( 𝑘𝐴𝐵 ) ↾ ( 𝐴𝑎 ) ) = ( 𝑘 ∈ ( 𝐴𝑎 ) ↦ 𝐵 )
100 99 oveq2i ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( ( 𝑘𝐴𝐵 ) ↾ ( 𝐴𝑎 ) ) ) = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝐴𝑎 ) ↦ 𝐵 ) )
101 100 a1i ( ( 𝜑𝑎𝐴 ) → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( ( 𝑘𝐴𝐵 ) ↾ ( 𝐴𝑎 ) ) ) = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝐴𝑎 ) ↦ 𝐵 ) ) )
102 96 101 oveq12d ( ( 𝜑𝑎𝐴 ) → ( ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( ( 𝑘𝐴𝐵 ) ↾ 𝑎 ) ) +𝑒 ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( ( 𝑘𝐴𝐵 ) ↾ ( 𝐴𝑎 ) ) ) ) = ( ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) +𝑒 ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝐴𝑎 ) ↦ 𝐵 ) ) ) )
103 93 102 eqtrd ( ( 𝜑𝑎𝐴 ) → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) = ( ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) +𝑒 ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝐴𝑎 ) ↦ 𝐵 ) ) ) )
104 72 73 103 syl2anc ( ( ( 𝜑𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ) ) ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) = ( ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) +𝑒 ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝐴𝑎 ) ↦ 𝐵 ) ) ) )
105 71 104 breqtrrd ( ( ( 𝜑𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ) ) ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) ≤ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) )
106 105 ralrimiva ( ( 𝜑𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ) ) → ∀ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) ≤ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) )
107 r19.29r ( ( ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑦 = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) ∧ ∀ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) ≤ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) ) → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) ∧ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) ≤ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) ) )
108 breq1 ( 𝑦 = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) → ( 𝑦 ≤ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) ↔ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) ≤ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) ) )
109 108 biimpar ( ( 𝑦 = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) ∧ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) ≤ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) ) → 𝑦 ≤ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) )
110 109 rexlimivw ( ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) ∧ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) ≤ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) ) → 𝑦 ≤ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) )
111 107 110 syl ( ( ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑦 = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) ∧ ∀ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑎𝐵 ) ) ≤ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) ) → 𝑦 ≤ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) )
112 35 106 111 syl2anc ( ( 𝜑𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ) ) → 𝑦 ≤ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) )
113 16 adantr ( ( 𝜑𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ) ) → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) ∈ ℝ* )
114 11 a1i ( ( 𝜑𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ℝ*𝑠s ( 0 [,] +∞ ) ) ∈ CMnd )
115 simpr ( ( 𝜑𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) )
116 37 115 sselid ( ( 𝜑𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥 ∈ Fin )
117 nfv 𝑘 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin )
118 1 117 nfan 𝑘 ( 𝜑𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) )
119 simpll ( ( ( 𝜑𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘𝑥 ) → 𝜑 )
120 43 sseli ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑥 ∈ 𝒫 𝐴 )
121 120 ad2antlr ( ( ( 𝜑𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘𝑥 ) → 𝑥 ∈ 𝒫 𝐴 )
122 121 elpwid ( ( ( 𝜑𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘𝑥 ) → 𝑥𝐴 )
123 simpr ( ( ( 𝜑𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘𝑥 ) → 𝑘𝑥 )
124 122 123 sseldd ( ( ( 𝜑𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘𝑥 ) → 𝑘𝐴 )
125 119 124 3 syl2anc ( ( ( 𝜑𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘𝑥 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
126 125 ex ( ( 𝜑𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑘𝑥𝐵 ∈ ( 0 [,] +∞ ) ) )
127 118 126 ralrimi ( ( 𝜑𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ∀ 𝑘𝑥 𝐵 ∈ ( 0 [,] +∞ ) )
128 10 114 116 127 gsummptcl ( ( 𝜑𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ∈ ( 0 [,] +∞ ) )
129 9 128 sselid ( ( 𝜑𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ∈ ℝ* )
130 129 ralrimiva ( 𝜑 → ∀ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ∈ ℝ* )
131 25 rnmptss ( ∀ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ∈ ℝ* → ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ) ⊆ ℝ* )
132 130 131 syl ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ) ⊆ ℝ* )
133 132 sselda ( ( 𝜑𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ) ) → 𝑦 ∈ ℝ* )
134 xrltnle ( ( ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) ∈ ℝ*𝑦 ∈ ℝ* ) → ( ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) < 𝑦 ↔ ¬ 𝑦 ≤ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) ) )
135 134 con2bid ( ( ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) ∈ ℝ*𝑦 ∈ ℝ* ) → ( 𝑦 ≤ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) ↔ ¬ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) < 𝑦 ) )
136 113 133 135 syl2anc ( ( 𝜑𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ) ) → ( 𝑦 ≤ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) ↔ ¬ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) < 𝑦 ) )
137 112 136 mpbid ( ( 𝜑𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ) ) → ¬ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) < 𝑦 )
138 8 16 28 137 supmax ( 𝜑 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝑥𝐵 ) ) ) , ℝ* , < ) = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) )
139 6 138 eqtr2d ( 𝜑 → ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) Σg ( 𝑘𝐴𝐵 ) ) = Σ* 𝑘𝐴 𝐵 )