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 |
1 2
|
i1fadd |
⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) ∈ dom ∫1 ) |
6 |
|
ax-addf |
⊢ + : ( ℂ × ℂ ) ⟶ ℂ |
7 |
|
ffn |
⊢ ( + : ( ℂ × ℂ ) ⟶ ℂ → + Fn ( ℂ × ℂ ) ) |
8 |
6 7
|
ax-mp |
⊢ + Fn ( ℂ × ℂ ) |
9 |
|
i1frn |
⊢ ( 𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin ) |
10 |
1 9
|
syl |
⊢ ( 𝜑 → ran 𝐹 ∈ Fin ) |
11 |
|
i1frn |
⊢ ( 𝐺 ∈ dom ∫1 → ran 𝐺 ∈ Fin ) |
12 |
2 11
|
syl |
⊢ ( 𝜑 → ran 𝐺 ∈ Fin ) |
13 |
|
xpfi |
⊢ ( ( ran 𝐹 ∈ Fin ∧ ran 𝐺 ∈ Fin ) → ( ran 𝐹 × ran 𝐺 ) ∈ Fin ) |
14 |
10 12 13
|
syl2anc |
⊢ ( 𝜑 → ( ran 𝐹 × ran 𝐺 ) ∈ Fin ) |
15 |
|
resfnfinfin |
⊢ ( ( + Fn ( ℂ × ℂ ) ∧ ( ran 𝐹 × ran 𝐺 ) ∈ Fin ) → ( + ↾ ( ran 𝐹 × ran 𝐺 ) ) ∈ Fin ) |
16 |
8 14 15
|
sylancr |
⊢ ( 𝜑 → ( + ↾ ( ran 𝐹 × ran 𝐺 ) ) ∈ Fin ) |
17 |
4 16
|
eqeltrid |
⊢ ( 𝜑 → 𝑃 ∈ Fin ) |
18 |
|
rnfi |
⊢ ( 𝑃 ∈ Fin → ran 𝑃 ∈ Fin ) |
19 |
17 18
|
syl |
⊢ ( 𝜑 → ran 𝑃 ∈ Fin ) |
20 |
|
difss |
⊢ ( ran 𝑃 ∖ { 0 } ) ⊆ ran 𝑃 |
21 |
|
ssfi |
⊢ ( ( ran 𝑃 ∈ Fin ∧ ( ran 𝑃 ∖ { 0 } ) ⊆ ran 𝑃 ) → ( ran 𝑃 ∖ { 0 } ) ∈ Fin ) |
22 |
19 20 21
|
sylancl |
⊢ ( 𝜑 → ( ran 𝑃 ∖ { 0 } ) ∈ Fin ) |
23 |
|
ffun |
⊢ ( + : ( ℂ × ℂ ) ⟶ ℂ → Fun + ) |
24 |
6 23
|
ax-mp |
⊢ Fun + |
25 |
|
i1ff |
⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ ) |
26 |
1 25
|
syl |
⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ ) |
27 |
26
|
frnd |
⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ ) |
28 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
29 |
27 28
|
sstrdi |
⊢ ( 𝜑 → ran 𝐹 ⊆ ℂ ) |
30 |
|
i1ff |
⊢ ( 𝐺 ∈ dom ∫1 → 𝐺 : ℝ ⟶ ℝ ) |
31 |
2 30
|
syl |
⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ℝ ) |
32 |
31
|
frnd |
⊢ ( 𝜑 → ran 𝐺 ⊆ ℝ ) |
33 |
32 28
|
sstrdi |
⊢ ( 𝜑 → ran 𝐺 ⊆ ℂ ) |
34 |
|
xpss12 |
⊢ ( ( ran 𝐹 ⊆ ℂ ∧ ran 𝐺 ⊆ ℂ ) → ( ran 𝐹 × ran 𝐺 ) ⊆ ( ℂ × ℂ ) ) |
35 |
29 33 34
|
syl2anc |
⊢ ( 𝜑 → ( ran 𝐹 × ran 𝐺 ) ⊆ ( ℂ × ℂ ) ) |
36 |
6
|
fdmi |
⊢ dom + = ( ℂ × ℂ ) |
37 |
35 36
|
sseqtrrdi |
⊢ ( 𝜑 → ( ran 𝐹 × ran 𝐺 ) ⊆ dom + ) |
38 |
|
funfvima2 |
⊢ ( ( Fun + ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ dom + ) → ( 〈 𝑥 , 𝑦 〉 ∈ ( ran 𝐹 × ran 𝐺 ) → ( + ‘ 〈 𝑥 , 𝑦 〉 ) ∈ ( + “ ( ran 𝐹 × ran 𝐺 ) ) ) ) |
39 |
24 37 38
|
sylancr |
⊢ ( 𝜑 → ( 〈 𝑥 , 𝑦 〉 ∈ ( ran 𝐹 × ran 𝐺 ) → ( + ‘ 〈 𝑥 , 𝑦 〉 ) ∈ ( + “ ( ran 𝐹 × ran 𝐺 ) ) ) ) |
40 |
|
opelxpi |
⊢ ( ( 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺 ) → 〈 𝑥 , 𝑦 〉 ∈ ( ran 𝐹 × ran 𝐺 ) ) |
41 |
39 40
|
impel |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺 ) ) → ( + ‘ 〈 𝑥 , 𝑦 〉 ) ∈ ( + “ ( ran 𝐹 × ran 𝐺 ) ) ) |
42 |
|
df-ov |
⊢ ( 𝑥 + 𝑦 ) = ( + ‘ 〈 𝑥 , 𝑦 〉 ) |
43 |
4
|
rneqi |
⊢ ran 𝑃 = ran ( + ↾ ( ran 𝐹 × ran 𝐺 ) ) |
44 |
|
df-ima |
⊢ ( + “ ( ran 𝐹 × ran 𝐺 ) ) = ran ( + ↾ ( ran 𝐹 × ran 𝐺 ) ) |
45 |
43 44
|
eqtr4i |
⊢ ran 𝑃 = ( + “ ( ran 𝐹 × ran 𝐺 ) ) |
46 |
41 42 45
|
3eltr4g |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐺 ) ) → ( 𝑥 + 𝑦 ) ∈ ran 𝑃 ) |
47 |
26
|
ffnd |
⊢ ( 𝜑 → 𝐹 Fn ℝ ) |
48 |
|
dffn3 |
⊢ ( 𝐹 Fn ℝ ↔ 𝐹 : ℝ ⟶ ran 𝐹 ) |
49 |
47 48
|
sylib |
⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ran 𝐹 ) |
50 |
31
|
ffnd |
⊢ ( 𝜑 → 𝐺 Fn ℝ ) |
51 |
|
dffn3 |
⊢ ( 𝐺 Fn ℝ ↔ 𝐺 : ℝ ⟶ ran 𝐺 ) |
52 |
50 51
|
sylib |
⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ran 𝐺 ) |
53 |
|
reex |
⊢ ℝ ∈ V |
54 |
53
|
a1i |
⊢ ( 𝜑 → ℝ ∈ V ) |
55 |
|
inidm |
⊢ ( ℝ ∩ ℝ ) = ℝ |
56 |
46 49 52 54 54 55
|
off |
⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) : ℝ ⟶ ran 𝑃 ) |
57 |
56
|
frnd |
⊢ ( 𝜑 → ran ( 𝐹 ∘f + 𝐺 ) ⊆ ran 𝑃 ) |
58 |
57
|
ssdifd |
⊢ ( 𝜑 → ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ⊆ ( ran 𝑃 ∖ { 0 } ) ) |
59 |
27
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ∈ ℝ ) |
60 |
32
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → 𝑧 ∈ ℝ ) |
61 |
59 60
|
anim12dan |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺 ) ) → ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) |
62 |
|
readdcl |
⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝑦 + 𝑧 ) ∈ ℝ ) |
63 |
61 62
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐺 ) ) → ( 𝑦 + 𝑧 ) ∈ ℝ ) |
64 |
63
|
ralrimivva |
⊢ ( 𝜑 → ∀ 𝑦 ∈ ran 𝐹 ∀ 𝑧 ∈ ran 𝐺 ( 𝑦 + 𝑧 ) ∈ ℝ ) |
65 |
|
funimassov |
⊢ ( ( Fun + ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ dom + ) → ( ( + “ ( ran 𝐹 × ran 𝐺 ) ) ⊆ ℝ ↔ ∀ 𝑦 ∈ ran 𝐹 ∀ 𝑧 ∈ ran 𝐺 ( 𝑦 + 𝑧 ) ∈ ℝ ) ) |
66 |
24 37 65
|
sylancr |
⊢ ( 𝜑 → ( ( + “ ( ran 𝐹 × ran 𝐺 ) ) ⊆ ℝ ↔ ∀ 𝑦 ∈ ran 𝐹 ∀ 𝑧 ∈ ran 𝐺 ( 𝑦 + 𝑧 ) ∈ ℝ ) ) |
67 |
64 66
|
mpbird |
⊢ ( 𝜑 → ( + “ ( ran 𝐹 × ran 𝐺 ) ) ⊆ ℝ ) |
68 |
45 67
|
eqsstrid |
⊢ ( 𝜑 → ran 𝑃 ⊆ ℝ ) |
69 |
68
|
ssdifd |
⊢ ( 𝜑 → ( ran 𝑃 ∖ { 0 } ) ⊆ ( ℝ ∖ { 0 } ) ) |
70 |
|
itg1val2 |
⊢ ( ( ( 𝐹 ∘f + 𝐺 ) ∈ dom ∫1 ∧ ( ( ran 𝑃 ∖ { 0 } ) ∈ Fin ∧ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { 0 } ) ⊆ ( ran 𝑃 ∖ { 0 } ) ∧ ( ran 𝑃 ∖ { 0 } ) ⊆ ( ℝ ∖ { 0 } ) ) ) → ( ∫1 ‘ ( 𝐹 ∘f + 𝐺 ) ) = Σ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ( 𝑤 · ( vol ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑤 } ) ) ) ) |
71 |
5 22 58 69 70
|
syl13anc |
⊢ ( 𝜑 → ( ∫1 ‘ ( 𝐹 ∘f + 𝐺 ) ) = Σ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ( 𝑤 · ( vol ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑤 } ) ) ) ) |
72 |
31
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → 𝐺 : ℝ ⟶ ℝ ) |
73 |
12
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → ran 𝐺 ∈ Fin ) |
74 |
|
inss2 |
⊢ ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ( ◡ 𝐺 “ { 𝑧 } ) |
75 |
74
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ( ◡ 𝐺 “ { 𝑧 } ) ) |
76 |
|
i1fima |
⊢ ( 𝐹 ∈ dom ∫1 → ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∈ dom vol ) |
77 |
1 76
|
syl |
⊢ ( 𝜑 → ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∈ dom vol ) |
78 |
|
i1fima |
⊢ ( 𝐺 ∈ dom ∫1 → ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol ) |
79 |
2 78
|
syl |
⊢ ( 𝜑 → ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol ) |
80 |
|
inmbl |
⊢ ( ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∈ dom vol ∧ ( ◡ 𝐺 “ { 𝑧 } ) ∈ dom vol ) → ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol ) |
81 |
77 79 80
|
syl2anc |
⊢ ( 𝜑 → ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol ) |
82 |
81
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ∈ dom vol ) |
83 |
20 68
|
sstrid |
⊢ ( 𝜑 → ( ran 𝑃 ∖ { 0 } ) ⊆ ℝ ) |
84 |
83
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → 𝑤 ∈ ℝ ) |
85 |
84
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑤 ∈ ℝ ) |
86 |
60
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑧 ∈ ℝ ) |
87 |
85 86
|
resubcld |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑤 − 𝑧 ) ∈ ℝ ) |
88 |
85
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑤 ∈ ℂ ) |
89 |
86
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑧 ∈ ℂ ) |
90 |
88 89
|
npcand |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ( 𝑤 − 𝑧 ) + 𝑧 ) = 𝑤 ) |
91 |
|
eldifsni |
⊢ ( 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) → 𝑤 ≠ 0 ) |
92 |
91
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑤 ≠ 0 ) |
93 |
90 92
|
eqnetrd |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ( 𝑤 − 𝑧 ) + 𝑧 ) ≠ 0 ) |
94 |
|
oveq12 |
⊢ ( ( ( 𝑤 − 𝑧 ) = 0 ∧ 𝑧 = 0 ) → ( ( 𝑤 − 𝑧 ) + 𝑧 ) = ( 0 + 0 ) ) |
95 |
|
00id |
⊢ ( 0 + 0 ) = 0 |
96 |
94 95
|
eqtrdi |
⊢ ( ( ( 𝑤 − 𝑧 ) = 0 ∧ 𝑧 = 0 ) → ( ( 𝑤 − 𝑧 ) + 𝑧 ) = 0 ) |
97 |
96
|
necon3ai |
⊢ ( ( ( 𝑤 − 𝑧 ) + 𝑧 ) ≠ 0 → ¬ ( ( 𝑤 − 𝑧 ) = 0 ∧ 𝑧 = 0 ) ) |
98 |
93 97
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ¬ ( ( 𝑤 − 𝑧 ) = 0 ∧ 𝑧 = 0 ) ) |
99 |
1 2 3
|
itg1addlem3 |
⊢ ( ( ( ( 𝑤 − 𝑧 ) ∈ ℝ ∧ 𝑧 ∈ ℝ ) ∧ ¬ ( ( 𝑤 − 𝑧 ) = 0 ∧ 𝑧 = 0 ) ) → ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) = ( vol ‘ ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ) |
100 |
87 86 98 99
|
syl21anc |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) = ( vol ‘ ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ) |
101 |
1 2 3
|
itg1addlem2 |
⊢ ( 𝜑 → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ ) |
102 |
101
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ ) |
103 |
102 87 86
|
fovrnd |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ∈ ℝ ) |
104 |
100 103
|
eqeltrrd |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( vol ‘ ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ∈ ℝ ) |
105 |
72 73 75 82 104
|
itg1addlem1 |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → ( vol ‘ ∪ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) = Σ 𝑧 ∈ ran 𝐺 ( vol ‘ ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ) |
106 |
84
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → 𝑤 ∈ ℂ ) |
107 |
1 2
|
i1faddlem |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℂ ) → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑤 } ) = ∪ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) |
108 |
106 107
|
syldan |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑤 } ) = ∪ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) |
109 |
108
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → ( vol ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑤 } ) ) = ( vol ‘ ∪ 𝑧 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ) |
110 |
100
|
sumeq2dv |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → Σ 𝑧 ∈ ran 𝐺 ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) = Σ 𝑧 ∈ ran 𝐺 ( vol ‘ ( ( ◡ 𝐹 “ { ( 𝑤 − 𝑧 ) } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ) |
111 |
105 109 110
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → ( vol ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑤 } ) ) = Σ 𝑧 ∈ ran 𝐺 ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) |
112 |
111
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → ( 𝑤 · ( vol ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑤 } ) ) ) = ( 𝑤 · Σ 𝑧 ∈ ran 𝐺 ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) ) |
113 |
103
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ∈ ℂ ) |
114 |
73 106 113
|
fsummulc2 |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → ( 𝑤 · Σ 𝑧 ∈ ran 𝐺 ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) = Σ 𝑧 ∈ ran 𝐺 ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) ) |
115 |
112 114
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → ( 𝑤 · ( vol ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑤 } ) ) ) = Σ 𝑧 ∈ ran 𝐺 ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) ) |
116 |
115
|
sumeq2dv |
⊢ ( 𝜑 → Σ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ( 𝑤 · ( vol ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑤 } ) ) ) = Σ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) Σ 𝑧 ∈ ran 𝐺 ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) ) |
117 |
88 113
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) ∈ ℂ ) |
118 |
117
|
anasss |
⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ∧ 𝑧 ∈ ran 𝐺 ) ) → ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) ∈ ℂ ) |
119 |
22 12 118
|
fsumcom |
⊢ ( 𝜑 → Σ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) Σ 𝑧 ∈ ran 𝐺 ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) = Σ 𝑧 ∈ ran 𝐺 Σ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) ) |
120 |
71 116 119
|
3eqtrd |
⊢ ( 𝜑 → ( ∫1 ‘ ( 𝐹 ∘f + 𝐺 ) ) = Σ 𝑧 ∈ ran 𝐺 Σ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) ) |
121 |
|
oveq1 |
⊢ ( 𝑦 = ( 𝑤 − 𝑧 ) → ( 𝑦 + 𝑧 ) = ( ( 𝑤 − 𝑧 ) + 𝑧 ) ) |
122 |
|
oveq1 |
⊢ ( 𝑦 = ( 𝑤 − 𝑧 ) → ( 𝑦 𝐼 𝑧 ) = ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) |
123 |
121 122
|
oveq12d |
⊢ ( 𝑦 = ( 𝑤 − 𝑧 ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = ( ( ( 𝑤 − 𝑧 ) + 𝑧 ) · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) ) |
124 |
19
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ran 𝑃 ∈ Fin ) |
125 |
68
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ran 𝑃 ⊆ ℝ ) |
126 |
125
|
sselda |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑣 ∈ ran 𝑃 ) → 𝑣 ∈ ℝ ) |
127 |
60
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑣 ∈ ran 𝑃 ) → 𝑧 ∈ ℝ ) |
128 |
126 127
|
resubcld |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑣 ∈ ran 𝑃 ) → ( 𝑣 − 𝑧 ) ∈ ℝ ) |
129 |
128
|
ex |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑣 ∈ ran 𝑃 → ( 𝑣 − 𝑧 ) ∈ ℝ ) ) |
130 |
126
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑣 ∈ ran 𝑃 ) → 𝑣 ∈ ℂ ) |
131 |
130
|
adantrr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃 ) ) → 𝑣 ∈ ℂ ) |
132 |
68
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝑃 ) → 𝑦 ∈ ℝ ) |
133 |
132
|
ad2ant2rl |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃 ) ) → 𝑦 ∈ ℝ ) |
134 |
133
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃 ) ) → 𝑦 ∈ ℂ ) |
135 |
60
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → 𝑧 ∈ ℂ ) |
136 |
135
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃 ) ) → 𝑧 ∈ ℂ ) |
137 |
131 134 136
|
subcan2ad |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃 ) ) → ( ( 𝑣 − 𝑧 ) = ( 𝑦 − 𝑧 ) ↔ 𝑣 = 𝑦 ) ) |
138 |
137
|
ex |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ( ( 𝑣 ∈ ran 𝑃 ∧ 𝑦 ∈ ran 𝑃 ) → ( ( 𝑣 − 𝑧 ) = ( 𝑦 − 𝑧 ) ↔ 𝑣 = 𝑦 ) ) ) |
139 |
129 138
|
dom2lem |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) : ran 𝑃 –1-1→ ℝ ) |
140 |
|
f1f1orn |
⊢ ( ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) : ran 𝑃 –1-1→ ℝ → ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) : ran 𝑃 –1-1-onto→ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ) |
141 |
139 140
|
syl |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) : ran 𝑃 –1-1-onto→ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ) |
142 |
|
oveq1 |
⊢ ( 𝑣 = 𝑤 → ( 𝑣 − 𝑧 ) = ( 𝑤 − 𝑧 ) ) |
143 |
|
eqid |
⊢ ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) = ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) |
144 |
|
ovex |
⊢ ( 𝑤 − 𝑧 ) ∈ V |
145 |
142 143 144
|
fvmpt |
⊢ ( 𝑤 ∈ ran 𝑃 → ( ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ‘ 𝑤 ) = ( 𝑤 − 𝑧 ) ) |
146 |
145
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ ran 𝑃 ) → ( ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ‘ 𝑤 ) = ( 𝑤 − 𝑧 ) ) |
147 |
|
f1f |
⊢ ( ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) : ran 𝑃 –1-1→ ℝ → ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) : ran 𝑃 ⟶ ℝ ) |
148 |
|
frn |
⊢ ( ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) : ran 𝑃 ⟶ ℝ → ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ⊆ ℝ ) |
149 |
139 147 148
|
3syl |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ⊆ ℝ ) |
150 |
149
|
sselda |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ) → 𝑦 ∈ ℝ ) |
151 |
60
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ) → 𝑧 ∈ ℝ ) |
152 |
150 151
|
readdcld |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ) → ( 𝑦 + 𝑧 ) ∈ ℝ ) |
153 |
101
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ) → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ ) |
154 |
153 150 151
|
fovrnd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ) → ( 𝑦 𝐼 𝑧 ) ∈ ℝ ) |
155 |
152 154
|
remulcld |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) ∈ ℝ ) |
156 |
155
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ ) |
157 |
123 124 141 146 156
|
fsumf1o |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → Σ 𝑦 ∈ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑤 ∈ ran 𝑃 ( ( ( 𝑤 − 𝑧 ) + 𝑧 ) · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) ) |
158 |
125
|
sselda |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ ran 𝑃 ) → 𝑤 ∈ ℝ ) |
159 |
158
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ ran 𝑃 ) → 𝑤 ∈ ℂ ) |
160 |
135
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ ran 𝑃 ) → 𝑧 ∈ ℂ ) |
161 |
159 160
|
npcand |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ ran 𝑃 ) → ( ( 𝑤 − 𝑧 ) + 𝑧 ) = 𝑤 ) |
162 |
161
|
oveq1d |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ ran 𝑃 ) → ( ( ( 𝑤 − 𝑧 ) + 𝑧 ) · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) = ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) ) |
163 |
162
|
sumeq2dv |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → Σ 𝑤 ∈ ran 𝑃 ( ( ( 𝑤 − 𝑧 ) + 𝑧 ) · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) = Σ 𝑤 ∈ ran 𝑃 ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) ) |
164 |
157 163
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → Σ 𝑦 ∈ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑤 ∈ ran 𝑃 ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) ) |
165 |
37
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( ran 𝐹 × ran 𝐺 ) ⊆ dom + ) |
166 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ∈ ran 𝐹 ) |
167 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑧 ∈ ran 𝐺 ) |
168 |
166 167
|
opelxpd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 〈 𝑦 , 𝑧 〉 ∈ ( ran 𝐹 × ran 𝐺 ) ) |
169 |
|
funfvima2 |
⊢ ( ( Fun + ∧ ( ran 𝐹 × ran 𝐺 ) ⊆ dom + ) → ( 〈 𝑦 , 𝑧 〉 ∈ ( ran 𝐹 × ran 𝐺 ) → ( + ‘ 〈 𝑦 , 𝑧 〉 ) ∈ ( + “ ( ran 𝐹 × ran 𝐺 ) ) ) ) |
170 |
24 169
|
mpan |
⊢ ( ( ran 𝐹 × ran 𝐺 ) ⊆ dom + → ( 〈 𝑦 , 𝑧 〉 ∈ ( ran 𝐹 × ran 𝐺 ) → ( + ‘ 〈 𝑦 , 𝑧 〉 ) ∈ ( + “ ( ran 𝐹 × ran 𝐺 ) ) ) ) |
171 |
165 168 170
|
sylc |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( + ‘ 〈 𝑦 , 𝑧 〉 ) ∈ ( + “ ( ran 𝐹 × ran 𝐺 ) ) ) |
172 |
|
df-ov |
⊢ ( 𝑦 + 𝑧 ) = ( + ‘ 〈 𝑦 , 𝑧 〉 ) |
173 |
171 172 45
|
3eltr4g |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑦 + 𝑧 ) ∈ ran 𝑃 ) |
174 |
59
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ∈ ℝ ) |
175 |
174
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ∈ ℂ ) |
176 |
135
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑧 ∈ ℂ ) |
177 |
175 176
|
pncand |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( ( 𝑦 + 𝑧 ) − 𝑧 ) = 𝑦 ) |
178 |
177
|
eqcomd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 = ( ( 𝑦 + 𝑧 ) − 𝑧 ) ) |
179 |
|
oveq1 |
⊢ ( 𝑣 = ( 𝑦 + 𝑧 ) → ( 𝑣 − 𝑧 ) = ( ( 𝑦 + 𝑧 ) − 𝑧 ) ) |
180 |
179
|
rspceeqv |
⊢ ( ( ( 𝑦 + 𝑧 ) ∈ ran 𝑃 ∧ 𝑦 = ( ( 𝑦 + 𝑧 ) − 𝑧 ) ) → ∃ 𝑣 ∈ ran 𝑃 𝑦 = ( 𝑣 − 𝑧 ) ) |
181 |
173 178 180
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ∃ 𝑣 ∈ ran 𝑃 𝑦 = ( 𝑣 − 𝑧 ) ) |
182 |
181
|
ralrimiva |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ∀ 𝑦 ∈ ran 𝐹 ∃ 𝑣 ∈ ran 𝑃 𝑦 = ( 𝑣 − 𝑧 ) ) |
183 |
|
ssabral |
⊢ ( ran 𝐹 ⊆ { 𝑦 ∣ ∃ 𝑣 ∈ ran 𝑃 𝑦 = ( 𝑣 − 𝑧 ) } ↔ ∀ 𝑦 ∈ ran 𝐹 ∃ 𝑣 ∈ ran 𝑃 𝑦 = ( 𝑣 − 𝑧 ) ) |
184 |
182 183
|
sylibr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ran 𝐹 ⊆ { 𝑦 ∣ ∃ 𝑣 ∈ ran 𝑃 𝑦 = ( 𝑣 − 𝑧 ) } ) |
185 |
143
|
rnmpt |
⊢ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) = { 𝑦 ∣ ∃ 𝑣 ∈ ran 𝑃 𝑦 = ( 𝑣 − 𝑧 ) } |
186 |
184 185
|
sseqtrrdi |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ran 𝐹 ⊆ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ) |
187 |
60
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝑧 ∈ ℝ ) |
188 |
174 187
|
readdcld |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑦 + 𝑧 ) ∈ ℝ ) |
189 |
101
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ ) |
190 |
189 174 187
|
fovrnd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑦 𝐼 𝑧 ) ∈ ℝ ) |
191 |
188 190
|
remulcld |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) ∈ ℝ ) |
192 |
191
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ ) |
193 |
149
|
ssdifd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ( ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ∖ ran 𝐹 ) ⊆ ( ℝ ∖ ran 𝐹 ) ) |
194 |
193
|
sselda |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ( ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ∖ ran 𝐹 ) ) → 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ) |
195 |
|
eldifi |
⊢ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) → 𝑦 ∈ ℝ ) |
196 |
195
|
ad2antrl |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → 𝑦 ∈ ℝ ) |
197 |
60
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → 𝑧 ∈ ℝ ) |
198 |
|
simprr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) |
199 |
1 2 3
|
itg1addlem3 |
⊢ ( ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) → ( 𝑦 𝐼 𝑧 ) = ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ) |
200 |
196 197 198 199
|
syl21anc |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( 𝑦 𝐼 𝑧 ) = ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) ) |
201 |
|
inss1 |
⊢ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ( ◡ 𝐹 “ { 𝑦 } ) |
202 |
|
eldifn |
⊢ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) → ¬ 𝑦 ∈ ran 𝐹 ) |
203 |
202
|
ad2antrl |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ¬ 𝑦 ∈ ran 𝐹 ) |
204 |
|
vex |
⊢ 𝑣 ∈ V |
205 |
204
|
eliniseg |
⊢ ( 𝑦 ∈ V → ( 𝑣 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ↔ 𝑣 𝐹 𝑦 ) ) |
206 |
205
|
elv |
⊢ ( 𝑣 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ↔ 𝑣 𝐹 𝑦 ) |
207 |
|
vex |
⊢ 𝑦 ∈ V |
208 |
204 207
|
brelrn |
⊢ ( 𝑣 𝐹 𝑦 → 𝑦 ∈ ran 𝐹 ) |
209 |
206 208
|
sylbi |
⊢ ( 𝑣 ∈ ( ◡ 𝐹 “ { 𝑦 } ) → 𝑦 ∈ ran 𝐹 ) |
210 |
203 209
|
nsyl |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ¬ 𝑣 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) |
211 |
210
|
pm2.21d |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( 𝑣 ∈ ( ◡ 𝐹 “ { 𝑦 } ) → 𝑣 ∈ ∅ ) ) |
212 |
211
|
ssrdv |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( ◡ 𝐹 “ { 𝑦 } ) ⊆ ∅ ) |
213 |
201 212
|
sstrid |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ∅ ) |
214 |
|
ss0 |
⊢ ( ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ⊆ ∅ → ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) = ∅ ) |
215 |
213 214
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) = ∅ ) |
216 |
215
|
fveq2d |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) = ( vol ‘ ∅ ) ) |
217 |
|
0mbl |
⊢ ∅ ∈ dom vol |
218 |
|
mblvol |
⊢ ( ∅ ∈ dom vol → ( vol ‘ ∅ ) = ( vol* ‘ ∅ ) ) |
219 |
217 218
|
ax-mp |
⊢ ( vol ‘ ∅ ) = ( vol* ‘ ∅ ) |
220 |
|
ovol0 |
⊢ ( vol* ‘ ∅ ) = 0 |
221 |
219 220
|
eqtri |
⊢ ( vol ‘ ∅ ) = 0 |
222 |
216 221
|
eqtrdi |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( vol ‘ ( ( ◡ 𝐹 “ { 𝑦 } ) ∩ ( ◡ 𝐺 “ { 𝑧 } ) ) ) = 0 ) |
223 |
200 222
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( 𝑦 𝐼 𝑧 ) = 0 ) |
224 |
223
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = ( ( 𝑦 + 𝑧 ) · 0 ) ) |
225 |
196 197
|
readdcld |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( 𝑦 + 𝑧 ) ∈ ℝ ) |
226 |
225
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( 𝑦 + 𝑧 ) ∈ ℂ ) |
227 |
226
|
mul01d |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( ( 𝑦 + 𝑧 ) · 0 ) = 0 ) |
228 |
224 227
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ ( 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ∧ ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) ) ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = 0 ) |
229 |
228
|
expr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ) → ( ¬ ( 𝑦 = 0 ∧ 𝑧 = 0 ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = 0 ) ) |
230 |
|
oveq12 |
⊢ ( ( 𝑦 = 0 ∧ 𝑧 = 0 ) → ( 𝑦 + 𝑧 ) = ( 0 + 0 ) ) |
231 |
230 95
|
eqtrdi |
⊢ ( ( 𝑦 = 0 ∧ 𝑧 = 0 ) → ( 𝑦 + 𝑧 ) = 0 ) |
232 |
|
oveq12 |
⊢ ( ( 𝑦 = 0 ∧ 𝑧 = 0 ) → ( 𝑦 𝐼 𝑧 ) = ( 0 𝐼 0 ) ) |
233 |
|
0re |
⊢ 0 ∈ ℝ |
234 |
|
iftrue |
⊢ ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) → if ( ( 𝑖 = 0 ∧ 𝑗 = 0 ) , 0 , ( vol ‘ ( ( ◡ 𝐹 “ { 𝑖 } ) ∩ ( ◡ 𝐺 “ { 𝑗 } ) ) ) ) = 0 ) |
235 |
|
c0ex |
⊢ 0 ∈ V |
236 |
234 3 235
|
ovmpoa |
⊢ ( ( 0 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 0 𝐼 0 ) = 0 ) |
237 |
233 233 236
|
mp2an |
⊢ ( 0 𝐼 0 ) = 0 |
238 |
232 237
|
eqtrdi |
⊢ ( ( 𝑦 = 0 ∧ 𝑧 = 0 ) → ( 𝑦 𝐼 𝑧 ) = 0 ) |
239 |
231 238
|
oveq12d |
⊢ ( ( 𝑦 = 0 ∧ 𝑧 = 0 ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = ( 0 · 0 ) ) |
240 |
|
0cn |
⊢ 0 ∈ ℂ |
241 |
240
|
mul01i |
⊢ ( 0 · 0 ) = 0 |
242 |
239 241
|
eqtrdi |
⊢ ( ( 𝑦 = 0 ∧ 𝑧 = 0 ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = 0 ) |
243 |
229 242
|
pm2.61d2 |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ( ℝ ∖ ran 𝐹 ) ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = 0 ) |
244 |
194 243
|
syldan |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑦 ∈ ( ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ∖ ran 𝐹 ) ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = 0 ) |
245 |
|
f1ofo |
⊢ ( ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) : ran 𝑃 –1-1-onto→ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) → ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) : ran 𝑃 –onto→ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ) |
246 |
141 245
|
syl |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) : ran 𝑃 –onto→ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ) |
247 |
|
fofi |
⊢ ( ( ran 𝑃 ∈ Fin ∧ ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) : ran 𝑃 –onto→ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ) → ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ∈ Fin ) |
248 |
124 246 247
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ∈ Fin ) |
249 |
186 192 244 248
|
fsumss |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → Σ 𝑦 ∈ ran 𝐹 ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑦 ∈ ran ( 𝑣 ∈ ran 𝑃 ↦ ( 𝑣 − 𝑧 ) ) ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) ) |
250 |
20
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ( ran 𝑃 ∖ { 0 } ) ⊆ ran 𝑃 ) |
251 |
117
|
an32s |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ) → ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) ∈ ℂ ) |
252 |
|
dfin4 |
⊢ ( ran 𝑃 ∩ { 0 } ) = ( ran 𝑃 ∖ ( ran 𝑃 ∖ { 0 } ) ) |
253 |
|
inss2 |
⊢ ( ran 𝑃 ∩ { 0 } ) ⊆ { 0 } |
254 |
252 253
|
eqsstrri |
⊢ ( ran 𝑃 ∖ ( ran 𝑃 ∖ { 0 } ) ) ⊆ { 0 } |
255 |
254
|
sseli |
⊢ ( 𝑤 ∈ ( ran 𝑃 ∖ ( ran 𝑃 ∖ { 0 } ) ) → 𝑤 ∈ { 0 } ) |
256 |
|
elsni |
⊢ ( 𝑤 ∈ { 0 } → 𝑤 = 0 ) |
257 |
256
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ { 0 } ) → 𝑤 = 0 ) |
258 |
257
|
oveq1d |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ { 0 } ) → ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) = ( 0 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) ) |
259 |
101
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ { 0 } ) → 𝐼 : ( ℝ × ℝ ) ⟶ ℝ ) |
260 |
257 233
|
eqeltrdi |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ { 0 } ) → 𝑤 ∈ ℝ ) |
261 |
60
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ { 0 } ) → 𝑧 ∈ ℝ ) |
262 |
260 261
|
resubcld |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ { 0 } ) → ( 𝑤 − 𝑧 ) ∈ ℝ ) |
263 |
259 262 261
|
fovrnd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ { 0 } ) → ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ∈ ℝ ) |
264 |
263
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ { 0 } ) → ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ∈ ℂ ) |
265 |
264
|
mul02d |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ { 0 } ) → ( 0 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) = 0 ) |
266 |
258 265
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ { 0 } ) → ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) = 0 ) |
267 |
255 266
|
sylan2 |
⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) ∧ 𝑤 ∈ ( ran 𝑃 ∖ ( ran 𝑃 ∖ { 0 } ) ) ) → ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) = 0 ) |
268 |
250 251 267 124
|
fsumss |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → Σ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) = Σ 𝑤 ∈ ran 𝑃 ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) ) |
269 |
164 249 268
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → Σ 𝑦 ∈ ran 𝐹 ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) ) |
270 |
269
|
sumeq2dv |
⊢ ( 𝜑 → Σ 𝑧 ∈ ran 𝐺 Σ 𝑦 ∈ ran 𝐹 ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑧 ∈ ran 𝐺 Σ 𝑤 ∈ ( ran 𝑃 ∖ { 0 } ) ( 𝑤 · ( ( 𝑤 − 𝑧 ) 𝐼 𝑧 ) ) ) |
271 |
192
|
anasss |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐹 ) ) → ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) ∈ ℂ ) |
272 |
12 10 271
|
fsumcom |
⊢ ( 𝜑 → Σ 𝑧 ∈ ran 𝐺 Σ 𝑦 ∈ ran 𝐹 ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) = Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) ) |
273 |
120 270 272
|
3eqtr2d |
⊢ ( 𝜑 → ( ∫1 ‘ ( 𝐹 ∘f + 𝐺 ) ) = Σ 𝑦 ∈ ran 𝐹 Σ 𝑧 ∈ ran 𝐺 ( ( 𝑦 + 𝑧 ) · ( 𝑦 𝐼 𝑧 ) ) ) |