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 sseldi ⊢ ( 𝜑 → ( ( ℝ*𝑠 ↾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 sseldi ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ 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 sseldi ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ 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 sseldi ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ 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 sseldi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ 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 sseldi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ 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 ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = Σ* 𝑘 ∈ 𝐴 𝐵 )