Step | Hyp | Ref
| Expression |
1 | | itg10 23455 |
. . 3
⊢
(∫1‘(ℝ × {0})) = 0 |
2 | | reex 10027 |
. . . . . 6
⊢ ℝ
∈ V |
3 | 2 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = 0) → ℝ ∈
V) |
4 | | i1fmulc.2 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ dom
∫1) |
5 | | i1ff 23443 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
6 | 4, 5 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
7 | 6 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = 0) → 𝐹:ℝ⟶ℝ) |
8 | | i1fmulc.3 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℝ) |
9 | 8 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = 0) → 𝐴 ∈ ℝ) |
10 | | 0red 10041 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = 0) → 0 ∈
ℝ) |
11 | | simplr 792 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝑥 ∈ ℝ) → 𝐴 = 0) |
12 | 11 | oveq1d 6665 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝑥 ∈ ℝ) → (𝐴 · 𝑥) = (0 · 𝑥)) |
13 | | mul02lem2 10213 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ → (0
· 𝑥) =
0) |
14 | 13 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝑥 ∈ ℝ) → (0 · 𝑥) = 0) |
15 | 12, 14 | eqtrd 2656 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝑥 ∈ ℝ) → (𝐴 · 𝑥) = 0) |
16 | 3, 7, 9, 10, 15 | caofid2 6928 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 = 0) → ((ℝ × {𝐴}) ∘𝑓
· 𝐹) = (ℝ
× {0})) |
17 | 16 | fveq2d 6195 |
. . 3
⊢ ((𝜑 ∧ 𝐴 = 0) →
(∫1‘((ℝ × {𝐴}) ∘𝑓 ·
𝐹)) =
(∫1‘(ℝ × {0}))) |
18 | | simpr 477 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = 0) → 𝐴 = 0) |
19 | 18 | oveq1d 6665 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 = 0) → (𝐴 · (∫1‘𝐹)) = (0 ·
(∫1‘𝐹))) |
20 | | itg1cl 23452 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ (∫1‘𝐹) ∈ ℝ) |
21 | 4, 20 | syl 17 |
. . . . . . 7
⊢ (𝜑 →
(∫1‘𝐹)
∈ ℝ) |
22 | 21 | recnd 10068 |
. . . . . 6
⊢ (𝜑 →
(∫1‘𝐹)
∈ ℂ) |
23 | 22 | mul02d 10234 |
. . . . 5
⊢ (𝜑 → (0 ·
(∫1‘𝐹)) = 0) |
24 | 23 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 = 0) → (0 ·
(∫1‘𝐹)) = 0) |
25 | 19, 24 | eqtrd 2656 |
. . 3
⊢ ((𝜑 ∧ 𝐴 = 0) → (𝐴 · (∫1‘𝐹)) = 0) |
26 | 1, 17, 25 | 3eqtr4a 2682 |
. 2
⊢ ((𝜑 ∧ 𝐴 = 0) →
(∫1‘((ℝ × {𝐴}) ∘𝑓 ·
𝐹)) = (𝐴 · (∫1‘𝐹))) |
27 | 4, 8 | i1fmulc 23470 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∈ dom
∫1) |
28 | 27 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∈ dom
∫1) |
29 | | i1ff 23443 |
. . . . . . . . . . . . 13
⊢
(((ℝ × {𝐴}) ∘𝑓 ·
𝐹) ∈ dom
∫1 → ((ℝ × {𝐴}) ∘𝑓 ·
𝐹):ℝ⟶ℝ) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((ℝ × {𝐴}) ∘𝑓
· 𝐹):ℝ⟶ℝ) |
31 | | frn 6053 |
. . . . . . . . . . . 12
⊢
(((ℝ × {𝐴}) ∘𝑓 ·
𝐹):ℝ⟶ℝ
→ ran ((ℝ × {𝐴}) ∘𝑓 ·
𝐹) ⊆
ℝ) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ⊆
ℝ) |
33 | 32 | ssdifssd 3748 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (ran ((ℝ ×
{𝐴})
∘𝑓 · 𝐹) ∖ {0}) ⊆
ℝ) |
34 | 33 | sselda 3603 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ 𝑚 ∈
ℝ) |
35 | 34 | recnd 10068 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ 𝑚 ∈
ℂ) |
36 | 8 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℝ) |
37 | 36 | recnd 10068 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℂ) |
38 | 37 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ 𝐴 ∈
ℂ) |
39 | | simplr 792 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ 𝐴 ≠
0) |
40 | 35, 38, 39 | divcan2d 10803 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ (𝐴 · (𝑚 / 𝐴)) = 𝑚) |
41 | 4, 8 | i1fmulclem 23469 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ ℝ) → (◡((ℝ × {𝐴}) ∘𝑓 ·
𝐹) “ {𝑚}) = (◡𝐹 “ {(𝑚 / 𝐴)})) |
42 | 34, 41 | syldan 487 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ (◡((ℝ × {𝐴}) ∘𝑓
· 𝐹) “ {𝑚}) = (◡𝐹 “ {(𝑚 / 𝐴)})) |
43 | 42 | fveq2d 6195 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ (vol‘(◡((ℝ ×
{𝐴})
∘𝑓 · 𝐹) “ {𝑚})) = (vol‘(◡𝐹 “ {(𝑚 / 𝐴)}))) |
44 | 43 | eqcomd 2628 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ (vol‘(◡𝐹 “ {(𝑚 / 𝐴)})) = (vol‘(◡((ℝ × {𝐴}) ∘𝑓 ·
𝐹) “ {𝑚}))) |
45 | 40, 44 | oveq12d 6668 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ ((𝐴 · (𝑚 / 𝐴)) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)}))) = (𝑚 · (vol‘(◡((ℝ × {𝐴}) ∘𝑓 ·
𝐹) “ {𝑚})))) |
46 | 8 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ 𝐴 ∈
ℝ) |
47 | 34, 46, 39 | redivcld 10853 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ (𝑚 / 𝐴) ∈
ℝ) |
48 | 47 | recnd 10068 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ (𝑚 / 𝐴) ∈
ℂ) |
49 | 4 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ 𝐹 ∈ dom
∫1) |
50 | 46 | recnd 10068 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ 𝐴 ∈
ℂ) |
51 | | eldifsni 4320 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ (ran ((ℝ ×
{𝐴})
∘𝑓 · 𝐹) ∖ {0}) → 𝑚 ≠ 0) |
52 | 51 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ 𝑚 ≠
0) |
53 | 35, 50, 52, 39 | divne0d 10817 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ (𝑚 / 𝐴) ≠ 0) |
54 | | eldifsn 4317 |
. . . . . . . . . 10
⊢ ((𝑚 / 𝐴) ∈ (ℝ ∖ {0}) ↔
((𝑚 / 𝐴) ∈ ℝ ∧ (𝑚 / 𝐴) ≠ 0)) |
55 | 47, 53, 54 | sylanbrc 698 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ (𝑚 / 𝐴) ∈ (ℝ ∖
{0})) |
56 | | i1fima2sn 23447 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ (𝑚 / 𝐴) ∈ (ℝ ∖ {0}))
→ (vol‘(◡𝐹 “ {(𝑚 / 𝐴)})) ∈ ℝ) |
57 | 49, 55, 56 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ (vol‘(◡𝐹 “ {(𝑚 / 𝐴)})) ∈ ℝ) |
58 | 57 | recnd 10068 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ (vol‘(◡𝐹 “ {(𝑚 / 𝐴)})) ∈ ℂ) |
59 | 38, 48, 58 | mulassd 10063 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ ((𝐴 · (𝑚 / 𝐴)) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)}))) = (𝐴 · ((𝑚 / 𝐴) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)}))))) |
60 | 45, 59 | eqtr3d 2658 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ (𝑚 ·
(vol‘(◡((ℝ × {𝐴}) ∘𝑓
· 𝐹) “ {𝑚}))) = (𝐴 · ((𝑚 / 𝐴) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)}))))) |
61 | 60 | sumeq2dv 14433 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖
{0})(𝑚 ·
(vol‘(◡((ℝ × {𝐴}) ∘𝑓
· 𝐹) “ {𝑚}))) = Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖
{0})(𝐴 · ((𝑚 / 𝐴) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)}))))) |
62 | | i1frn 23444 |
. . . . . . 7
⊢
(((ℝ × {𝐴}) ∘𝑓 ·
𝐹) ∈ dom
∫1 → ran ((ℝ × {𝐴}) ∘𝑓 ·
𝐹) ∈
Fin) |
63 | 28, 62 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∈
Fin) |
64 | | difss 3737 |
. . . . . 6
⊢ (ran
((ℝ × {𝐴})
∘𝑓 · 𝐹) ∖ {0}) ⊆ ran ((ℝ ×
{𝐴})
∘𝑓 · 𝐹) |
65 | | ssfi 8180 |
. . . . . 6
⊢ ((ran
((ℝ × {𝐴})
∘𝑓 · 𝐹) ∈ Fin ∧ (ran ((ℝ ×
{𝐴})
∘𝑓 · 𝐹) ∖ {0}) ⊆ ran ((ℝ ×
{𝐴})
∘𝑓 · 𝐹)) → (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0})
∈ Fin) |
66 | 63, 64, 65 | sylancl 694 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (ran ((ℝ ×
{𝐴})
∘𝑓 · 𝐹) ∖ {0}) ∈ Fin) |
67 | 48, 58 | mulcld 10060 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ ((𝑚 / 𝐴) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)}))) ∈ ℂ) |
68 | 66, 37, 67 | fsummulc2 14516 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (𝐴 · Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖
{0})((𝑚 / 𝐴) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)})))) = Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖
{0})(𝐴 · ((𝑚 / 𝐴) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)}))))) |
69 | 61, 68 | eqtr4d 2659 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖
{0})(𝑚 ·
(vol‘(◡((ℝ × {𝐴}) ∘𝑓
· 𝐹) “ {𝑚}))) = (𝐴 · Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖
{0})((𝑚 / 𝐴) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)}))))) |
70 | | itg1val 23450 |
. . . 4
⊢
(((ℝ × {𝐴}) ∘𝑓 ·
𝐹) ∈ dom
∫1 → (∫1‘((ℝ × {𝐴}) ∘𝑓
· 𝐹)) = Σ𝑚 ∈ (ran ((ℝ ×
{𝐴})
∘𝑓 · 𝐹) ∖ {0})(𝑚 · (vol‘(◡((ℝ × {𝐴}) ∘𝑓 ·
𝐹) “ {𝑚})))) |
71 | 28, 70 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(∫1‘((ℝ × {𝐴}) ∘𝑓 ·
𝐹)) = Σ𝑚 ∈ (ran ((ℝ ×
{𝐴})
∘𝑓 · 𝐹) ∖ {0})(𝑚 · (vol‘(◡((ℝ × {𝐴}) ∘𝑓 ·
𝐹) “ {𝑚})))) |
72 | 4 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 𝐹 ∈ dom
∫1) |
73 | | itg1val 23450 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (∫1‘𝐹) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(◡𝐹 “ {𝑘})))) |
74 | 72, 73 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(∫1‘𝐹)
= Σ𝑘 ∈ (ran
𝐹 ∖ {0})(𝑘 · (vol‘(◡𝐹 “ {𝑘})))) |
75 | | id 22 |
. . . . . . 7
⊢ (𝑘 = (𝑚 / 𝐴) → 𝑘 = (𝑚 / 𝐴)) |
76 | | sneq 4187 |
. . . . . . . . 9
⊢ (𝑘 = (𝑚 / 𝐴) → {𝑘} = {(𝑚 / 𝐴)}) |
77 | 76 | imaeq2d 5466 |
. . . . . . . 8
⊢ (𝑘 = (𝑚 / 𝐴) → (◡𝐹 “ {𝑘}) = (◡𝐹 “ {(𝑚 / 𝐴)})) |
78 | 77 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑘 = (𝑚 / 𝐴) → (vol‘(◡𝐹 “ {𝑘})) = (vol‘(◡𝐹 “ {(𝑚 / 𝐴)}))) |
79 | 75, 78 | oveq12d 6668 |
. . . . . 6
⊢ (𝑘 = (𝑚 / 𝐴) → (𝑘 · (vol‘(◡𝐹 “ {𝑘}))) = ((𝑚 / 𝐴) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)})))) |
80 | | eqid 2622 |
. . . . . . 7
⊢ (𝑛 ∈ (ran ((ℝ ×
{𝐴})
∘𝑓 · 𝐹) ∖ {0}) ↦ (𝑛 / 𝐴)) = (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0})
↦ (𝑛 / 𝐴)) |
81 | | eldifi 3732 |
. . . . . . . . 9
⊢ (𝑛 ∈ (ran ((ℝ ×
{𝐴})
∘𝑓 · 𝐹) ∖ {0}) → 𝑛 ∈ ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹)) |
82 | 2 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ℝ ∈
V) |
83 | | ffn 6045 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:ℝ⟶ℝ →
𝐹 Fn
ℝ) |
84 | 6, 83 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 Fn ℝ) |
85 | | eqidd 2623 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) = (𝐹‘𝑦)) |
86 | 82, 8, 84, 85 | ofc1 6920 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (((ℝ ×
{𝐴})
∘𝑓 · 𝐹)‘𝑦) = (𝐴 · (𝐹‘𝑦))) |
87 | 86 | adantlr 751 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (((ℝ ×
{𝐴})
∘𝑓 · 𝐹)‘𝑦) = (𝐴 · (𝐹‘𝑦))) |
88 | 87 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → ((((ℝ ×
{𝐴})
∘𝑓 · 𝐹)‘𝑦) / 𝐴) = ((𝐴 · (𝐹‘𝑦)) / 𝐴)) |
89 | 6 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 𝐹:ℝ⟶ℝ) |
90 | 89 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ ℝ) |
91 | 90 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ ℂ) |
92 | 37 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → 𝐴 ∈ ℂ) |
93 | | simplr 792 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → 𝐴 ≠ 0) |
94 | 91, 92, 93 | divcan3d 10806 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → ((𝐴 · (𝐹‘𝑦)) / 𝐴) = (𝐹‘𝑦)) |
95 | 88, 94 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → ((((ℝ ×
{𝐴})
∘𝑓 · 𝐹)‘𝑦) / 𝐴) = (𝐹‘𝑦)) |
96 | 89, 83 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 𝐹 Fn ℝ) |
97 | | fnfvelrn 6356 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 Fn ℝ ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ ran 𝐹) |
98 | 96, 97 | sylan 488 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ ran 𝐹) |
99 | 95, 98 | eqeltrd 2701 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → ((((ℝ ×
{𝐴})
∘𝑓 · 𝐹)‘𝑦) / 𝐴) ∈ ran 𝐹) |
100 | 99 | ralrimiva 2966 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ∀𝑦 ∈ ℝ ((((ℝ × {𝐴}) ∘𝑓
· 𝐹)‘𝑦) / 𝐴) ∈ ran 𝐹) |
101 | | ffn 6045 |
. . . . . . . . . . . . 13
⊢
(((ℝ × {𝐴}) ∘𝑓 ·
𝐹):ℝ⟶ℝ
→ ((ℝ × {𝐴}) ∘𝑓 ·
𝐹) Fn
ℝ) |
102 | 30, 101 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((ℝ × {𝐴}) ∘𝑓
· 𝐹) Fn
ℝ) |
103 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (((ℝ × {𝐴}) ∘𝑓
· 𝐹)‘𝑦) → (𝑛 / 𝐴) = ((((ℝ × {𝐴}) ∘𝑓 ·
𝐹)‘𝑦) / 𝐴)) |
104 | 103 | eleq1d 2686 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (((ℝ × {𝐴}) ∘𝑓
· 𝐹)‘𝑦) → ((𝑛 / 𝐴) ∈ ran 𝐹 ↔ ((((ℝ × {𝐴}) ∘𝑓
· 𝐹)‘𝑦) / 𝐴) ∈ ran 𝐹)) |
105 | 104 | ralrn 6362 |
. . . . . . . . . . . 12
⊢
(((ℝ × {𝐴}) ∘𝑓 ·
𝐹) Fn ℝ →
(∀𝑛 ∈ ran
((ℝ × {𝐴})
∘𝑓 · 𝐹)(𝑛 / 𝐴) ∈ ran 𝐹 ↔ ∀𝑦 ∈ ℝ ((((ℝ × {𝐴}) ∘𝑓
· 𝐹)‘𝑦) / 𝐴) ∈ ran 𝐹)) |
106 | 102, 105 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (∀𝑛 ∈ ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹)(𝑛 / 𝐴) ∈ ran 𝐹 ↔ ∀𝑦 ∈ ℝ ((((ℝ × {𝐴}) ∘𝑓
· 𝐹)‘𝑦) / 𝐴) ∈ ran 𝐹)) |
107 | 100, 106 | mpbird 247 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ∀𝑛 ∈ ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹)(𝑛 / 𝐴) ∈ ran 𝐹) |
108 | 107 | r19.21bi 2932 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑛 ∈ ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹)) → (𝑛 / 𝐴) ∈ ran 𝐹) |
109 | 81, 108 | sylan2 491 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ (𝑛 / 𝐴) ∈ ran 𝐹) |
110 | 33 | sselda 3603 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ 𝑛 ∈
ℝ) |
111 | 110 | recnd 10068 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ 𝑛 ∈
ℂ) |
112 | 37 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ 𝐴 ∈
ℂ) |
113 | | eldifsni 4320 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ran ((ℝ ×
{𝐴})
∘𝑓 · 𝐹) ∖ {0}) → 𝑛 ≠ 0) |
114 | 113 | adantl 482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ 𝑛 ≠
0) |
115 | | simplr 792 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ 𝐴 ≠
0) |
116 | 111, 112,
114, 115 | divne0d 10817 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ (𝑛 / 𝐴) ≠ 0) |
117 | | eldifsn 4317 |
. . . . . . . 8
⊢ ((𝑛 / 𝐴) ∈ (ran 𝐹 ∖ {0}) ↔ ((𝑛 / 𝐴) ∈ ran 𝐹 ∧ (𝑛 / 𝐴) ≠ 0)) |
118 | 109, 116,
117 | sylanbrc 698 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ (𝑛 / 𝐴) ∈ (ran 𝐹 ∖ {0})) |
119 | | eldifi 3732 |
. . . . . . . . 9
⊢ (𝑘 ∈ (ran 𝐹 ∖ {0}) → 𝑘 ∈ ran 𝐹) |
120 | | fnfvelrn 6356 |
. . . . . . . . . . . . . 14
⊢
((((ℝ × {𝐴}) ∘𝑓 ·
𝐹) Fn ℝ ∧ 𝑦 ∈ ℝ) →
(((ℝ × {𝐴})
∘𝑓 · 𝐹)‘𝑦) ∈ ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹)) |
121 | 102, 120 | sylan 488 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (((ℝ ×
{𝐴})
∘𝑓 · 𝐹)‘𝑦) ∈ ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹)) |
122 | 87, 121 | eqeltrrd 2702 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (𝐴 · (𝐹‘𝑦)) ∈ ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹)) |
123 | 122 | ralrimiva 2966 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ∀𝑦 ∈ ℝ (𝐴 · (𝐹‘𝑦)) ∈ ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹)) |
124 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝐹‘𝑦) → (𝐴 · 𝑘) = (𝐴 · (𝐹‘𝑦))) |
125 | 124 | eleq1d 2686 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝐹‘𝑦) → ((𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ↔ (𝐴 · (𝐹‘𝑦)) ∈ ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹))) |
126 | 125 | ralrn 6362 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn ℝ →
(∀𝑘 ∈ ran 𝐹(𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ↔
∀𝑦 ∈ ℝ
(𝐴 · (𝐹‘𝑦)) ∈ ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹))) |
127 | 96, 126 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (∀𝑘 ∈ ran 𝐹(𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ↔
∀𝑦 ∈ ℝ
(𝐴 · (𝐹‘𝑦)) ∈ ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹))) |
128 | 123, 127 | mpbird 247 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ∀𝑘 ∈ ran 𝐹(𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹)) |
129 | 128 | r19.21bi 2932 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ ran 𝐹) → (𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹)) |
130 | 119, 129 | sylan2 491 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹)) |
131 | 37 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐴 ∈ ℂ) |
132 | | frn 6053 |
. . . . . . . . . . . . 13
⊢ (𝐹:ℝ⟶ℝ →
ran 𝐹 ⊆
ℝ) |
133 | 89, 132 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ran 𝐹 ⊆ ℝ) |
134 | 133 | ssdifssd 3748 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (ran 𝐹 ∖ {0}) ⊆
ℝ) |
135 | 134 | sselda 3603 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑘 ∈ ℝ) |
136 | 135 | recnd 10068 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑘 ∈ ℂ) |
137 | | simplr 792 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐴 ≠ 0) |
138 | | eldifsni 4320 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (ran 𝐹 ∖ {0}) → 𝑘 ≠ 0) |
139 | 138 | adantl 482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑘 ≠ 0) |
140 | 131, 136,
137, 139 | mulne0d 10679 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝐴 · 𝑘) ≠ 0) |
141 | | eldifsn 4317 |
. . . . . . . 8
⊢ ((𝐴 · 𝑘) ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0})
↔ ((𝐴 · 𝑘) ∈ ran ((ℝ ×
{𝐴})
∘𝑓 · 𝐹) ∧ (𝐴 · 𝑘) ≠ 0)) |
142 | 130, 140,
141 | sylanbrc 698 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝐴 · 𝑘) ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖
{0})) |
143 | | simpl 473 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ (ran ((ℝ ×
{𝐴})
∘𝑓 · 𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖
{0})) |
144 | | ssel2 3598 |
. . . . . . . . . . . 12
⊢ (((ran
((ℝ × {𝐴})
∘𝑓 · 𝐹) ∖ {0}) ⊆ ℝ ∧ 𝑛 ∈ (ran ((ℝ ×
{𝐴})
∘𝑓 · 𝐹) ∖ {0})) → 𝑛 ∈ ℝ) |
145 | 33, 143, 144 | syl2an 494 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0})
∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝑛 ∈
ℝ) |
146 | 145 | recnd 10068 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0})
∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝑛 ∈
ℂ) |
147 | 8 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0})
∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝐴 ∈
ℝ) |
148 | 147 | recnd 10068 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0})
∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝐴 ∈
ℂ) |
149 | 135 | adantrl 752 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0})
∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝑘 ∈
ℝ) |
150 | 149 | recnd 10068 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0})
∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝑘 ∈
ℂ) |
151 | | simplr 792 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0})
∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝐴 ≠ 0) |
152 | 146, 148,
150, 151 | divmuld 10823 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0})
∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → ((𝑛 / 𝐴) = 𝑘 ↔ (𝐴 · 𝑘) = 𝑛)) |
153 | 152 | bicomd 213 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0})
∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → ((𝐴 · 𝑘) = 𝑛 ↔ (𝑛 / 𝐴) = 𝑘)) |
154 | | eqcom 2629 |
. . . . . . . 8
⊢ (𝑛 = (𝐴 · 𝑘) ↔ (𝐴 · 𝑘) = 𝑛) |
155 | | eqcom 2629 |
. . . . . . . 8
⊢ (𝑘 = (𝑛 / 𝐴) ↔ (𝑛 / 𝐴) = 𝑘) |
156 | 153, 154,
155 | 3bitr4g 303 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0})
∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → (𝑛 = (𝐴 · 𝑘) ↔ 𝑘 = (𝑛 / 𝐴))) |
157 | 80, 118, 142, 156 | f1o2d 6887 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0})
↦ (𝑛 / 𝐴)):(ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖
{0})–1-1-onto→(ran 𝐹 ∖ {0})) |
158 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (𝑛 / 𝐴) = (𝑚 / 𝐴)) |
159 | | ovex 6678 |
. . . . . . . 8
⊢ (𝑚 / 𝐴) ∈ V |
160 | 158, 80, 159 | fvmpt 6282 |
. . . . . . 7
⊢ (𝑚 ∈ (ran ((ℝ ×
{𝐴})
∘𝑓 · 𝐹) ∖ {0}) → ((𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0})
↦ (𝑛 / 𝐴))‘𝑚) = (𝑚 / 𝐴)) |
161 | 160 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ ((𝑛 ∈ (ran
((ℝ × {𝐴})
∘𝑓 · 𝐹) ∖ {0}) ↦ (𝑛 / 𝐴))‘𝑚) = (𝑚 / 𝐴)) |
162 | | i1fima2sn 23447 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) →
(vol‘(◡𝐹 “ {𝑘})) ∈ ℝ) |
163 | 72, 162 | sylan 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(◡𝐹 “ {𝑘})) ∈ ℝ) |
164 | 135, 163 | remulcld 10070 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑘 · (vol‘(◡𝐹 “ {𝑘}))) ∈ ℝ) |
165 | 164 | recnd 10068 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑘 · (vol‘(◡𝐹 “ {𝑘}))) ∈ ℂ) |
166 | 79, 66, 157, 161, 165 | fsumf1o 14454 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(◡𝐹 “ {𝑘}))) = Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖
{0})((𝑚 / 𝐴) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)})))) |
167 | 74, 166 | eqtrd 2656 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(∫1‘𝐹)
= Σ𝑚 ∈ (ran
((ℝ × {𝐴})
∘𝑓 · 𝐹) ∖ {0})((𝑚 / 𝐴) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)})))) |
168 | 167 | oveq2d 6666 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (𝐴 · (∫1‘𝐹)) = (𝐴 · Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖
{0})((𝑚 / 𝐴) · (vol‘(◡𝐹 “ {(𝑚 / 𝐴)}))))) |
169 | 69, 71, 168 | 3eqtr4d 2666 |
. 2
⊢ ((𝜑 ∧ 𝐴 ≠ 0) →
(∫1‘((ℝ × {𝐴}) ∘𝑓 ·
𝐹)) = (𝐴 · (∫1‘𝐹))) |
170 | 26, 169 | pm2.61dane 2881 |
1
⊢ (𝜑 →
(∫1‘((ℝ × {𝐴}) ∘𝑓 ·
𝐹)) = (𝐴 · (∫1‘𝐹))) |