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

Theorem itg1mulc 23870
Description: The integral of a constant times a simple function is the constant times the original integral. (Contributed by Mario Carneiro, 25-Jun-2014.)
Hypotheses
Ref Expression
i1fmulc.2 (𝜑𝐹 ∈ dom ∫1)
i1fmulc.3 (𝜑𝐴 ∈ ℝ)
Assertion
Ref Expression
itg1mulc (𝜑 → (∫1‘((ℝ × {𝐴}) ∘𝑓 · 𝐹)) = (𝐴 · (∫1𝐹)))

Proof of Theorem itg1mulc
Dummy variables 𝑘 𝑚 𝑛 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 itg10 23854 . . 3 (∫1‘(ℝ × {0})) = 0
2 reex 10343 . . . . . 6 ℝ ∈ V
32a1i 11 . . . . 5 ((𝜑𝐴 = 0) → ℝ ∈ V)
4 i1fmulc.2 . . . . . . 7 (𝜑𝐹 ∈ dom ∫1)
5 i1ff 23842 . . . . . . 7 (𝐹 ∈ dom ∫1𝐹:ℝ⟶ℝ)
64, 5syl 17 . . . . . 6 (𝜑𝐹:ℝ⟶ℝ)
76adantr 474 . . . . 5 ((𝜑𝐴 = 0) → 𝐹:ℝ⟶ℝ)
8 i1fmulc.3 . . . . . 6 (𝜑𝐴 ∈ ℝ)
98adantr 474 . . . . 5 ((𝜑𝐴 = 0) → 𝐴 ∈ ℝ)
10 0red 10360 . . . . 5 ((𝜑𝐴 = 0) → 0 ∈ ℝ)
11 simplr 787 . . . . . . 7 (((𝜑𝐴 = 0) ∧ 𝑥 ∈ ℝ) → 𝐴 = 0)
1211oveq1d 6920 . . . . . 6 (((𝜑𝐴 = 0) ∧ 𝑥 ∈ ℝ) → (𝐴 · 𝑥) = (0 · 𝑥))
13 mul02lem2 10532 . . . . . . 7 (𝑥 ∈ ℝ → (0 · 𝑥) = 0)
1413adantl 475 . . . . . 6 (((𝜑𝐴 = 0) ∧ 𝑥 ∈ ℝ) → (0 · 𝑥) = 0)
1512, 14eqtrd 2861 . . . . 5 (((𝜑𝐴 = 0) ∧ 𝑥 ∈ ℝ) → (𝐴 · 𝑥) = 0)
163, 7, 9, 10, 15caofid2 7188 . . . 4 ((𝜑𝐴 = 0) → ((ℝ × {𝐴}) ∘𝑓 · 𝐹) = (ℝ × {0}))
1716fveq2d 6437 . . 3 ((𝜑𝐴 = 0) → (∫1‘((ℝ × {𝐴}) ∘𝑓 · 𝐹)) = (∫1‘(ℝ × {0})))
18 simpr 479 . . . . 5 ((𝜑𝐴 = 0) → 𝐴 = 0)
1918oveq1d 6920 . . . 4 ((𝜑𝐴 = 0) → (𝐴 · (∫1𝐹)) = (0 · (∫1𝐹)))
20 itg1cl 23851 . . . . . . . 8 (𝐹 ∈ dom ∫1 → (∫1𝐹) ∈ ℝ)
214, 20syl 17 . . . . . . 7 (𝜑 → (∫1𝐹) ∈ ℝ)
2221recnd 10385 . . . . . 6 (𝜑 → (∫1𝐹) ∈ ℂ)
2322mul02d 10553 . . . . 5 (𝜑 → (0 · (∫1𝐹)) = 0)
2423adantr 474 . . . 4 ((𝜑𝐴 = 0) → (0 · (∫1𝐹)) = 0)
2519, 24eqtrd 2861 . . 3 ((𝜑𝐴 = 0) → (𝐴 · (∫1𝐹)) = 0)
261, 17, 253eqtr4a 2887 . 2 ((𝜑𝐴 = 0) → (∫1‘((ℝ × {𝐴}) ∘𝑓 · 𝐹)) = (𝐴 · (∫1𝐹)))
274, 8i1fmulc 23869 . . . . . . . . . . . . . 14 (𝜑 → ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∈ dom ∫1)
2827adantr 474 . . . . . . . . . . . . 13 ((𝜑𝐴 ≠ 0) → ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∈ dom ∫1)
29 i1ff 23842 . . . . . . . . . . . . 13 (((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∈ dom ∫1 → ((ℝ × {𝐴}) ∘𝑓 · 𝐹):ℝ⟶ℝ)
3028, 29syl 17 . . . . . . . . . . . 12 ((𝜑𝐴 ≠ 0) → ((ℝ × {𝐴}) ∘𝑓 · 𝐹):ℝ⟶ℝ)
3130frnd 6285 . . . . . . . . . . 11 ((𝜑𝐴 ≠ 0) → ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ⊆ ℝ)
3231ssdifssd 3975 . . . . . . . . . 10 ((𝜑𝐴 ≠ 0) → (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ⊆ ℝ)
3332sselda 3827 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝑚 ∈ ℝ)
3433recnd 10385 . . . . . . . 8 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝑚 ∈ ℂ)
358adantr 474 . . . . . . . . . 10 ((𝜑𝐴 ≠ 0) → 𝐴 ∈ ℝ)
3635recnd 10385 . . . . . . . . 9 ((𝜑𝐴 ≠ 0) → 𝐴 ∈ ℂ)
3736adantr 474 . . . . . . . 8 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝐴 ∈ ℂ)
38 simplr 787 . . . . . . . 8 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝐴 ≠ 0)
3934, 37, 38divcan2d 11129 . . . . . . 7 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (𝐴 · (𝑚 / 𝐴)) = 𝑚)
404, 8i1fmulclem 23868 . . . . . . . . . 10 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ ℝ) → (((ℝ × {𝐴}) ∘𝑓 · 𝐹) “ {𝑚}) = (𝐹 “ {(𝑚 / 𝐴)}))
4133, 40syldan 587 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (((ℝ × {𝐴}) ∘𝑓 · 𝐹) “ {𝑚}) = (𝐹 “ {(𝑚 / 𝐴)}))
4241fveq2d 6437 . . . . . . . 8 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (vol‘(((ℝ × {𝐴}) ∘𝑓 · 𝐹) “ {𝑚})) = (vol‘(𝐹 “ {(𝑚 / 𝐴)})))
4342eqcomd 2831 . . . . . . 7 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (vol‘(𝐹 “ {(𝑚 / 𝐴)})) = (vol‘(((ℝ × {𝐴}) ∘𝑓 · 𝐹) “ {𝑚})))
4439, 43oveq12d 6923 . . . . . 6 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → ((𝐴 · (𝑚 / 𝐴)) · (vol‘(𝐹 “ {(𝑚 / 𝐴)}))) = (𝑚 · (vol‘(((ℝ × {𝐴}) ∘𝑓 · 𝐹) “ {𝑚}))))
458ad2antrr 719 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝐴 ∈ ℝ)
4633, 45, 38redivcld 11179 . . . . . . . 8 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (𝑚 / 𝐴) ∈ ℝ)
4746recnd 10385 . . . . . . 7 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (𝑚 / 𝐴) ∈ ℂ)
484ad2antrr 719 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝐹 ∈ dom ∫1)
4945recnd 10385 . . . . . . . . . . 11 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝐴 ∈ ℂ)
50 eldifsni 4540 . . . . . . . . . . . 12 (𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) → 𝑚 ≠ 0)
5150adantl 475 . . . . . . . . . . 11 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝑚 ≠ 0)
5234, 49, 51, 38divne0d 11143 . . . . . . . . . 10 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (𝑚 / 𝐴) ≠ 0)
53 eldifsn 4536 . . . . . . . . . 10 ((𝑚 / 𝐴) ∈ (ℝ ∖ {0}) ↔ ((𝑚 / 𝐴) ∈ ℝ ∧ (𝑚 / 𝐴) ≠ 0))
5446, 52, 53sylanbrc 580 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (𝑚 / 𝐴) ∈ (ℝ ∖ {0}))
55 i1fima2sn 23846 . . . . . . . . 9 ((𝐹 ∈ dom ∫1 ∧ (𝑚 / 𝐴) ∈ (ℝ ∖ {0})) → (vol‘(𝐹 “ {(𝑚 / 𝐴)})) ∈ ℝ)
5648, 54, 55syl2anc 581 . . . . . . . 8 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (vol‘(𝐹 “ {(𝑚 / 𝐴)})) ∈ ℝ)
5756recnd 10385 . . . . . . 7 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (vol‘(𝐹 “ {(𝑚 / 𝐴)})) ∈ ℂ)
5837, 47, 57mulassd 10380 . . . . . 6 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → ((𝐴 · (𝑚 / 𝐴)) · (vol‘(𝐹 “ {(𝑚 / 𝐴)}))) = (𝐴 · ((𝑚 / 𝐴) · (vol‘(𝐹 “ {(𝑚 / 𝐴)})))))
5944, 58eqtr3d 2863 . . . . 5 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (𝑚 · (vol‘(((ℝ × {𝐴}) ∘𝑓 · 𝐹) “ {𝑚}))) = (𝐴 · ((𝑚 / 𝐴) · (vol‘(𝐹 “ {(𝑚 / 𝐴)})))))
6059sumeq2dv 14810 . . . 4 ((𝜑𝐴 ≠ 0) → Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})(𝑚 · (vol‘(((ℝ × {𝐴}) ∘𝑓 · 𝐹) “ {𝑚}))) = Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})(𝐴 · ((𝑚 / 𝐴) · (vol‘(𝐹 “ {(𝑚 / 𝐴)})))))
61 i1frn 23843 . . . . . . 7 (((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∈ dom ∫1 → ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∈ Fin)
6228, 61syl 17 . . . . . 6 ((𝜑𝐴 ≠ 0) → ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∈ Fin)
63 difss 3964 . . . . . 6 (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ⊆ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹)
64 ssfi 8449 . . . . . 6 ((ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∈ Fin ∧ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ⊆ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹)) → (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∈ Fin)
6562, 63, 64sylancl 582 . . . . 5 ((𝜑𝐴 ≠ 0) → (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∈ Fin)
6647, 57mulcld 10377 . . . . 5 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → ((𝑚 / 𝐴) · (vol‘(𝐹 “ {(𝑚 / 𝐴)}))) ∈ ℂ)
6765, 36, 66fsummulc2 14890 . . . 4 ((𝜑𝐴 ≠ 0) → (𝐴 · Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})((𝑚 / 𝐴) · (vol‘(𝐹 “ {(𝑚 / 𝐴)})))) = Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})(𝐴 · ((𝑚 / 𝐴) · (vol‘(𝐹 “ {(𝑚 / 𝐴)})))))
6860, 67eqtr4d 2864 . . 3 ((𝜑𝐴 ≠ 0) → Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})(𝑚 · (vol‘(((ℝ × {𝐴}) ∘𝑓 · 𝐹) “ {𝑚}))) = (𝐴 · Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})((𝑚 / 𝐴) · (vol‘(𝐹 “ {(𝑚 / 𝐴)})))))
69 itg1val 23849 . . . 4 (((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∈ dom ∫1 → (∫1‘((ℝ × {𝐴}) ∘𝑓 · 𝐹)) = Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})(𝑚 · (vol‘(((ℝ × {𝐴}) ∘𝑓 · 𝐹) “ {𝑚}))))
7028, 69syl 17 . . 3 ((𝜑𝐴 ≠ 0) → (∫1‘((ℝ × {𝐴}) ∘𝑓 · 𝐹)) = Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})(𝑚 · (vol‘(((ℝ × {𝐴}) ∘𝑓 · 𝐹) “ {𝑚}))))
714adantr 474 . . . . . 6 ((𝜑𝐴 ≠ 0) → 𝐹 ∈ dom ∫1)
72 itg1val 23849 . . . . . 6 (𝐹 ∈ dom ∫1 → (∫1𝐹) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(𝐹 “ {𝑘}))))
7371, 72syl 17 . . . . 5 ((𝜑𝐴 ≠ 0) → (∫1𝐹) = Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(𝐹 “ {𝑘}))))
74 id 22 . . . . . . 7 (𝑘 = (𝑚 / 𝐴) → 𝑘 = (𝑚 / 𝐴))
75 sneq 4407 . . . . . . . . 9 (𝑘 = (𝑚 / 𝐴) → {𝑘} = {(𝑚 / 𝐴)})
7675imaeq2d 5707 . . . . . . . 8 (𝑘 = (𝑚 / 𝐴) → (𝐹 “ {𝑘}) = (𝐹 “ {(𝑚 / 𝐴)}))
7776fveq2d 6437 . . . . . . 7 (𝑘 = (𝑚 / 𝐴) → (vol‘(𝐹 “ {𝑘})) = (vol‘(𝐹 “ {(𝑚 / 𝐴)})))
7874, 77oveq12d 6923 . . . . . 6 (𝑘 = (𝑚 / 𝐴) → (𝑘 · (vol‘(𝐹 “ {𝑘}))) = ((𝑚 / 𝐴) · (vol‘(𝐹 “ {(𝑚 / 𝐴)}))))
79 eqid 2825 . . . . . . 7 (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ↦ (𝑛 / 𝐴)) = (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ↦ (𝑛 / 𝐴))
80 eldifi 3959 . . . . . . . . 9 (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) → 𝑛 ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹))
812a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → ℝ ∈ V)
826ffnd 6279 . . . . . . . . . . . . . . . . 17 (𝜑𝐹 Fn ℝ)
83 eqidd 2826 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ ℝ) → (𝐹𝑦) = (𝐹𝑦))
8481, 8, 82, 83ofc1 7180 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ ℝ) → (((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) = (𝐴 · (𝐹𝑦)))
8584adantlr 708 . . . . . . . . . . . . . . 15 (((𝜑𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) = (𝐴 · (𝐹𝑦)))
8685oveq1d 6920 . . . . . . . . . . . . . 14 (((𝜑𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → ((((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) / 𝐴) = ((𝐴 · (𝐹𝑦)) / 𝐴))
876adantr 474 . . . . . . . . . . . . . . . . 17 ((𝜑𝐴 ≠ 0) → 𝐹:ℝ⟶ℝ)
8887ffvelrnda 6608 . . . . . . . . . . . . . . . 16 (((𝜑𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (𝐹𝑦) ∈ ℝ)
8988recnd 10385 . . . . . . . . . . . . . . 15 (((𝜑𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (𝐹𝑦) ∈ ℂ)
9036adantr 474 . . . . . . . . . . . . . . 15 (((𝜑𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → 𝐴 ∈ ℂ)
91 simplr 787 . . . . . . . . . . . . . . 15 (((𝜑𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → 𝐴 ≠ 0)
9289, 90, 91divcan3d 11132 . . . . . . . . . . . . . 14 (((𝜑𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → ((𝐴 · (𝐹𝑦)) / 𝐴) = (𝐹𝑦))
9386, 92eqtrd 2861 . . . . . . . . . . . . 13 (((𝜑𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → ((((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) / 𝐴) = (𝐹𝑦))
9487ffnd 6279 . . . . . . . . . . . . . 14 ((𝜑𝐴 ≠ 0) → 𝐹 Fn ℝ)
95 fnfvelrn 6605 . . . . . . . . . . . . . 14 ((𝐹 Fn ℝ ∧ 𝑦 ∈ ℝ) → (𝐹𝑦) ∈ ran 𝐹)
9694, 95sylan 577 . . . . . . . . . . . . 13 (((𝜑𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (𝐹𝑦) ∈ ran 𝐹)
9793, 96eqeltrd 2906 . . . . . . . . . . . 12 (((𝜑𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → ((((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) / 𝐴) ∈ ran 𝐹)
9897ralrimiva 3175 . . . . . . . . . . 11 ((𝜑𝐴 ≠ 0) → ∀𝑦 ∈ ℝ ((((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) / 𝐴) ∈ ran 𝐹)
9930ffnd 6279 . . . . . . . . . . . 12 ((𝜑𝐴 ≠ 0) → ((ℝ × {𝐴}) ∘𝑓 · 𝐹) Fn ℝ)
100 oveq1 6912 . . . . . . . . . . . . . 14 (𝑛 = (((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) → (𝑛 / 𝐴) = ((((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) / 𝐴))
101100eleq1d 2891 . . . . . . . . . . . . 13 (𝑛 = (((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) → ((𝑛 / 𝐴) ∈ ran 𝐹 ↔ ((((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) / 𝐴) ∈ ran 𝐹))
102101ralrn 6611 . . . . . . . . . . . 12 (((ℝ × {𝐴}) ∘𝑓 · 𝐹) Fn ℝ → (∀𝑛 ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹)(𝑛 / 𝐴) ∈ ran 𝐹 ↔ ∀𝑦 ∈ ℝ ((((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) / 𝐴) ∈ ran 𝐹))
10399, 102syl 17 . . . . . . . . . . 11 ((𝜑𝐴 ≠ 0) → (∀𝑛 ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹)(𝑛 / 𝐴) ∈ ran 𝐹 ↔ ∀𝑦 ∈ ℝ ((((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) / 𝐴) ∈ ran 𝐹))
10498, 103mpbird 249 . . . . . . . . . 10 ((𝜑𝐴 ≠ 0) → ∀𝑛 ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹)(𝑛 / 𝐴) ∈ ran 𝐹)
105104r19.21bi 3141 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑛 ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹)) → (𝑛 / 𝐴) ∈ ran 𝐹)
10680, 105sylan2 588 . . . . . . . 8 (((𝜑𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (𝑛 / 𝐴) ∈ ran 𝐹)
10732sselda 3827 . . . . . . . . . 10 (((𝜑𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝑛 ∈ ℝ)
108107recnd 10385 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝑛 ∈ ℂ)
10936adantr 474 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝐴 ∈ ℂ)
110 eldifsni 4540 . . . . . . . . . 10 (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) → 𝑛 ≠ 0)
111110adantl 475 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝑛 ≠ 0)
112 simplr 787 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝐴 ≠ 0)
113108, 109, 111, 112divne0d 11143 . . . . . . . 8 (((𝜑𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (𝑛 / 𝐴) ≠ 0)
114 eldifsn 4536 . . . . . . . 8 ((𝑛 / 𝐴) ∈ (ran 𝐹 ∖ {0}) ↔ ((𝑛 / 𝐴) ∈ ran 𝐹 ∧ (𝑛 / 𝐴) ≠ 0))
115106, 113, 114sylanbrc 580 . . . . . . 7 (((𝜑𝐴 ≠ 0) ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → (𝑛 / 𝐴) ∈ (ran 𝐹 ∖ {0}))
116 eldifi 3959 . . . . . . . . 9 (𝑘 ∈ (ran 𝐹 ∖ {0}) → 𝑘 ∈ ran 𝐹)
117 fnfvelrn 6605 . . . . . . . . . . . . . 14 ((((ℝ × {𝐴}) ∘𝑓 · 𝐹) Fn ℝ ∧ 𝑦 ∈ ℝ) → (((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹))
11899, 117sylan 577 . . . . . . . . . . . . 13 (((𝜑𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (((ℝ × {𝐴}) ∘𝑓 · 𝐹)‘𝑦) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹))
11985, 118eqeltrrd 2907 . . . . . . . . . . . 12 (((𝜑𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (𝐴 · (𝐹𝑦)) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹))
120119ralrimiva 3175 . . . . . . . . . . 11 ((𝜑𝐴 ≠ 0) → ∀𝑦 ∈ ℝ (𝐴 · (𝐹𝑦)) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹))
121 oveq2 6913 . . . . . . . . . . . . . 14 (𝑘 = (𝐹𝑦) → (𝐴 · 𝑘) = (𝐴 · (𝐹𝑦)))
122121eleq1d 2891 . . . . . . . . . . . . 13 (𝑘 = (𝐹𝑦) → ((𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ↔ (𝐴 · (𝐹𝑦)) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹)))
123122ralrn 6611 . . . . . . . . . . . 12 (𝐹 Fn ℝ → (∀𝑘 ∈ ran 𝐹(𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ↔ ∀𝑦 ∈ ℝ (𝐴 · (𝐹𝑦)) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹)))
12494, 123syl 17 . . . . . . . . . . 11 ((𝜑𝐴 ≠ 0) → (∀𝑘 ∈ ran 𝐹(𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ↔ ∀𝑦 ∈ ℝ (𝐴 · (𝐹𝑦)) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹)))
125120, 124mpbird 249 . . . . . . . . . 10 ((𝜑𝐴 ≠ 0) → ∀𝑘 ∈ ran 𝐹(𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹))
126125r19.21bi 3141 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑘 ∈ ran 𝐹) → (𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹))
127116, 126sylan2 588 . . . . . . . 8 (((𝜑𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹))
12836adantr 474 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐴 ∈ ℂ)
12987frnd 6285 . . . . . . . . . . . 12 ((𝜑𝐴 ≠ 0) → ran 𝐹 ⊆ ℝ)
130129ssdifssd 3975 . . . . . . . . . . 11 ((𝜑𝐴 ≠ 0) → (ran 𝐹 ∖ {0}) ⊆ ℝ)
131130sselda 3827 . . . . . . . . . 10 (((𝜑𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑘 ∈ ℝ)
132131recnd 10385 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑘 ∈ ℂ)
133 simplr 787 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝐴 ≠ 0)
134 eldifsni 4540 . . . . . . . . . 10 (𝑘 ∈ (ran 𝐹 ∖ {0}) → 𝑘 ≠ 0)
135134adantl 475 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑘 ≠ 0)
136128, 132, 133, 135mulne0d 11004 . . . . . . . 8 (((𝜑𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝐴 · 𝑘) ≠ 0)
137 eldifsn 4536 . . . . . . . 8 ((𝐴 · 𝑘) ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ↔ ((𝐴 · 𝑘) ∈ ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∧ (𝐴 · 𝑘) ≠ 0))
138127, 136, 137sylanbrc 580 . . . . . . 7 (((𝜑𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝐴 · 𝑘) ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}))
139 simpl 476 . . . . . . . . . . . 12 ((𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}))
140 ssel2 3822 . . . . . . . . . . . 12 (((ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ⊆ ℝ ∧ 𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → 𝑛 ∈ ℝ)
14132, 139, 140syl2an 591 . . . . . . . . . . 11 (((𝜑𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝑛 ∈ ℝ)
142141recnd 10385 . . . . . . . . . 10 (((𝜑𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝑛 ∈ ℂ)
1438ad2antrr 719 . . . . . . . . . . 11 (((𝜑𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝐴 ∈ ℝ)
144143recnd 10385 . . . . . . . . . 10 (((𝜑𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝐴 ∈ ℂ)
145131adantrl 709 . . . . . . . . . . 11 (((𝜑𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝑘 ∈ ℝ)
146145recnd 10385 . . . . . . . . . 10 (((𝜑𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝑘 ∈ ℂ)
147 simplr 787 . . . . . . . . . 10 (((𝜑𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → 𝐴 ≠ 0)
148142, 144, 146, 147divmuld 11149 . . . . . . . . 9 (((𝜑𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → ((𝑛 / 𝐴) = 𝑘 ↔ (𝐴 · 𝑘) = 𝑛))
149148bicomd 215 . . . . . . . 8 (((𝜑𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → ((𝐴 · 𝑘) = 𝑛 ↔ (𝑛 / 𝐴) = 𝑘))
150 eqcom 2832 . . . . . . . 8 (𝑛 = (𝐴 · 𝑘) ↔ (𝐴 · 𝑘) = 𝑛)
151 eqcom 2832 . . . . . . . 8 (𝑘 = (𝑛 / 𝐴) ↔ (𝑛 / 𝐴) = 𝑘)
152149, 150, 1513bitr4g 306 . . . . . . 7 (((𝜑𝐴 ≠ 0) ∧ (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0}))) → (𝑛 = (𝐴 · 𝑘) ↔ 𝑘 = (𝑛 / 𝐴)))
15379, 115, 138, 152f1o2d 7147 . . . . . 6 ((𝜑𝐴 ≠ 0) → (𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ↦ (𝑛 / 𝐴)):(ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})–1-1-onto→(ran 𝐹 ∖ {0}))
154 oveq1 6912 . . . . . . . 8 (𝑛 = 𝑚 → (𝑛 / 𝐴) = (𝑚 / 𝐴))
155 ovex 6937 . . . . . . . 8 (𝑚 / 𝐴) ∈ V
156154, 79, 155fvmpt 6529 . . . . . . 7 (𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) → ((𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ↦ (𝑛 / 𝐴))‘𝑚) = (𝑚 / 𝐴))
157156adantl 475 . . . . . 6 (((𝜑𝐴 ≠ 0) ∧ 𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})) → ((𝑛 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0}) ↦ (𝑛 / 𝐴))‘𝑚) = (𝑚 / 𝐴))
158 i1fima2sn 23846 . . . . . . . . 9 ((𝐹 ∈ dom ∫1𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(𝐹 “ {𝑘})) ∈ ℝ)
15971, 158sylan 577 . . . . . . . 8 (((𝜑𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (vol‘(𝐹 “ {𝑘})) ∈ ℝ)
160131, 159remulcld 10387 . . . . . . 7 (((𝜑𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑘 · (vol‘(𝐹 “ {𝑘}))) ∈ ℝ)
161160recnd 10385 . . . . . 6 (((𝜑𝐴 ≠ 0) ∧ 𝑘 ∈ (ran 𝐹 ∖ {0})) → (𝑘 · (vol‘(𝐹 “ {𝑘}))) ∈ ℂ)
16278, 65, 153, 157, 161fsumf1o 14831 . . . . 5 ((𝜑𝐴 ≠ 0) → Σ𝑘 ∈ (ran 𝐹 ∖ {0})(𝑘 · (vol‘(𝐹 “ {𝑘}))) = Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})((𝑚 / 𝐴) · (vol‘(𝐹 “ {(𝑚 / 𝐴)}))))
16373, 162eqtrd 2861 . . . 4 ((𝜑𝐴 ≠ 0) → (∫1𝐹) = Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})((𝑚 / 𝐴) · (vol‘(𝐹 “ {(𝑚 / 𝐴)}))))
164163oveq2d 6921 . . 3 ((𝜑𝐴 ≠ 0) → (𝐴 · (∫1𝐹)) = (𝐴 · Σ𝑚 ∈ (ran ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∖ {0})((𝑚 / 𝐴) · (vol‘(𝐹 “ {(𝑚 / 𝐴)})))))
16568, 70, 1643eqtr4d 2871 . 2 ((𝜑𝐴 ≠ 0) → (∫1‘((ℝ × {𝐴}) ∘𝑓 · 𝐹)) = (𝐴 · (∫1𝐹)))
16626, 165pm2.61dane 3086 1 (𝜑 → (∫1‘((ℝ × {𝐴}) ∘𝑓 · 𝐹)) = (𝐴 · (∫1𝐹)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386   = wceq 1658  wcel 2166  wne 2999  wral 3117  Vcvv 3414  cdif 3795  wss 3798  {csn 4397  cmpt 4952   × cxp 5340  ccnv 5341  dom cdm 5342  ran crn 5343  cima 5345   Fn wfn 6118  wf 6119  cfv 6123  (class class class)co 6905  𝑓 cof 7155  Fincfn 8222  cc 10250  cr 10251  0cc0 10252   · cmul 10257   / cdiv 11009  Σcsu 14793  volcvol 23629  1citg1 23781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-inf2 8815  ax-cnex 10308  ax-resscn 10309  ax-1cn 10310  ax-icn 10311  ax-addcl 10312  ax-addrcl 10313  ax-mulcl 10314  ax-mulrcl 10315  ax-mulcom 10316  ax-addass 10317  ax-mulass 10318  ax-distr 10319  ax-i2m1 10320  ax-1ne0 10321  ax-1rid 10322  ax-rnegex 10323  ax-rrecex 10324  ax-cnre 10325  ax-pre-lttri 10326  ax-pre-lttrn 10327  ax-pre-ltadd 10328  ax-pre-mulgt0 10329  ax-pre-sup 10330
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-fal 1672  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-int 4698  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-se 5302  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-isom 6132  df-riota 6866  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-of 7157  df-om 7327  df-1st 7428  df-2nd 7429  df-wrecs 7672  df-recs 7734  df-rdg 7772  df-1o 7826  df-2o 7827  df-oadd 7830  df-er 8009  df-map 8124  df-pm 8125  df-en 8223  df-dom 8224  df-sdom 8225  df-fin 8226  df-sup 8617  df-inf 8618  df-oi 8684  df-card 9078  df-cda 9305  df-pnf 10393  df-mnf 10394  df-xr 10395  df-ltxr 10396  df-le 10397  df-sub 10587  df-neg 10588  df-div 11010  df-nn 11351  df-2 11414  df-3 11415  df-n0 11619  df-z 11705  df-uz 11969  df-q 12072  df-rp 12113  df-xadd 12233  df-ioo 12467  df-ico 12469  df-icc 12470  df-fz 12620  df-fzo 12761  df-fl 12888  df-seq 13096  df-exp 13155  df-hash 13411  df-cj 14216  df-re 14217  df-im 14218  df-sqrt 14352  df-abs 14353  df-clim 14596  df-sum 14794  df-xmet 20099  df-met 20100  df-ovol 23630  df-vol 23631  df-mbf 23785  df-itg1 23786
This theorem is referenced by:  itg1sub  23875  itg2const  23906  itg2mulclem  23912  itg2monolem1  23916  itg2addnclem  34004
  Copyright terms: Public domain W3C validator