Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sge0resplit Structured version   Visualization version   GIF version

Theorem sge0resplit 46361
Description: Σ^ splits into two parts, when it's a real number. This is a special case of sge0split 46364. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
sge0resplit.a (𝜑𝐴𝑉)
sge0resplit.b (𝜑𝐵𝑊)
sge0resplit.u 𝑈 = (𝐴𝐵)
sge0resplit.in0 (𝜑 → (𝐴𝐵) = ∅)
sge0resplit.f (𝜑𝐹:𝑈⟶(0[,]+∞))
sge0resplit.re (𝜑 → (Σ^𝐹) ∈ ℝ)
Assertion
Ref Expression
sge0resplit (𝜑 → (Σ^𝐹) = ((Σ^‘(𝐹𝐴)) + (Σ^‘(𝐹𝐵))))

Proof of Theorem sge0resplit
Dummy variables 𝑎 𝑏 𝑟 𝑢 𝑣 𝑥 𝑦 𝑡 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sge0resplit.a . . . . . . 7 (𝜑𝐴𝑉)
2 sge0resplit.f . . . . . . . 8 (𝜑𝐹:𝑈⟶(0[,]+∞))
3 ssun1 4187 . . . . . . . . . 10 𝐴 ⊆ (𝐴𝐵)
4 sge0resplit.u . . . . . . . . . . 11 𝑈 = (𝐴𝐵)
54eqcomi 2743 . . . . . . . . . 10 (𝐴𝐵) = 𝑈
63, 5sseqtri 4031 . . . . . . . . 9 𝐴𝑈
76a1i 11 . . . . . . . 8 (𝜑𝐴𝑈)
82, 7fssresd 6775 . . . . . . 7 (𝜑 → (𝐹𝐴):𝐴⟶(0[,]+∞))
94a1i 11 . . . . . . . . 9 (𝜑𝑈 = (𝐴𝐵))
10 sge0resplit.b . . . . . . . . . 10 (𝜑𝐵𝑊)
11 unexg 7761 . . . . . . . . . 10 ((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)
121, 10, 11syl2anc 584 . . . . . . . . 9 (𝜑 → (𝐴𝐵) ∈ V)
139, 12eqeltrd 2838 . . . . . . . 8 (𝜑𝑈 ∈ V)
14 sge0resplit.re . . . . . . . 8 (𝜑 → (Σ^𝐹) ∈ ℝ)
1513, 2, 14sge0ssre 46352 . . . . . . 7 (𝜑 → (Σ^‘(𝐹𝐴)) ∈ ℝ)
161, 8, 15sge0supre 46344 . . . . . 6 (𝜑 → (Σ^‘(𝐹𝐴)) = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ))
1716, 15eqeltrrd 2839 . . . . 5 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) ∈ ℝ)
18 ssun2 4188 . . . . . . . . . 10 𝐵 ⊆ (𝐴𝐵)
1918, 5sseqtri 4031 . . . . . . . . 9 𝐵𝑈
2019a1i 11 . . . . . . . 8 (𝜑𝐵𝑈)
212, 20fssresd 6775 . . . . . . 7 (𝜑 → (𝐹𝐵):𝐵⟶(0[,]+∞))
2213, 2, 14sge0ssre 46352 . . . . . . 7 (𝜑 → (Σ^‘(𝐹𝐵)) ∈ ℝ)
2310, 21, 22sge0supre 46344 . . . . . 6 (𝜑 → (Σ^‘(𝐹𝐵)) = sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < ))
2423, 22eqeltrrd 2839 . . . . 5 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < ) ∈ ℝ)
25 rexadd 13270 . . . . 5 ((sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) ∈ ℝ ∧ sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < ) ∈ ℝ) → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) +𝑒 sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )) = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) + sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )))
2617, 24, 25syl2anc 584 . . . 4 (𝜑 → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) +𝑒 sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )) = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) + sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )))
2713, 2, 14sge0rern 46343 . . . . . . . 8 (𝜑 → ¬ +∞ ∈ ran 𝐹)
28 nelrnres 45129 . . . . . . . 8 (¬ +∞ ∈ ran 𝐹 → ¬ +∞ ∈ ran (𝐹𝐴))
2927, 28syl 17 . . . . . . 7 (𝜑 → ¬ +∞ ∈ ran (𝐹𝐴))
308, 29fge0iccico 46325 . . . . . 6 (𝜑 → (𝐹𝐴):𝐴⟶(0[,)+∞))
3130sge0rnre 46319 . . . . 5 (𝜑 → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ⊆ ℝ)
32 sge0rnn0 46323 . . . . . 6 ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ≠ ∅
3332a1i 11 . . . . 5 (𝜑 → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ≠ ∅)
341, 30sge0reval 46327 . . . . . . . 8 (𝜑 → (Σ^‘(𝐹𝐴)) = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ*, < ))
3534eqcomd 2740 . . . . . . 7 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ*, < ) = (Σ^‘(𝐹𝐴)))
3635, 15eqeltrd 2838 . . . . . 6 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ*, < ) ∈ ℝ)
37 supxrre3 45274 . . . . . . 7 ((ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ⊆ ℝ ∧ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ≠ ∅) → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ*, < ) ∈ ℝ ↔ ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))𝑡𝑤))
3831, 33, 37syl2anc 584 . . . . . 6 (𝜑 → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ*, < ) ∈ ℝ ↔ ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))𝑡𝑤))
3936, 38mpbid 232 . . . . 5 (𝜑 → ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))𝑡𝑤)
40 nelrnres 45129 . . . . . . . 8 (¬ +∞ ∈ ran 𝐹 → ¬ +∞ ∈ ran (𝐹𝐵))
4127, 40syl 17 . . . . . . 7 (𝜑 → ¬ +∞ ∈ ran (𝐹𝐵))
4221, 41fge0iccico 46325 . . . . . 6 (𝜑 → (𝐹𝐵):𝐵⟶(0[,)+∞))
4342sge0rnre 46319 . . . . 5 (𝜑 → ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ⊆ ℝ)
44 sge0rnn0 46323 . . . . . 6 ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ≠ ∅
4544a1i 11 . . . . 5 (𝜑 → ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ≠ ∅)
4610, 42sge0reval 46327 . . . . . . . 8 (𝜑 → (Σ^‘(𝐹𝐵)) = sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ*, < ))
4746eqcomd 2740 . . . . . . 7 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ*, < ) = (Σ^‘(𝐹𝐵)))
4847, 22eqeltrd 2838 . . . . . 6 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ*, < ) ∈ ℝ)
49 supxrre3 45274 . . . . . . 7 ((ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ⊆ ℝ ∧ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ≠ ∅) → (sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ*, < ) ∈ ℝ ↔ ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑡𝑤))
5043, 45, 49syl2anc 584 . . . . . 6 (𝜑 → (sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ*, < ) ∈ ℝ ↔ ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑡𝑤))
5148, 50mpbid 232 . . . . 5 (𝜑 → ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑡𝑤)
52 eqid 2734 . . . . 5 {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} = {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}
5331, 33, 39, 43, 45, 51, 52supadd 12233 . . . 4 (𝜑 → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) + sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )) = sup({𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}, ℝ, < ))
54 simpl 482 . . . . . . . . . 10 ((𝜑𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}) → 𝜑)
55 vex 3481 . . . . . . . . . . . . 13 𝑟 ∈ V
56 eqeq1 2738 . . . . . . . . . . . . . . 15 (𝑧 = 𝑟 → (𝑧 = (𝑣 + 𝑢) ↔ 𝑟 = (𝑣 + 𝑢)))
5756rexbidv 3176 . . . . . . . . . . . . . 14 (𝑧 = 𝑟 → (∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢) ↔ ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)))
5857rexbidv 3176 . . . . . . . . . . . . 13 (𝑧 = 𝑟 → (∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢) ↔ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)))
5955, 58elab 3680 . . . . . . . . . . . 12 (𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} ↔ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
6059biimpi 216 . . . . . . . . . . 11 (𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
6160adantl 481 . . . . . . . . . 10 ((𝜑𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
62 simpl 482 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)))) → 𝜑)
63 vex 3481 . . . . . . . . . . . . . . . . . . . 20 𝑣 ∈ V
64 sumeq1 15721 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑎 → Σ𝑦𝑥 ((𝐹𝐴)‘𝑦) = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦))
6564cbvmptv 5260 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) = (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑎 ((𝐹𝐴)‘𝑦))
6665elrnmpt 5971 . . . . . . . . . . . . . . . . . . . 20 (𝑣 ∈ V → (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ↔ ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦)))
6763, 66ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ↔ ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦))
6867biimpi 216 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦))
6968adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦))
70 vex 3481 . . . . . . . . . . . . . . . . . . . 20 𝑢 ∈ V
71 sumeq1 15721 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑏 → Σ𝑦𝑥 ((𝐹𝐵)‘𝑦) = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))
7271cbvmptv 5260 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) = (𝑏 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))
7372elrnmpt 5971 . . . . . . . . . . . . . . . . . . . 20 (𝑢 ∈ V → (𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ↔ ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
7470, 73ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ↔ ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))
7574biimpi 216 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) → ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))
7675adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))) → ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))
7769, 76jca 511 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))) → (∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
78 reeanv 3226 . . . . . . . . . . . . . . . 16 (∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) ↔ (∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
7977, 78sylibr 234 . . . . . . . . . . . . . . 15 ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
8079adantl 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
81 eqid 2734 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) = (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))
82 elinel1 4210 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎 ∈ 𝒫 𝐴)
83 elpwi 4611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 ∈ 𝒫 𝐴𝑎𝐴)
84 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎𝐴𝑎𝐴)
8584, 6sstrdi 4007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎𝐴𝑎𝑈)
8683, 85syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 ∈ 𝒫 𝐴𝑎𝑈)
8782, 86syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎𝑈)
8887adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎𝑈)
89 elinel1 4210 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → 𝑏 ∈ 𝒫 𝐵)
90 elpwi 4611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑏 ∈ 𝒫 𝐵𝑏𝐵)
91 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑏𝐵𝑏𝐵)
9291, 19sstrdi 4007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑏𝐵𝑏𝑈)
9390, 92syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑏 ∈ 𝒫 𝐵𝑏𝑈)
9489, 93syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → 𝑏𝑈)
9594adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑏𝑈)
9688, 95unssd 4201 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑎𝑏) ⊆ 𝑈)
97 vex 3481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑎 ∈ V
98 vex 3481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑏 ∈ V
9997, 98unex 7762 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎𝑏) ∈ V
10099elpw 4608 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎𝑏) ∈ 𝒫 𝑈 ↔ (𝑎𝑏) ⊆ 𝑈)
10196, 100sylibr 234 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑎𝑏) ∈ 𝒫 𝑈)
102 elinel2 4211 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎 ∈ Fin)
103102adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎 ∈ Fin)
104 elinel2 4211 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → 𝑏 ∈ Fin)
105104adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑏 ∈ Fin)
106 unfi 9209 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ Fin ∧ 𝑏 ∈ Fin) → (𝑎𝑏) ∈ Fin)
107103, 105, 106syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑎𝑏) ∈ Fin)
108101, 107elind 4209 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑎𝑏) ∈ (𝒫 𝑈 ∩ Fin))
109108adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝑎𝑏) ∈ (𝒫 𝑈 ∩ Fin))
110109ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → (𝑎𝑏) ∈ (𝒫 𝑈 ∩ Fin))
111 simpl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) → 𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦))
112 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) → 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))
113111, 112oveq12d 7448 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) → (𝑣 + 𝑢) = (Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) + Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
114113adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) → (𝑣 + 𝑢) = (Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) + Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
11582, 83syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎𝐴)
116115sselda 3994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑦𝑎) → 𝑦𝐴)
117 fvres 6925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦𝐴 → ((𝐹𝐴)‘𝑦) = (𝐹𝑦))
118116, 117syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑦𝑎) → ((𝐹𝐴)‘𝑦) = (𝐹𝑦))
119118sumeq2dv 15734 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) = Σ𝑦𝑎 (𝐹𝑦))
120119adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) = Σ𝑦𝑎 (𝐹𝑦))
12189, 90syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → 𝑏𝐵)
122121sselda 3994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑏 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑦𝑏) → 𝑦𝐵)
123 fvres 6925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦𝐵 → ((𝐹𝐵)‘𝑦) = (𝐹𝑦))
124122, 123syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑏 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑦𝑏) → ((𝐹𝐵)‘𝑦) = (𝐹𝑦))
125124sumeq2dv 15734 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → Σ𝑦𝑏 ((𝐹𝐵)‘𝑦) = Σ𝑦𝑏 (𝐹𝑦))
126125adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → Σ𝑦𝑏 ((𝐹𝐵)‘𝑦) = Σ𝑦𝑏 (𝐹𝑦))
127120, 126oveq12d 7448 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) + Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) = (Σ𝑦𝑎 (𝐹𝑦) + Σ𝑦𝑏 (𝐹𝑦)))
128127adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) → (Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) + Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) = (Σ𝑦𝑎 (𝐹𝑦) + Σ𝑦𝑏 (𝐹𝑦)))
129114, 128eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) → (𝑣 + 𝑢) = (Σ𝑦𝑎 (𝐹𝑦) + Σ𝑦𝑏 (𝐹𝑦)))
130129ad4ant23 753 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → (𝑣 + 𝑢) = (Σ𝑦𝑎 (𝐹𝑦) + Σ𝑦𝑏 (𝐹𝑦)))
131 simpr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → 𝑟 = (𝑣 + 𝑢))
132 sge0resplit.in0 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴𝐵) = ∅)
133132adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝐴𝐵) = ∅)
134115ad2antrl 728 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → 𝑎𝐴)
135121adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑏𝐵)
136135adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → 𝑏𝐵)
137 ssin0 44994 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴𝐵) = ∅ ∧ 𝑎𝐴𝑏𝐵) → (𝑎𝑏) = ∅)
138133, 134, 136, 137syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝑎𝑏) = ∅)
139 eqidd 2735 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝑎𝑏) = (𝑎𝑏))
140107adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝑎𝑏) ∈ Fin)
141 rge0ssre 13492 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0[,)+∞) ⊆ ℝ
142 ax-resscn 11209 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ℝ ⊆ ℂ
143141, 142sstri 4004 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0[,)+∞) ⊆ ℂ
1442, 27fge0iccico 46325 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐹:𝑈⟶(0[,)+∞))
145144ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ 𝑦 ∈ (𝑎𝑏)) → 𝐹:𝑈⟶(0[,)+∞))
14696sselda 3994 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) ∧ 𝑦 ∈ (𝑎𝑏)) → 𝑦𝑈)
147146adantll 714 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ 𝑦 ∈ (𝑎𝑏)) → 𝑦𝑈)
148145, 147ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ 𝑦 ∈ (𝑎𝑏)) → (𝐹𝑦) ∈ (0[,)+∞))
149143, 148sselid 3992 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ 𝑦 ∈ (𝑎𝑏)) → (𝐹𝑦) ∈ ℂ)
150138, 139, 140, 149fsumsplit 15773 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → Σ𝑦 ∈ (𝑎𝑏)(𝐹𝑦) = (Σ𝑦𝑎 (𝐹𝑦) + Σ𝑦𝑏 (𝐹𝑦)))
151150ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → Σ𝑦 ∈ (𝑎𝑏)(𝐹𝑦) = (Σ𝑦𝑎 (𝐹𝑦) + Σ𝑦𝑏 (𝐹𝑦)))
152130, 131, 1513eqtr4d 2784 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → 𝑟 = Σ𝑦 ∈ (𝑎𝑏)(𝐹𝑦))
153 sumeq1 15721 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = (𝑎𝑏) → Σ𝑦𝑥 (𝐹𝑦) = Σ𝑦 ∈ (𝑎𝑏)(𝐹𝑦))
154153rspceeqv 3644 . . . . . . . . . . . . . . . . . . . . 21 (((𝑎𝑏) ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦 ∈ (𝑎𝑏)(𝐹𝑦)) → ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦𝑥 (𝐹𝑦))
155110, 152, 154syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦𝑥 (𝐹𝑦))
15655a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → 𝑟 ∈ V)
15781, 155, 156elrnmptd 5976 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))
158157ex 412 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
159158ex 412 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → ((𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))))
160159ex 412 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → ((𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))))
161160rexlimdvv 3209 . . . . . . . . . . . . . . 15 (𝜑 → (∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))))
162161imp 406 . . . . . . . . . . . . . 14 ((𝜑 ∧ ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
16362, 80, 162syl2anc 584 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)))) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
164163ex 412 . . . . . . . . . . . 12 (𝜑 → ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))))
165164rexlimdvv 3209 . . . . . . . . . . 11 (𝜑 → (∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
166165imp 406 . . . . . . . . . 10 ((𝜑 ∧ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))
16754, 61, 166syl2anc 584 . . . . . . . . 9 ((𝜑𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))
168167ex 412 . . . . . . . 8 (𝜑 → (𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
16981elrnmpt 5971 . . . . . . . . . . . . 13 (𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) → (𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦𝑥 (𝐹𝑦)))
170169ibi 267 . . . . . . . . . . . 12 (𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) → ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦𝑥 (𝐹𝑦))
171170adantl 481 . . . . . . . . . . 11 ((𝜑𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦𝑥 (𝐹𝑦))
172 nfv 1911 . . . . . . . . . . . . 13 𝑥𝜑
173 nfcv 2902 . . . . . . . . . . . . . 14 𝑥𝑟
174 nfmpt1 5255 . . . . . . . . . . . . . . 15 𝑥(𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))
175174nfrn 5965 . . . . . . . . . . . . . 14 𝑥ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))
176173, 175nfel 2917 . . . . . . . . . . . . 13 𝑥 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))
177172, 176nfan 1896 . . . . . . . . . . . 12 𝑥(𝜑𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))
178 nfmpt1 5255 . . . . . . . . . . . . . 14 𝑥(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))
179178nfrn 5965 . . . . . . . . . . . . 13 𝑥ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))
180 nfmpt1 5255 . . . . . . . . . . . . . . 15 𝑥(𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))
181180nfrn 5965 . . . . . . . . . . . . . 14 𝑥ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))
182 nfv 1911 . . . . . . . . . . . . . 14 𝑥 𝑟 = (𝑣 + 𝑢)
183181, 182nfrexw 3310 . . . . . . . . . . . . 13 𝑥𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)
184179, 183nfrexw 3310 . . . . . . . . . . . 12 𝑥𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)
185 inss2 4245 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐴) ⊆ 𝐴
186185sseli 3990 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝑥𝐴) → 𝑦𝐴)
187186adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦 ∈ (𝑥𝐴)) → 𝑦𝐴)
188117eqcomd 2740 . . . . . . . . . . . . . . . . . . 19 (𝑦𝐴 → (𝐹𝑦) = ((𝐹𝐴)‘𝑦))
189187, 188syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦 ∈ (𝑥𝐴)) → (𝐹𝑦) = ((𝐹𝐴)‘𝑦))
190189sumeq2dv 15734 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) = Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦))
191 sumeq1 15721 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 → Σ𝑦𝑥 ((𝐹𝐴)‘𝑦) = Σ𝑦𝑧 ((𝐹𝐴)‘𝑦))
192191cbvmptv 5260 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) = (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑧 ((𝐹𝐴)‘𝑦))
193 vex 3481 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥 ∈ V
194193inex1 5322 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥𝐴) ∈ V
195194elpw 4608 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝐴) ∈ 𝒫 𝐴 ↔ (𝑥𝐴) ⊆ 𝐴)
196185, 195mpbir 231 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐴) ∈ 𝒫 𝐴
197196a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐴) ∈ 𝒫 𝐴)
198 elinel2 4211 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 ∈ Fin)
199 inss1 4244 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐴) ⊆ 𝑥
200199a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐴) ⊆ 𝑥)
201 ssfi 9211 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ Fin ∧ (𝑥𝐴) ⊆ 𝑥) → (𝑥𝐴) ∈ Fin)
202198, 200, 201syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐴) ∈ Fin)
203197, 202elind 4209 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐴) ∈ (𝒫 𝐴 ∩ Fin))
204 eqidd 2735 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) = Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦))
205 sumeq1 15721 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝑥𝐴) → Σ𝑦𝑧 ((𝐹𝐴)‘𝑦) = Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦))
206205rspceeqv 3644 . . . . . . . . . . . . . . . . . . 19 (((𝑥𝐴) ∈ (𝒫 𝐴 ∩ Fin) ∧ Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) = Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) = Σ𝑦𝑧 ((𝐹𝐴)‘𝑦))
207203, 204, 206syl2anc 584 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) = Σ𝑦𝑧 ((𝐹𝐴)‘𝑦))
208 sumex 15720 . . . . . . . . . . . . . . . . . . 19 Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) ∈ V
209208a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) ∈ V)
210192, 207, 209elrnmptd 5976 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)))
211190, 210eqeltrd 2838 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)))
2122113ad2ant2 1133 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)))
213 sumeq1 15721 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → Σ𝑦𝑥 ((𝐹𝐵)‘𝑦) = Σ𝑦𝑧 ((𝐹𝐵)‘𝑦))
214213cbvmptv 5260 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) = (𝑧 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑧 ((𝐹𝐵)‘𝑦))
215 inss2 4245 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐵) ⊆ 𝐵
216193inex1 5322 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐵) ∈ V
217216elpw 4608 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝐵) ∈ 𝒫 𝐵 ↔ (𝑥𝐵) ⊆ 𝐵)
218215, 217mpbir 231 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝐵) ∈ 𝒫 𝐵
219218a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → (𝑥𝐵) ∈ 𝒫 𝐵)
220 inss1 4244 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐵) ⊆ 𝑥
221220a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐵) ⊆ 𝑥)
222 ssfi 9211 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ Fin ∧ (𝑥𝐵) ⊆ 𝑥) → (𝑥𝐵) ∈ Fin)
223198, 221, 222syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐵) ∈ Fin)
2242233ad2ant2 1133 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → (𝑥𝐵) ∈ Fin)
225219, 224elind 4209 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → (𝑥𝐵) ∈ (𝒫 𝐵 ∩ Fin))
226215sseli 3990 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (𝑥𝐵) → 𝑦𝐵)
227123eqcomd 2740 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝐵 → (𝐹𝑦) = ((𝐹𝐵)‘𝑦))
228226, 227syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (𝑥𝐵) → (𝐹𝑦) = ((𝐹𝐵)‘𝑦))
229228sumeq2i 15730 . . . . . . . . . . . . . . . . . . . 20 Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦)
230229a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦))
2312303adant3 1131 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦))
232 sumeq1 15721 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑥𝐵) → Σ𝑦𝑧 ((𝐹𝐵)‘𝑦) = Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦))
233232rspceeqv 3644 . . . . . . . . . . . . . . . . . 18 (((𝑥𝐵) ∈ (𝒫 𝐵 ∩ Fin) ∧ Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦)) → ∃𝑧 ∈ (𝒫 𝐵 ∩ Fin)Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦𝑧 ((𝐹𝐵)‘𝑦))
234225, 231, 233syl2anc 584 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → ∃𝑧 ∈ (𝒫 𝐵 ∩ Fin)Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦𝑧 ((𝐹𝐵)‘𝑦))
235 sumex 15720 . . . . . . . . . . . . . . . . . 18 Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ V
236235a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ V)
237214, 234, 236elrnmptd 5976 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)))
238 simp3 1137 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → 𝑟 = Σ𝑦𝑥 (𝐹𝑦))
239185a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑥𝐴) ⊆ 𝐴)
240215a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑥𝐵) ⊆ 𝐵)
241 ssin0 44994 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴𝐵) = ∅ ∧ (𝑥𝐴) ⊆ 𝐴 ∧ (𝑥𝐵) ⊆ 𝐵) → ((𝑥𝐴) ∩ (𝑥𝐵)) = ∅)
242132, 239, 240, 241syl3anc 1370 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑥𝐴) ∩ (𝑥𝐵)) = ∅)
243242adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → ((𝑥𝐴) ∩ (𝑥𝐵)) = ∅)
244 elinel1 4210 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 ∈ 𝒫 𝑈)
245 elpwi 4611 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ 𝒫 𝑈𝑥𝑈)
246244, 245syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥𝑈)
2474ineq2i 4224 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥𝑈) = (𝑥 ∩ (𝐴𝐵))
248247a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝑈 → (𝑥𝑈) = (𝑥 ∩ (𝐴𝐵)))
249 dfss 3981 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥𝑈𝑥 = (𝑥𝑈))
250249biimpi 216 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝑈𝑥 = (𝑥𝑈))
251 indi 4289 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∩ (𝐴𝐵)) = ((𝑥𝐴) ∪ (𝑥𝐵))
252251eqcomi 2743 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥𝐴) ∪ (𝑥𝐵)) = (𝑥 ∩ (𝐴𝐵))
253252a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝑈 → ((𝑥𝐴) ∪ (𝑥𝐵)) = (𝑥 ∩ (𝐴𝐵)))
254248, 250, 2533eqtr4d 2784 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑈𝑥 = ((𝑥𝐴) ∪ (𝑥𝐵)))
255246, 254syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 = ((𝑥𝐴) ∪ (𝑥𝐵)))
256255adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝑥 = ((𝑥𝐴) ∪ (𝑥𝐵)))
257198adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝑥 ∈ Fin)
258144ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → 𝐹:𝑈⟶(0[,)+∞))
259246sselda 3994 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦𝑥) → 𝑦𝑈)
260259adantll 714 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → 𝑦𝑈)
261258, 260ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ (0[,)+∞))
262143, 261sselid 3992 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ ℂ)
263243, 256, 257, 262fsumsplit 15773 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦𝑥 (𝐹𝑦) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
2642633adant3 1131 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → Σ𝑦𝑥 (𝐹𝑦) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
265238, 264eqtrd 2774 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → 𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
266 oveq2 7438 . . . . . . . . . . . . . . . . 17 (𝑢 = Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) → (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
267266rspceeqv 3644 . . . . . . . . . . . . . . . 16 ((Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ∧ 𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦))) → ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢))
268237, 265, 267syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢))
269 oveq1 7437 . . . . . . . . . . . . . . . . . 18 (𝑣 = Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) → (𝑣 + 𝑢) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢))
270269eqeq2d 2745 . . . . . . . . . . . . . . . . 17 (𝑣 = Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) → (𝑟 = (𝑣 + 𝑢) ↔ 𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢)))
271270rexbidv 3176 . . . . . . . . . . . . . . . 16 (𝑣 = Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) → (∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢) ↔ ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢)))
272271rspcev 3621 . . . . . . . . . . . . . . 15 ((Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢)) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
273212, 268, 272syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
2742733exp 1118 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑟 = Σ𝑦𝑥 (𝐹𝑦) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))))
275274adantr 480 . . . . . . . . . . . 12 ((𝜑𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑟 = Σ𝑦𝑥 (𝐹𝑦) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))))
276177, 184, 275rexlimd 3263 . . . . . . . . . . 11 ((𝜑𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → (∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦𝑥 (𝐹𝑦) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)))
277171, 276mpd 15 . . . . . . . . . 10 ((𝜑𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
278277, 59sylibr 234 . . . . . . . . 9 ((𝜑𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → 𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)})
279278ex 412 . . . . . . . 8 (𝜑 → (𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) → 𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}))
280168, 279impbid 212 . . . . . . 7 (𝜑 → (𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} ↔ 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
281280alrimiv 1924 . . . . . 6 (𝜑 → ∀𝑟(𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} ↔ 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
282 dfcleq 2727 . . . . . 6 ({𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} = ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ↔ ∀𝑟(𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} ↔ 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
283281, 282sylibr 234 . . . . 5 (𝜑 → {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} = ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))
284283supeq1d 9483 . . . 4 (𝜑 → sup({𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}, ℝ, < ) = sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ, < ))
28526, 53, 2843eqtrrd 2779 . . 3 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ, < ) = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) +𝑒 sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )))
28613, 2, 14sge0supre 46344 . . 3 (𝜑 → (Σ^𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ, < ))
28716, 23oveq12d 7448 . . 3 (𝜑 → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) +𝑒 sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )))
288285, 286, 2873eqtr4d 2784 . 2 (𝜑 → (Σ^𝐹) = ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
289 rexadd 13270 . . 3 (((Σ^‘(𝐹𝐴)) ∈ ℝ ∧ (Σ^‘(𝐹𝐵)) ∈ ℝ) → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = ((Σ^‘(𝐹𝐴)) + (Σ^‘(𝐹𝐵))))
29015, 22, 289syl2anc 584 . 2 (𝜑 → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = ((Σ^‘(𝐹𝐴)) + (Σ^‘(𝐹𝐵))))
291288, 290eqtrd 2774 1 (𝜑 → (Σ^𝐹) = ((Σ^‘(𝐹𝐴)) + (Σ^‘(𝐹𝐵))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086  wal 1534   = wceq 1536  wcel 2105  {cab 2711  wne 2937  wral 3058  wrex 3067  Vcvv 3477  cun 3960  cin 3961  wss 3962  c0 4338  𝒫 cpw 4604   class class class wbr 5147  cmpt 5230  ran crn 5689  cres 5690  wf 6558  cfv 6562  (class class class)co 7430  Fincfn 8983  supcsup 9477  cc 11150  cr 11151  0cc0 11152   + caddc 11155  +∞cpnf 11289  *cxr 11291   < clt 11292  cle 11293   +𝑒 cxad 13149  [,)cico 13385  [,]cicc 13386  Σcsu 15718  Σ^csumge0 46317
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-sup 9479  df-oi 9547  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-z 12611  df-uz 12876  df-rp 13032  df-xadd 13152  df-ico 13389  df-icc 13390  df-fz 13544  df-fzo 13691  df-seq 14039  df-exp 14099  df-hash 14366  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-clim 15520  df-sum 15719  df-sumge0 46318
This theorem is referenced by:  sge0split  46364
  Copyright terms: Public domain W3C validator