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 44995
Description: Σ^ splits into two parts, when it's a real number. This is a special case of sge0split 44998. (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 4170 . . . . . . . . . 10 𝐴 ⊆ (𝐴𝐵)
4 sge0resplit.u . . . . . . . . . . 11 𝑈 = (𝐴𝐵)
54eqcomi 2742 . . . . . . . . . 10 (𝐴𝐵) = 𝑈
63, 5sseqtri 4016 . . . . . . . . 9 𝐴𝑈
76a1i 11 . . . . . . . 8 (𝜑𝐴𝑈)
82, 7fssresd 6748 . . . . . . 7 (𝜑 → (𝐹𝐴):𝐴⟶(0[,]+∞))
94a1i 11 . . . . . . . . 9 (𝜑𝑈 = (𝐴𝐵))
10 sge0resplit.b . . . . . . . . . 10 (𝜑𝐵𝑊)
11 unexg 7723 . . . . . . . . . 10 ((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)
121, 10, 11syl2anc 585 . . . . . . . . 9 (𝜑 → (𝐴𝐵) ∈ V)
139, 12eqeltrd 2834 . . . . . . . 8 (𝜑𝑈 ∈ V)
14 sge0resplit.re . . . . . . . 8 (𝜑 → (Σ^𝐹) ∈ ℝ)
1513, 2, 14sge0ssre 44986 . . . . . . 7 (𝜑 → (Σ^‘(𝐹𝐴)) ∈ ℝ)
161, 8, 15sge0supre 44978 . . . . . 6 (𝜑 → (Σ^‘(𝐹𝐴)) = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ))
1716, 15eqeltrrd 2835 . . . . 5 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) ∈ ℝ)
18 ssun2 4171 . . . . . . . . . 10 𝐵 ⊆ (𝐴𝐵)
1918, 5sseqtri 4016 . . . . . . . . 9 𝐵𝑈
2019a1i 11 . . . . . . . 8 (𝜑𝐵𝑈)
212, 20fssresd 6748 . . . . . . 7 (𝜑 → (𝐹𝐵):𝐵⟶(0[,]+∞))
2213, 2, 14sge0ssre 44986 . . . . . . 7 (𝜑 → (Σ^‘(𝐹𝐵)) ∈ ℝ)
2310, 21, 22sge0supre 44978 . . . . . 6 (𝜑 → (Σ^‘(𝐹𝐵)) = sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < ))
2423, 22eqeltrrd 2835 . . . . 5 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < ) ∈ ℝ)
25 rexadd 13198 . . . . 5 ((sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) ∈ ℝ ∧ sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < ) ∈ ℝ) → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) +𝑒 sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )) = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) + sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )))
2617, 24, 25syl2anc 585 . . . 4 (𝜑 → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) +𝑒 sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )) = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) + sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )))
2713, 2, 14sge0rern 44977 . . . . . . . 8 (𝜑 → ¬ +∞ ∈ ran 𝐹)
28 nelrnres 43756 . . . . . . . 8 (¬ +∞ ∈ ran 𝐹 → ¬ +∞ ∈ ran (𝐹𝐴))
2927, 28syl 17 . . . . . . 7 (𝜑 → ¬ +∞ ∈ ran (𝐹𝐴))
308, 29fge0iccico 44959 . . . . . 6 (𝜑 → (𝐹𝐴):𝐴⟶(0[,)+∞))
3130sge0rnre 44953 . . . . 5 (𝜑 → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ⊆ ℝ)
32 sge0rnn0 44957 . . . . . 6 ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ≠ ∅
3332a1i 11 . . . . 5 (𝜑 → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ≠ ∅)
341, 30sge0reval 44961 . . . . . . . 8 (𝜑 → (Σ^‘(𝐹𝐴)) = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ*, < ))
3534eqcomd 2739 . . . . . . 7 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ*, < ) = (Σ^‘(𝐹𝐴)))
3635, 15eqeltrd 2834 . . . . . 6 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ*, < ) ∈ ℝ)
37 supxrre3 43908 . . . . . . 7 ((ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ⊆ ℝ ∧ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ≠ ∅) → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ*, < ) ∈ ℝ ↔ ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))𝑡𝑤))
3831, 33, 37syl2anc 585 . . . . . 6 (𝜑 → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ*, < ) ∈ ℝ ↔ ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))𝑡𝑤))
3936, 38mpbid 231 . . . . 5 (𝜑 → ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))𝑡𝑤)
40 nelrnres 43756 . . . . . . . 8 (¬ +∞ ∈ ran 𝐹 → ¬ +∞ ∈ ran (𝐹𝐵))
4127, 40syl 17 . . . . . . 7 (𝜑 → ¬ +∞ ∈ ran (𝐹𝐵))
4221, 41fge0iccico 44959 . . . . . 6 (𝜑 → (𝐹𝐵):𝐵⟶(0[,)+∞))
4342sge0rnre 44953 . . . . 5 (𝜑 → ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ⊆ ℝ)
44 sge0rnn0 44957 . . . . . 6 ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ≠ ∅
4544a1i 11 . . . . 5 (𝜑 → ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ≠ ∅)
4610, 42sge0reval 44961 . . . . . . . 8 (𝜑 → (Σ^‘(𝐹𝐵)) = sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ*, < ))
4746eqcomd 2739 . . . . . . 7 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ*, < ) = (Σ^‘(𝐹𝐵)))
4847, 22eqeltrd 2834 . . . . . 6 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ*, < ) ∈ ℝ)
49 supxrre3 43908 . . . . . . 7 ((ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ⊆ ℝ ∧ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ≠ ∅) → (sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ*, < ) ∈ ℝ ↔ ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑡𝑤))
5043, 45, 49syl2anc 585 . . . . . 6 (𝜑 → (sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ*, < ) ∈ ℝ ↔ ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑡𝑤))
5148, 50mpbid 231 . . . . 5 (𝜑 → ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑡𝑤)
52 eqid 2733 . . . . 5 {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} = {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}
5331, 33, 39, 43, 45, 51, 52supadd 12169 . . . 4 (𝜑 → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) + sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )) = sup({𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}, ℝ, < ))
54 simpl 484 . . . . . . . . . 10 ((𝜑𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}) → 𝜑)
55 vex 3479 . . . . . . . . . . . . 13 𝑟 ∈ V
56 eqeq1 2737 . . . . . . . . . . . . . . 15 (𝑧 = 𝑟 → (𝑧 = (𝑣 + 𝑢) ↔ 𝑟 = (𝑣 + 𝑢)))
5756rexbidv 3179 . . . . . . . . . . . . . 14 (𝑧 = 𝑟 → (∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢) ↔ ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)))
5857rexbidv 3179 . . . . . . . . . . . . 13 (𝑧 = 𝑟 → (∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢) ↔ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)))
5955, 58elab 3666 . . . . . . . . . . . 12 (𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} ↔ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
6059biimpi 215 . . . . . . . . . . 11 (𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
6160adantl 483 . . . . . . . . . 10 ((𝜑𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
62 simpl 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)))) → 𝜑)
63 vex 3479 . . . . . . . . . . . . . . . . . . . 20 𝑣 ∈ V
64 sumeq1 15622 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑎 → Σ𝑦𝑥 ((𝐹𝐴)‘𝑦) = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦))
6564cbvmptv 5257 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) = (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑎 ((𝐹𝐴)‘𝑦))
6665elrnmpt 5950 . . . . . . . . . . . . . . . . . . . 20 (𝑣 ∈ V → (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ↔ ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦)))
6763, 66ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ↔ ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦))
6867biimpi 215 . . . . . . . . . . . . . . . . . 18 (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦))
6968adantr 482 . . . . . . . . . . . . . . . . 17 ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦))
70 vex 3479 . . . . . . . . . . . . . . . . . . . 20 𝑢 ∈ V
71 sumeq1 15622 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑏 → Σ𝑦𝑥 ((𝐹𝐵)‘𝑦) = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))
7271cbvmptv 5257 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) = (𝑏 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))
7372elrnmpt 5950 . . . . . . . . . . . . . . . . . . . 20 (𝑢 ∈ V → (𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ↔ ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
7470, 73ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ↔ ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))
7574biimpi 215 . . . . . . . . . . . . . . . . . 18 (𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) → ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))
7675adantl 483 . . . . . . . . . . . . . . . . 17 ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))) → ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))
7769, 76jca 513 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))) → (∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
78 reeanv 3227 . . . . . . . . . . . . . . . 16 (∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) ↔ (∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
7977, 78sylibr 233 . . . . . . . . . . . . . . 15 ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
8079adantl 483 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
81 eqid 2733 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) = (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))
82 elinel1 4193 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎 ∈ 𝒫 𝐴)
83 elpwi 4605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 ∈ 𝒫 𝐴𝑎𝐴)
84 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎𝐴𝑎𝐴)
8584, 6sstrdi 3992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎𝐴𝑎𝑈)
8683, 85syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 ∈ 𝒫 𝐴𝑎𝑈)
8782, 86syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎𝑈)
8887adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎𝑈)
89 elinel1 4193 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → 𝑏 ∈ 𝒫 𝐵)
90 elpwi 4605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑏 ∈ 𝒫 𝐵𝑏𝐵)
91 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑏𝐵𝑏𝐵)
9291, 19sstrdi 3992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑏𝐵𝑏𝑈)
9390, 92syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑏 ∈ 𝒫 𝐵𝑏𝑈)
9489, 93syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → 𝑏𝑈)
9594adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑏𝑈)
9688, 95unssd 4184 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑎𝑏) ⊆ 𝑈)
97 vex 3479 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑎 ∈ V
98 vex 3479 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑏 ∈ V
9997, 98unex 7720 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎𝑏) ∈ V
10099elpw 4602 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎𝑏) ∈ 𝒫 𝑈 ↔ (𝑎𝑏) ⊆ 𝑈)
10196, 100sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑎𝑏) ∈ 𝒫 𝑈)
102 elinel2 4194 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎 ∈ Fin)
103102adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎 ∈ Fin)
104 elinel2 4194 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → 𝑏 ∈ Fin)
105104adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑏 ∈ Fin)
106 unfi 9160 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ Fin ∧ 𝑏 ∈ Fin) → (𝑎𝑏) ∈ Fin)
107103, 105, 106syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑎𝑏) ∈ Fin)
108101, 107elind 4192 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑎𝑏) ∈ (𝒫 𝑈 ∩ Fin))
109108adantl 483 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝑎𝑏) ∈ (𝒫 𝑈 ∩ Fin))
110109ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → (𝑎𝑏) ∈ (𝒫 𝑈 ∩ Fin))
111 simpl 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) → 𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦))
112 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) → 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))
113111, 112oveq12d 7414 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) → (𝑣 + 𝑢) = (Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) + Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
114113adantl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) → (𝑣 + 𝑢) = (Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) + Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)))
11582, 83syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎𝐴)
116115sselda 3980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑦𝑎) → 𝑦𝐴)
117 fvres 6900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦𝐴 → ((𝐹𝐴)‘𝑦) = (𝐹𝑦))
118116, 117syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑦𝑎) → ((𝐹𝐴)‘𝑦) = (𝐹𝑦))
119118sumeq2dv 15636 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) = Σ𝑦𝑎 (𝐹𝑦))
120119adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) = Σ𝑦𝑎 (𝐹𝑦))
12189, 90syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → 𝑏𝐵)
122121sselda 3980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑏 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑦𝑏) → 𝑦𝐵)
123 fvres 6900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦𝐵 → ((𝐹𝐵)‘𝑦) = (𝐹𝑦))
124122, 123syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑏 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑦𝑏) → ((𝐹𝐵)‘𝑦) = (𝐹𝑦))
125124sumeq2dv 15636 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → Σ𝑦𝑏 ((𝐹𝐵)‘𝑦) = Σ𝑦𝑏 (𝐹𝑦))
126125adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → Σ𝑦𝑏 ((𝐹𝐵)‘𝑦) = Σ𝑦𝑏 (𝐹𝑦))
127120, 126oveq12d 7414 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) + Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) = (Σ𝑦𝑎 (𝐹𝑦) + Σ𝑦𝑏 (𝐹𝑦)))
128127adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) → (Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) + Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) = (Σ𝑦𝑎 (𝐹𝑦) + Σ𝑦𝑏 (𝐹𝑦)))
129114, 128eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) → (𝑣 + 𝑢) = (Σ𝑦𝑎 (𝐹𝑦) + Σ𝑦𝑏 (𝐹𝑦)))
130129ad4ant23 752 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → (𝑣 + 𝑢) = (Σ𝑦𝑎 (𝐹𝑦) + Σ𝑦𝑏 (𝐹𝑦)))
131 simpr 486 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → 𝑟 = (𝑣 + 𝑢))
132 sge0resplit.in0 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴𝐵) = ∅)
133132adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝐴𝐵) = ∅)
134115ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → 𝑎𝐴)
135121adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑏𝐵)
136135adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → 𝑏𝐵)
137 ssin0 43613 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴𝐵) = ∅ ∧ 𝑎𝐴𝑏𝐵) → (𝑎𝑏) = ∅)
138133, 134, 136, 137syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝑎𝑏) = ∅)
139 eqidd 2734 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝑎𝑏) = (𝑎𝑏))
140107adantl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝑎𝑏) ∈ Fin)
141 rge0ssre 13420 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0[,)+∞) ⊆ ℝ
142 ax-resscn 11154 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ℝ ⊆ ℂ
143141, 142sstri 3989 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0[,)+∞) ⊆ ℂ
1442, 27fge0iccico 44959 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐹:𝑈⟶(0[,)+∞))
145144ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ 𝑦 ∈ (𝑎𝑏)) → 𝐹:𝑈⟶(0[,)+∞))
14696sselda 3980 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) ∧ 𝑦 ∈ (𝑎𝑏)) → 𝑦𝑈)
147146adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ 𝑦 ∈ (𝑎𝑏)) → 𝑦𝑈)
148145, 147ffvelcdmd 7075 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ 𝑦 ∈ (𝑎𝑏)) → (𝐹𝑦) ∈ (0[,)+∞))
149143, 148sselid 3978 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ 𝑦 ∈ (𝑎𝑏)) → (𝐹𝑦) ∈ ℂ)
150138, 139, 140, 149fsumsplit 15674 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → Σ𝑦 ∈ (𝑎𝑏)(𝐹𝑦) = (Σ𝑦𝑎 (𝐹𝑦) + Σ𝑦𝑏 (𝐹𝑦)))
151150ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → Σ𝑦 ∈ (𝑎𝑏)(𝐹𝑦) = (Σ𝑦𝑎 (𝐹𝑦) + Σ𝑦𝑏 (𝐹𝑦)))
152130, 131, 1513eqtr4d 2783 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → 𝑟 = Σ𝑦 ∈ (𝑎𝑏)(𝐹𝑦))
153 sumeq1 15622 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = (𝑎𝑏) → Σ𝑦𝑥 (𝐹𝑦) = Σ𝑦 ∈ (𝑎𝑏)(𝐹𝑦))
154153rspceeqv 3631 . . . . . . . . . . . . . . . . . . . . 21 (((𝑎𝑏) ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦 ∈ (𝑎𝑏)(𝐹𝑦)) → ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦𝑥 (𝐹𝑦))
155110, 152, 154syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦𝑥 (𝐹𝑦))
15655a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → 𝑟 ∈ V)
15781, 155, 156elrnmptd 5955 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))
158157ex 414 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
159158ex 414 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → ((𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))))
160159ex 414 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → ((𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))))
161160rexlimdvv 3211 . . . . . . . . . . . . . . 15 (𝜑 → (∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦)) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))))
162161imp 408 . . . . . . . . . . . . . 14 ((𝜑 ∧ ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦𝑎 ((𝐹𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦𝑏 ((𝐹𝐵)‘𝑦))) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
16362, 80, 162syl2anc 585 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)))) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
164163ex 414 . . . . . . . . . . . 12 (𝜑 → ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))))
165164rexlimdvv 3211 . . . . . . . . . . 11 (𝜑 → (∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
166165imp 408 . . . . . . . . . 10 ((𝜑 ∧ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))
16754, 61, 166syl2anc 585 . . . . . . . . 9 ((𝜑𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))
168167ex 414 . . . . . . . 8 (𝜑 → (𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
16981elrnmpt 5950 . . . . . . . . . . . . 13 (𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) → (𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦𝑥 (𝐹𝑦)))
170169ibi 267 . . . . . . . . . . . 12 (𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) → ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦𝑥 (𝐹𝑦))
171170adantl 483 . . . . . . . . . . 11 ((𝜑𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦𝑥 (𝐹𝑦))
172 nfv 1918 . . . . . . . . . . . . 13 𝑥𝜑
173 nfcv 2904 . . . . . . . . . . . . . 14 𝑥𝑟
174 nfmpt1 5252 . . . . . . . . . . . . . . 15 𝑥(𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))
175174nfrn 5946 . . . . . . . . . . . . . 14 𝑥ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))
176173, 175nfel 2918 . . . . . . . . . . . . 13 𝑥 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))
177172, 176nfan 1903 . . . . . . . . . . . 12 𝑥(𝜑𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))
178 nfmpt1 5252 . . . . . . . . . . . . . 14 𝑥(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))
179178nfrn 5946 . . . . . . . . . . . . 13 𝑥ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))
180 nfmpt1 5252 . . . . . . . . . . . . . . 15 𝑥(𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))
181180nfrn 5946 . . . . . . . . . . . . . 14 𝑥ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))
182 nfv 1918 . . . . . . . . . . . . . 14 𝑥 𝑟 = (𝑣 + 𝑢)
183181, 182nfrexw 3311 . . . . . . . . . . . . 13 𝑥𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)
184179, 183nfrexw 3311 . . . . . . . . . . . 12 𝑥𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)
185 inss2 4227 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐴) ⊆ 𝐴
186185sseli 3976 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝑥𝐴) → 𝑦𝐴)
187186adantl 483 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦 ∈ (𝑥𝐴)) → 𝑦𝐴)
188117eqcomd 2739 . . . . . . . . . . . . . . . . . . 19 (𝑦𝐴 → (𝐹𝑦) = ((𝐹𝐴)‘𝑦))
189187, 188syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦 ∈ (𝑥𝐴)) → (𝐹𝑦) = ((𝐹𝐴)‘𝑦))
190189sumeq2dv 15636 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) = Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦))
191 sumeq1 15622 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 → Σ𝑦𝑥 ((𝐹𝐴)‘𝑦) = Σ𝑦𝑧 ((𝐹𝐴)‘𝑦))
192191cbvmptv 5257 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) = (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑧 ((𝐹𝐴)‘𝑦))
193 vex 3479 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥 ∈ V
194193inex1 5313 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥𝐴) ∈ V
195194elpw 4602 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝐴) ∈ 𝒫 𝐴 ↔ (𝑥𝐴) ⊆ 𝐴)
196185, 195mpbir 230 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐴) ∈ 𝒫 𝐴
197196a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐴) ∈ 𝒫 𝐴)
198 elinel2 4194 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 ∈ Fin)
199 inss1 4226 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐴) ⊆ 𝑥
200199a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐴) ⊆ 𝑥)
201 ssfi 9161 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ Fin ∧ (𝑥𝐴) ⊆ 𝑥) → (𝑥𝐴) ∈ Fin)
202198, 200, 201syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐴) ∈ Fin)
203197, 202elind 4192 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐴) ∈ (𝒫 𝐴 ∩ Fin))
204 eqidd 2734 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) = Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦))
205 sumeq1 15622 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝑥𝐴) → Σ𝑦𝑧 ((𝐹𝐴)‘𝑦) = Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦))
206205rspceeqv 3631 . . . . . . . . . . . . . . . . . . 19 (((𝑥𝐴) ∈ (𝒫 𝐴 ∩ Fin) ∧ Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) = Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) = Σ𝑦𝑧 ((𝐹𝐴)‘𝑦))
207203, 204, 206syl2anc 585 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) = Σ𝑦𝑧 ((𝐹𝐴)‘𝑦))
208 sumex 15621 . . . . . . . . . . . . . . . . . . 19 Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) ∈ V
209208a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) ∈ V)
210192, 207, 209elrnmptd 5955 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)))
211190, 210eqeltrd 2834 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)))
2122113ad2ant2 1135 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)))
213 sumeq1 15622 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → Σ𝑦𝑥 ((𝐹𝐵)‘𝑦) = Σ𝑦𝑧 ((𝐹𝐵)‘𝑦))
214213cbvmptv 5257 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) = (𝑧 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑧 ((𝐹𝐵)‘𝑦))
215 inss2 4227 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐵) ⊆ 𝐵
216193inex1 5313 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐵) ∈ V
217216elpw 4602 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝐵) ∈ 𝒫 𝐵 ↔ (𝑥𝐵) ⊆ 𝐵)
218215, 217mpbir 230 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝐵) ∈ 𝒫 𝐵
219218a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → (𝑥𝐵) ∈ 𝒫 𝐵)
220 inss1 4226 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐵) ⊆ 𝑥
221220a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐵) ⊆ 𝑥)
222 ssfi 9161 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ Fin ∧ (𝑥𝐵) ⊆ 𝑥) → (𝑥𝐵) ∈ Fin)
223198, 221, 222syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐵) ∈ Fin)
2242233ad2ant2 1135 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → (𝑥𝐵) ∈ Fin)
225219, 224elind 4192 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → (𝑥𝐵) ∈ (𝒫 𝐵 ∩ Fin))
226215sseli 3976 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (𝑥𝐵) → 𝑦𝐵)
227123eqcomd 2739 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝐵 → (𝐹𝑦) = ((𝐹𝐵)‘𝑦))
228226, 227syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (𝑥𝐵) → (𝐹𝑦) = ((𝐹𝐵)‘𝑦))
229228sumeq2i 15632 . . . . . . . . . . . . . . . . . . . 20 Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦)
230229a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦))
2312303adant3 1133 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦))
232 sumeq1 15622 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑥𝐵) → Σ𝑦𝑧 ((𝐹𝐵)‘𝑦) = Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦))
233232rspceeqv 3631 . . . . . . . . . . . . . . . . . 18 (((𝑥𝐵) ∈ (𝒫 𝐵 ∩ Fin) ∧ Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦)) → ∃𝑧 ∈ (𝒫 𝐵 ∩ Fin)Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦𝑧 ((𝐹𝐵)‘𝑦))
234225, 231, 233syl2anc 585 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → ∃𝑧 ∈ (𝒫 𝐵 ∩ Fin)Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) = Σ𝑦𝑧 ((𝐹𝐵)‘𝑦))
235 sumex 15621 . . . . . . . . . . . . . . . . . 18 Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ V
236235a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ V)
237214, 234, 236elrnmptd 5955 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)))
238 simp3 1139 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → 𝑟 = Σ𝑦𝑥 (𝐹𝑦))
239185a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑥𝐴) ⊆ 𝐴)
240215a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑥𝐵) ⊆ 𝐵)
241 ssin0 43613 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴𝐵) = ∅ ∧ (𝑥𝐴) ⊆ 𝐴 ∧ (𝑥𝐵) ⊆ 𝐵) → ((𝑥𝐴) ∩ (𝑥𝐵)) = ∅)
242132, 239, 240, 241syl3anc 1372 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑥𝐴) ∩ (𝑥𝐵)) = ∅)
243242adantr 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → ((𝑥𝐴) ∩ (𝑥𝐵)) = ∅)
244 elinel1 4193 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 ∈ 𝒫 𝑈)
245 elpwi 4605 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ 𝒫 𝑈𝑥𝑈)
246244, 245syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥𝑈)
2474ineq2i 4207 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥𝑈) = (𝑥 ∩ (𝐴𝐵))
248247a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝑈 → (𝑥𝑈) = (𝑥 ∩ (𝐴𝐵)))
249 dfss 3964 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥𝑈𝑥 = (𝑥𝑈))
250249biimpi 215 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝑈𝑥 = (𝑥𝑈))
251 indi 4271 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∩ (𝐴𝐵)) = ((𝑥𝐴) ∪ (𝑥𝐵))
252251eqcomi 2742 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥𝐴) ∪ (𝑥𝐵)) = (𝑥 ∩ (𝐴𝐵))
253252a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝑈 → ((𝑥𝐴) ∪ (𝑥𝐵)) = (𝑥 ∩ (𝐴𝐵)))
254248, 250, 2533eqtr4d 2783 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑈𝑥 = ((𝑥𝐴) ∪ (𝑥𝐵)))
255246, 254syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 = ((𝑥𝐴) ∪ (𝑥𝐵)))
256255adantl 483 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝑥 = ((𝑥𝐴) ∪ (𝑥𝐵)))
257198adantl 483 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝑥 ∈ Fin)
258144ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → 𝐹:𝑈⟶(0[,)+∞))
259246sselda 3980 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦𝑥) → 𝑦𝑈)
260259adantll 713 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → 𝑦𝑈)
261258, 260ffvelcdmd 7075 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ (0[,)+∞))
262143, 261sselid 3978 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ ℂ)
263243, 256, 257, 262fsumsplit 15674 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦𝑥 (𝐹𝑦) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
2642633adant3 1133 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → Σ𝑦𝑥 (𝐹𝑦) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
265238, 264eqtrd 2773 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → 𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
266 oveq2 7404 . . . . . . . . . . . . . . . . 17 (𝑢 = Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) → (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
267266rspceeqv 3631 . . . . . . . . . . . . . . . 16 ((Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)) ∧ 𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦))) → ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢))
268237, 265, 267syl2anc 585 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢))
269 oveq1 7403 . . . . . . . . . . . . . . . . . 18 (𝑣 = Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) → (𝑣 + 𝑢) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢))
270269eqeq2d 2744 . . . . . . . . . . . . . . . . 17 (𝑣 = Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) → (𝑟 = (𝑣 + 𝑢) ↔ 𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢)))
271270rexbidv 3179 . . . . . . . . . . . . . . . 16 (𝑣 = Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) → (∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢) ↔ ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢)))
272271rspcev 3611 . . . . . . . . . . . . . . 15 ((Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)) ∧ ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + 𝑢)) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
273212, 268, 272syl2anc 585 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦𝑥 (𝐹𝑦)) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
2742733exp 1120 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑟 = Σ𝑦𝑥 (𝐹𝑦) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))))
275274adantr 482 . . . . . . . . . . . 12 ((𝜑𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑟 = Σ𝑦𝑥 (𝐹𝑦) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))))
276177, 184, 275rexlimd 3264 . . . . . . . . . . 11 ((𝜑𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → (∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦𝑥 (𝐹𝑦) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)))
277171, 276mpd 15 . . . . . . . . . 10 ((𝜑𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
278277, 59sylibr 233 . . . . . . . . 9 ((𝜑𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → 𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)})
279278ex 414 . . . . . . . 8 (𝜑 → (𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) → 𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}))
280168, 279impbid 211 . . . . . . 7 (𝜑 → (𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} ↔ 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
281280alrimiv 1931 . . . . . 6 (𝜑 → ∀𝑟(𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} ↔ 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
282 dfcleq 2726 . . . . . 6 ({𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} = ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ↔ ∀𝑟(𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} ↔ 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))))
283281, 282sylibr 233 . . . . 5 (𝜑 → {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} = ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))
284283supeq1d 9428 . . . 4 (𝜑 → sup({𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}, ℝ, < ) = sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ, < ))
28526, 53, 2843eqtrrd 2778 . . 3 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ, < ) = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) +𝑒 sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )))
28613, 2, 14sge0supre 44978 . . 3 (𝜑 → (Σ^𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ, < ))
28716, 23oveq12d 7414 . . 3 (𝜑 → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐴)‘𝑦)), ℝ, < ) +𝑒 sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦𝑥 ((𝐹𝐵)‘𝑦)), ℝ, < )))
288285, 286, 2873eqtr4d 2783 . 2 (𝜑 → (Σ^𝐹) = ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
289 rexadd 13198 . . 3 (((Σ^‘(𝐹𝐴)) ∈ ℝ ∧ (Σ^‘(𝐹𝐵)) ∈ ℝ) → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = ((Σ^‘(𝐹𝐴)) + (Σ^‘(𝐹𝐵))))
29015, 22, 289syl2anc 585 . 2 (𝜑 → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = ((Σ^‘(𝐹𝐴)) + (Σ^‘(𝐹𝐵))))
291288, 290eqtrd 2773 1 (𝜑 → (Σ^𝐹) = ((Σ^‘(𝐹𝐴)) + (Σ^‘(𝐹𝐵))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  w3a 1088  wal 1540   = wceq 1542  wcel 2107  {cab 2710  wne 2941  wral 3062  wrex 3071  Vcvv 3475  cun 3944  cin 3945  wss 3946  c0 4320  𝒫 cpw 4598   class class class wbr 5144  cmpt 5227  ran crn 5673  cres 5674  wf 6531  cfv 6535  (class class class)co 7396  Fincfn 8927  supcsup 9422  cc 11095  cr 11096  0cc0 11097   + caddc 11100  +∞cpnf 11232  *cxr 11234   < clt 11235  cle 11236   +𝑒 cxad 13077  [,)cico 13313  [,]cicc 13314  Σcsu 15619  Σ^csumge0 44951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5359  ax-pr 5423  ax-un 7712  ax-inf2 9623  ax-cnex 11153  ax-resscn 11154  ax-1cn 11155  ax-icn 11156  ax-addcl 11157  ax-addrcl 11158  ax-mulcl 11159  ax-mulrcl 11160  ax-mulcom 11161  ax-addass 11162  ax-mulass 11163  ax-distr 11164  ax-i2m1 11165  ax-1ne0 11166  ax-1rid 11167  ax-rnegex 11168  ax-rrecex 11169  ax-cnre 11170  ax-pre-lttri 11171  ax-pre-lttrn 11172  ax-pre-ltadd 11173  ax-pre-mulgt0 11174  ax-pre-sup 11175
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3965  df-nul 4321  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4905  df-int 4947  df-iun 4995  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6292  df-ord 6359  df-on 6360  df-lim 6361  df-suc 6362  df-iota 6487  df-fun 6537  df-fn 6538  df-f 6539  df-f1 6540  df-fo 6541  df-f1o 6542  df-fv 6543  df-isom 6544  df-riota 7352  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7843  df-1st 7962  df-2nd 7963  df-frecs 8253  df-wrecs 8284  df-recs 8358  df-rdg 8397  df-1o 8453  df-er 8691  df-en 8928  df-dom 8929  df-sdom 8930  df-fin 8931  df-sup 9424  df-oi 9492  df-card 9921  df-pnf 11237  df-mnf 11238  df-xr 11239  df-ltxr 11240  df-le 11241  df-sub 11433  df-neg 11434  df-div 11859  df-nn 12200  df-2 12262  df-3 12263  df-n0 12460  df-z 12546  df-uz 12810  df-rp 12962  df-xadd 13080  df-ico 13317  df-icc 13318  df-fz 13472  df-fzo 13615  df-seq 13954  df-exp 14015  df-hash 14278  df-cj 15033  df-re 15034  df-im 15035  df-sqrt 15169  df-abs 15170  df-clim 15419  df-sum 15620  df-sumge0 44952
This theorem is referenced by:  sge0split  44998
  Copyright terms: Public domain W3C validator