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⁢∫ABdx=∫AC⁢Bdx

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 ⊢φ→ifx∈AB0∈0+∞
13 12 adantr ⊢φ∧x∈ℝ→ifx∈AB0∈0+∞
14 13 fmpttd ⊢φ→x∈ℝ⟼ifx∈AB0:ℝ⟶0+∞
15 5 7 iblpos ⊢φ→x∈A⟼B∈𝐿1↔x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈AB0∈ℝ
16 3 15 mpbid ⊢φ→x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈AB0∈ℝ
17 16 simprd ⊢φ→∫2⁡x∈ℝ⟼ifx∈AB0∈ℝ
18 elrege0 ⊢C∈0+∞↔C∈ℝ∧0≤C
19 4 6 18 sylanbrc ⊢φ→C∈0+∞
20 14 17 19 itg2mulc ⊢φ→∫2⁡ℝ×C×fx∈ℝ⟼ifx∈AB0=C⁢∫2⁡x∈ℝ⟼ifx∈AB0
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∈ℝ⟼ifx∈AB0=x∈ℝ⟼ifx∈AB0
27 22 23 13 25 26 offval2 ⊢φ→ℝ×C×fx∈ℝ⟼ifx∈AB0=x∈ℝ⟼C⁢ifx∈AB0
28 ovif2 ⊢C⁢ifx∈AB0=ifx∈AC⁢BC⋅0
29 1 mul01d ⊢φ→C⋅0=0
30 29 adantr ⊢φ∧x∈ℝ→C⋅0=0
31 30 ifeq2d ⊢φ∧x∈ℝ→ifx∈AC⁢BC⋅0=ifx∈AC⁢B0
32 28 31 eqtrid ⊢φ∧x∈ℝ→C⁢ifx∈AB0=ifx∈AC⁢B0
33 32 mpteq2dva ⊢φ→x∈ℝ⟼C⁢ifx∈AB0=x∈ℝ⟼ifx∈AC⁢B0
34 27 33 eqtrd ⊢φ→ℝ×C×fx∈ℝ⟼ifx∈AB0=x∈ℝ⟼ifx∈AC⁢B0
35 34 fveq2d ⊢φ→∫2⁡ℝ×C×fx∈ℝ⟼ifx∈AB0=∫2⁡x∈ℝ⟼ifx∈AC⁢B0
36 20 35 eqtr3d ⊢φ→C⁢∫2⁡x∈ℝ⟼ifx∈AB0=∫2⁡x∈ℝ⟼ifx∈AC⁢B0
37 5 3 7 itgposval ⊢φ→∫ABdx=∫2⁡x∈ℝ⟼ifx∈AB0
38 37 oveq2d ⊢φ→C⁢∫ABdx=C⁢∫2⁡x∈ℝ⟼ifx∈AB0
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 ⊢φ→∫AC⁢Bdx=∫2⁡x∈ℝ⟼ifx∈AC⁢B0
45 36 38 44 3eqtr4d ⊢φ→C⁢∫ABdx=∫AC⁢Bdx