Metamath Proof Explorer

Theorem itgmulc2nclem1

Description: Lemma for itgmulc2nc ; cf. itgmulc2lem1 . (Contributed by Brendan Leahy, 17-Nov-2017)

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

Proof

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