Step |
Hyp |
Ref |
Expression |
1 |
|
i1fadd.1 |
⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 ) |
2 |
|
i1fadd.2 |
⊢ ( 𝜑 → 𝐺 ∈ dom ∫1 ) |
3 |
|
itg1add.3 |
⊢ 𝐼 = ( 𝑖 ∈ ℝ , 𝑗 ∈ ℝ ↦ if ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ) ) |
4 |
|
itg1add.4 |
⊢ 𝑃 = ( + ↾ ( ran 𝐹 × ran 𝐺 ) ) |
5 |
|
i1frn |
⊢ ( 𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin ) |
6 |
1 5
|
syl |
⊢ ( 𝜑 → ran 𝐹 ∈ Fin ) |
7 |
|
i1frn |
⊢ ( 𝐺 ∈ dom ∫1 → ran 𝐺 ∈ Fin ) |
8 |
2 7
|
syl |
⊢ ( 𝜑 → ran 𝐺 ∈ Fin ) |
9 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) → ran 𝐺 ∈ Fin ) |
10 |
|
i1ff |
⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ ) |
11 |
1 10
|
syl |
⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ ) |
12 |
11
|
frnd |
⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ ) |
13 |
12
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ∈ ℝ ) |
14 |
13
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑦 ∈ ℝ ) |
15 |
14
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑦 ∈ ℂ ) |
16 |
1 2 3
|
itg1addlem2 |
⊢ ( 𝜑 → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ ) |
17 |
16
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ ) |
18 |
|
i1ff |
⊢ ( 𝐺 ∈ dom ∫1 → 𝐺 : ℝ ⟶ ℝ ) |
19 |
2 18
|
syl |
⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ℝ ) |
20 |
19
|
frnd |
⊢ ( 𝜑 → ran 𝐺 ⊆ ℝ ) |
21 |
20
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → 𝑧 ∈ ℝ ) |
22 |
21
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑧 ∈ ℝ ) |
23 |
17 14 22
|
fovrnd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℝ ) |
24 |
23
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℂ ) |
25 |
15 24
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ ) |
26 |
9 25
|
fsumcl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) → Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ ) |
27 |
22
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑧 ∈ ℂ ) |
28 |
27 24
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ ) |
29 |
9 28
|
fsumcl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) → Σ 𝑧 ∈ ran 𝐺 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ ) |
30 |
6 26 29
|
fsumadd |
⊢ ( 𝜑 → Σ 𝑦 ∈ ran 𝐹 ( Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) + Σ 𝑧 ∈ ran 𝐺 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) = ( Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) + Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) ) |
31 |
1 2 3 4
|
itg1addlem4 |
⊢ ( 𝜑 → ( ∫1 ‘ ( 𝐹 ∘f + 𝐺 ) ) = Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) ) |
32 |
15 27 24
|
adddird |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = ( ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) + ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) ) |
33 |
32
|
sumeq2dv |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) → Σ 𝑧 ∈ ran 𝐺 ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑧 ∈ ran 𝐺 ( ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) + ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) ) |
34 |
9 25 28
|
fsumadd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) → Σ 𝑧 ∈ ran 𝐺 ( ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) + ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) = ( Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) + Σ 𝑧 ∈ ran 𝐺 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) ) |
35 |
33 34
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) → Σ 𝑧 ∈ ran 𝐺 ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = ( Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) + Σ 𝑧 ∈ ran 𝐺 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) ) |
36 |
35
|
sumeq2dv |
⊢ ( 𝜑 → Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑦 ∈ ran 𝐹 ( Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) + Σ 𝑧 ∈ ran 𝐺 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) ) |
37 |
31 36
|
eqtrd |
⊢ ( 𝜑 → ( ∫1 ‘ ( 𝐹 ∘f + 𝐺 ) ) = Σ 𝑦 ∈ ran 𝐹 ( Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) + Σ 𝑧 ∈ ran 𝐺 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) ) |
38 |
|
itg1val |
⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ 𝐹 ) = Σ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑦 · ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ) |
39 |
1 38
|
syl |
⊢ ( 𝜑 → ( ∫1 ‘ 𝐹 ) = Σ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑦 · ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ) |
40 |
19
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝐺 : ℝ ⟶ ℝ ) |
41 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ran 𝐺 ∈ Fin ) |
42 |
|
inss2 |
⊢ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ( ◡ 𝐺 “ { 𝑧 } ) |
43 |
42
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ( ◡ 𝐺 “ { 𝑧 } ) ) |
44 |
|
i1fima |
⊢ ( 𝐹 ∈ dom ∫1 → ( ◡ 𝐹 “ { 𝑦 } ) ∈ dom vol ) |
45 |
1 44
|
syl |
⊢ ( 𝜑 → ( ◡ 𝐹 “ { 𝑦 } ) ∈ dom vol ) |
46 |
45
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ◡ 𝐹 “ { 𝑦 } ) ∈ dom vol ) |
47 |
|
i1fima |
⊢ ( 𝐺 ∈ dom ∫1 → ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol ) |
48 |
2 47
|
syl |
⊢ ( 𝜑 → ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol ) |
49 |
48
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol ) |
50 |
|
inmbl |
⊢ ( ( ( ◡ 𝐹 “ { 𝑦 } ) ∈ dom vol ∧ ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol ) → ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol ) |
51 |
46 49 50
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol ) |
52 |
12
|
ssdifssd |
⊢ ( 𝜑 → ( ran 𝐹 ∖ { 0 } ) ⊆ ℝ ) |
53 |
52
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝑦 ∈ ℝ ) |
54 |
53
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑦 ∈ ℝ ) |
55 |
20
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ran 𝐺 ⊆ ℝ ) |
56 |
55
|
sselda |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑧 ∈ ℝ ) |
57 |
|
eldifsni |
⊢ ( 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) → 𝑦 ≠ 0 ) |
58 |
57
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑦 ≠ 0 ) |
59 |
|
simpl |
⊢ ( ( 𝑦 = 0 ∧ 𝑧 = 0 ) → 𝑦 = 0 ) |
60 |
59
|
necon3ai |
⊢ ( 𝑦 ≠ 0 → ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) |
61 |
58 60
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) |
62 |
1 2 3
|
itg1addlem3 |
⊢ ( ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) → ( 𝑦 𝐼 𝑧 ) = ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ) |
63 |
54 56 61 62
|
syl21anc |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑦 𝐼 𝑧 ) = ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ) |
64 |
16
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ ) |
65 |
64 54 56
|
fovrnd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℝ ) |
66 |
63 65
|
eqeltrrd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ ) |
67 |
40 41 43 51 66
|
itg1addlem1 |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ∪ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) = Σ 𝑧 ∈ ran 𝐺 ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ) |
68 |
|
iunin2 |
⊢ ∪ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) = ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ∪ 𝑧 ∈ ran 𝐺 ( ◡ 𝐺 “ { 𝑧 } ) ) |
69 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝐹 ∈ dom ∫1 ) |
70 |
69 44
|
syl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ◡ 𝐹 “ { 𝑦 } ) ∈ dom vol ) |
71 |
|
mblss |
⊢ ( ( ◡ 𝐹 “ { 𝑦 } ) ∈ dom vol → ( ◡ 𝐹 “ { 𝑦 } ) ⊆ ℝ ) |
72 |
70 71
|
syl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ◡ 𝐹 “ { 𝑦 } ) ⊆ ℝ ) |
73 |
|
iunid |
⊢ ∪ 𝑧 ∈ ran 𝐺 { 𝑧 } = ran 𝐺 |
74 |
73
|
imaeq2i |
⊢ ( ◡ 𝐺 “ ∪ 𝑧 ∈ ran 𝐺 { 𝑧 } ) = ( ◡ 𝐺 “ ran 𝐺 ) |
75 |
|
imaiun |
⊢ ( ◡ 𝐺 “ ∪ 𝑧 ∈ ran 𝐺 { 𝑧 } ) = ∪ 𝑧 ∈ ran 𝐺 ( ◡ 𝐺 “ { 𝑧 } ) |
76 |
|
cnvimarndm |
⊢ ( ◡ 𝐺 “ ran 𝐺 ) = dom 𝐺 |
77 |
74 75 76
|
3eqtr3i |
⊢ ∪ 𝑧 ∈ ran 𝐺 ( ◡ 𝐺 “ { 𝑧 } ) = dom 𝐺 |
78 |
40
|
fdmd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → dom 𝐺 = ℝ ) |
79 |
77 78
|
syl5eq |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ∪ 𝑧 ∈ ran 𝐺 ( ◡ 𝐺 “ { 𝑧 } ) = ℝ ) |
80 |
72 79
|
sseqtrrd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ◡ 𝐹 “ { 𝑦 } ) ⊆ ∪ 𝑧 ∈ ran 𝐺 ( ◡ 𝐺 “ { 𝑧 } ) ) |
81 |
|
df-ss |
⊢ ( ( ◡ 𝐹 “ { 𝑦 } ) ⊆ ∪ 𝑧 ∈ ran 𝐺 ( ◡ 𝐺 “ { 𝑧 } ) ↔ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ∪ 𝑧 ∈ ran 𝐺 ( ◡ 𝐺 “ { 𝑧 } ) ) = ( ◡ 𝐹 “ { 𝑦 } ) ) |
82 |
80 81
|
sylib |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ∪ 𝑧 ∈ ran 𝐺 ( ◡ 𝐺 “ { 𝑧 } ) ) = ( ◡ 𝐹 “ { 𝑦 } ) ) |
83 |
68 82
|
eqtr2id |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ◡ 𝐹 “ { 𝑦 } ) = ∪ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) |
84 |
83
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) = ( vol ‘ ∪ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ) |
85 |
63
|
sumeq2dv |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → Σ 𝑧 ∈ ran 𝐺 ( 𝑦 𝐼 𝑧 ) = Σ 𝑧 ∈ ran 𝐺 ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ) |
86 |
67 84 85
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) = Σ 𝑧 ∈ ran 𝐺 ( 𝑦 𝐼 𝑧 ) ) |
87 |
86
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑦 · ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) ) = ( 𝑦 · Σ 𝑧 ∈ ran 𝐺 ( 𝑦 𝐼 𝑧 ) ) ) |
88 |
53
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝑦 ∈ ℂ ) |
89 |
65
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℂ ) |
90 |
41 88 89
|
fsummulc2 |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑦 · Σ 𝑧 ∈ ran 𝐺 ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) ) |
91 |
87 90
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑦 · ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) ) = Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) ) |
92 |
91
|
sumeq2dv |
⊢ ( 𝜑 → Σ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ( 𝑦 · ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) ) = Σ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) ) |
93 |
|
difssd |
⊢ ( 𝜑 → ( ran 𝐹 ∖ { 0 } ) ⊆ ran 𝐹 ) |
94 |
54
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑦 ∈ ℂ ) |
95 |
94 89
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ ) |
96 |
41 95
|
fsumcl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ ) |
97 |
|
dfin4 |
⊢ ( ran 𝐹 ∩ { 0 } ) = ( ran 𝐹 ∖ ( ran 𝐹 ∖ { 0 } ) ) |
98 |
|
inss2 |
⊢ ( ran 𝐹 ∩ { 0 } ) ⊆ { 0 } |
99 |
97 98
|
eqsstrri |
⊢ ( ran 𝐹 ∖ ( ran 𝐹 ∖ { 0 } ) ) ⊆ { 0 } |
100 |
99
|
sseli |
⊢ ( 𝑦 ∈ ( ran 𝐹 ∖ ( ran 𝐹 ∖ { 0 } ) ) → 𝑦 ∈ { 0 } ) |
101 |
|
elsni |
⊢ ( 𝑦 ∈ { 0 } → 𝑦 = 0 ) |
102 |
101
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑦 = 0 ) |
103 |
102
|
oveq1d |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) = ( 0 · ( 𝑦 𝐼 𝑧 ) ) ) |
104 |
16
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ ) |
105 |
|
0re |
⊢ 0 ∈ ℝ |
106 |
102 105
|
eqeltrdi |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑦 ∈ ℝ ) |
107 |
21
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑧 ∈ ℝ ) |
108 |
104 106 107
|
fovrnd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℝ ) |
109 |
108
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℂ ) |
110 |
109
|
mul02d |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 0 · ( 𝑦 𝐼 𝑧 ) ) = 0 ) |
111 |
103 110
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) = 0 ) |
112 |
111
|
sumeq2dv |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) → Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑧 ∈ ran 𝐺 0 ) |
113 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) → ran 𝐺 ∈ Fin ) |
114 |
113
|
olcd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) → ( ran 𝐺 ⊆ ( ℤ≥ ‘ 0 ) ∨ ran 𝐺 ∈ Fin ) ) |
115 |
|
sumz |
⊢ ( ( ran 𝐺 ⊆ ( ℤ≥ ‘ 0 ) ∨ ran 𝐺 ∈ Fin ) → Σ 𝑧 ∈ ran 𝐺 0 = 0 ) |
116 |
114 115
|
syl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) → Σ 𝑧 ∈ ran 𝐺 0 = 0 ) |
117 |
112 116
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 0 } ) → Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) = 0 ) |
118 |
100 117
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ran 𝐹 ∖ ( ran 𝐹 ∖ { 0 } ) ) ) → Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) = 0 ) |
119 |
93 96 118 6
|
fsumss |
⊢ ( 𝜑 → Σ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) ) |
120 |
39 92 119
|
3eqtrd |
⊢ ( 𝜑 → ( ∫1 ‘ 𝐹 ) = Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) ) |
121 |
|
itg1val |
⊢ ( 𝐺 ∈ dom ∫1 → ( ∫1 ‘ 𝐺 ) = Σ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ( 𝑧 · ( vol ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ) |
122 |
2 121
|
syl |
⊢ ( 𝜑 → ( ∫1 ‘ 𝐺 ) = Σ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ( 𝑧 · ( vol ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ) |
123 |
11
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → 𝐹 : ℝ ⟶ ℝ ) |
124 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ran 𝐹 ∈ Fin ) |
125 |
|
inss1 |
⊢ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ( ◡ 𝐹 “ { 𝑦 } ) |
126 |
125
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ( ◡ 𝐹 “ { 𝑦 } ) ) |
127 |
45
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ( ◡ 𝐹 “ { 𝑦 } ) ∈ dom vol ) |
128 |
48
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol ) |
129 |
127 128 50
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol ) |
130 |
12
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ran 𝐹 ⊆ ℝ ) |
131 |
130
|
sselda |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ∈ ℝ ) |
132 |
20
|
ssdifssd |
⊢ ( 𝜑 → ( ran 𝐺 ∖ { 0 } ) ⊆ ℝ ) |
133 |
132
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → 𝑧 ∈ ℝ ) |
134 |
133
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑧 ∈ ℝ ) |
135 |
|
eldifsni |
⊢ ( 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) → 𝑧 ≠ 0 ) |
136 |
135
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑧 ≠ 0 ) |
137 |
|
simpr |
⊢ ( ( 𝑦 = 0 ∧ 𝑧 = 0 ) → 𝑧 = 0 ) |
138 |
137
|
necon3ai |
⊢ ( 𝑧 ≠ 0 → ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) |
139 |
136 138
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) |
140 |
131 134 139 62
|
syl21anc |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑦 𝐼 𝑧 ) = ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ) |
141 |
16
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ ) |
142 |
141 131 134
|
fovrnd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℝ ) |
143 |
140 142
|
eqeltrrd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ ) |
144 |
123 124 126 129 143
|
itg1addlem1 |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ∪ 𝑦 ∈ ran 𝐹 ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) = Σ 𝑦 ∈ ran 𝐹 ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ) |
145 |
|
incom |
⊢ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) = ( ( ◡ 𝐺 “ { 𝑧 } ) ∩ ( ◡ 𝐹 “ { 𝑦 } ) ) |
146 |
145
|
a1i |
⊢ ( 𝑦 ∈ ran 𝐹 → ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) = ( ( ◡ 𝐺 “ { 𝑧 } ) ∩ ( ◡ 𝐹 “ { 𝑦 } ) ) ) |
147 |
146
|
iuneq2i |
⊢ ∪ 𝑦 ∈ ran 𝐹 ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) = ∪ 𝑦 ∈ ran 𝐹 ( ( ◡ 𝐺 “ { 𝑧 } ) ∩ ( ◡ 𝐹 “ { 𝑦 } ) ) |
148 |
|
iunin2 |
⊢ ∪ 𝑦 ∈ ran 𝐹 ( ( ◡ 𝐺 “ { 𝑧 } ) ∩ ( ◡ 𝐹 “ { 𝑦 } ) ) = ( ( ◡ 𝐺 “ { 𝑧 } ) ∩ ∪ 𝑦 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑦 } ) ) |
149 |
147 148
|
eqtri |
⊢ ∪ 𝑦 ∈ ran 𝐹 ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) = ( ( ◡ 𝐺 “ { 𝑧 } ) ∩ ∪ 𝑦 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑦 } ) ) |
150 |
|
cnvimass |
⊢ ( ◡ 𝐺 “ { 𝑧 } ) ⊆ dom 𝐺 |
151 |
19
|
fdmd |
⊢ ( 𝜑 → dom 𝐺 = ℝ ) |
152 |
151
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → dom 𝐺 = ℝ ) |
153 |
150 152
|
sseqtrid |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ◡ 𝐺 “ { 𝑧 } ) ⊆ ℝ ) |
154 |
|
iunid |
⊢ ∪ 𝑦 ∈ ran 𝐹 { 𝑦 } = ran 𝐹 |
155 |
154
|
imaeq2i |
⊢ ( ◡ 𝐹 “ ∪ 𝑦 ∈ ran 𝐹 { 𝑦 } ) = ( ◡ 𝐹 “ ran 𝐹 ) |
156 |
|
imaiun |
⊢ ( ◡ 𝐹 “ ∪ 𝑦 ∈ ran 𝐹 { 𝑦 } ) = ∪ 𝑦 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑦 } ) |
157 |
|
cnvimarndm |
⊢ ( ◡ 𝐹 “ ran 𝐹 ) = dom 𝐹 |
158 |
155 156 157
|
3eqtr3i |
⊢ ∪ 𝑦 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑦 } ) = dom 𝐹 |
159 |
11
|
fdmd |
⊢ ( 𝜑 → dom 𝐹 = ℝ ) |
160 |
159
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → dom 𝐹 = ℝ ) |
161 |
158 160
|
syl5eq |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ∪ 𝑦 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑦 } ) = ℝ ) |
162 |
153 161
|
sseqtrrd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ◡ 𝐺 “ { 𝑧 } ) ⊆ ∪ 𝑦 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑦 } ) ) |
163 |
|
df-ss |
⊢ ( ( ◡ 𝐺 “ { 𝑧 } ) ⊆ ∪ 𝑦 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑦 } ) ↔ ( ( ◡ 𝐺 “ { 𝑧 } ) ∩ ∪ 𝑦 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑦 } ) ) = ( ◡ 𝐺 “ { 𝑧 } ) ) |
164 |
162 163
|
sylib |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ( ◡ 𝐺 “ { 𝑧 } ) ∩ ∪ 𝑦 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑦 } ) ) = ( ◡ 𝐺 “ { 𝑧 } ) ) |
165 |
149 164
|
eqtr2id |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ◡ 𝐺 “ { 𝑧 } ) = ∪ 𝑦 ∈ ran 𝐹 ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) |
166 |
165
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) = ( vol ‘ ∪ 𝑦 ∈ ran 𝐹 ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ) |
167 |
140
|
sumeq2dv |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → Σ 𝑦 ∈ ran 𝐹 ( 𝑦 𝐼 𝑧 ) = Σ 𝑦 ∈ ran 𝐹 ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ) |
168 |
144 166 167
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) = Σ 𝑦 ∈ ran 𝐹 ( 𝑦 𝐼 𝑧 ) ) |
169 |
168
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( 𝑧 · ( vol ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) ) = ( 𝑧 · Σ 𝑦 ∈ ran 𝐹 ( 𝑦 𝐼 𝑧 ) ) ) |
170 |
133
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → 𝑧 ∈ ℂ ) |
171 |
142
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℂ ) |
172 |
124 170 171
|
fsummulc2 |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( 𝑧 · Σ 𝑦 ∈ ran 𝐹 ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑦 ∈ ran 𝐹 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) |
173 |
169 172
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( 𝑧 · ( vol ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) ) = Σ 𝑦 ∈ ran 𝐹 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) |
174 |
173
|
sumeq2dv |
⊢ ( 𝜑 → Σ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ( 𝑧 · ( vol ‘ ( ◡ 𝐺 “ { 𝑧 } ) ) ) = Σ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) Σ 𝑦 ∈ ran 𝐹 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) |
175 |
|
difssd |
⊢ ( 𝜑 → ( ran 𝐺 ∖ { 0 } ) ⊆ ran 𝐺 ) |
176 |
170
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑧 ∈ ℂ ) |
177 |
176 171
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ ) |
178 |
124 177
|
fsumcl |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) ) → Σ 𝑦 ∈ ran 𝐹 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ ) |
179 |
|
dfin4 |
⊢ ( ran 𝐺 ∩ { 0 } ) = ( ran 𝐺 ∖ ( ran 𝐺 ∖ { 0 } ) ) |
180 |
|
inss2 |
⊢ ( ran 𝐺 ∩ { 0 } ) ⊆ { 0 } |
181 |
179 180
|
eqsstrri |
⊢ ( ran 𝐺 ∖ ( ran 𝐺 ∖ { 0 } ) ) ⊆ { 0 } |
182 |
181
|
sseli |
⊢ ( 𝑧 ∈ ( ran 𝐺 ∖ ( ran 𝐺 ∖ { 0 } ) ) → 𝑧 ∈ { 0 } ) |
183 |
|
elsni |
⊢ ( 𝑧 ∈ { 0 } → 𝑧 = 0 ) |
184 |
183
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑧 = 0 ) |
185 |
184
|
oveq1d |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) = ( 0 · ( 𝑦 𝐼 𝑧 ) ) ) |
186 |
16
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ ) |
187 |
13
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ∈ ℝ ) |
188 |
184 105
|
eqeltrdi |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑧 ∈ ℝ ) |
189 |
186 187 188
|
fovrnd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℝ ) |
190 |
189
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℂ ) |
191 |
190
|
mul02d |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 0 · ( 𝑦 𝐼 𝑧 ) ) = 0 ) |
192 |
185 191
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) = 0 ) |
193 |
192
|
sumeq2dv |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) → Σ 𝑦 ∈ ran 𝐹 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑦 ∈ ran 𝐹 0 ) |
194 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) → ran 𝐹 ∈ Fin ) |
195 |
194
|
olcd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) → ( ran 𝐹 ⊆ ( ℤ≥ ‘ 0 ) ∨ ran 𝐹 ∈ Fin ) ) |
196 |
|
sumz |
⊢ ( ( ran 𝐹 ⊆ ( ℤ≥ ‘ 0 ) ∨ ran 𝐹 ∈ Fin ) → Σ 𝑦 ∈ ran 𝐹 0 = 0 ) |
197 |
195 196
|
syl |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) → Σ 𝑦 ∈ ran 𝐹 0 = 0 ) |
198 |
193 197
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ { 0 } ) → Σ 𝑦 ∈ ran 𝐹 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) = 0 ) |
199 |
182 198
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran 𝐺 ∖ ( ran 𝐺 ∖ { 0 } ) ) ) → Σ 𝑦 ∈ ran 𝐹 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) = 0 ) |
200 |
175 178 199 8
|
fsumss |
⊢ ( 𝜑 → Σ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) Σ 𝑦 ∈ ran 𝐹 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑧 ∈ ran 𝐺 Σ 𝑦 ∈ ran 𝐹 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) |
201 |
21
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑧 ∈ ℝ ) |
202 |
201
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑧 ∈ ℂ ) |
203 |
16
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ ) |
204 |
12
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ran 𝐹 ⊆ ℝ ) |
205 |
204
|
sselda |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ∈ ℝ ) |
206 |
203 205 201
|
fovrnd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℝ ) |
207 |
206
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℂ ) |
208 |
202 207
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ ) |
209 |
208
|
anasss |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐹 ) ) → ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ ) |
210 |
8 6 209
|
fsumcom |
⊢ ( 𝜑 → Σ 𝑧 ∈ ran 𝐺 Σ 𝑦 ∈ ran 𝐹 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) |
211 |
200 210
|
eqtrd |
⊢ ( 𝜑 → Σ 𝑧 ∈ ( ran 𝐺 ∖ { 0 } ) Σ 𝑦 ∈ ran 𝐹 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) |
212 |
122 174 211
|
3eqtrd |
⊢ ( 𝜑 → ( ∫1 ‘ 𝐺 ) = Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) |
213 |
120 212
|
oveq12d |
⊢ ( 𝜑 → ( ( ∫1 ‘ 𝐹 ) + ( ∫1 ‘ 𝐺 ) ) = ( Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( 𝑦 · ( 𝑦 𝐼 𝑧 ) ) + Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( 𝑧 · ( 𝑦 𝐼 𝑧 ) ) ) ) |
214 |
30 37 213
|
3eqtr4d |
⊢ ( 𝜑 → ( ∫1 ‘ ( 𝐹 ∘f + 𝐺 ) ) = ( ( ∫1 ‘ 𝐹 ) + ( ∫1 ‘ 𝐺 ) ) ) |