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