Metamath Proof Explorer

Theorem itgmulc2nclem2

Description: Lemma for itgmulc2nc ; cf. itgmulc2lem2 . (Contributed by Brendan Leahy, 19-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∈ℝ
Assertion itgmulc2nclem2 ⊢φ→C⁢∫ABdx=∫AC⁢Bdx

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 max0sub ⊢C∈ℝ→if0≤CC0−if0≤−C−C0=C
8 5 7 syl ⊢φ→if0≤CC0−if0≤−C−C0=C
9 8 oveq1d ⊢φ→if0≤CC0−if0≤−C−C0⁢B=C⁢B
10 9 adantr ⊢φ∧x∈A→if0≤CC0−if0≤−C−C0⁢B=C⁢B
11 0re ⊢0∈ℝ
12 ifcl ⊢C∈ℝ∧0∈ℝ→if0≤CC0∈ℝ
13 5 11 12 sylancl ⊢φ→if0≤CC0∈ℝ
14 13 recnd ⊢φ→if0≤CC0∈ℂ
15 14 adantr ⊢φ∧x∈A→if0≤CC0∈ℂ
16 5 renegcld ⊢φ→−C∈ℝ
17 ifcl ⊢−C∈ℝ∧0∈ℝ→if0≤−C−C0∈ℝ
18 16 11 17 sylancl ⊢φ→if0≤−C−C0∈ℝ
19 18 recnd ⊢φ→if0≤−C−C0∈ℂ
20 19 adantr ⊢φ∧x∈A→if0≤−C−C0∈ℂ
21 6 recnd ⊢φ∧x∈A→B∈ℂ
22 15 20 21 subdird ⊢φ∧x∈A→if0≤CC0−if0≤−C−C0⁢B=if0≤CC0⁢B−if0≤−C−C0⁢B
23 10 22 eqtr3d ⊢φ∧x∈A→C⁢B=if0≤CC0⁢B−if0≤−C−C0⁢B
24 23 itgeq2dv ⊢φ→∫AC⁢Bdx=∫Aif0≤CC0⁢B−if0≤−C−C0⁢Bdx
25 ovexd ⊢φ∧x∈A→if0≤CC0⁢B∈V
26 ovexd ⊢φ∧x∈A→C⁢B∈V
27 4 26 mbfdm2 ⊢φ→A∈dom⁡vol
28 13 adantr ⊢φ∧x∈A→if0≤CC0∈ℝ
29 fconstmpt ⊢A×if0≤CC0=x∈A⟼if0≤CC0
30 29 a1i ⊢φ→A×if0≤CC0=x∈A⟼if0≤CC0
31 eqidd ⊢φ→x∈A⟼B=x∈A⟼B
32 27 28 6 30 31 offval2 ⊢φ→A×if0≤CC0×fx∈A⟼B=x∈A⟼if0≤CC0⁢B
33 iblmbf ⊢x∈A⟼B∈𝐿1→x∈A⟼B∈MblFn
34 3 33 syl ⊢φ→x∈A⟼B∈MblFn
35 21 fmpttd ⊢φ→x∈A⟼B:A⟶ℂ
36 34 13 35 mbfmulc2re ⊢φ→A×if0≤CC0×fx∈A⟼B∈MblFn
37 32 36 eqeltrrd ⊢φ→x∈A⟼if0≤CC0⁢B∈MblFn
38 14 6 3 37 iblmulc2nc ⊢φ→x∈A⟼if0≤CC0⁢B∈𝐿1
39 ovexd ⊢φ∧x∈A→if0≤−C−C0⁢B∈V
40 18 adantr ⊢φ∧x∈A→if0≤−C−C0∈ℝ
41 fconstmpt ⊢A×if0≤−C−C0=x∈A⟼if0≤−C−C0
42 41 a1i ⊢φ→A×if0≤−C−C0=x∈A⟼if0≤−C−C0
43 27 40 6 42 31 offval2 ⊢φ→A×if0≤−C−C0×fx∈A⟼B=x∈A⟼if0≤−C−C0⁢B
44 34 18 35 mbfmulc2re ⊢φ→A×if0≤−C−C0×fx∈A⟼B∈MblFn
45 43 44 eqeltrrd ⊢φ→x∈A⟼if0≤−C−C0⁢B∈MblFn
46 19 6 3 45 iblmulc2nc ⊢φ→x∈A⟼if0≤−C−C0⁢B∈𝐿1
47 23 mpteq2dva ⊢φ→x∈A⟼C⁢B=x∈A⟼if0≤CC0⁢B−if0≤−C−C0⁢B
48 47 4 eqeltrrd ⊢φ→x∈A⟼if0≤CC0⁢B−if0≤−C−C0⁢B∈MblFn
49 25 38 39 46 48 itgsubnc ⊢φ→∫Aif0≤CC0⁢B−if0≤−C−C0⁢Bdx=∫Aif0≤CC0⁢Bdx−∫Aif0≤−C−C0⁢Bdx
50 ovexd ⊢φ∧x∈A→if0≤CC0⁢if0≤BB0∈V
51 ifcl ⊢B∈ℝ∧0∈ℝ→if0≤BB0∈ℝ
52 6 11 51 sylancl ⊢φ∧x∈A→if0≤BB0∈ℝ
53 6 iblre ⊢φ→x∈A⟼B∈𝐿1↔x∈A⟼if0≤BB0∈𝐿1∧x∈A⟼if0≤−B−B0∈𝐿1
54 3 53 mpbid ⊢φ→x∈A⟼if0≤BB0∈𝐿1∧x∈A⟼if0≤−B−B0∈𝐿1
55 54 simpld ⊢φ→x∈A⟼if0≤BB0∈𝐿1
56 eqidd ⊢φ→x∈A⟼if0≤BB0=x∈A⟼if0≤BB0
57 27 28 52 30 56 offval2 ⊢φ→A×if0≤CC0×fx∈A⟼if0≤BB0=x∈A⟼if0≤CC0⁢if0≤BB0
58 6 34 mbfpos ⊢φ→x∈A⟼if0≤BB0∈MblFn
59 52 recnd ⊢φ∧x∈A→if0≤BB0∈ℂ
60 59 fmpttd ⊢φ→x∈A⟼if0≤BB0:A⟶ℂ
61 58 13 60 mbfmulc2re ⊢φ→A×if0≤CC0×fx∈A⟼if0≤BB0∈MblFn
62 57 61 eqeltrrd ⊢φ→x∈A⟼if0≤CC0⁢if0≤BB0∈MblFn
63 14 52 55 62 iblmulc2nc ⊢φ→x∈A⟼if0≤CC0⁢if0≤BB0∈𝐿1
64 ovexd ⊢φ∧x∈A→if0≤CC0⁢if0≤−B−B0∈V
65 6 renegcld ⊢φ∧x∈A→−B∈ℝ
66 ifcl ⊢−B∈ℝ∧0∈ℝ→if0≤−B−B0∈ℝ
67 65 11 66 sylancl ⊢φ∧x∈A→if0≤−B−B0∈ℝ
68 54 simprd ⊢φ→x∈A⟼if0≤−B−B0∈𝐿1
69 eqidd ⊢φ→x∈A⟼if0≤−B−B0=x∈A⟼if0≤−B−B0
70 27 28 67 30 69 offval2 ⊢φ→A×if0≤CC0×fx∈A⟼if0≤−B−B0=x∈A⟼if0≤CC0⁢if0≤−B−B0
71 6 34 mbfneg ⊢φ→x∈A⟼−B∈MblFn
72 65 71 mbfpos ⊢φ→x∈A⟼if0≤−B−B0∈MblFn
73 67 recnd ⊢φ∧x∈A→if0≤−B−B0∈ℂ
74 73 fmpttd ⊢φ→x∈A⟼if0≤−B−B0:A⟶ℂ
75 72 13 74 mbfmulc2re ⊢φ→A×if0≤CC0×fx∈A⟼if0≤−B−B0∈MblFn
76 70 75 eqeltrrd ⊢φ→x∈A⟼if0≤CC0⁢if0≤−B−B0∈MblFn
77 14 67 68 76 iblmulc2nc ⊢φ→x∈A⟼if0≤CC0⁢if0≤−B−B0∈𝐿1
78 max0sub ⊢B∈ℝ→if0≤BB0−if0≤−B−B0=B
79 6 78 syl ⊢φ∧x∈A→if0≤BB0−if0≤−B−B0=B
80 79 oveq2d ⊢φ∧x∈A→if0≤CC0⁢if0≤BB0−if0≤−B−B0=if0≤CC0⁢B
81 15 59 73 subdid ⊢φ∧x∈A→if0≤CC0⁢if0≤BB0−if0≤−B−B0=if0≤CC0⁢if0≤BB0−if0≤CC0⁢if0≤−B−B0
82 80 81 eqtr3d ⊢φ∧x∈A→if0≤CC0⁢B=if0≤CC0⁢if0≤BB0−if0≤CC0⁢if0≤−B−B0
83 82 mpteq2dva ⊢φ→x∈A⟼if0≤CC0⁢B=x∈A⟼if0≤CC0⁢if0≤BB0−if0≤CC0⁢if0≤−B−B0
84 32 83 eqtrd ⊢φ→A×if0≤CC0×fx∈A⟼B=x∈A⟼if0≤CC0⁢if0≤BB0−if0≤CC0⁢if0≤−B−B0
85 84 36 eqeltrrd ⊢φ→x∈A⟼if0≤CC0⁢if0≤BB0−if0≤CC0⁢if0≤−B−B0∈MblFn
86 50 63 64 77 85 itgsubnc ⊢φ→∫Aif0≤CC0⁢if0≤BB0−if0≤CC0⁢if0≤−B−B0dx=∫Aif0≤CC0⁢if0≤BB0dx−∫Aif0≤CC0⁢if0≤−B−B0dx
87 82 itgeq2dv ⊢φ→∫Aif0≤CC0⁢Bdx=∫Aif0≤CC0⁢if0≤BB0−if0≤CC0⁢if0≤−B−B0dx
88 6 3 itgreval ⊢φ→∫ABdx=∫Aif0≤BB0dx−∫Aif0≤−B−B0dx
89 88 oveq2d ⊢φ→if0≤CC0⁢∫ABdx=if0≤CC0⁢∫Aif0≤BB0dx−∫Aif0≤−B−B0dx
90 52 55 itgcl ⊢φ→∫Aif0≤BB0dx∈ℂ
91 67 68 itgcl ⊢φ→∫Aif0≤−B−B0dx∈ℂ
92 14 90 91 subdid ⊢φ→if0≤CC0⁢∫Aif0≤BB0dx−∫Aif0≤−B−B0dx=if0≤CC0⁢∫Aif0≤BB0dx−if0≤CC0⁢∫Aif0≤−B−B0dx
93 max1 ⊢0∈ℝ∧C∈ℝ→0≤if0≤CC0
94 11 5 93 sylancr ⊢φ→0≤if0≤CC0
95 max1 ⊢0∈ℝ∧B∈ℝ→0≤if0≤BB0
96 11 6 95 sylancr ⊢φ∧x∈A→0≤if0≤BB0
97 14 52 55 62 13 52 94 96 itgmulc2nclem1 ⊢φ→if0≤CC0⁢∫Aif0≤BB0dx=∫Aif0≤CC0⁢if0≤BB0dx
98 max1 ⊢0∈ℝ∧−B∈ℝ→0≤if0≤−B−B0
99 11 65 98 sylancr ⊢φ∧x∈A→0≤if0≤−B−B0
100 14 67 68 76 13 67 94 99 itgmulc2nclem1 ⊢φ→if0≤CC0⁢∫Aif0≤−B−B0dx=∫Aif0≤CC0⁢if0≤−B−B0dx
101 97 100 oveq12d ⊢φ→if0≤CC0⁢∫Aif0≤BB0dx−if0≤CC0⁢∫Aif0≤−B−B0dx=∫Aif0≤CC0⁢if0≤BB0dx−∫Aif0≤CC0⁢if0≤−B−B0dx
102 89 92 101 3eqtrd ⊢φ→if0≤CC0⁢∫ABdx=∫Aif0≤CC0⁢if0≤BB0dx−∫Aif0≤CC0⁢if0≤−B−B0dx
103 86 87 102 3eqtr4d ⊢φ→∫Aif0≤CC0⁢Bdx=if0≤CC0⁢∫ABdx
104 ovexd ⊢φ∧x∈A→if0≤−C−C0⁢if0≤BB0∈V
105 27 40 52 42 56 offval2 ⊢φ→A×if0≤−C−C0×fx∈A⟼if0≤BB0=x∈A⟼if0≤−C−C0⁢if0≤BB0
106 58 18 60 mbfmulc2re ⊢φ→A×if0≤−C−C0×fx∈A⟼if0≤BB0∈MblFn
107 105 106 eqeltrrd ⊢φ→x∈A⟼if0≤−C−C0⁢if0≤BB0∈MblFn
108 19 52 55 107 iblmulc2nc ⊢φ→x∈A⟼if0≤−C−C0⁢if0≤BB0∈𝐿1
109 ovexd ⊢φ∧x∈A→if0≤−C−C0⁢if0≤−B−B0∈V
110 27 40 67 42 69 offval2 ⊢φ→A×if0≤−C−C0×fx∈A⟼if0≤−B−B0=x∈A⟼if0≤−C−C0⁢if0≤−B−B0
111 72 18 74 mbfmulc2re ⊢φ→A×if0≤−C−C0×fx∈A⟼if0≤−B−B0∈MblFn
112 110 111 eqeltrrd ⊢φ→x∈A⟼if0≤−C−C0⁢if0≤−B−B0∈MblFn
113 19 67 68 112 iblmulc2nc ⊢φ→x∈A⟼if0≤−C−C0⁢if0≤−B−B0∈𝐿1
114 79 oveq2d ⊢φ∧x∈A→if0≤−C−C0⁢if0≤BB0−if0≤−B−B0=if0≤−C−C0⁢B
115 20 59 73 subdid ⊢φ∧x∈A→if0≤−C−C0⁢if0≤BB0−if0≤−B−B0=if0≤−C−C0⁢if0≤BB0−if0≤−C−C0⁢if0≤−B−B0
116 114 115 eqtr3d ⊢φ∧x∈A→if0≤−C−C0⁢B=if0≤−C−C0⁢if0≤BB0−if0≤−C−C0⁢if0≤−B−B0
117 116 mpteq2dva ⊢φ→x∈A⟼if0≤−C−C0⁢B=x∈A⟼if0≤−C−C0⁢if0≤BB0−if0≤−C−C0⁢if0≤−B−B0
118 43 117 eqtrd ⊢φ→A×if0≤−C−C0×fx∈A⟼B=x∈A⟼if0≤−C−C0⁢if0≤BB0−if0≤−C−C0⁢if0≤−B−B0
119 118 44 eqeltrrd ⊢φ→x∈A⟼if0≤−C−C0⁢if0≤BB0−if0≤−C−C0⁢if0≤−B−B0∈MblFn
120 104 108 109 113 119 itgsubnc ⊢φ→∫Aif0≤−C−C0⁢if0≤BB0−if0≤−C−C0⁢if0≤−B−B0dx=∫Aif0≤−C−C0⁢if0≤BB0dx−∫Aif0≤−C−C0⁢if0≤−B−B0dx
121 116 itgeq2dv ⊢φ→∫Aif0≤−C−C0⁢Bdx=∫Aif0≤−C−C0⁢if0≤BB0−if0≤−C−C0⁢if0≤−B−B0dx
122 88 oveq2d ⊢φ→if0≤−C−C0⁢∫ABdx=if0≤−C−C0⁢∫Aif0≤BB0dx−∫Aif0≤−B−B0dx
123 19 90 91 subdid ⊢φ→if0≤−C−C0⁢∫Aif0≤BB0dx−∫Aif0≤−B−B0dx=if0≤−C−C0⁢∫Aif0≤BB0dx−if0≤−C−C0⁢∫Aif0≤−B−B0dx
124 max1 ⊢0∈ℝ∧−C∈ℝ→0≤if0≤−C−C0
125 11 16 124 sylancr ⊢φ→0≤if0≤−C−C0
126 19 52 55 107 18 52 125 96 itgmulc2nclem1 ⊢φ→if0≤−C−C0⁢∫Aif0≤BB0dx=∫Aif0≤−C−C0⁢if0≤BB0dx
127 19 67 68 112 18 67 125 99 itgmulc2nclem1 ⊢φ→if0≤−C−C0⁢∫Aif0≤−B−B0dx=∫Aif0≤−C−C0⁢if0≤−B−B0dx
128 126 127 oveq12d ⊢φ→if0≤−C−C0⁢∫Aif0≤BB0dx−if0≤−C−C0⁢∫Aif0≤−B−B0dx=∫Aif0≤−C−C0⁢if0≤BB0dx−∫Aif0≤−C−C0⁢if0≤−B−B0dx
129 122 123 128 3eqtrd ⊢φ→if0≤−C−C0⁢∫ABdx=∫Aif0≤−C−C0⁢if0≤BB0dx−∫Aif0≤−C−C0⁢if0≤−B−B0dx
130 120 121 129 3eqtr4d ⊢φ→∫Aif0≤−C−C0⁢Bdx=if0≤−C−C0⁢∫ABdx
131 103 130 oveq12d ⊢φ→∫Aif0≤CC0⁢Bdx−∫Aif0≤−C−C0⁢Bdx=if0≤CC0⁢∫ABdx−if0≤−C−C0⁢∫ABdx
132 6 3 itgcl ⊢φ→∫ABdx∈ℂ
133 14 19 132 subdird ⊢φ→if0≤CC0−if0≤−C−C0⁢∫ABdx=if0≤CC0⁢∫ABdx−if0≤−C−C0⁢∫ABdx
134 8 oveq1d ⊢φ→if0≤CC0−if0≤−C−C0⁢∫ABdx=C⁢∫ABdx
135 131 133 134 3eqtr2d ⊢φ→∫Aif0≤CC0⁢Bdx−∫Aif0≤−C−C0⁢Bdx=C⁢∫ABdx
136 24 49 135 3eqtrrd ⊢φ→C⁢∫ABdx=∫AC⁢Bdx