Metamath Proof Explorer

Theorem itgmulc2lem1

Description: Lemma for itgmulc2 : positive real case. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses itgmulc2.1 ⊢ φ → C ∈ ℂ
itgmulc2.2 ⊢ φ ∧ x ∈ A → B ∈ V
itgmulc2.3 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
itgmulc2.4 ⊢ φ → C ∈ ℝ
itgmulc2.5 ⊢ φ ∧ x ∈ A → B ∈ ℝ
itgmulc2.6 ⊢ φ → 0 ≤ C
itgmulc2.7 ⊢ φ ∧ x ∈ A → 0 ≤ B
Assertion itgmulc2lem1 ⊢ φ → C ⁢ ∫ A B dx = ∫ A C ⁢ B dx

Proof

Step Hyp Ref Expression
1 itgmulc2.1 ⊢ φ → C ∈ ℂ
2 itgmulc2.2 ⊢ φ ∧ x ∈ A → B ∈ V
3 itgmulc2.3 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
4 itgmulc2.4 ⊢ φ → C ∈ ℝ
5 itgmulc2.5 ⊢ φ ∧ x ∈ A → B ∈ ℝ
6 itgmulc2.6 ⊢ φ → 0 ≤ C
7 itgmulc2.7 ⊢ φ ∧ x ∈ A → 0 ≤ B
8 elrege0 ⊢ B ∈ 0 +∞ ↔ B ∈ ℝ ∧ 0 ≤ B
9 5 7 8 sylanbrc ⊢ φ ∧ x ∈ A → B ∈ 0 +∞
10 0e0icopnf ⊢ 0 ∈ 0 +∞
11 10 a1i ⊢ φ ∧ ¬ x ∈ A → 0 ∈ 0 +∞
12 9 11 ifclda ⊢ φ → if x ∈ A B 0 ∈ 0 +∞
13 12 adantr ⊢ φ ∧ x ∈ ℝ → if x ∈ A B 0 ∈ 0 +∞
14 13 fmpttd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A B 0 : ℝ ⟶ 0 +∞
15 5 7 iblpos ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1 ↔ x ∈ A ⟼ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 ∈ ℝ
16 3 15 mpbid ⊢ φ → x ∈ A ⟼ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 ∈ ℝ
17 16 simprd ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 ∈ ℝ
18 elrege0 ⊢ C ∈ 0 +∞ ↔ C ∈ ℝ ∧ 0 ≤ C
19 4 6 18 sylanbrc ⊢ φ → C ∈ 0 +∞
20 14 17 19 itg2mulc ⊢ φ → ∫ 2 ⁡ ℝ × C × f x ∈ ℝ ⟼ if x ∈ A B 0 = C ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0
21 reex ⊢ ℝ ∈ V
22 21 a1i ⊢ φ → ℝ ∈ V
23 4 adantr ⊢ φ ∧ x ∈ ℝ → C ∈ ℝ
24 fconstmpt ⊢ ℝ × C = x ∈ ℝ ⟼ C
25 24 a1i ⊢ φ → ℝ × C = x ∈ ℝ ⟼ C
26 eqidd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A B 0 = x ∈ ℝ ⟼ if x ∈ A B 0
27 22 23 13 25 26 offval2 ⊢ φ → ℝ × C × f x ∈ ℝ ⟼ if x ∈ A B 0 = x ∈ ℝ ⟼ C ⁢ if x ∈ A B 0
28 ovif2 ⊢ C ⁢ if x ∈ A B 0 = if x ∈ A C ⁢ B C ⋅ 0
29 1 mul01d ⊢ φ → C ⋅ 0 = 0
30 29 adantr ⊢ φ ∧ x ∈ ℝ → C ⋅ 0 = 0
31 30 ifeq2d ⊢ φ ∧ x ∈ ℝ → if x ∈ A C ⁢ B C ⋅ 0 = if x ∈ A C ⁢ B 0
32 28 31 syl5eq ⊢ φ ∧ x ∈ ℝ → C ⁢ if x ∈ A B 0 = if x ∈ A C ⁢ B 0
33 32 mpteq2dva ⊢ φ → x ∈ ℝ ⟼ C ⁢ if x ∈ A B 0 = x ∈ ℝ ⟼ if x ∈ A C ⁢ B 0
34 27 33 eqtrd ⊢ φ → ℝ × C × f x ∈ ℝ ⟼ if x ∈ A B 0 = x ∈ ℝ ⟼ if x ∈ A C ⁢ B 0
35 34 fveq2d ⊢ φ → ∫ 2 ⁡ ℝ × C × f x ∈ ℝ ⟼ if x ∈ A B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A C ⁢ B 0
36 20 35 eqtr3d ⊢ φ → C ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A C ⁢ B 0
37 5 3 7 itgposval ⊢ φ → ∫ A B dx = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0
38 37 oveq2d ⊢ φ → C ⁢ ∫ A B dx = C ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0
39 4 adantr ⊢ φ ∧ x ∈ A → C ∈ ℝ
40 39 5 remulcld ⊢ φ ∧ x ∈ A → C ⁢ B ∈ ℝ
41 1 2 3 iblmulc2 ⊢ φ → x ∈ A ⟼ C ⁢ B ∈ 𝐿 1
42 6 adantr ⊢ φ ∧ x ∈ A → 0 ≤ C
43 39 5 42 7 mulge0d ⊢ φ ∧ x ∈ A → 0 ≤ C ⁢ B
44 40 41 43 itgposval ⊢ φ → ∫ A C ⁢ B dx = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A C ⁢ B 0
45 36 38 44 3eqtr4d ⊢ φ → C ⁢ ∫ A B dx = ∫ A C ⁢ B dx