This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itgfsum

Description: Take a finite sum of integrals over the same domain. (Contributed by Mario Carneiro, 24-Aug-2014)

Ref Expression
Hypotheses itgfsum.1 ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
itgfsum.2 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
itgfsum.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐶 ∈ 𝑉 )
itgfsum.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
Assertion itgfsum ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝐵 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝐵 ∫ 𝐴 𝐶 d 𝑥 ) )

Proof

Step Hyp Ref Expression
1 itgfsum.1 ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
2 itgfsum.2 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
3 itgfsum.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐶 ∈ 𝑉 )
4 itgfsum.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
5 ssid ⊢ 𝐵 ⊆ 𝐵
6 sseq1 ⊢ ( 𝑡 = ∅ → ( 𝑡 ⊆ 𝐵 ↔ ∅ ⊆ 𝐵 ) )
7 itgz ⊢ ∫ 𝐴 0 d 𝑥 = 0
8 sumeq1 ⊢ ( 𝑡 = ∅ → Σ 𝑘 ∈ 𝑡 𝐶 = Σ 𝑘 ∈ ∅ 𝐶 )
9 sum0 ⊢ Σ 𝑘 ∈ ∅ 𝐶 = 0
10 8 9 eqtrdi ⊢ ( 𝑡 = ∅ → Σ 𝑘 ∈ 𝑡 𝐶 = 0 )
11 10 adantr ⊢ ( ( 𝑡 = ∅ ∧ 𝑥 ∈ 𝐴 ) → Σ 𝑘 ∈ 𝑡 𝐶 = 0 )
12 11 itgeq2dv ⊢ ( 𝑡 = ∅ → ∫ 𝐴 Σ 𝑘 ∈ 𝑡 𝐶 d 𝑥 = ∫ 𝐴 0 d 𝑥 )
13 sumeq1 ⊢ ( 𝑡 = ∅ → Σ 𝑘 ∈ 𝑡 ∫ 𝐴 𝐶 d 𝑥 = Σ 𝑘 ∈ ∅ ∫ 𝐴 𝐶 d 𝑥 )
14 sum0 ⊢ Σ 𝑘 ∈ ∅ ∫ 𝐴 𝐶 d 𝑥 = 0
15 13 14 eqtrdi ⊢ ( 𝑡 = ∅ → Σ 𝑘 ∈ 𝑡 ∫ 𝐴 𝐶 d 𝑥 = 0 )
16 7 12 15 3eqtr4a ⊢ ( 𝑡 = ∅ → ∫ 𝐴 Σ 𝑘 ∈ 𝑡 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑡 ∫ 𝐴 𝐶 d 𝑥 )
17 10 mpteq2dv ⊢ ( 𝑡 = ∅ → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑡 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 0 ) )
18 fconstmpt ⊢ ( 𝐴 × { 0 } ) = ( 𝑥 ∈ 𝐴 ↦ 0 )
19 17 18 eqtr4di ⊢ ( 𝑡 = ∅ → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑡 𝐶 ) = ( 𝐴 × { 0 } ) )
20 19 eleq1d ⊢ ( 𝑡 = ∅ → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑡 𝐶 ) ∈ 𝐿1 ↔ ( 𝐴 × { 0 } ) ∈ 𝐿1 ) )
21 20 anbi1d ⊢ ( 𝑡 = ∅ → ( ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑡 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑡 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑡 ∫ 𝐴 𝐶 d 𝑥 ) ↔ ( ( 𝐴 × { 0 } ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑡 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑡 ∫ 𝐴 𝐶 d 𝑥 ) ) )
22 16 21 mpbiran2d ⊢ ( 𝑡 = ∅ → ( ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑡 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑡 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑡 ∫ 𝐴 𝐶 d 𝑥 ) ↔ ( 𝐴 × { 0 } ) ∈ 𝐿1 ) )
23 6 22 imbi12d ⊢ ( 𝑡 = ∅ → ( ( 𝑡 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑡 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑡 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑡 ∫ 𝐴 𝐶 d 𝑥 ) ) ↔ ( ∅ ⊆ 𝐵 → ( 𝐴 × { 0 } ) ∈ 𝐿1 ) ) )
24 23 imbi2d ⊢ ( 𝑡 = ∅ → ( ( 𝜑 → ( 𝑡 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑡 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑡 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑡 ∫ 𝐴 𝐶 d 𝑥 ) ) ) ↔ ( 𝜑 → ( ∅ ⊆ 𝐵 → ( 𝐴 × { 0 } ) ∈ 𝐿1 ) ) ) )
25 sseq1 ⊢ ( 𝑡 = 𝑤 → ( 𝑡 ⊆ 𝐵 ↔ 𝑤 ⊆ 𝐵 ) )
26 sumeq1 ⊢ ( 𝑡 = 𝑤 → Σ 𝑘 ∈ 𝑡 𝐶 = Σ 𝑘 ∈ 𝑤 𝐶 )
27 26 mpteq2dv ⊢ ( 𝑡 = 𝑤 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑡 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) )
28 27 eleq1d ⊢ ( 𝑡 = 𝑤 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑡 𝐶 ) ∈ 𝐿1 ↔ ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ) )
29 26 adantr ⊢ ( ( 𝑡 = 𝑤 ∧ 𝑥 ∈ 𝐴 ) → Σ 𝑘 ∈ 𝑡 𝐶 = Σ 𝑘 ∈ 𝑤 𝐶 )
30 29 itgeq2dv ⊢ ( 𝑡 = 𝑤 → ∫ 𝐴 Σ 𝑘 ∈ 𝑡 𝐶 d 𝑥 = ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 )
31 sumeq1 ⊢ ( 𝑡 = 𝑤 → Σ 𝑘 ∈ 𝑡 ∫ 𝐴 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 )
32 30 31 eqeq12d ⊢ ( 𝑡 = 𝑤 → ( ∫ 𝐴 Σ 𝑘 ∈ 𝑡 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑡 ∫ 𝐴 𝐶 d 𝑥 ↔ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) )
33 28 32 anbi12d ⊢ ( 𝑡 = 𝑤 → ( ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑡 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑡 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑡 ∫ 𝐴 𝐶 d 𝑥 ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) )
34 25 33 imbi12d ⊢ ( 𝑡 = 𝑤 → ( ( 𝑡 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑡 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑡 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑡 ∫ 𝐴 𝐶 d 𝑥 ) ) ↔ ( 𝑤 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) ) )
35 34 imbi2d ⊢ ( 𝑡 = 𝑤 → ( ( 𝜑 → ( 𝑡 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑡 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑡 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑡 ∫ 𝐴 𝐶 d 𝑥 ) ) ) ↔ ( 𝜑 → ( 𝑤 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) ) ) )
36 sseq1 ⊢ ( 𝑡 = ( 𝑤 ∪ { 𝑧 } ) → ( 𝑡 ⊆ 𝐵 ↔ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) )
37 sumeq1 ⊢ ( 𝑡 = ( 𝑤 ∪ { 𝑧 } ) → Σ 𝑘 ∈ 𝑡 𝐶 = Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 )
38 37 mpteq2dv ⊢ ( 𝑡 = ( 𝑤 ∪ { 𝑧 } ) → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑡 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 ) )
39 38 eleq1d ⊢ ( 𝑡 = ( 𝑤 ∪ { 𝑧 } ) → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑡 𝐶 ) ∈ 𝐿1 ↔ ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 ) ∈ 𝐿1 ) )
40 37 adantr ⊢ ( ( 𝑡 = ( 𝑤 ∪ { 𝑧 } ) ∧ 𝑥 ∈ 𝐴 ) → Σ 𝑘 ∈ 𝑡 𝐶 = Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 )
41 40 itgeq2dv ⊢ ( 𝑡 = ( 𝑤 ∪ { 𝑧 } ) → ∫ 𝐴 Σ 𝑘 ∈ 𝑡 𝐶 d 𝑥 = ∫ 𝐴 Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 d 𝑥 )
42 sumeq1 ⊢ ( 𝑡 = ( 𝑤 ∪ { 𝑧 } ) → Σ 𝑘 ∈ 𝑡 ∫ 𝐴 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) ∫ 𝐴 𝐶 d 𝑥 )
43 41 42 eqeq12d ⊢ ( 𝑡 = ( 𝑤 ∪ { 𝑧 } ) → ( ∫ 𝐴 Σ 𝑘 ∈ 𝑡 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑡 ∫ 𝐴 𝐶 d 𝑥 ↔ ∫ 𝐴 Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) ∫ 𝐴 𝐶 d 𝑥 ) )
44 39 43 anbi12d ⊢ ( 𝑡 = ( 𝑤 ∪ { 𝑧 } ) → ( ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑡 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑡 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑡 ∫ 𝐴 𝐶 d 𝑥 ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) ∫ 𝐴 𝐶 d 𝑥 ) ) )
45 36 44 imbi12d ⊢ ( 𝑡 = ( 𝑤 ∪ { 𝑧 } ) → ( ( 𝑡 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑡 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑡 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑡 ∫ 𝐴 𝐶 d 𝑥 ) ) ↔ ( ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) ∫ 𝐴 𝐶 d 𝑥 ) ) ) )
46 45 imbi2d ⊢ ( 𝑡 = ( 𝑤 ∪ { 𝑧 } ) → ( ( 𝜑 → ( 𝑡 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑡 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑡 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑡 ∫ 𝐴 𝐶 d 𝑥 ) ) ) ↔ ( 𝜑 → ( ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) ∫ 𝐴 𝐶 d 𝑥 ) ) ) ) )
47 sseq1 ⊢ ( 𝑡 = 𝐵 → ( 𝑡 ⊆ 𝐵 ↔ 𝐵 ⊆ 𝐵 ) )
48 sumeq1 ⊢ ( 𝑡 = 𝐵 → Σ 𝑘 ∈ 𝑡 𝐶 = Σ 𝑘 ∈ 𝐵 𝐶 )
49 48 mpteq2dv ⊢ ( 𝑡 = 𝐵 → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑡 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝐵 𝐶 ) )
50 49 eleq1d ⊢ ( 𝑡 = 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑡 𝐶 ) ∈ 𝐿1 ↔ ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝐵 𝐶 ) ∈ 𝐿1 ) )
51 48 adantr ⊢ ( ( 𝑡 = 𝐵 ∧ 𝑥 ∈ 𝐴 ) → Σ 𝑘 ∈ 𝑡 𝐶 = Σ 𝑘 ∈ 𝐵 𝐶 )
52 51 itgeq2dv ⊢ ( 𝑡 = 𝐵 → ∫ 𝐴 Σ 𝑘 ∈ 𝑡 𝐶 d 𝑥 = ∫ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 d 𝑥 )
53 sumeq1 ⊢ ( 𝑡 = 𝐵 → Σ 𝑘 ∈ 𝑡 ∫ 𝐴 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝐵 ∫ 𝐴 𝐶 d 𝑥 )
54 52 53 eqeq12d ⊢ ( 𝑡 = 𝐵 → ( ∫ 𝐴 Σ 𝑘 ∈ 𝑡 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑡 ∫ 𝐴 𝐶 d 𝑥 ↔ ∫ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝐵 ∫ 𝐴 𝐶 d 𝑥 ) )
55 50 54 anbi12d ⊢ ( 𝑡 = 𝐵 → ( ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑡 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑡 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑡 ∫ 𝐴 𝐶 d 𝑥 ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝐵 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝐵 ∫ 𝐴 𝐶 d 𝑥 ) ) )
56 47 55 imbi12d ⊢ ( 𝑡 = 𝐵 → ( ( 𝑡 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑡 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑡 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑡 ∫ 𝐴 𝐶 d 𝑥 ) ) ↔ ( 𝐵 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝐵 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝐵 ∫ 𝐴 𝐶 d 𝑥 ) ) ) )
57 56 imbi2d ⊢ ( 𝑡 = 𝐵 → ( ( 𝜑 → ( 𝑡 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑡 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑡 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑡 ∫ 𝐴 𝐶 d 𝑥 ) ) ) ↔ ( 𝜑 → ( 𝐵 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝐵 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝐵 ∫ 𝐴 𝐶 d 𝑥 ) ) ) ) )
58 ibl0 ⊢ ( 𝐴 ∈ dom vol → ( 𝐴 × { 0 } ) ∈ 𝐿1 )
59 1 58 syl ⊢ ( 𝜑 → ( 𝐴 × { 0 } ) ∈ 𝐿1 )
60 59 a1d ⊢ ( 𝜑 → ( ∅ ⊆ 𝐵 → ( 𝐴 × { 0 } ) ∈ 𝐿1 ) )
61 ssun1 ⊢ 𝑤 ⊆ ( 𝑤 ∪ { 𝑧 } )
62 sstr ⊢ ( ( 𝑤 ⊆ ( 𝑤 ∪ { 𝑧 } ) ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) → 𝑤 ⊆ 𝐵 )
63 61 62 mpan ⊢ ( ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 → 𝑤 ⊆ 𝐵 )
64 63 imim1i ⊢ ( ( 𝑤 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → ( ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) )
65 csbeq1a ⊢ ( 𝑘 = 𝑚 → 𝐶 = ⦋ 𝑚 / 𝑘 ⦌ 𝐶 )
66 nfcv ⊢ Ⅎ 𝑚 𝐶
67 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑚 / 𝑘 ⦌ 𝐶
68 65 66 67 cbvsum ⊢ Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 = Σ 𝑚 ∈ ( 𝑤 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐶
69 simprl ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ¬ 𝑧 ∈ 𝑤 )
70 disjsn ⊢ ( ( 𝑤 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ 𝑤 )
71 69 70 sylibr ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( 𝑤 ∩ { 𝑧 } ) = ∅ )
72 71 adantr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑤 ∩ { 𝑧 } ) = ∅ )
73 eqidd ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑤 ∪ { 𝑧 } ) = ( 𝑤 ∪ { 𝑧 } ) )
74 2 adantr ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → 𝐵 ∈ Fin )
75 simprr ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 )
76 74 75 ssfid ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( 𝑤 ∪ { 𝑧 } ) ∈ Fin )
77 76 adantr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑤 ∪ { 𝑧 } ) ∈ Fin )
78 simplrr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 )
79 78 sselda ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ∪ { 𝑧 } ) ) → 𝑚 ∈ 𝐵 )
80 iblmbf ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
81 4 80 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
82 3 anass1rs ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
83 81 82 mbfmptcl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
84 83 an32s ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
85 84 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ )
86 85 adantlr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ )
87 66 nfel1 ⊢ Ⅎ 𝑚 𝐶 ∈ ℂ
88 67 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ∈ ℂ
89 65 eleq1d ⊢ ( 𝑘 = 𝑚 → ( 𝐶 ∈ ℂ ↔ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ∈ ℂ ) )
90 87 88 89 cbvralw ⊢ ( ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ ↔ ∀ 𝑚 ∈ 𝐵 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ∈ ℂ )
91 86 90 sylib ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑚 ∈ 𝐵 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ∈ ℂ )
92 91 r19.21bi ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑚 ∈ 𝐵 ) → ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ∈ ℂ )
93 79 92 syldan ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ∪ { 𝑧 } ) ) → ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ∈ ℂ )
94 72 73 77 93 fsumsplit ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → Σ 𝑚 ∈ ( 𝑤 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐶 = ( Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 + Σ 𝑚 ∈ { 𝑧 } ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) )
95 vex ⊢ 𝑧 ∈ V
96 csbeq1 ⊢ ( 𝑚 = 𝑧 → ⦋ 𝑚 / 𝑘 ⦌ 𝐶 = ⦋ 𝑧 / 𝑘 ⦌ 𝐶 )
97 96 eleq1d ⊢ ( 𝑚 = 𝑧 → ( ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ∈ ℂ ↔ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ ℂ ) )
98 75 unssbd ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → { 𝑧 } ⊆ 𝐵 )
99 95 snss ⊢ ( 𝑧 ∈ 𝐵 ↔ { 𝑧 } ⊆ 𝐵 )
100 98 99 sylibr ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → 𝑧 ∈ 𝐵 )
101 100 adantr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑧 ∈ 𝐵 )
102 97 91 101 rspcdva ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ ℂ )
103 96 sumsn ⊢ ( ( 𝑧 ∈ V ∧ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ ℂ ) → Σ 𝑚 ∈ { 𝑧 } ⦋ 𝑚 / 𝑘 ⦌ 𝐶 = ⦋ 𝑧 / 𝑘 ⦌ 𝐶 )
104 95 102 103 sylancr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → Σ 𝑚 ∈ { 𝑧 } ⦋ 𝑚 / 𝑘 ⦌ 𝐶 = ⦋ 𝑧 / 𝑘 ⦌ 𝐶 )
105 104 oveq2d ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 + Σ 𝑚 ∈ { 𝑧 } ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) = ( Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 + ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) )
106 94 105 eqtrd ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → Σ 𝑚 ∈ ( 𝑤 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐶 = ( Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 + ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) )
107 68 106 eqtrid ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 = ( Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 + ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) )
108 107 mpteq2dva ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ ( Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 + ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) ) )
109 nfcv ⊢ Ⅎ 𝑦 ( Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 + ⦋ 𝑧 / 𝑘 ⦌ 𝐶 )
110 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶
111 nfcv ⊢ Ⅎ 𝑥 +
112 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶
113 110 111 112 nfov ⊢ Ⅎ 𝑥 ( ⦋ 𝑦 / 𝑥 ⦌ Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 + ⦋ 𝑦 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 )
114 csbeq1a ⊢ ( 𝑥 = 𝑦 → Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 )
115 csbeq1a ⊢ ( 𝑥 = 𝑦 → ⦋ 𝑧 / 𝑘 ⦌ 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 )
116 114 115 oveq12d ⊢ ( 𝑥 = 𝑦 → ( Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 + ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) = ( ⦋ 𝑦 / 𝑥 ⦌ Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 + ⦋ 𝑦 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) )
117 109 113 116 cbvmpt ⊢ ( 𝑥 ∈ 𝐴 ↦ ( Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 + ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) ) = ( 𝑦 ∈ 𝐴 ↦ ( ⦋ 𝑦 / 𝑥 ⦌ Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 + ⦋ 𝑦 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) )
118 108 117 eqtrdi ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 ) = ( 𝑦 ∈ 𝐴 ↦ ( ⦋ 𝑦 / 𝑥 ⦌ Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 + ⦋ 𝑦 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) ) )
119 118 adantr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 ) = ( 𝑦 ∈ 𝐴 ↦ ( ⦋ 𝑦 / 𝑥 ⦌ Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 + ⦋ 𝑦 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) ) )
120 sumex ⊢ Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ∈ V
121 120 csbex ⊢ ⦋ 𝑦 / 𝑥 ⦌ Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ∈ V
122 121 a1i ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ∈ V )
123 65 66 67 cbvsum ⊢ Σ 𝑘 ∈ 𝑤 𝐶 = Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶
124 123 mpteq2i ⊢ ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 )
125 nfcv ⊢ Ⅎ 𝑦 Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶
126 125 110 114 cbvmpt ⊢ ( 𝑥 ∈ 𝐴 ↦ Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) = ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 )
127 124 126 eqtri ⊢ ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) = ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 )
128 simprl ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 )
129 127 128 eqeltrrid ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) ∈ 𝐿1 )
130 102 elexd ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ V )
131 130 ralrimiva ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ V )
132 131 adantr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → ∀ 𝑥 ∈ 𝐴 ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ V )
133 nfv ⊢ Ⅎ 𝑦 ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ V
134 112 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ V
135 115 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ V ↔ ⦋ 𝑦 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ V ) )
136 133 134 135 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝐴 ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ V ↔ ∀ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ V )
137 132 136 sylib ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → ∀ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ V )
138 137 r19.21bi ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ∈ V )
139 nfcv ⊢ Ⅎ 𝑦 ⦋ 𝑧 / 𝑘 ⦌ 𝐶
140 139 112 115 cbvmpt ⊢ ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) = ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 )
141 96 mpteq2dv ⊢ ( 𝑚 = 𝑧 → ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) )
142 141 eleq1d ⊢ ( 𝑚 = 𝑧 → ( ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) ∈ 𝐿1 ↔ ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) ∈ 𝐿1 ) )
143 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐵 ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
144 nfv ⊢ Ⅎ 𝑚 ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1
145 nfcv ⊢ Ⅎ 𝑘 𝐴
146 145 67 nfmpt ⊢ Ⅎ 𝑘 ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 )
147 146 nfel1 ⊢ Ⅎ 𝑘 ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) ∈ 𝐿1
148 65 mpteq2dv ⊢ ( 𝑘 = 𝑚 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) )
149 148 eleq1d ⊢ ( 𝑘 = 𝑚 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 ↔ ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) ∈ 𝐿1 ) )
150 144 147 149 cbvralw ⊢ ( ∀ 𝑘 ∈ 𝐵 ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 ↔ ∀ 𝑚 ∈ 𝐵 ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) ∈ 𝐿1 )
151 143 150 sylib ⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝐵 ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) ∈ 𝐿1 )
152 151 adantr ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ∀ 𝑚 ∈ 𝐵 ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) ∈ 𝐿1 )
153 142 152 100 rspcdva ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) ∈ 𝐿1 )
154 140 153 eqeltrrid ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) ∈ 𝐿1 )
155 154 adantr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) ∈ 𝐿1 )
156 122 129 138 155 ibladd ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → ( 𝑦 ∈ 𝐴 ↦ ( ⦋ 𝑦 / 𝑥 ⦌ Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 + ⦋ 𝑦 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) ) ∈ 𝐿1 )
157 119 156 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 ) ∈ 𝐿1 )
158 122 129 138 155 itgadd ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → ∫ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 + ⦋ 𝑦 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) d 𝑦 = ( ∫ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑦 + ∫ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 d 𝑦 ) )
159 116 109 113 cbvitg ⊢ ∫ 𝐴 ( Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 + ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) d 𝑥 = ∫ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 + ⦋ 𝑦 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) d 𝑦
160 114 125 110 cbvitg ⊢ ∫ 𝐴 Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 = ∫ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑦
161 115 139 112 cbvitg ⊢ ∫ 𝐴 ⦋ 𝑧 / 𝑘 ⦌ 𝐶 d 𝑥 = ∫ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 d 𝑦
162 160 161 oveq12i ⊢ ( ∫ 𝐴 Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 + ∫ 𝐴 ⦋ 𝑧 / 𝑘 ⦌ 𝐶 d 𝑥 ) = ( ∫ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑦 + ∫ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ ⦋ 𝑧 / 𝑘 ⦌ 𝐶 d 𝑦 )
163 158 159 162 3eqtr4g ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → ∫ 𝐴 ( Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 + ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) d 𝑥 = ( ∫ 𝐴 Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 + ∫ 𝐴 ⦋ 𝑧 / 𝑘 ⦌ 𝐶 d 𝑥 ) )
164 106 itgeq2dv ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ∫ 𝐴 Σ 𝑚 ∈ ( 𝑤 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 = ∫ 𝐴 ( Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 + ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) d 𝑥 )
165 164 adantr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → ∫ 𝐴 Σ 𝑚 ∈ ( 𝑤 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 = ∫ 𝐴 ( Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 + ⦋ 𝑧 / 𝑘 ⦌ 𝐶 ) d 𝑥 )
166 eqidd ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( 𝑤 ∪ { 𝑧 } ) = ( 𝑤 ∪ { 𝑧 } ) )
167 75 sselda ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑚 ∈ ( 𝑤 ∪ { 𝑧 } ) ) → 𝑚 ∈ 𝐵 )
168 92 an32s ⊢ ( ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ∈ ℂ )
169 152 r19.21bi ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑚 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) ∈ 𝐿1 )
170 168 169 itgcl ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑚 ∈ 𝐵 ) → ∫ 𝐴 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 ∈ ℂ )
171 167 170 syldan ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ 𝑚 ∈ ( 𝑤 ∪ { 𝑧 } ) ) → ∫ 𝐴 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 ∈ ℂ )
172 71 166 76 171 fsumsplit ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → Σ 𝑚 ∈ ( 𝑤 ∪ { 𝑧 } ) ∫ 𝐴 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 = ( Σ 𝑚 ∈ 𝑤 ∫ 𝐴 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 + Σ 𝑚 ∈ { 𝑧 } ∫ 𝐴 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 ) )
173 172 adantr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → Σ 𝑚 ∈ ( 𝑤 ∪ { 𝑧 } ) ∫ 𝐴 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 = ( Σ 𝑚 ∈ 𝑤 ∫ 𝐴 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 + Σ 𝑚 ∈ { 𝑧 } ∫ 𝐴 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 ) )
174 simprr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 )
175 itgeq2 ⊢ ( ∀ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 = Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 → ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = ∫ 𝐴 Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 )
176 123 a1i ⊢ ( 𝑥 ∈ 𝐴 → Σ 𝑘 ∈ 𝑤 𝐶 = Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 )
177 175 176 mprg ⊢ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = ∫ 𝐴 Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥
178 65 adantr ⊢ ( ( 𝑘 = 𝑚 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 = ⦋ 𝑚 / 𝑘 ⦌ 𝐶 )
179 178 itgeq2dv ⊢ ( 𝑘 = 𝑚 → ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐴 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 )
180 nfcv ⊢ Ⅎ 𝑚 ∫ 𝐴 𝐶 d 𝑥
181 145 67 nfitg ⊢ Ⅎ 𝑘 ∫ 𝐴 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥
182 179 180 181 cbvsum ⊢ Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 = Σ 𝑚 ∈ 𝑤 ∫ 𝐴 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥
183 174 177 182 3eqtr3g ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → ∫ 𝐴 Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 = Σ 𝑚 ∈ 𝑤 ∫ 𝐴 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 )
184 102 153 itgcl ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ∫ 𝐴 ⦋ 𝑧 / 𝑘 ⦌ 𝐶 d 𝑥 ∈ ℂ )
185 184 adantr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → ∫ 𝐴 ⦋ 𝑧 / 𝑘 ⦌ 𝐶 d 𝑥 ∈ ℂ )
186 96 adantr ⊢ ( ( 𝑚 = 𝑧 ∧ 𝑥 ∈ 𝐴 ) → ⦋ 𝑚 / 𝑘 ⦌ 𝐶 = ⦋ 𝑧 / 𝑘 ⦌ 𝐶 )
187 186 itgeq2dv ⊢ ( 𝑚 = 𝑧 → ∫ 𝐴 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 = ∫ 𝐴 ⦋ 𝑧 / 𝑘 ⦌ 𝐶 d 𝑥 )
188 187 sumsn ⊢ ( ( 𝑧 ∈ V ∧ ∫ 𝐴 ⦋ 𝑧 / 𝑘 ⦌ 𝐶 d 𝑥 ∈ ℂ ) → Σ 𝑚 ∈ { 𝑧 } ∫ 𝐴 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 = ∫ 𝐴 ⦋ 𝑧 / 𝑘 ⦌ 𝐶 d 𝑥 )
189 95 185 188 sylancr ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → Σ 𝑚 ∈ { 𝑧 } ∫ 𝐴 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 = ∫ 𝐴 ⦋ 𝑧 / 𝑘 ⦌ 𝐶 d 𝑥 )
190 189 eqcomd ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → ∫ 𝐴 ⦋ 𝑧 / 𝑘 ⦌ 𝐶 d 𝑥 = Σ 𝑚 ∈ { 𝑧 } ∫ 𝐴 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 )
191 183 190 oveq12d ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → ( ∫ 𝐴 Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 + ∫ 𝐴 ⦋ 𝑧 / 𝑘 ⦌ 𝐶 d 𝑥 ) = ( Σ 𝑚 ∈ 𝑤 ∫ 𝐴 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 + Σ 𝑚 ∈ { 𝑧 } ∫ 𝐴 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 ) )
192 173 191 eqtr4d ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → Σ 𝑚 ∈ ( 𝑤 ∪ { 𝑧 } ) ∫ 𝐴 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 = ( ∫ 𝐴 Σ 𝑚 ∈ 𝑤 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 + ∫ 𝐴 ⦋ 𝑧 / 𝑘 ⦌ 𝐶 d 𝑥 ) )
193 163 165 192 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → ∫ 𝐴 Σ 𝑚 ∈ ( 𝑤 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 = Σ 𝑚 ∈ ( 𝑤 ∪ { 𝑧 } ) ∫ 𝐴 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 )
194 itgeq2 ⊢ ( ∀ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 = Σ 𝑚 ∈ ( 𝑤 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐶 → ∫ 𝐴 Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 d 𝑥 = ∫ 𝐴 Σ 𝑚 ∈ ( 𝑤 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥 )
195 68 a1i ⊢ ( 𝑥 ∈ 𝐴 → Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 = Σ 𝑚 ∈ ( 𝑤 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐶 )
196 194 195 mprg ⊢ ∫ 𝐴 Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 d 𝑥 = ∫ 𝐴 Σ 𝑚 ∈ ( 𝑤 ∪ { 𝑧 } ) ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥
197 179 180 181 cbvsum ⊢ Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) ∫ 𝐴 𝐶 d 𝑥 = Σ 𝑚 ∈ ( 𝑤 ∪ { 𝑧 } ) ∫ 𝐴 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 d 𝑥
198 193 196 197 3eqtr4g ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → ∫ 𝐴 Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) ∫ 𝐴 𝐶 d 𝑥 )
199 157 198 jca ⊢ ( ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) ∫ 𝐴 𝐶 d 𝑥 ) )
200 199 ex ⊢ ( ( 𝜑 ∧ ( ¬ 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 ) ) → ( ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) ∫ 𝐴 𝐶 d 𝑥 ) ) )
201 200 expr ⊢ ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑤 ) → ( ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 → ( ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) ∫ 𝐴 𝐶 d 𝑥 ) ) ) )
202 201 a2d ⊢ ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑤 ) → ( ( ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → ( ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) ∫ 𝐴 𝐶 d 𝑥 ) ) ) )
203 64 202 syl5 ⊢ ( ( 𝜑 ∧ ¬ 𝑧 ∈ 𝑤 ) → ( ( 𝑤 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → ( ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) ∫ 𝐴 𝐶 d 𝑥 ) ) ) )
204 203 expcom ⊢ ( ¬ 𝑧 ∈ 𝑤 → ( 𝜑 → ( ( 𝑤 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → ( ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) ∫ 𝐴 𝐶 d 𝑥 ) ) ) ) )
205 204 adantl ⊢ ( ( 𝑤 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑤 ) → ( 𝜑 → ( ( 𝑤 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) → ( ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) ∫ 𝐴 𝐶 d 𝑥 ) ) ) ) )
206 205 a2d ⊢ ( ( 𝑤 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑤 ) → ( ( 𝜑 → ( 𝑤 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝑤 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝑤 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝑤 ∫ 𝐴 𝐶 d 𝑥 ) ) ) → ( 𝜑 → ( ( 𝑤 ∪ { 𝑧 } ) ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 𝑤 ∪ { 𝑧 } ) ∫ 𝐴 𝐶 d 𝑥 ) ) ) ) )
207 24 35 46 57 60 206 findcard2s ⊢ ( 𝐵 ∈ Fin → ( 𝜑 → ( 𝐵 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝐵 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝐵 ∫ 𝐴 𝐶 d 𝑥 ) ) ) )
208 2 207 mpcom ⊢ ( 𝜑 → ( 𝐵 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝐵 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝐵 ∫ 𝐴 𝐶 d 𝑥 ) ) )
209 5 208 mpi ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ Σ 𝑘 ∈ 𝐵 𝐶 ) ∈ 𝐿1 ∧ ∫ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 d 𝑥 = Σ 𝑘 ∈ 𝐵 ∫ 𝐴 𝐶 d 𝑥 ) )