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

Theorem sge0resplit 39299
 Description: Σ^ splits into two parts, when it's a real number. This is a special case of sge0split 39302. (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 3738 . . . . . . . . . 10 𝐴 ⊆ (𝐴𝐵)
4 sge0resplit.u . . . . . . . . . . 11 𝑈 = (𝐴𝐵)
54eqcomi 2619 . . . . . . . . . 10 (𝐴𝐵) = 𝑈
63, 5sseqtri 3600 . . . . . . . . 9 𝐴𝑈
76a1i 11 . . . . . . . 8 (𝜑𝐴𝑈)
82, 7fssresd 5984 . . . . . . 7 (𝜑 → (𝐹𝐴):𝐴⟶(0[,]+∞))
94a1i 11 . . . . . . . . 9 (𝜑𝑈 = (𝐴𝐵))
10 sge0resplit.b . . . . . . . . . 10 (𝜑𝐵𝑊)
11 unexg 6857 . . . . . . . . . 10 ((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)
121, 10, 11syl2anc 691 . . . . . . . . 9 (𝜑 → (𝐴𝐵) ∈ V)
139, 12eqeltrd 2688 . . . . . . . 8 (𝜑𝑈 ∈ V)
14 sge0resplit.re . . . . . . . 8 (𝜑 → (Σ^𝐹) ∈ ℝ)
1513, 2, 14sge0ssre 39290 . . . . . . 7 (𝜑 → (Σ^‘(𝐹𝐴)) ∈ ℝ)
161, 8, 15sge0supre 39282 . . . . . 6 (𝜑 → (Σ^‘(𝐹𝐴)) = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ))
1716, 15eqeltrrd 2689 . . . . 5 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) ∈ ℝ)
18 ssun2 3739 . . . . . . . . . 10 𝐵 ⊆ (𝐴𝐵)
1918, 5sseqtri 3600 . . . . . . . . 9 𝐵𝑈
2019a1i 11 . . . . . . . 8 (𝜑𝐵𝑈)
212, 20fssresd 5984 . . . . . . 7 (𝜑 → (𝐹𝐵):𝐵⟶(0[,]+∞))
2213, 2, 14sge0ssre 39290 . . . . . . 7 (𝜑 → (Σ^‘(𝐹𝐵)) ∈ ℝ)
2310, 21, 22sge0supre 39282 . . . . . 6 (𝜑 → (Σ^‘(𝐹𝐵)) = sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < ))
2423, 22eqeltrrd 2689 . . . . 5 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < ) ∈ ℝ)
25 rexadd 11937 . . . . 5 ((sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) ∈ ℝ ∧ sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < ) ∈ ℝ) → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) +𝑒 sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )) = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) + sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )))
2617, 24, 25syl2anc 691 . . . 4 (𝜑 → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) +𝑒 sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )) = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) + sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )))
2713, 2, 14sge0rern 39281 . . . . . . . 8 (𝜑 → ¬ +∞ ∈ ran 𝐹)
28 nelrnres 38369 . . . . . . . 8 (¬ +∞ ∈ ran 𝐹 → ¬ +∞ ∈ ran (𝐹𝐴))
2927, 28syl 17 . . . . . . 7 (𝜑 → ¬ +∞ ∈ ran (𝐹𝐴))
308, 29fge0iccico 39263 . . . . . 6 (𝜑 → (𝐹𝐴):𝐴⟶(0[,)+∞))
3130sge0rnre 39257 . . . . 5 (𝜑 → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ⊆ ℝ)
32 sge0rnn0 39261 . . . . . 6 ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ≠ ∅
3332a1i 11 . . . . 5 (𝜑 → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ≠ ∅)
341, 30sge0reval 39265 . . . . . . . 8 (𝜑 → (Σ^‘(𝐹𝐴)) = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ*, < ))
3534eqcomd 2616 . . . . . . 7 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ*, < ) = (Σ^‘(𝐹𝐴)))
3635, 15eqeltrd 2688 . . . . . 6 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ*, < ) ∈ ℝ)
37 supxrre3 38482 . . . . . . 7 ((ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ⊆ ℝ ∧ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ≠ ∅) → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ*, < ) ∈ ℝ ↔ ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))𝑡𝑤))
3831, 33, 37syl2anc 691 . . . . . 6 (𝜑 → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ*, < ) ∈ ℝ ↔ ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))𝑡𝑤))
3936, 38mpbid 221 . . . . 5 (𝜑 → ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))𝑡𝑤)
40 nelrnres 38369 . . . . . . . 8 (¬ +∞ ∈ ran 𝐹 → ¬ +∞ ∈ ran (𝐹𝐵))
4127, 40syl 17 . . . . . . 7 (𝜑 → ¬ +∞ ∈ ran (𝐹𝐵))
4221, 41fge0iccico 39263 . . . . . 6 (𝜑 → (𝐹𝐵):𝐵⟶(0[,)+∞))
4342sge0rnre 39257 . . . . 5 (𝜑 → ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ⊆ ℝ)
44 sge0rnn0 39261 . . . . . 6 ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ≠ ∅
4544a1i 11 . . . . 5 (𝜑 → ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ≠ ∅)
4610, 42sge0reval 39265 . . . . . . . 8 (𝜑 → (Σ^‘(𝐹𝐵)) = sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ*, < ))
4746eqcomd 2616 . . . . . . 7 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ*, < ) = (Σ^‘(𝐹𝐵)))
4847, 22eqeltrd 2688 . . . . . 6 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ*, < ) ∈ ℝ)
49 supxrre3 38482 . . . . . . 7 ((ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ⊆ ℝ ∧ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ≠ ∅) → (sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ*, < ) ∈ ℝ ↔ ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑡𝑤))
5043, 45, 49syl2anc 691 . . . . . 6 (𝜑 → (sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ*, < ) ∈ ℝ ↔ ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑡𝑤))
5148, 50mpbid 221 . . . . 5 (𝜑 → ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑡𝑤)
52 eqid 2610 . . . . 5 {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} = {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}
5331, 33, 39, 43, 45, 51, 52supadd 10868 . . . 4 (𝜑 → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) + sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )) = sup({𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}, ℝ, < ))
54 simpl 472 . . . . . . . . . 10 ((𝜑𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}) → 𝜑)
55 vex 3176 . . . . . . . . . . . . 13 𝑟 ∈ V
56 eqeq1 2614 . . . . . . . . . . . . . . 15 (𝑧 = 𝑟 → (𝑧 = (𝑣 + 𝑢) ↔ 𝑟 = (𝑣 + 𝑢)))
5756rexbidv 3034 . . . . . . . . . . . . . 14 (𝑧 = 𝑟 → (∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢) ↔ ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)))
5857rexbidv 3034 . . . . . . . . . . . . 13 (𝑧 = 𝑟 → (∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢) ↔ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)))
5955, 58elab 3319 . . . . . . . . . . . 12 (𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} ↔ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
6059biimpi 205 . . . . . . . . . . 11 (𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
6160adantl 481 . . . . . . . . . 10 ((𝜑𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
62 simpl 472 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)))) → 𝜑)
63 vex 3176 . . . . . . . . . . . . . . . . . . . 20 𝑣 ∈ V
64 sumeq1 14267 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑎 → Σ𝑦𝑥 ((𝐹𝐴)‘𝑦) = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦))
6564cbvmptv 4678 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) = (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑎 ((𝐹𝐴)‘𝑦))
6665elrnmpt 5293 . . . . . . . . . . . . . . . . . . . 20 (𝑣 ∈ V → (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ↔ ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦)))
6763, 66ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ↔ ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦))
6867biimpi 205 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦))
6968adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦))
70 vex 3176 . . . . . . . . . . . . . . . . . . . 20 𝑢 ∈ V
71 sumeq1 14267 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑏 → Σ𝑦𝑥 ((𝐹𝐵)‘𝑦) = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))
7271cbvmptv 4678 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) = (𝑏 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))
7372elrnmpt 5293 . . . . . . . . . . . . . . . . . . . 20 (𝑢 ∈ V → (𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ↔ ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
7470, 73ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ↔ ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))
7574biimpi 205 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) → ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))
7675adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))) → ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))
7769, 76jca 553 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))) → (∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
78 reeanv 3086 . . . . . . . . . . . . . . . 16 (∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) ↔ (∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
7977, 78sylibr 223 . . . . . . . . . . . . . . 15 ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
8079adantl 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
81 eqid 2610 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) = (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))
82 elinel1 3761 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎 ∈ 𝒫 𝐴)
83 elpwi 4117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 ∈ 𝒫 𝐴𝑎𝐴)
84 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎𝐴𝑎𝐴)
8584, 6syl6ss 3580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎𝐴𝑎𝑈)
8683, 85syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 ∈ 𝒫 𝐴𝑎𝑈)
8782, 86syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎𝑈)
8887adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎𝑈)
89 elinel1 3761 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → 𝑏 ∈ 𝒫 𝐵)
90 elpwi 4117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑏 ∈ 𝒫 𝐵𝑏𝐵)
91 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑏𝐵𝑏𝐵)
9291, 19syl6ss 3580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑏𝐵𝑏𝑈)
9390, 92syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑏 ∈ 𝒫 𝐵𝑏𝑈)
9489, 93syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → 𝑏𝑈)
9594adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑏𝑈)
9688, 95unssd 3751 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑎𝑏) ⊆ 𝑈)
97 vex 3176 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑎 ∈ V
98 vex 3176 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑏 ∈ V
9997, 98unex 6854 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎𝑏) ∈ V
10099elpw 4114 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎𝑏) ∈ 𝒫 𝑈 ↔ (𝑎𝑏) ⊆ 𝑈)
10196, 100sylibr 223 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑎𝑏) ∈ 𝒫 𝑈)
102 elinel2 3762 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎 ∈ Fin)
103102adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎 ∈ Fin)
104 elinel2 3762 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → 𝑏 ∈ Fin)
105104adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑏 ∈ Fin)
106 unfi 8112 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ Fin ∧ 𝑏 ∈ Fin) → (𝑎𝑏) ∈ Fin)
107103, 105, 106syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑎𝑏) ∈ Fin)
108101, 107elind 3760 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑎𝑏) ∈ (𝒫 𝑈 ∩ Fin))
109108adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝑎𝑏) ∈ (𝒫 𝑈 ∩ Fin))
110109ad2antrr 758 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → (𝑎𝑏) ∈ (𝒫 𝑈 ∩ Fin))
111 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) → 𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦))
112 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) → 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))
113111, 112oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) → (𝑣 + 𝑢) = (Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) + Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
114113adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) → (𝑣 + 𝑢) = (Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) + Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
11582, 83syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎𝐴)
116115sselda 3568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑦𝑎) → 𝑦𝐴)
117 fvres 6117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦𝐴 → ((𝐹𝐴)‘𝑦) = (𝐹𝑦))
118116, 117syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑦𝑎) → ((𝐹𝐴)‘𝑦) = (𝐹𝑦))
119118sumeq2dv 14281 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) = Σ𝑦𝑎 (𝐹𝑦))
120119adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) = Σ𝑦𝑎 (𝐹𝑦))
12189, 90syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → 𝑏𝐵)
122121sselda 3568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑏 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑦𝑏) → 𝑦𝐵)
123 fvres 6117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦𝐵 → ((𝐹𝐵)‘𝑦) = (𝐹𝑦))
124122, 123syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑏 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑦𝑏) → ((𝐹𝐵)‘𝑦) = (𝐹𝑦))
125124sumeq2dv 14281 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → Σ𝑦𝑏 ((𝐹𝐵)‘𝑦) = Σ𝑦𝑏 (𝐹𝑦))
126125adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → Σ𝑦𝑏 ((𝐹𝐵)‘𝑦) = Σ𝑦𝑏 (𝐹𝑦))
127120, 126oveq12d 6567 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) + Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) = (Σ𝑦𝑎 (𝐹𝑦) + Σ𝑦𝑏 (𝐹𝑦)))
128127adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) → (Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) + Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) = (Σ𝑦𝑎 (𝐹𝑦) + Σ𝑦𝑏 (𝐹𝑦)))
129114, 128eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) → (𝑣 + 𝑢) = (Σ𝑦𝑎 (𝐹𝑦) + Σ𝑦𝑏 (𝐹𝑦)))
130129ad4ant23 1289 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → (𝑣 + 𝑢) = (Σ𝑦𝑎 (𝐹𝑦) + Σ𝑦𝑏 (𝐹𝑦)))
131 simpr 476 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → 𝑟 = (𝑣 + 𝑢))
132 sge0resplit.in0 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴𝐵) = ∅)
133132adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝐴𝐵) = ∅)
134115ad2antrl 760 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → 𝑎𝐴)
135121adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑏𝐵)
136135adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → 𝑏𝐵)
137 ssin0 38248 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴𝐵) = ∅ ∧ 𝑎𝐴𝑏𝐵) → (𝑎𝑏) = ∅)
138133, 134, 136, 137syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝑎𝑏) = ∅)
139 eqidd 2611 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝑎𝑏) = (𝑎𝑏))
140107adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝑎𝑏) ∈ Fin)
141 rge0ssre 12151 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0[,)+∞) ⊆ ℝ
142 ax-resscn 9872 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ℝ ⊆ ℂ
143141, 142sstri 3577 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0[,)+∞) ⊆ ℂ
1442, 27fge0iccico 39263 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐹:𝑈⟶(0[,)+∞))
145144ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ 𝑦 ∈ (𝑎𝑏)) → 𝐹:𝑈⟶(0[,)+∞))
14696sselda 3568 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) ∧ 𝑦 ∈ (𝑎𝑏)) → 𝑦𝑈)
147146adantll 746 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ 𝑦 ∈ (𝑎𝑏)) → 𝑦𝑈)
148145, 147ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ 𝑦 ∈ (𝑎𝑏)) → (𝐹𝑦) ∈ (0[,)+∞))
149143, 148sseldi 3566 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ 𝑦 ∈ (𝑎𝑏)) → (𝐹𝑦) ∈ ℂ)
150138, 139, 140, 149fsumsplit 14318 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → Σ𝑦 ∈ (𝑎𝑏)(𝐹𝑦) = (Σ𝑦𝑎 (𝐹𝑦) + Σ𝑦𝑏 (𝐹𝑦)))
151150ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → Σ𝑦 ∈ (𝑎𝑏)(𝐹𝑦) = (Σ𝑦𝑎 (𝐹𝑦) + Σ𝑦𝑏 (𝐹𝑦)))
152130, 131, 1513eqtr4d 2654 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → 𝑟 = Σ𝑦 ∈ (𝑎𝑏)(𝐹𝑦))
153 sumeq1 14267 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = (𝑎𝑏) → Σ𝑦𝑥 (𝐹𝑦) = Σ𝑦 ∈ (𝑎𝑏)(𝐹𝑦))
154153eqeq2d 2620 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = (𝑎𝑏) → (𝑟 = Σ𝑦𝑥 (𝐹𝑦) ↔ 𝑟 = Σ𝑦 ∈ (𝑎𝑏)(𝐹𝑦)))
155154rspcev 3282 . . . . . . . . . . . . . . . . . . . . 21 (((𝑎𝑏) ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦 ∈ (𝑎𝑏)(𝐹𝑦)) → ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦𝑥 (𝐹𝑦))
156110, 152, 155syl2anc 691 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦𝑥 (𝐹𝑦))
15755a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → 𝑟 ∈ V)
15881, 156, 157elrnmptd 38361 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))
159158ex 449 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
160159ex 449 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → ((𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))))
161160ex 449 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → ((𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))))
162161rexlimdvv 3019 . . . . . . . . . . . . . . 15 (𝜑 → (∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))))
163162imp 444 . . . . . . . . . . . . . 14 ((𝜑 ∧ ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
16462, 80, 163syl2anc 691 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)))) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
165164ex 449 . . . . . . . . . . . 12 (𝜑 → ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))))
166165rexlimdvv 3019 . . . . . . . . . . 11 (𝜑 → (∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
167166imp 444 . . . . . . . . . 10 ((𝜑 ∧ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))
16854, 61, 167syl2anc 691 . . . . . . . . 9 ((𝜑𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))
169168ex 449 . . . . . . . 8 (𝜑 → (𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
17081elrnmpt 5293 . . . . . . . . . . . . 13 (𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) → (𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦𝑥 (𝐹𝑦)))
171170ibi 255 . . . . . . . . . . . 12 (𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) → ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦𝑥 (𝐹𝑦))
172171adantl 481 . . . . . . . . . . 11 ((𝜑𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦𝑥 (𝐹𝑦))
173 nfv 1830 . . . . . . . . . . . . 13 𝑥𝜑
174 nfcv 2751 . . . . . . . . . . . . . 14 𝑥𝑟
175 nfmpt1 4675 . . . . . . . . . . . . . . 15 𝑥(𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))
176175nfrn 5289 . . . . . . . . . . . . . 14 𝑥ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))
177174, 176nfel 2763 . . . . . . . . . . . . 13 𝑥 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))
178173, 177nfan 1816 . . . . . . . . . . . 12 𝑥(𝜑𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))
179 nfmpt1 4675 . . . . . . . . . . . . . 14 𝑥(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))
180179nfrn 5289 . . . . . . . . . . . . 13 𝑥ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))
181 nfmpt1 4675 . . . . . . . . . . . . . . 15 𝑥(𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))
182181nfrn 5289 . . . . . . . . . . . . . 14 𝑥ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))
183 nfv 1830 . . . . . . . . . . . . . 14 𝑥 𝑟 = (𝑣 + 𝑢)
184182, 183nfrex 2990 . . . . . . . . . . . . 13 𝑥𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)
185180, 184nfrex 2990 . . . . . . . . . . . 12 𝑥𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)
186 inss2 3796 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐴) ⊆ 𝐴
187186sseli 3564 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝑥𝐴) → 𝑦𝐴)
188187adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦 ∈ (𝑥𝐴)) → 𝑦𝐴)
189117eqcomd 2616 . . . . . . . . . . . . . . . . . . 19 (𝑦𝐴 → (𝐹𝑦) = ((𝐹𝐴)‘𝑦))
190188, 189syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦 ∈ (𝑥𝐴)) → (𝐹𝑦) = ((𝐹𝐴)‘𝑦))
191190sumeq2dv 14281 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) = Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦))
192 sumeq1 14267 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 → Σ𝑦𝑥 ((𝐹𝐴)‘𝑦) = Σ𝑦𝑧 ((𝐹𝐴)‘𝑦))
193192cbvmptv 4678 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) = (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑧 ((𝐹𝐴)‘𝑦))
194 vex 3176 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥 ∈ V
195194inex1 4727 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥𝐴) ∈ V
196195elpw 4114 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝐴) ∈ 𝒫 𝐴 ↔ (𝑥𝐴) ⊆ 𝐴)
197186, 196mpbir 220 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐴) ∈ 𝒫 𝐴
198197a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐴) ∈ 𝒫 𝐴)
199 elinel2 3762 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 ∈ Fin)
200 inss1 3795 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐴) ⊆ 𝑥
201200a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐴) ⊆ 𝑥)
202 ssfi 8065 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ Fin ∧ (𝑥𝐴) ⊆ 𝑥) → (𝑥𝐴) ∈ Fin)
203199, 201, 202syl2anc 691 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐴) ∈ Fin)
204198, 203elind 3760 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐴) ∈ (𝒫 𝐴 ∩ Fin))
205 eqidd 2611 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) = Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦))
206 sumeq1 14267 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = (𝑥𝐴) → Σ𝑦𝑧 ((𝐹𝐴)‘𝑦) = Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦))
207206eqeq2d 2620 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝑥𝐴) → (Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) = Σ𝑦𝑧 ((𝐹𝐴)‘𝑦) ↔ Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) = Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦)))
208207rspcev 3282 . . . . . . . . . . . . . . . . . . 19 (((𝑥𝐴) ∈ (𝒫 𝐴 ∩ Fin) ∧ Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) = Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) = Σ𝑦𝑧 ((𝐹𝐴)‘𝑦))
209204, 205, 208syl2anc 691 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) = Σ𝑦𝑧 ((𝐹𝐴)‘𝑦))
210 sumex 14266 . . . . . . . . . . . . . . . . . . 19 Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) ∈ V
211210a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) ∈ V)
212193, 209, 211elrnmptd 38361 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)))
213191, 212eqeltrd 2688 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)))
2142133ad2ant2 1076 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)))
215 sumeq1 14267 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → Σ𝑦𝑥 ((𝐹𝐵)‘𝑦) = Σ𝑦𝑧 ((𝐹𝐵)‘𝑦))
216215cbvmptv 4678 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) = (𝑧 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑧 ((𝐹𝐵)‘𝑦))
217 inss2 3796 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐵) ⊆ 𝐵
218194inex1 4727 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐵) ∈ V
219218elpw 4114 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝐵) ∈ 𝒫 𝐵 ↔ (𝑥𝐵) ⊆ 𝐵)
220217, 219mpbir 220 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝐵) ∈ 𝒫 𝐵
221220a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → (𝑥𝐵) ∈ 𝒫 𝐵)
222 inss1 3795 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐵) ⊆ 𝑥
223222a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐵) ⊆ 𝑥)
224 ssfi 8065 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ Fin ∧ (𝑥𝐵) ⊆ 𝑥) → (𝑥𝐵) ∈ Fin)
225199, 223, 224syl2anc 691 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐵) ∈ Fin)
2262253ad2ant2 1076 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → (𝑥𝐵) ∈ Fin)
227221, 226elind 3760 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → (𝑥𝐵) ∈ (𝒫 𝐵 ∩ Fin))
228217sseli 3564 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (𝑥𝐵) → 𝑦𝐵)
229123eqcomd 2616 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝐵 → (𝐹𝑦) = ((𝐹𝐵)‘𝑦))
230228, 229syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (𝑥𝐵) → (𝐹𝑦) = ((𝐹𝐵)‘𝑦))
231230sumeq2i 14277 . . . . . . . . . . . . . . . . . . . 20 Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦)
232231a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦))
2332323adant3 1074 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦))
234 sumeq1 14267 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝑥𝐵) → Σ𝑦𝑧 ((𝐹𝐵)‘𝑦) = Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦))
235234eqeq2d 2620 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑥𝐵) → (Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦𝑧 ((𝐹𝐵)‘𝑦) ↔ Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦)))
236235rspcev 3282 . . . . . . . . . . . . . . . . . 18 (((𝑥𝐵) ∈ (𝒫 𝐵 ∩ Fin) ∧ Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦)) → ∃𝑧 ∈ (𝒫 𝐵 ∩ Fin)Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦𝑧 ((𝐹𝐵)‘𝑦))
237227, 233, 236syl2anc 691 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → ∃𝑧 ∈ (𝒫 𝐵 ∩ Fin)Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦𝑧 ((𝐹𝐵)‘𝑦))
238 sumex 14266 . . . . . . . . . . . . . . . . . 18 Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ V
239238a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ V)
240216, 237, 239elrnmptd 38361 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)))
241 simp3 1056 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → 𝑟 = Σ𝑦𝑥 (𝐹𝑦))
242186a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑥𝐴) ⊆ 𝐴)
243217a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑥𝐵) ⊆ 𝐵)
244 ssin0 38248 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴𝐵) = ∅ ∧ (𝑥𝐴) ⊆ 𝐴 ∧ (𝑥𝐵) ⊆ 𝐵) → ((𝑥𝐴) ∩ (𝑥𝐵)) = ∅)
245132, 242, 243, 244syl3anc 1318 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑥𝐴) ∩ (𝑥𝐵)) = ∅)
246245adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → ((𝑥𝐴) ∩ (𝑥𝐵)) = ∅)
247 elinel1 3761 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 ∈ 𝒫 𝑈)
248 elpwi 4117 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ 𝒫 𝑈𝑥𝑈)
249247, 248syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥𝑈)
2504ineq2i 3773 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥𝑈) = (𝑥 ∩ (𝐴𝐵))
251250a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝑈 → (𝑥𝑈) = (𝑥 ∩ (𝐴𝐵)))
252 dfss 3555 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥𝑈𝑥 = (𝑥𝑈))
253252biimpi 205 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝑈𝑥 = (𝑥𝑈))
254 indi 3832 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∩ (𝐴𝐵)) = ((𝑥𝐴) ∪ (𝑥𝐵))
255254eqcomi 2619 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥𝐴) ∪ (𝑥𝐵)) = (𝑥 ∩ (𝐴𝐵))
256255a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝑈 → ((𝑥𝐴) ∪ (𝑥𝐵)) = (𝑥 ∩ (𝐴𝐵)))
257251, 253, 2563eqtr4d 2654 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑈𝑥 = ((𝑥𝐴) ∪ (𝑥𝐵)))
258249, 257syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 = ((𝑥𝐴) ∪ (𝑥𝐵)))
259258adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝑥 = ((𝑥𝐴) ∪ (𝑥𝐵)))
260199adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝑥 ∈ Fin)
261144ad2antrr 758 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → 𝐹:𝑈⟶(0[,)+∞))
262249sselda 3568 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦𝑥) → 𝑦𝑈)
263262adantll 746 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → 𝑦𝑈)
264261, 263ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ (0[,)+∞))
265143, 264sseldi 3566 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ ℂ)
266246, 259, 260, 265fsumsplit 14318 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦𝑥 (𝐹𝑦) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
2672663adant3 1074 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → Σ𝑦𝑥 (𝐹𝑦) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
268241, 267eqtrd 2644 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → 𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
269 oveq2 6557 . . . . . . . . . . . . . . . . . 18 (𝑢 = Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) → (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
270269eqeq2d 2620 . . . . . . . . . . . . . . . . 17 (𝑢 = Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) → (𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢) ↔ 𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦))))
271270rspcev 3282 . . . . . . . . . . . . . . . 16 ((Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ∧ 𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦))) → ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢))
272240, 268, 271syl2anc 691 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢))
273 oveq1 6556 . . . . . . . . . . . . . . . . . 18 (𝑣 = Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) → (𝑣 + 𝑢) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢))
274273eqeq2d 2620 . . . . . . . . . . . . . . . . 17 (𝑣 = Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) → (𝑟 = (𝑣 + 𝑢) ↔ 𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢)))
275274rexbidv 3034 . . . . . . . . . . . . . . . 16 (𝑣 = Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) → (∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢) ↔ ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢)))
276275rspcev 3282 . . . . . . . . . . . . . . 15 ((Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢)) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
277214, 272, 276syl2anc 691 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
2782773exp 1256 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑟 = Σ𝑦𝑥 (𝐹𝑦) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))))
279278adantr 480 . . . . . . . . . . . 12 ((𝜑𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑟 = Σ𝑦𝑥 (𝐹𝑦) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))))
280178, 185, 279rexlimd 3008 . . . . . . . . . . 11 ((𝜑𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → (∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦𝑥 (𝐹𝑦) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)))
281172, 280mpd 15 . . . . . . . . . 10 ((𝜑𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
282281, 59sylibr 223 . . . . . . . . 9 ((𝜑𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → 𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)})
283282ex 449 . . . . . . . 8 (𝜑 → (𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) → 𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}))
284169, 283impbid 201 . . . . . . 7 (𝜑 → (𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} ↔ 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
285284alrimiv 1842 . . . . . 6 (𝜑 → ∀𝑟(𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} ↔ 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
286 dfcleq 2604 . . . . . 6 ({𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} = ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ↔ ∀𝑟(𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} ↔ 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
287285, 286sylibr 223 . . . . 5 (𝜑 → {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} = ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))
288287supeq1d 8235 . . . 4 (𝜑 → sup({𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}, ℝ, < ) = sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ, < ))
28926, 53, 2883eqtrrd 2649 . . 3 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ, < ) = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) +𝑒 sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )))
29013, 2, 14sge0supre 39282 . . 3 (𝜑 → (Σ^𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ, < ))
29116, 23oveq12d 6567 . . 3 (𝜑 → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) +𝑒 sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )))
292289, 290, 2913eqtr4d 2654 . 2 (𝜑 → (Σ^𝐹) = ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
293 rexadd 11937 . . 3 (((Σ^‘(𝐹𝐴)) ∈ ℝ ∧ (Σ^‘(𝐹𝐵)) ∈ ℝ) → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = ((Σ^‘(𝐹𝐴)) + (Σ^‘(𝐹𝐵))))
29415, 22, 293syl2anc 691 . 2 (𝜑 → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = ((Σ^‘(𝐹𝐴)) + (Σ^‘(𝐹𝐵))))
295292, 294eqtrd 2644 1 (𝜑 → (Σ^𝐹) = ((Σ^‘(𝐹𝐴)) + (Σ^‘(𝐹𝐵))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031  ∀wal 1473   = wceq 1475   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108   class class class wbr 4583   ↦ cmpt 4643  ran crn 5039   ↾ cres 5040  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  Fincfn 7841  supcsup 8229  ℂcc 9813  ℝcr 9814  0cc0 9815   + caddc 9818  +∞cpnf 9950  ℝ*cxr 9952   < clt 9953   ≤ cle 9954   +𝑒 cxad 11820  [,)cico 12048  [,]cicc 12049  Σcsu 14264  Σ^csumge0 39255 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-xadd 11823  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-sum 14265  df-sumge0 39256 This theorem is referenced by:  sge0split  39302
 Copyright terms: Public domain W3C validator