MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  itgfsum Structured version   Visualization version   GIF version

Theorem itgfsum 25275
Description: Take a finite sum of integrals over the same domain. (Contributed by Mario Carneiro, 24-Aug-2014.)
Hypotheses
Ref Expression
itgfsum.1 (𝜑𝐴 ∈ dom vol)
itgfsum.2 (𝜑𝐵 ∈ Fin)
itgfsum.3 ((𝜑 ∧ (𝑥𝐴𝑘𝐵)) → 𝐶𝑉)
itgfsum.4 ((𝜑𝑘𝐵) → (𝑥𝐴𝐶) ∈ 𝐿1)
Assertion
Ref Expression
itgfsum (𝜑 → ((𝑥𝐴 ↦ Σ𝑘𝐵 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝐵 𝐶 d𝑥 = Σ𝑘𝐵𝐴𝐶 d𝑥))
Distinct variable groups:   𝑥,𝑘,𝐴   𝐵,𝑘,𝑥   𝜑,𝑘,𝑥
Allowed substitution hints:   𝐶(𝑥,𝑘)   𝑉(𝑥,𝑘)

Proof of Theorem itgfsum
Dummy variables 𝑚 𝑡 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssid 4001 . 2 𝐵𝐵
2 itgfsum.2 . . 3 (𝜑𝐵 ∈ Fin)
3 sseq1 4004 . . . . . 6 (𝑡 = ∅ → (𝑡𝐵 ↔ ∅ ⊆ 𝐵))
4 itgz 25229 . . . . . . . 8 𝐴0 d𝑥 = 0
5 sumeq1 15619 . . . . . . . . . . 11 (𝑡 = ∅ → Σ𝑘𝑡 𝐶 = Σ𝑘 ∈ ∅ 𝐶)
6 sum0 15651 . . . . . . . . . . 11 Σ𝑘 ∈ ∅ 𝐶 = 0
75, 6eqtrdi 2788 . . . . . . . . . 10 (𝑡 = ∅ → Σ𝑘𝑡 𝐶 = 0)
87adantr 481 . . . . . . . . 9 ((𝑡 = ∅ ∧ 𝑥𝐴) → Σ𝑘𝑡 𝐶 = 0)
98itgeq2dv 25230 . . . . . . . 8 (𝑡 = ∅ → ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = ∫𝐴0 d𝑥)
10 sumeq1 15619 . . . . . . . . 9 (𝑡 = ∅ → Σ𝑘𝑡𝐴𝐶 d𝑥 = Σ𝑘 ∈ ∅ ∫𝐴𝐶 d𝑥)
11 sum0 15651 . . . . . . . . 9 Σ𝑘 ∈ ∅ ∫𝐴𝐶 d𝑥 = 0
1210, 11eqtrdi 2788 . . . . . . . 8 (𝑡 = ∅ → Σ𝑘𝑡𝐴𝐶 d𝑥 = 0)
134, 9, 123eqtr4a 2798 . . . . . . 7 (𝑡 = ∅ → ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = Σ𝑘𝑡𝐴𝐶 d𝑥)
147mpteq2dv 5244 . . . . . . . . . 10 (𝑡 = ∅ → (𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) = (𝑥𝐴 ↦ 0))
15 fconstmpt 5731 . . . . . . . . . 10 (𝐴 × {0}) = (𝑥𝐴 ↦ 0)
1614, 15eqtr4di 2790 . . . . . . . . 9 (𝑡 = ∅ → (𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) = (𝐴 × {0}))
1716eleq1d 2818 . . . . . . . 8 (𝑡 = ∅ → ((𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) ∈ 𝐿1 ↔ (𝐴 × {0}) ∈ 𝐿1))
1817anbi1d 630 . . . . . . 7 (𝑡 = ∅ → (((𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = Σ𝑘𝑡𝐴𝐶 d𝑥) ↔ ((𝐴 × {0}) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = Σ𝑘𝑡𝐴𝐶 d𝑥)))
1913, 18mpbiran2d 706 . . . . . 6 (𝑡 = ∅ → (((𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = Σ𝑘𝑡𝐴𝐶 d𝑥) ↔ (𝐴 × {0}) ∈ 𝐿1))
203, 19imbi12d 344 . . . . 5 (𝑡 = ∅ → ((𝑡𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = Σ𝑘𝑡𝐴𝐶 d𝑥)) ↔ (∅ ⊆ 𝐵 → (𝐴 × {0}) ∈ 𝐿1)))
2120imbi2d 340 . . . 4 (𝑡 = ∅ → ((𝜑 → (𝑡𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = Σ𝑘𝑡𝐴𝐶 d𝑥))) ↔ (𝜑 → (∅ ⊆ 𝐵 → (𝐴 × {0}) ∈ 𝐿1))))
22 sseq1 4004 . . . . . 6 (𝑡 = 𝑤 → (𝑡𝐵𝑤𝐵))
23 sumeq1 15619 . . . . . . . . 9 (𝑡 = 𝑤 → Σ𝑘𝑡 𝐶 = Σ𝑘𝑤 𝐶)
2423mpteq2dv 5244 . . . . . . . 8 (𝑡 = 𝑤 → (𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) = (𝑥𝐴 ↦ Σ𝑘𝑤 𝐶))
2524eleq1d 2818 . . . . . . 7 (𝑡 = 𝑤 → ((𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) ∈ 𝐿1 ↔ (𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1))
2623adantr 481 . . . . . . . . 9 ((𝑡 = 𝑤𝑥𝐴) → Σ𝑘𝑡 𝐶 = Σ𝑘𝑤 𝐶)
2726itgeq2dv 25230 . . . . . . . 8 (𝑡 = 𝑤 → ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = ∫𝐴Σ𝑘𝑤 𝐶 d𝑥)
28 sumeq1 15619 . . . . . . . 8 (𝑡 = 𝑤 → Σ𝑘𝑡𝐴𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)
2927, 28eqeq12d 2748 . . . . . . 7 (𝑡 = 𝑤 → (∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = Σ𝑘𝑡𝐴𝐶 d𝑥 ↔ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥))
3025, 29anbi12d 631 . . . . . 6 (𝑡 = 𝑤 → (((𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = Σ𝑘𝑡𝐴𝐶 d𝑥) ↔ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)))
3122, 30imbi12d 344 . . . . 5 (𝑡 = 𝑤 → ((𝑡𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = Σ𝑘𝑡𝐴𝐶 d𝑥)) ↔ (𝑤𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥))))
3231imbi2d 340 . . . 4 (𝑡 = 𝑤 → ((𝜑 → (𝑡𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = Σ𝑘𝑡𝐴𝐶 d𝑥))) ↔ (𝜑 → (𝑤𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)))))
33 sseq1 4004 . . . . . 6 (𝑡 = (𝑤 ∪ {𝑧}) → (𝑡𝐵 ↔ (𝑤 ∪ {𝑧}) ⊆ 𝐵))
34 sumeq1 15619 . . . . . . . . 9 (𝑡 = (𝑤 ∪ {𝑧}) → Σ𝑘𝑡 𝐶 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶)
3534mpteq2dv 5244 . . . . . . . 8 (𝑡 = (𝑤 ∪ {𝑧}) → (𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) = (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶))
3635eleq1d 2818 . . . . . . 7 (𝑡 = (𝑤 ∪ {𝑧}) → ((𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) ∈ 𝐿1 ↔ (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) ∈ 𝐿1))
3734adantr 481 . . . . . . . . 9 ((𝑡 = (𝑤 ∪ {𝑧}) ∧ 𝑥𝐴) → Σ𝑘𝑡 𝐶 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶)
3837itgeq2dv 25230 . . . . . . . 8 (𝑡 = (𝑤 ∪ {𝑧}) → ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = ∫𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥)
39 sumeq1 15619 . . . . . . . 8 (𝑡 = (𝑤 ∪ {𝑧}) → Σ𝑘𝑡𝐴𝐶 d𝑥 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})∫𝐴𝐶 d𝑥)
4038, 39eqeq12d 2748 . . . . . . 7 (𝑡 = (𝑤 ∪ {𝑧}) → (∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = Σ𝑘𝑡𝐴𝐶 d𝑥 ↔ ∫𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})∫𝐴𝐶 d𝑥))
4136, 40anbi12d 631 . . . . . 6 (𝑡 = (𝑤 ∪ {𝑧}) → (((𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = Σ𝑘𝑡𝐴𝐶 d𝑥) ↔ ((𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})∫𝐴𝐶 d𝑥)))
4233, 41imbi12d 344 . . . . 5 (𝑡 = (𝑤 ∪ {𝑧}) → ((𝑡𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = Σ𝑘𝑡𝐴𝐶 d𝑥)) ↔ ((𝑤 ∪ {𝑧}) ⊆ 𝐵 → ((𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})∫𝐴𝐶 d𝑥))))
4342imbi2d 340 . . . 4 (𝑡 = (𝑤 ∪ {𝑧}) → ((𝜑 → (𝑡𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = Σ𝑘𝑡𝐴𝐶 d𝑥))) ↔ (𝜑 → ((𝑤 ∪ {𝑧}) ⊆ 𝐵 → ((𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})∫𝐴𝐶 d𝑥)))))
44 sseq1 4004 . . . . . 6 (𝑡 = 𝐵 → (𝑡𝐵𝐵𝐵))
45 sumeq1 15619 . . . . . . . . 9 (𝑡 = 𝐵 → Σ𝑘𝑡 𝐶 = Σ𝑘𝐵 𝐶)
4645mpteq2dv 5244 . . . . . . . 8 (𝑡 = 𝐵 → (𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) = (𝑥𝐴 ↦ Σ𝑘𝐵 𝐶))
4746eleq1d 2818 . . . . . . 7 (𝑡 = 𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) ∈ 𝐿1 ↔ (𝑥𝐴 ↦ Σ𝑘𝐵 𝐶) ∈ 𝐿1))
4845adantr 481 . . . . . . . . 9 ((𝑡 = 𝐵𝑥𝐴) → Σ𝑘𝑡 𝐶 = Σ𝑘𝐵 𝐶)
4948itgeq2dv 25230 . . . . . . . 8 (𝑡 = 𝐵 → ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = ∫𝐴Σ𝑘𝐵 𝐶 d𝑥)
50 sumeq1 15619 . . . . . . . 8 (𝑡 = 𝐵 → Σ𝑘𝑡𝐴𝐶 d𝑥 = Σ𝑘𝐵𝐴𝐶 d𝑥)
5149, 50eqeq12d 2748 . . . . . . 7 (𝑡 = 𝐵 → (∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = Σ𝑘𝑡𝐴𝐶 d𝑥 ↔ ∫𝐴Σ𝑘𝐵 𝐶 d𝑥 = Σ𝑘𝐵𝐴𝐶 d𝑥))
5247, 51anbi12d 631 . . . . . 6 (𝑡 = 𝐵 → (((𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = Σ𝑘𝑡𝐴𝐶 d𝑥) ↔ ((𝑥𝐴 ↦ Σ𝑘𝐵 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝐵 𝐶 d𝑥 = Σ𝑘𝐵𝐴𝐶 d𝑥)))
5344, 52imbi12d 344 . . . . 5 (𝑡 = 𝐵 → ((𝑡𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = Σ𝑘𝑡𝐴𝐶 d𝑥)) ↔ (𝐵𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝐵 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝐵 𝐶 d𝑥 = Σ𝑘𝐵𝐴𝐶 d𝑥))))
5453imbi2d 340 . . . 4 (𝑡 = 𝐵 → ((𝜑 → (𝑡𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = Σ𝑘𝑡𝐴𝐶 d𝑥))) ↔ (𝜑 → (𝐵𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝐵 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝐵 𝐶 d𝑥 = Σ𝑘𝐵𝐴𝐶 d𝑥)))))
55 itgfsum.1 . . . . . 6 (𝜑𝐴 ∈ dom vol)
56 ibl0 25235 . . . . . 6 (𝐴 ∈ dom vol → (𝐴 × {0}) ∈ 𝐿1)
5755, 56syl 17 . . . . 5 (𝜑 → (𝐴 × {0}) ∈ 𝐿1)
5857a1d 25 . . . 4 (𝜑 → (∅ ⊆ 𝐵 → (𝐴 × {0}) ∈ 𝐿1))
59 ssun1 4169 . . . . . . . . . 10 𝑤 ⊆ (𝑤 ∪ {𝑧})
60 sstr 3987 . . . . . . . . . 10 ((𝑤 ⊆ (𝑤 ∪ {𝑧}) ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵) → 𝑤𝐵)
6159, 60mpan 688 . . . . . . . . 9 ((𝑤 ∪ {𝑧}) ⊆ 𝐵𝑤𝐵)
6261imim1i 63 . . . . . . . 8 ((𝑤𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ((𝑤 ∪ {𝑧}) ⊆ 𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)))
63 nfcv 2903 . . . . . . . . . . . . . . . . . 18 𝑚𝐶
64 nfcsb1v 3915 . . . . . . . . . . . . . . . . . 18 𝑘𝑚 / 𝑘𝐶
65 csbeq1a 3904 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑚𝐶 = 𝑚 / 𝑘𝐶)
6663, 64, 65cbvsumi 15627 . . . . . . . . . . . . . . . . 17 Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 = Σ𝑚 ∈ (𝑤 ∪ {𝑧})𝑚 / 𝑘𝐶
67 simprl 769 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → ¬ 𝑧𝑤)
68 disjsn 4709 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑤)
6967, 68sylibr 233 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → (𝑤 ∩ {𝑧}) = ∅)
7069adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → (𝑤 ∩ {𝑧}) = ∅)
71 eqidd 2733 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → (𝑤 ∪ {𝑧}) = (𝑤 ∪ {𝑧}))
722adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → 𝐵 ∈ Fin)
73 simprr 771 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → (𝑤 ∪ {𝑧}) ⊆ 𝐵)
7472, 73ssfid 9252 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → (𝑤 ∪ {𝑧}) ∈ Fin)
7574adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → (𝑤 ∪ {𝑧}) ∈ Fin)
76 simplrr 776 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → (𝑤 ∪ {𝑧}) ⊆ 𝐵)
7776sselda 3979 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) ∧ 𝑚 ∈ (𝑤 ∪ {𝑧})) → 𝑚𝐵)
78 itgfsum.4 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑘𝐵) → (𝑥𝐴𝐶) ∈ 𝐿1)
79 iblmbf 25216 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥𝐴𝐶) ∈ 𝐿1 → (𝑥𝐴𝐶) ∈ MblFn)
8078, 79syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘𝐵) → (𝑥𝐴𝐶) ∈ MblFn)
81 itgfsum.3 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑥𝐴𝑘𝐵)) → 𝐶𝑉)
8281anass1rs 653 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑘𝐵) ∧ 𝑥𝐴) → 𝐶𝑉)
8380, 82mbfmptcl 25084 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑘𝐵) ∧ 𝑥𝐴) → 𝐶 ∈ ℂ)
8483an32s 650 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ ℂ)
8584ralrimiva 3146 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥𝐴) → ∀𝑘𝐵 𝐶 ∈ ℂ)
8685adantlr 713 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → ∀𝑘𝐵 𝐶 ∈ ℂ)
8763nfel1 2919 . . . . . . . . . . . . . . . . . . . . . . 23 𝑚 𝐶 ∈ ℂ
8864nfel1 2919 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘𝑚 / 𝑘𝐶 ∈ ℂ
8965eleq1d 2818 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝑚 → (𝐶 ∈ ℂ ↔ 𝑚 / 𝑘𝐶 ∈ ℂ))
9087, 88, 89cbvralw 3303 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑘𝐵 𝐶 ∈ ℂ ↔ ∀𝑚𝐵 𝑚 / 𝑘𝐶 ∈ ℂ)
9186, 90sylib 217 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → ∀𝑚𝐵 𝑚 / 𝑘𝐶 ∈ ℂ)
9291r19.21bi 3248 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) ∧ 𝑚𝐵) → 𝑚 / 𝑘𝐶 ∈ ℂ)
9377, 92syldan 591 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) ∧ 𝑚 ∈ (𝑤 ∪ {𝑧})) → 𝑚 / 𝑘𝐶 ∈ ℂ)
9470, 71, 75, 93fsumsplit 15671 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → Σ𝑚 ∈ (𝑤 ∪ {𝑧})𝑚 / 𝑘𝐶 = (Σ𝑚𝑤 𝑚 / 𝑘𝐶 + Σ𝑚 ∈ {𝑧}𝑚 / 𝑘𝐶))
95 vex 3478 . . . . . . . . . . . . . . . . . . . 20 𝑧 ∈ V
96 csbeq1 3893 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑧𝑚 / 𝑘𝐶 = 𝑧 / 𝑘𝐶)
9796eleq1d 2818 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑧 → (𝑚 / 𝑘𝐶 ∈ ℂ ↔ 𝑧 / 𝑘𝐶 ∈ ℂ))
9873unssbd 4185 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → {𝑧} ⊆ 𝐵)
9995snss 4783 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝐵 ↔ {𝑧} ⊆ 𝐵)
10098, 99sylibr 233 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → 𝑧𝐵)
101100adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → 𝑧𝐵)
10297, 91, 101rspcdva 3611 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → 𝑧 / 𝑘𝐶 ∈ ℂ)
10396sumsn 15676 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ V ∧ 𝑧 / 𝑘𝐶 ∈ ℂ) → Σ𝑚 ∈ {𝑧}𝑚 / 𝑘𝐶 = 𝑧 / 𝑘𝐶)
10495, 102, 103sylancr 587 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → Σ𝑚 ∈ {𝑧}𝑚 / 𝑘𝐶 = 𝑧 / 𝑘𝐶)
105104oveq2d 7410 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → (Σ𝑚𝑤 𝑚 / 𝑘𝐶 + Σ𝑚 ∈ {𝑧}𝑚 / 𝑘𝐶) = (Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑧 / 𝑘𝐶))
10694, 105eqtrd 2772 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → Σ𝑚 ∈ (𝑤 ∪ {𝑧})𝑚 / 𝑘𝐶 = (Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑧 / 𝑘𝐶))
10766, 106eqtrid 2784 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 = (Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑧 / 𝑘𝐶))
108107mpteq2dva 5242 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) = (𝑥𝐴 ↦ (Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑧 / 𝑘𝐶)))
109 nfcv 2903 . . . . . . . . . . . . . . . 16 𝑦𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑧 / 𝑘𝐶)
110 nfcsb1v 3915 . . . . . . . . . . . . . . . . 17 𝑥𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶
111 nfcv 2903 . . . . . . . . . . . . . . . . 17 𝑥 +
112 nfcsb1v 3915 . . . . . . . . . . . . . . . . 17 𝑥𝑦 / 𝑥𝑧 / 𝑘𝐶
113110, 111, 112nfov 7424 . . . . . . . . . . . . . . . 16 𝑥(𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑦 / 𝑥𝑧 / 𝑘𝐶)
114 csbeq1a 3904 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → Σ𝑚𝑤 𝑚 / 𝑘𝐶 = 𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶)
115 csbeq1a 3904 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦𝑧 / 𝑘𝐶 = 𝑦 / 𝑥𝑧 / 𝑘𝐶)
116114, 115oveq12d 7412 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑧 / 𝑘𝐶) = (𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑦 / 𝑥𝑧 / 𝑘𝐶))
117109, 113, 116cbvmpt 5253 . . . . . . . . . . . . . . 15 (𝑥𝐴 ↦ (Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑧 / 𝑘𝐶)) = (𝑦𝐴 ↦ (𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑦 / 𝑥𝑧 / 𝑘𝐶))
118108, 117eqtrdi 2788 . . . . . . . . . . . . . 14 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) = (𝑦𝐴 ↦ (𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑦 / 𝑥𝑧 / 𝑘𝐶)))
119118adantr 481 . . . . . . . . . . . . 13 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) = (𝑦𝐴 ↦ (𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑦 / 𝑥𝑧 / 𝑘𝐶)))
120 sumex 15618 . . . . . . . . . . . . . . . 16 Σ𝑚𝑤 𝑚 / 𝑘𝐶 ∈ V
121120csbex 5305 . . . . . . . . . . . . . . 15 𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 ∈ V
122121a1i 11 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) ∧ 𝑦𝐴) → 𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 ∈ V)
12363, 64, 65cbvsumi 15627 . . . . . . . . . . . . . . . . 17 Σ𝑘𝑤 𝐶 = Σ𝑚𝑤 𝑚 / 𝑘𝐶
124123mpteq2i 5247 . . . . . . . . . . . . . . . 16 (𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) = (𝑥𝐴 ↦ Σ𝑚𝑤 𝑚 / 𝑘𝐶)
125 nfcv 2903 . . . . . . . . . . . . . . . . 17 𝑦Σ𝑚𝑤 𝑚 / 𝑘𝐶
126125, 110, 114cbvmpt 5253 . . . . . . . . . . . . . . . 16 (𝑥𝐴 ↦ Σ𝑚𝑤 𝑚 / 𝑘𝐶) = (𝑦𝐴𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶)
127124, 126eqtri 2760 . . . . . . . . . . . . . . 15 (𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) = (𝑦𝐴𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶)
128 simprl 769 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → (𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1)
129127, 128eqeltrrid 2838 . . . . . . . . . . . . . 14 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → (𝑦𝐴𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶) ∈ 𝐿1)
130102elexd 3494 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → 𝑧 / 𝑘𝐶 ∈ V)
131130ralrimiva 3146 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → ∀𝑥𝐴 𝑧 / 𝑘𝐶 ∈ V)
132131adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ∀𝑥𝐴 𝑧 / 𝑘𝐶 ∈ V)
133 nfv 1917 . . . . . . . . . . . . . . . . 17 𝑦𝑧 / 𝑘𝐶 ∈ V
134112nfel1 2919 . . . . . . . . . . . . . . . . 17 𝑥𝑦 / 𝑥𝑧 / 𝑘𝐶 ∈ V
135115eleq1d 2818 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝑧 / 𝑘𝐶 ∈ V ↔ 𝑦 / 𝑥𝑧 / 𝑘𝐶 ∈ V))
136133, 134, 135cbvralw 3303 . . . . . . . . . . . . . . . 16 (∀𝑥𝐴 𝑧 / 𝑘𝐶 ∈ V ↔ ∀𝑦𝐴 𝑦 / 𝑥𝑧 / 𝑘𝐶 ∈ V)
137132, 136sylib 217 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ∀𝑦𝐴 𝑦 / 𝑥𝑧 / 𝑘𝐶 ∈ V)
138137r19.21bi 3248 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) ∧ 𝑦𝐴) → 𝑦 / 𝑥𝑧 / 𝑘𝐶 ∈ V)
139 nfcv 2903 . . . . . . . . . . . . . . . . 17 𝑦𝑧 / 𝑘𝐶
140139, 112, 115cbvmpt 5253 . . . . . . . . . . . . . . . 16 (𝑥𝐴𝑧 / 𝑘𝐶) = (𝑦𝐴𝑦 / 𝑥𝑧 / 𝑘𝐶)
14196mpteq2dv 5244 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑧 → (𝑥𝐴𝑚 / 𝑘𝐶) = (𝑥𝐴𝑧 / 𝑘𝐶))
142141eleq1d 2818 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑧 → ((𝑥𝐴𝑚 / 𝑘𝐶) ∈ 𝐿1 ↔ (𝑥𝐴𝑧 / 𝑘𝐶) ∈ 𝐿1))
14378ralrimiva 3146 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑘𝐵 (𝑥𝐴𝐶) ∈ 𝐿1)
144 nfv 1917 . . . . . . . . . . . . . . . . . . . 20 𝑚(𝑥𝐴𝐶) ∈ 𝐿1
145 nfcv 2903 . . . . . . . . . . . . . . . . . . . . . 22 𝑘𝐴
146145, 64nfmpt 5249 . . . . . . . . . . . . . . . . . . . . 21 𝑘(𝑥𝐴𝑚 / 𝑘𝐶)
147146nfel1 2919 . . . . . . . . . . . . . . . . . . . 20 𝑘(𝑥𝐴𝑚 / 𝑘𝐶) ∈ 𝐿1
14865mpteq2dv 5244 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑚 → (𝑥𝐴𝐶) = (𝑥𝐴𝑚 / 𝑘𝐶))
149148eleq1d 2818 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑚 → ((𝑥𝐴𝐶) ∈ 𝐿1 ↔ (𝑥𝐴𝑚 / 𝑘𝐶) ∈ 𝐿1))
150144, 147, 149cbvralw 3303 . . . . . . . . . . . . . . . . . . 19 (∀𝑘𝐵 (𝑥𝐴𝐶) ∈ 𝐿1 ↔ ∀𝑚𝐵 (𝑥𝐴𝑚 / 𝑘𝐶) ∈ 𝐿1)
151143, 150sylib 217 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑚𝐵 (𝑥𝐴𝑚 / 𝑘𝐶) ∈ 𝐿1)
152151adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → ∀𝑚𝐵 (𝑥𝐴𝑚 / 𝑘𝐶) ∈ 𝐿1)
153142, 152, 100rspcdva 3611 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → (𝑥𝐴𝑧 / 𝑘𝐶) ∈ 𝐿1)
154140, 153eqeltrrid 2838 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → (𝑦𝐴𝑦 / 𝑥𝑧 / 𝑘𝐶) ∈ 𝐿1)
155154adantr 481 . . . . . . . . . . . . . 14 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → (𝑦𝐴𝑦 / 𝑥𝑧 / 𝑘𝐶) ∈ 𝐿1)
156122, 129, 138, 155ibladd 25269 . . . . . . . . . . . . 13 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → (𝑦𝐴 ↦ (𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑦 / 𝑥𝑧 / 𝑘𝐶)) ∈ 𝐿1)
157119, 156eqeltrd 2833 . . . . . . . . . . . 12 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) ∈ 𝐿1)
158122, 129, 138, 155itgadd 25273 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ∫𝐴(𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑦 / 𝑥𝑧 / 𝑘𝐶) d𝑦 = (∫𝐴𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 d𝑦 + ∫𝐴𝑦 / 𝑥𝑧 / 𝑘𝐶 d𝑦))
159116, 109, 113cbvitg 25224 . . . . . . . . . . . . . . 15 𝐴𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑧 / 𝑘𝐶) d𝑥 = ∫𝐴(𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑦 / 𝑥𝑧 / 𝑘𝐶) d𝑦
160114, 125, 110cbvitg 25224 . . . . . . . . . . . . . . . 16 𝐴Σ𝑚𝑤 𝑚 / 𝑘𝐶 d𝑥 = ∫𝐴𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 d𝑦
161115, 139, 112cbvitg 25224 . . . . . . . . . . . . . . . 16 𝐴𝑧 / 𝑘𝐶 d𝑥 = ∫𝐴𝑦 / 𝑥𝑧 / 𝑘𝐶 d𝑦
162160, 161oveq12i 7406 . . . . . . . . . . . . . . 15 (∫𝐴Σ𝑚𝑤 𝑚 / 𝑘𝐶 d𝑥 + ∫𝐴𝑧 / 𝑘𝐶 d𝑥) = (∫𝐴𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 d𝑦 + ∫𝐴𝑦 / 𝑥𝑧 / 𝑘𝐶 d𝑦)
163158, 159, 1623eqtr4g 2797 . . . . . . . . . . . . . 14 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ∫𝐴𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑧 / 𝑘𝐶) d𝑥 = (∫𝐴Σ𝑚𝑤 𝑚 / 𝑘𝐶 d𝑥 + ∫𝐴𝑧 / 𝑘𝐶 d𝑥))
164106itgeq2dv 25230 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → ∫𝐴Σ𝑚 ∈ (𝑤 ∪ {𝑧})𝑚 / 𝑘𝐶 d𝑥 = ∫𝐴𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑧 / 𝑘𝐶) d𝑥)
165164adantr 481 . . . . . . . . . . . . . 14 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ∫𝐴Σ𝑚 ∈ (𝑤 ∪ {𝑧})𝑚 / 𝑘𝐶 d𝑥 = ∫𝐴𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑧 / 𝑘𝐶) d𝑥)
166 eqidd 2733 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → (𝑤 ∪ {𝑧}) = (𝑤 ∪ {𝑧}))
16773sselda 3979 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑚 ∈ (𝑤 ∪ {𝑧})) → 𝑚𝐵)
16892an32s 650 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑚𝐵) ∧ 𝑥𝐴) → 𝑚 / 𝑘𝐶 ∈ ℂ)
169152r19.21bi 3248 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑚𝐵) → (𝑥𝐴𝑚 / 𝑘𝐶) ∈ 𝐿1)
170168, 169itgcl 25232 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑚𝐵) → ∫𝐴𝑚 / 𝑘𝐶 d𝑥 ∈ ℂ)
171167, 170syldan 591 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑚 ∈ (𝑤 ∪ {𝑧})) → ∫𝐴𝑚 / 𝑘𝐶 d𝑥 ∈ ℂ)
17269, 166, 74, 171fsumsplit 15671 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → Σ𝑚 ∈ (𝑤 ∪ {𝑧})∫𝐴𝑚 / 𝑘𝐶 d𝑥 = (Σ𝑚𝑤𝐴𝑚 / 𝑘𝐶 d𝑥 + Σ𝑚 ∈ {𝑧}∫𝐴𝑚 / 𝑘𝐶 d𝑥))
173172adantr 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → Σ𝑚 ∈ (𝑤 ∪ {𝑧})∫𝐴𝑚 / 𝑘𝐶 d𝑥 = (Σ𝑚𝑤𝐴𝑚 / 𝑘𝐶 d𝑥 + Σ𝑚 ∈ {𝑧}∫𝐴𝑚 / 𝑘𝐶 d𝑥))
174 simprr 771 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)
175 itgeq2 25226 . . . . . . . . . . . . . . . . . 18 (∀𝑥𝐴 Σ𝑘𝑤 𝐶 = Σ𝑚𝑤 𝑚 / 𝑘𝐶 → ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = ∫𝐴Σ𝑚𝑤 𝑚 / 𝑘𝐶 d𝑥)
176123a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥𝐴 → Σ𝑘𝑤 𝐶 = Σ𝑚𝑤 𝑚 / 𝑘𝐶)
177175, 176mprg 3067 . . . . . . . . . . . . . . . . 17 𝐴Σ𝑘𝑤 𝐶 d𝑥 = ∫𝐴Σ𝑚𝑤 𝑚 / 𝑘𝐶 d𝑥
178 nfcv 2903 . . . . . . . . . . . . . . . . . 18 𝑚𝐴𝐶 d𝑥
179145, 64nfitg 25223 . . . . . . . . . . . . . . . . . 18 𝑘𝐴𝑚 / 𝑘𝐶 d𝑥
18065adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝑘 = 𝑚𝑥𝐴) → 𝐶 = 𝑚 / 𝑘𝐶)
181180itgeq2dv 25230 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑚 → ∫𝐴𝐶 d𝑥 = ∫𝐴𝑚 / 𝑘𝐶 d𝑥)
182178, 179, 181cbvsumi 15627 . . . . . . . . . . . . . . . . 17 Σ𝑘𝑤𝐴𝐶 d𝑥 = Σ𝑚𝑤𝐴𝑚 / 𝑘𝐶 d𝑥
183174, 177, 1823eqtr3g 2795 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ∫𝐴Σ𝑚𝑤 𝑚 / 𝑘𝐶 d𝑥 = Σ𝑚𝑤𝐴𝑚 / 𝑘𝐶 d𝑥)
184102, 153itgcl 25232 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → ∫𝐴𝑧 / 𝑘𝐶 d𝑥 ∈ ℂ)
185184adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ∫𝐴𝑧 / 𝑘𝐶 d𝑥 ∈ ℂ)
18696adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 = 𝑧𝑥𝐴) → 𝑚 / 𝑘𝐶 = 𝑧 / 𝑘𝐶)
187186itgeq2dv 25230 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑧 → ∫𝐴𝑚 / 𝑘𝐶 d𝑥 = ∫𝐴𝑧 / 𝑘𝐶 d𝑥)
188187sumsn 15676 . . . . . . . . . . . . . . . . . 18 ((𝑧 ∈ V ∧ ∫𝐴𝑧 / 𝑘𝐶 d𝑥 ∈ ℂ) → Σ𝑚 ∈ {𝑧}∫𝐴𝑚 / 𝑘𝐶 d𝑥 = ∫𝐴𝑧 / 𝑘𝐶 d𝑥)
18995, 185, 188sylancr 587 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → Σ𝑚 ∈ {𝑧}∫𝐴𝑚 / 𝑘𝐶 d𝑥 = ∫𝐴𝑧 / 𝑘𝐶 d𝑥)
190189eqcomd 2738 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ∫𝐴𝑧 / 𝑘𝐶 d𝑥 = Σ𝑚 ∈ {𝑧}∫𝐴𝑚 / 𝑘𝐶 d𝑥)
191183, 190oveq12d 7412 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → (∫𝐴Σ𝑚𝑤 𝑚 / 𝑘𝐶 d𝑥 + ∫𝐴𝑧 / 𝑘𝐶 d𝑥) = (Σ𝑚𝑤𝐴𝑚 / 𝑘𝐶 d𝑥 + Σ𝑚 ∈ {𝑧}∫𝐴𝑚 / 𝑘𝐶 d𝑥))
192173, 191eqtr4d 2775 . . . . . . . . . . . . . 14 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → Σ𝑚 ∈ (𝑤 ∪ {𝑧})∫𝐴𝑚 / 𝑘𝐶 d𝑥 = (∫𝐴Σ𝑚𝑤 𝑚 / 𝑘𝐶 d𝑥 + ∫𝐴𝑧 / 𝑘𝐶 d𝑥))
193163, 165, 1923eqtr4d 2782 . . . . . . . . . . . . 13 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ∫𝐴Σ𝑚 ∈ (𝑤 ∪ {𝑧})𝑚 / 𝑘𝐶 d𝑥 = Σ𝑚 ∈ (𝑤 ∪ {𝑧})∫𝐴𝑚 / 𝑘𝐶 d𝑥)
194 itgeq2 25226 . . . . . . . . . . . . . 14 (∀𝑥𝐴 Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 = Σ𝑚 ∈ (𝑤 ∪ {𝑧})𝑚 / 𝑘𝐶 → ∫𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥 = ∫𝐴Σ𝑚 ∈ (𝑤 ∪ {𝑧})𝑚 / 𝑘𝐶 d𝑥)
19566a1i 11 . . . . . . . . . . . . . 14 (𝑥𝐴 → Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 = Σ𝑚 ∈ (𝑤 ∪ {𝑧})𝑚 / 𝑘𝐶)
196194, 195mprg 3067 . . . . . . . . . . . . 13 𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥 = ∫𝐴Σ𝑚 ∈ (𝑤 ∪ {𝑧})𝑚 / 𝑘𝐶 d𝑥
197178, 179, 181cbvsumi 15627 . . . . . . . . . . . . 13 Σ𝑘 ∈ (𝑤 ∪ {𝑧})∫𝐴𝐶 d𝑥 = Σ𝑚 ∈ (𝑤 ∪ {𝑧})∫𝐴𝑚 / 𝑘𝐶 d𝑥
198193, 196, 1973eqtr4g 2797 . . . . . . . . . . . 12 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ∫𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})∫𝐴𝐶 d𝑥)
199157, 198jca 512 . . . . . . . . . . 11 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ((𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})∫𝐴𝐶 d𝑥))
200199ex 413 . . . . . . . . . 10 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → (((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥) → ((𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})∫𝐴𝐶 d𝑥)))
201200expr 457 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝑧𝑤) → ((𝑤 ∪ {𝑧}) ⊆ 𝐵 → (((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥) → ((𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})∫𝐴𝐶 d𝑥))))
202201a2d 29 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑧𝑤) → (((𝑤 ∪ {𝑧}) ⊆ 𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ((𝑤 ∪ {𝑧}) ⊆ 𝐵 → ((𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})∫𝐴𝐶 d𝑥))))
20362, 202syl5 34 . . . . . . 7 ((𝜑 ∧ ¬ 𝑧𝑤) → ((𝑤𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ((𝑤 ∪ {𝑧}) ⊆ 𝐵 → ((𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})∫𝐴𝐶 d𝑥))))
204203expcom 414 . . . . . 6 𝑧𝑤 → (𝜑 → ((𝑤𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ((𝑤 ∪ {𝑧}) ⊆ 𝐵 → ((𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})∫𝐴𝐶 d𝑥)))))
205204adantl 482 . . . . 5 ((𝑤 ∈ Fin ∧ ¬ 𝑧𝑤) → (𝜑 → ((𝑤𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ((𝑤 ∪ {𝑧}) ⊆ 𝐵 → ((𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})∫𝐴𝐶 d𝑥)))))
206205a2d 29 . . . 4 ((𝑤 ∈ Fin ∧ ¬ 𝑧𝑤) → ((𝜑 → (𝑤𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥))) → (𝜑 → ((𝑤 ∪ {𝑧}) ⊆ 𝐵 → ((𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})∫𝐴𝐶 d𝑥)))))
20721, 32, 43, 54, 58, 206findcard2s 9150 . . 3 (𝐵 ∈ Fin → (𝜑 → (𝐵𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝐵 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝐵 𝐶 d𝑥 = Σ𝑘𝐵𝐴𝐶 d𝑥))))
2082, 207mpcom 38 . 2 (𝜑 → (𝐵𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝐵 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝐵 𝐶 d𝑥 = Σ𝑘𝐵𝐴𝐶 d𝑥)))
2091, 208mpi 20 1 (𝜑 → ((𝑥𝐴 ↦ Σ𝑘𝐵 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝐵 𝐶 d𝑥 = Σ𝑘𝐵𝐴𝐶 d𝑥))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396   = wceq 1541  wcel 2106  wral 3061  Vcvv 3474  csb 3890  cun 3943  cin 3944  wss 3945  c0 4319  {csn 4623  cmpt 5225   × cxp 5668  dom cdm 5670  (class class class)co 7394  Fincfn 8924  cc 11092  0cc0 11094   + caddc 11097  Σcsu 15616  volcvol 24911  MblFncmbf 25062  𝐿1cibl 25065  citg 25066
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5357  ax-pr 5421  ax-un 7709  ax-inf2 9620  ax-cc 10414  ax-cnex 11150  ax-resscn 11151  ax-1cn 11152  ax-icn 11153  ax-addcl 11154  ax-addrcl 11155  ax-mulcl 11156  ax-mulrcl 11157  ax-mulcom 11158  ax-addass 11159  ax-mulass 11160  ax-distr 11161  ax-i2m1 11162  ax-1ne0 11163  ax-1rid 11164  ax-rnegex 11165  ax-rrecex 11166  ax-cnre 11167  ax-pre-lttri 11168  ax-pre-lttrn 11169  ax-pre-ltadd 11170  ax-pre-mulgt0 11171  ax-pre-sup 11172  ax-addf 11173
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4320  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-int 4945  df-iun 4993  df-disj 5108  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5568  df-eprel 5574  df-po 5582  df-so 5583  df-fr 5625  df-se 5626  df-we 5627  df-xp 5676  df-rel 5677  df-cnv 5678  df-co 5679  df-dm 5680  df-rn 5681  df-res 5682  df-ima 5683  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7350  df-ov 7397  df-oprab 7398  df-mpo 7399  df-of 7654  df-ofr 7655  df-om 7840  df-1st 7959  df-2nd 7960  df-frecs 8250  df-wrecs 8281  df-recs 8355  df-rdg 8394  df-1o 8450  df-2o 8451  df-oadd 8454  df-omul 8455  df-er 8688  df-map 8807  df-pm 8808  df-en 8925  df-dom 8926  df-sdom 8927  df-fin 8928  df-fi 9390  df-sup 9421  df-inf 9422  df-oi 9489  df-dju 9880  df-card 9918  df-acn 9921  df-pnf 11234  df-mnf 11235  df-xr 11236  df-ltxr 11237  df-le 11238  df-sub 11430  df-neg 11431  df-div 11856  df-nn 12197  df-2 12259  df-3 12260  df-4 12261  df-n0 12457  df-z 12543  df-uz 12807  df-q 12917  df-rp 12959  df-xneg 13076  df-xadd 13077  df-xmul 13078  df-ioo 13312  df-ioc 13313  df-ico 13314  df-icc 13315  df-fz 13469  df-fzo 13612  df-fl 13741  df-mod 13819  df-seq 13951  df-exp 14012  df-hash 14275  df-cj 15030  df-re 15031  df-im 15032  df-sqrt 15166  df-abs 15167  df-clim 15416  df-rlim 15417  df-sum 15617  df-rest 17352  df-topgen 17373  df-psmet 20872  df-xmet 20873  df-met 20874  df-bl 20875  df-mopn 20876  df-top 22327  df-topon 22344  df-bases 22380  df-cmp 22822  df-ovol 24912  df-vol 24913  df-mbf 25067  df-itg1 25068  df-itg2 25069  df-ibl 25070  df-itg 25071  df-0p 25118
This theorem is referenced by:  circlemeth  33547  3factsumint1  40755  fourierdlem83  44742
  Copyright terms: Public domain W3C validator