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

Theorem itgfsum 25882
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 4031 . 2 𝐵𝐵
2 itgfsum.2 . . 3 (𝜑𝐵 ∈ Fin)
3 sseq1 4034 . . . . . 6 (𝑡 = ∅ → (𝑡𝐵 ↔ ∅ ⊆ 𝐵))
4 itgz 25836 . . . . . . . 8 𝐴0 d𝑥 = 0
5 sumeq1 15737 . . . . . . . . . . 11 (𝑡 = ∅ → Σ𝑘𝑡 𝐶 = Σ𝑘 ∈ ∅ 𝐶)
6 sum0 15769 . . . . . . . . . . 11 Σ𝑘 ∈ ∅ 𝐶 = 0
75, 6eqtrdi 2796 . . . . . . . . . 10 (𝑡 = ∅ → Σ𝑘𝑡 𝐶 = 0)
87adantr 480 . . . . . . . . 9 ((𝑡 = ∅ ∧ 𝑥𝐴) → Σ𝑘𝑡 𝐶 = 0)
98itgeq2dv 25837 . . . . . . . 8 (𝑡 = ∅ → ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = ∫𝐴0 d𝑥)
10 sumeq1 15737 . . . . . . . . 9 (𝑡 = ∅ → Σ𝑘𝑡𝐴𝐶 d𝑥 = Σ𝑘 ∈ ∅ ∫𝐴𝐶 d𝑥)
11 sum0 15769 . . . . . . . . 9 Σ𝑘 ∈ ∅ ∫𝐴𝐶 d𝑥 = 0
1210, 11eqtrdi 2796 . . . . . . . 8 (𝑡 = ∅ → Σ𝑘𝑡𝐴𝐶 d𝑥 = 0)
134, 9, 123eqtr4a 2806 . . . . . . 7 (𝑡 = ∅ → ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = Σ𝑘𝑡𝐴𝐶 d𝑥)
147mpteq2dv 5268 . . . . . . . . . 10 (𝑡 = ∅ → (𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) = (𝑥𝐴 ↦ 0))
15 fconstmpt 5762 . . . . . . . . . 10 (𝐴 × {0}) = (𝑥𝐴 ↦ 0)
1614, 15eqtr4di 2798 . . . . . . . . 9 (𝑡 = ∅ → (𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) = (𝐴 × {0}))
1716eleq1d 2829 . . . . . . . 8 (𝑡 = ∅ → ((𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) ∈ 𝐿1 ↔ (𝐴 × {0}) ∈ 𝐿1))
1817anbi1d 630 . . . . . . 7 (𝑡 = ∅ → (((𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = Σ𝑘𝑡𝐴𝐶 d𝑥) ↔ ((𝐴 × {0}) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = Σ𝑘𝑡𝐴𝐶 d𝑥)))
1913, 18mpbiran2d 707 . . . . . 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 4034 . . . . . 6 (𝑡 = 𝑤 → (𝑡𝐵𝑤𝐵))
23 sumeq1 15737 . . . . . . . . 9 (𝑡 = 𝑤 → Σ𝑘𝑡 𝐶 = Σ𝑘𝑤 𝐶)
2423mpteq2dv 5268 . . . . . . . 8 (𝑡 = 𝑤 → (𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) = (𝑥𝐴 ↦ Σ𝑘𝑤 𝐶))
2524eleq1d 2829 . . . . . . 7 (𝑡 = 𝑤 → ((𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) ∈ 𝐿1 ↔ (𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1))
2623adantr 480 . . . . . . . . 9 ((𝑡 = 𝑤𝑥𝐴) → Σ𝑘𝑡 𝐶 = Σ𝑘𝑤 𝐶)
2726itgeq2dv 25837 . . . . . . . 8 (𝑡 = 𝑤 → ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = ∫𝐴Σ𝑘𝑤 𝐶 d𝑥)
28 sumeq1 15737 . . . . . . . 8 (𝑡 = 𝑤 → Σ𝑘𝑡𝐴𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)
2927, 28eqeq12d 2756 . . . . . . 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 4034 . . . . . 6 (𝑡 = (𝑤 ∪ {𝑧}) → (𝑡𝐵 ↔ (𝑤 ∪ {𝑧}) ⊆ 𝐵))
34 sumeq1 15737 . . . . . . . . 9 (𝑡 = (𝑤 ∪ {𝑧}) → Σ𝑘𝑡 𝐶 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶)
3534mpteq2dv 5268 . . . . . . . 8 (𝑡 = (𝑤 ∪ {𝑧}) → (𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) = (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶))
3635eleq1d 2829 . . . . . . 7 (𝑡 = (𝑤 ∪ {𝑧}) → ((𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) ∈ 𝐿1 ↔ (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) ∈ 𝐿1))
3734adantr 480 . . . . . . . . 9 ((𝑡 = (𝑤 ∪ {𝑧}) ∧ 𝑥𝐴) → Σ𝑘𝑡 𝐶 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶)
3837itgeq2dv 25837 . . . . . . . 8 (𝑡 = (𝑤 ∪ {𝑧}) → ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = ∫𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥)
39 sumeq1 15737 . . . . . . . 8 (𝑡 = (𝑤 ∪ {𝑧}) → Σ𝑘𝑡𝐴𝐶 d𝑥 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})∫𝐴𝐶 d𝑥)
4038, 39eqeq12d 2756 . . . . . . 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 4034 . . . . . 6 (𝑡 = 𝐵 → (𝑡𝐵𝐵𝐵))
45 sumeq1 15737 . . . . . . . . 9 (𝑡 = 𝐵 → Σ𝑘𝑡 𝐶 = Σ𝑘𝐵 𝐶)
4645mpteq2dv 5268 . . . . . . . 8 (𝑡 = 𝐵 → (𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) = (𝑥𝐴 ↦ Σ𝑘𝐵 𝐶))
4746eleq1d 2829 . . . . . . 7 (𝑡 = 𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑡 𝐶) ∈ 𝐿1 ↔ (𝑥𝐴 ↦ Σ𝑘𝐵 𝐶) ∈ 𝐿1))
4845adantr 480 . . . . . . . . 9 ((𝑡 = 𝐵𝑥𝐴) → Σ𝑘𝑡 𝐶 = Σ𝑘𝐵 𝐶)
4948itgeq2dv 25837 . . . . . . . 8 (𝑡 = 𝐵 → ∫𝐴Σ𝑘𝑡 𝐶 d𝑥 = ∫𝐴Σ𝑘𝐵 𝐶 d𝑥)
50 sumeq1 15737 . . . . . . . 8 (𝑡 = 𝐵 → Σ𝑘𝑡𝐴𝐶 d𝑥 = Σ𝑘𝐵𝐴𝐶 d𝑥)
5149, 50eqeq12d 2756 . . . . . . 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 25842 . . . . . 6 (𝐴 ∈ dom vol → (𝐴 × {0}) ∈ 𝐿1)
5755, 56syl 17 . . . . 5 (𝜑 → (𝐴 × {0}) ∈ 𝐿1)
5857a1d 25 . . . 4 (𝜑 → (∅ ⊆ 𝐵 → (𝐴 × {0}) ∈ 𝐿1))
59 ssun1 4201 . . . . . . . . . 10 𝑤 ⊆ (𝑤 ∪ {𝑧})
60 sstr 4017 . . . . . . . . . 10 ((𝑤 ⊆ (𝑤 ∪ {𝑧}) ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵) → 𝑤𝐵)
6159, 60mpan 689 . . . . . . . . 9 ((𝑤 ∪ {𝑧}) ⊆ 𝐵𝑤𝐵)
6261imim1i 63 . . . . . . . 8 ((𝑤𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ((𝑤 ∪ {𝑧}) ⊆ 𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)))
63 csbeq1a 3935 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑚𝐶 = 𝑚 / 𝑘𝐶)
64 nfcv 2908 . . . . . . . . . . . . . . . . . 18 𝑚𝐶
65 nfcsb1v 3946 . . . . . . . . . . . . . . . . . 18 𝑘𝑚 / 𝑘𝐶
6663, 64, 65cbvsum 15743 . . . . . . . . . . . . . . . . 17 Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 = Σ𝑚 ∈ (𝑤 ∪ {𝑧})𝑚 / 𝑘𝐶
67 simprl 770 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → ¬ 𝑧𝑤)
68 disjsn 4736 . . . . . . . . . . . . . . . . . . . . 21 ((𝑤 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑤)
6967, 68sylibr 234 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → (𝑤 ∩ {𝑧}) = ∅)
7069adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → (𝑤 ∩ {𝑧}) = ∅)
71 eqidd 2741 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → (𝑤 ∪ {𝑧}) = (𝑤 ∪ {𝑧}))
722adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → 𝐵 ∈ Fin)
73 simprr 772 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → (𝑤 ∪ {𝑧}) ⊆ 𝐵)
7472, 73ssfid 9329 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → (𝑤 ∪ {𝑧}) ∈ Fin)
7574adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → (𝑤 ∪ {𝑧}) ∈ Fin)
76 simplrr 777 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → (𝑤 ∪ {𝑧}) ⊆ 𝐵)
7776sselda 4008 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) ∧ 𝑚 ∈ (𝑤 ∪ {𝑧})) → 𝑚𝐵)
78 itgfsum.4 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑘𝐵) → (𝑥𝐴𝐶) ∈ 𝐿1)
79 iblmbf 25822 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥𝐴𝐶) ∈ 𝐿1 → (𝑥𝐴𝐶) ∈ MblFn)
8078, 79syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘𝐵) → (𝑥𝐴𝐶) ∈ MblFn)
81 itgfsum.3 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑥𝐴𝑘𝐵)) → 𝐶𝑉)
8281anass1rs 654 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑘𝐵) ∧ 𝑥𝐴) → 𝐶𝑉)
8380, 82mbfmptcl 25690 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑘𝐵) ∧ 𝑥𝐴) → 𝐶 ∈ ℂ)
8483an32s 651 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ ℂ)
8584ralrimiva 3152 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥𝐴) → ∀𝑘𝐵 𝐶 ∈ ℂ)
8685adantlr 714 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → ∀𝑘𝐵 𝐶 ∈ ℂ)
8764nfel1 2925 . . . . . . . . . . . . . . . . . . . . . . 23 𝑚 𝐶 ∈ ℂ
8865nfel1 2925 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘𝑚 / 𝑘𝐶 ∈ ℂ
8963eleq1d 2829 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝑚 → (𝐶 ∈ ℂ ↔ 𝑚 / 𝑘𝐶 ∈ ℂ))
9087, 88, 89cbvralw 3312 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑘𝐵 𝐶 ∈ ℂ ↔ ∀𝑚𝐵 𝑚 / 𝑘𝐶 ∈ ℂ)
9186, 90sylib 218 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → ∀𝑚𝐵 𝑚 / 𝑘𝐶 ∈ ℂ)
9291r19.21bi 3257 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) ∧ 𝑚𝐵) → 𝑚 / 𝑘𝐶 ∈ ℂ)
9377, 92syldan 590 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) ∧ 𝑚 ∈ (𝑤 ∪ {𝑧})) → 𝑚 / 𝑘𝐶 ∈ ℂ)
9470, 71, 75, 93fsumsplit 15789 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → Σ𝑚 ∈ (𝑤 ∪ {𝑧})𝑚 / 𝑘𝐶 = (Σ𝑚𝑤 𝑚 / 𝑘𝐶 + Σ𝑚 ∈ {𝑧}𝑚 / 𝑘𝐶))
95 vex 3492 . . . . . . . . . . . . . . . . . . . 20 𝑧 ∈ V
96 csbeq1 3924 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑧𝑚 / 𝑘𝐶 = 𝑧 / 𝑘𝐶)
9796eleq1d 2829 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑧 → (𝑚 / 𝑘𝐶 ∈ ℂ ↔ 𝑧 / 𝑘𝐶 ∈ ℂ))
9873unssbd 4217 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → {𝑧} ⊆ 𝐵)
9995snss 4810 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝐵 ↔ {𝑧} ⊆ 𝐵)
10098, 99sylibr 234 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → 𝑧𝐵)
101100adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → 𝑧𝐵)
10297, 91, 101rspcdva 3636 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → 𝑧 / 𝑘𝐶 ∈ ℂ)
10396sumsn 15794 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ V ∧ 𝑧 / 𝑘𝐶 ∈ ℂ) → Σ𝑚 ∈ {𝑧}𝑚 / 𝑘𝐶 = 𝑧 / 𝑘𝐶)
10495, 102, 103sylancr 586 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → Σ𝑚 ∈ {𝑧}𝑚 / 𝑘𝐶 = 𝑧 / 𝑘𝐶)
105104oveq2d 7464 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → (Σ𝑚𝑤 𝑚 / 𝑘𝐶 + Σ𝑚 ∈ {𝑧}𝑚 / 𝑘𝐶) = (Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑧 / 𝑘𝐶))
10694, 105eqtrd 2780 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → Σ𝑚 ∈ (𝑤 ∪ {𝑧})𝑚 / 𝑘𝐶 = (Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑧 / 𝑘𝐶))
10766, 106eqtrid 2792 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 = (Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑧 / 𝑘𝐶))
108107mpteq2dva 5266 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) = (𝑥𝐴 ↦ (Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑧 / 𝑘𝐶)))
109 nfcv 2908 . . . . . . . . . . . . . . . 16 𝑦𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑧 / 𝑘𝐶)
110 nfcsb1v 3946 . . . . . . . . . . . . . . . . 17 𝑥𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶
111 nfcv 2908 . . . . . . . . . . . . . . . . 17 𝑥 +
112 nfcsb1v 3946 . . . . . . . . . . . . . . . . 17 𝑥𝑦 / 𝑥𝑧 / 𝑘𝐶
113110, 111, 112nfov 7478 . . . . . . . . . . . . . . . 16 𝑥(𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑦 / 𝑥𝑧 / 𝑘𝐶)
114 csbeq1a 3935 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → Σ𝑚𝑤 𝑚 / 𝑘𝐶 = 𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶)
115 csbeq1a 3935 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦𝑧 / 𝑘𝐶 = 𝑦 / 𝑥𝑧 / 𝑘𝐶)
116114, 115oveq12d 7466 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑧 / 𝑘𝐶) = (𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑦 / 𝑥𝑧 / 𝑘𝐶))
117109, 113, 116cbvmpt 5277 . . . . . . . . . . . . . . 15 (𝑥𝐴 ↦ (Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑧 / 𝑘𝐶)) = (𝑦𝐴 ↦ (𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑦 / 𝑥𝑧 / 𝑘𝐶))
118108, 117eqtrdi 2796 . . . . . . . . . . . . . 14 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) = (𝑦𝐴 ↦ (𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑦 / 𝑥𝑧 / 𝑘𝐶)))
119118adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) = (𝑦𝐴 ↦ (𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑦 / 𝑥𝑧 / 𝑘𝐶)))
120 sumex 15736 . . . . . . . . . . . . . . . 16 Σ𝑚𝑤 𝑚 / 𝑘𝐶 ∈ V
121120csbex 5329 . . . . . . . . . . . . . . 15 𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 ∈ V
122121a1i 11 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) ∧ 𝑦𝐴) → 𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 ∈ V)
12363, 64, 65cbvsum 15743 . . . . . . . . . . . . . . . . 17 Σ𝑘𝑤 𝐶 = Σ𝑚𝑤 𝑚 / 𝑘𝐶
124123mpteq2i 5271 . . . . . . . . . . . . . . . 16 (𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) = (𝑥𝐴 ↦ Σ𝑚𝑤 𝑚 / 𝑘𝐶)
125 nfcv 2908 . . . . . . . . . . . . . . . . 17 𝑦Σ𝑚𝑤 𝑚 / 𝑘𝐶
126125, 110, 114cbvmpt 5277 . . . . . . . . . . . . . . . 16 (𝑥𝐴 ↦ Σ𝑚𝑤 𝑚 / 𝑘𝐶) = (𝑦𝐴𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶)
127124, 126eqtri 2768 . . . . . . . . . . . . . . 15 (𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) = (𝑦𝐴𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶)
128 simprl 770 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → (𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1)
129127, 128eqeltrrid 2849 . . . . . . . . . . . . . 14 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → (𝑦𝐴𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶) ∈ 𝐿1)
130102elexd 3512 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → 𝑧 / 𝑘𝐶 ∈ V)
131130ralrimiva 3152 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → ∀𝑥𝐴 𝑧 / 𝑘𝐶 ∈ V)
132131adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ∀𝑥𝐴 𝑧 / 𝑘𝐶 ∈ V)
133 nfv 1913 . . . . . . . . . . . . . . . . 17 𝑦𝑧 / 𝑘𝐶 ∈ V
134112nfel1 2925 . . . . . . . . . . . . . . . . 17 𝑥𝑦 / 𝑥𝑧 / 𝑘𝐶 ∈ V
135115eleq1d 2829 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝑧 / 𝑘𝐶 ∈ V ↔ 𝑦 / 𝑥𝑧 / 𝑘𝐶 ∈ V))
136133, 134, 135cbvralw 3312 . . . . . . . . . . . . . . . 16 (∀𝑥𝐴 𝑧 / 𝑘𝐶 ∈ V ↔ ∀𝑦𝐴 𝑦 / 𝑥𝑧 / 𝑘𝐶 ∈ V)
137132, 136sylib 218 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ∀𝑦𝐴 𝑦 / 𝑥𝑧 / 𝑘𝐶 ∈ V)
138137r19.21bi 3257 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) ∧ 𝑦𝐴) → 𝑦 / 𝑥𝑧 / 𝑘𝐶 ∈ V)
139 nfcv 2908 . . . . . . . . . . . . . . . . 17 𝑦𝑧 / 𝑘𝐶
140139, 112, 115cbvmpt 5277 . . . . . . . . . . . . . . . 16 (𝑥𝐴𝑧 / 𝑘𝐶) = (𝑦𝐴𝑦 / 𝑥𝑧 / 𝑘𝐶)
14196mpteq2dv 5268 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑧 → (𝑥𝐴𝑚 / 𝑘𝐶) = (𝑥𝐴𝑧 / 𝑘𝐶))
142141eleq1d 2829 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑧 → ((𝑥𝐴𝑚 / 𝑘𝐶) ∈ 𝐿1 ↔ (𝑥𝐴𝑧 / 𝑘𝐶) ∈ 𝐿1))
14378ralrimiva 3152 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑘𝐵 (𝑥𝐴𝐶) ∈ 𝐿1)
144 nfv 1913 . . . . . . . . . . . . . . . . . . . 20 𝑚(𝑥𝐴𝐶) ∈ 𝐿1
145 nfcv 2908 . . . . . . . . . . . . . . . . . . . . . 22 𝑘𝐴
146145, 65nfmpt 5273 . . . . . . . . . . . . . . . . . . . . 21 𝑘(𝑥𝐴𝑚 / 𝑘𝐶)
147146nfel1 2925 . . . . . . . . . . . . . . . . . . . 20 𝑘(𝑥𝐴𝑚 / 𝑘𝐶) ∈ 𝐿1
14863mpteq2dv 5268 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑚 → (𝑥𝐴𝐶) = (𝑥𝐴𝑚 / 𝑘𝐶))
149148eleq1d 2829 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑚 → ((𝑥𝐴𝐶) ∈ 𝐿1 ↔ (𝑥𝐴𝑚 / 𝑘𝐶) ∈ 𝐿1))
150144, 147, 149cbvralw 3312 . . . . . . . . . . . . . . . . . . 19 (∀𝑘𝐵 (𝑥𝐴𝐶) ∈ 𝐿1 ↔ ∀𝑚𝐵 (𝑥𝐴𝑚 / 𝑘𝐶) ∈ 𝐿1)
151143, 150sylib 218 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑚𝐵 (𝑥𝐴𝑚 / 𝑘𝐶) ∈ 𝐿1)
152151adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → ∀𝑚𝐵 (𝑥𝐴𝑚 / 𝑘𝐶) ∈ 𝐿1)
153142, 152, 100rspcdva 3636 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → (𝑥𝐴𝑧 / 𝑘𝐶) ∈ 𝐿1)
154140, 153eqeltrrid 2849 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → (𝑦𝐴𝑦 / 𝑥𝑧 / 𝑘𝐶) ∈ 𝐿1)
155154adantr 480 . . . . . . . . . . . . . 14 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → (𝑦𝐴𝑦 / 𝑥𝑧 / 𝑘𝐶) ∈ 𝐿1)
156122, 129, 138, 155ibladd 25876 . . . . . . . . . . . . 13 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → (𝑦𝐴 ↦ (𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑦 / 𝑥𝑧 / 𝑘𝐶)) ∈ 𝐿1)
157119, 156eqeltrd 2844 . . . . . . . . . . . 12 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) ∈ 𝐿1)
158122, 129, 138, 155itgadd 25880 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ∫𝐴(𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑦 / 𝑥𝑧 / 𝑘𝐶) d𝑦 = (∫𝐴𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 d𝑦 + ∫𝐴𝑦 / 𝑥𝑧 / 𝑘𝐶 d𝑦))
159116, 109, 113cbvitg 25831 . . . . . . . . . . . . . . 15 𝐴𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑧 / 𝑘𝐶) d𝑥 = ∫𝐴(𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑦 / 𝑥𝑧 / 𝑘𝐶) d𝑦
160114, 125, 110cbvitg 25831 . . . . . . . . . . . . . . . 16 𝐴Σ𝑚𝑤 𝑚 / 𝑘𝐶 d𝑥 = ∫𝐴𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 d𝑦
161115, 139, 112cbvitg 25831 . . . . . . . . . . . . . . . 16 𝐴𝑧 / 𝑘𝐶 d𝑥 = ∫𝐴𝑦 / 𝑥𝑧 / 𝑘𝐶 d𝑦
162160, 161oveq12i 7460 . . . . . . . . . . . . . . 15 (∫𝐴Σ𝑚𝑤 𝑚 / 𝑘𝐶 d𝑥 + ∫𝐴𝑧 / 𝑘𝐶 d𝑥) = (∫𝐴𝑦 / 𝑥Σ𝑚𝑤 𝑚 / 𝑘𝐶 d𝑦 + ∫𝐴𝑦 / 𝑥𝑧 / 𝑘𝐶 d𝑦)
163158, 159, 1623eqtr4g 2805 . . . . . . . . . . . . . 14 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ∫𝐴𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑧 / 𝑘𝐶) d𝑥 = (∫𝐴Σ𝑚𝑤 𝑚 / 𝑘𝐶 d𝑥 + ∫𝐴𝑧 / 𝑘𝐶 d𝑥))
164106itgeq2dv 25837 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → ∫𝐴Σ𝑚 ∈ (𝑤 ∪ {𝑧})𝑚 / 𝑘𝐶 d𝑥 = ∫𝐴𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑧 / 𝑘𝐶) d𝑥)
165164adantr 480 . . . . . . . . . . . . . 14 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ∫𝐴Σ𝑚 ∈ (𝑤 ∪ {𝑧})𝑚 / 𝑘𝐶 d𝑥 = ∫𝐴𝑚𝑤 𝑚 / 𝑘𝐶 + 𝑧 / 𝑘𝐶) d𝑥)
166 eqidd 2741 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → (𝑤 ∪ {𝑧}) = (𝑤 ∪ {𝑧}))
16773sselda 4008 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑚 ∈ (𝑤 ∪ {𝑧})) → 𝑚𝐵)
16892an32s 651 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑚𝐵) ∧ 𝑥𝐴) → 𝑚 / 𝑘𝐶 ∈ ℂ)
169152r19.21bi 3257 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑚𝐵) → (𝑥𝐴𝑚 / 𝑘𝐶) ∈ 𝐿1)
170168, 169itgcl 25839 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑚𝐵) → ∫𝐴𝑚 / 𝑘𝐶 d𝑥 ∈ ℂ)
171167, 170syldan 590 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑚 ∈ (𝑤 ∪ {𝑧})) → ∫𝐴𝑚 / 𝑘𝐶 d𝑥 ∈ ℂ)
17269, 166, 74, 171fsumsplit 15789 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → Σ𝑚 ∈ (𝑤 ∪ {𝑧})∫𝐴𝑚 / 𝑘𝐶 d𝑥 = (Σ𝑚𝑤𝐴𝑚 / 𝑘𝐶 d𝑥 + Σ𝑚 ∈ {𝑧}∫𝐴𝑚 / 𝑘𝐶 d𝑥))
173172adantr 480 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → Σ𝑚 ∈ (𝑤 ∪ {𝑧})∫𝐴𝑚 / 𝑘𝐶 d𝑥 = (Σ𝑚𝑤𝐴𝑚 / 𝑘𝐶 d𝑥 + Σ𝑚 ∈ {𝑧}∫𝐴𝑚 / 𝑘𝐶 d𝑥))
174 simprr 772 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)
175 itgeq2 25833 . . . . . . . . . . . . . . . . . 18 (∀𝑥𝐴 Σ𝑘𝑤 𝐶 = Σ𝑚𝑤 𝑚 / 𝑘𝐶 → ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = ∫𝐴Σ𝑚𝑤 𝑚 / 𝑘𝐶 d𝑥)
176123a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥𝐴 → Σ𝑘𝑤 𝐶 = Σ𝑚𝑤 𝑚 / 𝑘𝐶)
177175, 176mprg 3073 . . . . . . . . . . . . . . . . 17 𝐴Σ𝑘𝑤 𝐶 d𝑥 = ∫𝐴Σ𝑚𝑤 𝑚 / 𝑘𝐶 d𝑥
17863adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑘 = 𝑚𝑥𝐴) → 𝐶 = 𝑚 / 𝑘𝐶)
179178itgeq2dv 25837 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑚 → ∫𝐴𝐶 d𝑥 = ∫𝐴𝑚 / 𝑘𝐶 d𝑥)
180 nfcv 2908 . . . . . . . . . . . . . . . . . 18 𝑚𝐴𝐶 d𝑥
181145, 65nfitg 25830 . . . . . . . . . . . . . . . . . 18 𝑘𝐴𝑚 / 𝑘𝐶 d𝑥
182179, 180, 181cbvsum 15743 . . . . . . . . . . . . . . . . 17 Σ𝑘𝑤𝐴𝐶 d𝑥 = Σ𝑚𝑤𝐴𝑚 / 𝑘𝐶 d𝑥
183174, 177, 1823eqtr3g 2803 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ∫𝐴Σ𝑚𝑤 𝑚 / 𝑘𝐶 d𝑥 = Σ𝑚𝑤𝐴𝑚 / 𝑘𝐶 d𝑥)
184102, 153itgcl 25839 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → ∫𝐴𝑧 / 𝑘𝐶 d𝑥 ∈ ℂ)
185184adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ∫𝐴𝑧 / 𝑘𝐶 d𝑥 ∈ ℂ)
18696adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 = 𝑧𝑥𝐴) → 𝑚 / 𝑘𝐶 = 𝑧 / 𝑘𝐶)
187186itgeq2dv 25837 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑧 → ∫𝐴𝑚 / 𝑘𝐶 d𝑥 = ∫𝐴𝑧 / 𝑘𝐶 d𝑥)
188187sumsn 15794 . . . . . . . . . . . . . . . . . 18 ((𝑧 ∈ V ∧ ∫𝐴𝑧 / 𝑘𝐶 d𝑥 ∈ ℂ) → Σ𝑚 ∈ {𝑧}∫𝐴𝑚 / 𝑘𝐶 d𝑥 = ∫𝐴𝑧 / 𝑘𝐶 d𝑥)
18995, 185, 188sylancr 586 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → Σ𝑚 ∈ {𝑧}∫𝐴𝑚 / 𝑘𝐶 d𝑥 = ∫𝐴𝑧 / 𝑘𝐶 d𝑥)
190189eqcomd 2746 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ∫𝐴𝑧 / 𝑘𝐶 d𝑥 = Σ𝑚 ∈ {𝑧}∫𝐴𝑚 / 𝑘𝐶 d𝑥)
191183, 190oveq12d 7466 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → (∫𝐴Σ𝑚𝑤 𝑚 / 𝑘𝐶 d𝑥 + ∫𝐴𝑧 / 𝑘𝐶 d𝑥) = (Σ𝑚𝑤𝐴𝑚 / 𝑘𝐶 d𝑥 + Σ𝑚 ∈ {𝑧}∫𝐴𝑚 / 𝑘𝐶 d𝑥))
192173, 191eqtr4d 2783 . . . . . . . . . . . . . 14 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → Σ𝑚 ∈ (𝑤 ∪ {𝑧})∫𝐴𝑚 / 𝑘𝐶 d𝑥 = (∫𝐴Σ𝑚𝑤 𝑚 / 𝑘𝐶 d𝑥 + ∫𝐴𝑧 / 𝑘𝐶 d𝑥))
193163, 165, 1923eqtr4d 2790 . . . . . . . . . . . . 13 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ∫𝐴Σ𝑚 ∈ (𝑤 ∪ {𝑧})𝑚 / 𝑘𝐶 d𝑥 = Σ𝑚 ∈ (𝑤 ∪ {𝑧})∫𝐴𝑚 / 𝑘𝐶 d𝑥)
194 itgeq2 25833 . . . . . . . . . . . . . 14 (∀𝑥𝐴 Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 = Σ𝑚 ∈ (𝑤 ∪ {𝑧})𝑚 / 𝑘𝐶 → ∫𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥 = ∫𝐴Σ𝑚 ∈ (𝑤 ∪ {𝑧})𝑚 / 𝑘𝐶 d𝑥)
19566a1i 11 . . . . . . . . . . . . . 14 (𝑥𝐴 → Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 = Σ𝑚 ∈ (𝑤 ∪ {𝑧})𝑚 / 𝑘𝐶)
196194, 195mprg 3073 . . . . . . . . . . . . 13 𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥 = ∫𝐴Σ𝑚 ∈ (𝑤 ∪ {𝑧})𝑚 / 𝑘𝐶 d𝑥
197179, 180, 181cbvsum 15743 . . . . . . . . . . . . 13 Σ𝑘 ∈ (𝑤 ∪ {𝑧})∫𝐴𝐶 d𝑥 = Σ𝑚 ∈ (𝑤 ∪ {𝑧})∫𝐴𝑚 / 𝑘𝐶 d𝑥
198193, 196, 1973eqtr4g 2805 . . . . . . . . . . . 12 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ∫𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})∫𝐴𝐶 d𝑥)
199157, 198jca 511 . . . . . . . . . . 11 (((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) ∧ ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ((𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})∫𝐴𝐶 d𝑥))
200199ex 412 . . . . . . . . . 10 ((𝜑 ∧ (¬ 𝑧𝑤 ∧ (𝑤 ∪ {𝑧}) ⊆ 𝐵)) → (((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥) → ((𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})∫𝐴𝐶 d𝑥)))
201200expr 456 . . . . . . . . 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 413 . . . . . 6 𝑧𝑤 → (𝜑 → ((𝑤𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ((𝑤 ∪ {𝑧}) ⊆ 𝐵 → ((𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})∫𝐴𝐶 d𝑥)))))
205204adantl 481 . . . . 5 ((𝑤 ∈ Fin ∧ ¬ 𝑧𝑤) → (𝜑 → ((𝑤𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥)) → ((𝑤 ∪ {𝑧}) ⊆ 𝐵 → ((𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})∫𝐴𝐶 d𝑥)))))
206205a2d 29 . . . 4 ((𝑤 ∈ Fin ∧ ¬ 𝑧𝑤) → ((𝜑 → (𝑤𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘𝑤 𝐶 d𝑥 = Σ𝑘𝑤𝐴𝐶 d𝑥))) → (𝜑 → ((𝑤 ∪ {𝑧}) ⊆ 𝐵 → ((𝑥𝐴 ↦ Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘 ∈ (𝑤 ∪ {𝑧})𝐶 d𝑥 = Σ𝑘 ∈ (𝑤 ∪ {𝑧})∫𝐴𝐶 d𝑥)))))
20721, 32, 43, 54, 58, 206findcard2s 9231 . . 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 395   = wceq 1537  wcel 2108  wral 3067  Vcvv 3488  csb 3921  cun 3974  cin 3975  wss 3976  c0 4352  {csn 4648  cmpt 5249   × cxp 5698  dom cdm 5700  (class class class)co 7448  Fincfn 9003  cc 11182  0cc0 11184   + caddc 11187  Σcsu 15734  volcvol 25517  MblFncmbf 25668  𝐿1cibl 25671  citg 25672
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-inf2 9710  ax-cc 10504  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261  ax-pre-sup 11262  ax-addf 11263
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-disj 5134  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-isom 6582  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-of 7714  df-ofr 7715  df-om 7904  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-2o 8523  df-oadd 8526  df-omul 8527  df-er 8763  df-map 8886  df-pm 8887  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-fi 9480  df-sup 9511  df-inf 9512  df-oi 9579  df-dju 9970  df-card 10008  df-acn 10011  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-div 11948  df-nn 12294  df-2 12356  df-3 12357  df-4 12358  df-n0 12554  df-z 12640  df-uz 12904  df-q 13014  df-rp 13058  df-xneg 13175  df-xadd 13176  df-xmul 13177  df-ioo 13411  df-ioc 13412  df-ico 13413  df-icc 13414  df-fz 13568  df-fzo 13712  df-fl 13843  df-mod 13921  df-seq 14053  df-exp 14113  df-hash 14380  df-cj 15148  df-re 15149  df-im 15150  df-sqrt 15284  df-abs 15285  df-clim 15534  df-rlim 15535  df-sum 15735  df-rest 17482  df-topgen 17503  df-psmet 21379  df-xmet 21380  df-met 21381  df-bl 21382  df-mopn 21383  df-top 22921  df-topon 22938  df-bases 22974  df-cmp 23416  df-ovol 25518  df-vol 25519  df-mbf 25673  df-itg1 25674  df-itg2 25675  df-ibl 25676  df-itg 25677  df-0p 25724
This theorem is referenced by:  circlemeth  34617  3factsumint1  41978  fourierdlem83  46110
  Copyright terms: Public domain W3C validator