Metamath Proof Explorer


Theorem itgmulc2nc

Description: Choice-free analogue of itgmulc2 . (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
Assertion itgmulc2nc φ 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 1 recld φ C
6 5 recnd φ C
7 6 adantr φ x A C
8 iblmbf x A B 𝐿 1 x A B MblFn
9 3 8 syl φ x A B MblFn
10 9 2 mbfmptcl φ x A B
11 10 recld φ x A B
12 11 recnd φ x A B
13 7 12 mulcld φ x A C B
14 10 iblcn φ x A B 𝐿 1 x A B 𝐿 1 x A B 𝐿 1
15 3 14 mpbid φ x A B 𝐿 1 x A B 𝐿 1
16 15 simpld φ x A B 𝐿 1
17 ovexd φ x A C B V
18 4 17 mbfdm2 φ A dom vol
19 fconstmpt A × C = x A C
20 19 a1i φ A × C = x A C
21 eqidd φ x A B = x A B
22 18 7 11 20 21 offval2 φ A × C × f x A B = x A C B
23 iblmbf x A B 𝐿 1 x A B MblFn
24 16 23 syl φ x A B MblFn
25 12 fmpttd φ x A B : A
26 24 5 25 mbfmulc2re φ A × C × f x A B MblFn
27 22 26 eqeltrrd φ x A C B MblFn
28 6 11 16 27 iblmulc2nc φ x A C B 𝐿 1
29 13 28 itgcl φ A C B dx
30 ax-icn i
31 10 imcld φ x A B
32 31 recnd φ x A B
33 7 32 mulcld φ x A C B
34 15 simprd φ x A B 𝐿 1
35 eqidd φ x A B = x A B
36 18 7 31 20 35 offval2 φ A × C × f x A B = x A C B
37 iblmbf x A B 𝐿 1 x A B MblFn
38 34 37 syl φ x A B MblFn
39 32 fmpttd φ x A B : A
40 38 5 39 mbfmulc2re φ A × C × f x A B MblFn
41 36 40 eqeltrrd φ x A C B MblFn
42 6 31 34 41 iblmulc2nc φ x A C B 𝐿 1
43 33 42 itgcl φ A C B dx
44 mulcl i A C B dx i A C B dx
45 30 43 44 sylancr φ i A C B dx
46 1 imcld φ C
47 46 recnd φ C
48 47 negcld φ C
49 48 adantr φ x A C
50 49 32 mulcld φ x A C B
51 fconstmpt A × C = x A C
52 51 a1i φ A × C = x A C
53 18 49 31 52 35 offval2 φ A × C × f x A B = x A C B
54 46 renegcld φ C
55 38 54 39 mbfmulc2re φ A × C × f x A B MblFn
56 53 55 eqeltrrd φ x A C B MblFn
57 48 31 34 56 iblmulc2nc φ x A C B 𝐿 1
58 50 57 itgcl φ A C B dx
59 47 adantr φ x A C
60 59 12 mulcld φ x A C B
61 fconstmpt A × C = x A C
62 61 a1i φ A × C = x A C
63 18 59 11 62 21 offval2 φ A × C × f x A B = x A C B
64 24 46 25 mbfmulc2re φ A × C × f x A B MblFn
65 63 64 eqeltrrd φ x A C B MblFn
66 47 11 16 65 iblmulc2nc φ x A C B 𝐿 1
67 60 66 itgcl φ A C B dx
68 mulcl i A C B dx i A C B dx
69 30 67 68 sylancr φ i A C B dx
70 29 45 58 69 add4d φ A C B dx + i A C B dx + A C B dx + i A C B dx = A C B dx + A C B dx + i A C B dx + i A C B dx
71 30 a1i φ i
72 71 47 mulcld φ i C
73 2 3 itgcl φ A B dx
74 6 72 73 adddird φ C + i C A B dx = C A B dx + i C A B dx
75 2 3 itgcnval φ A B dx = A B dx + i A B dx
76 75 oveq2d φ C A B dx = C A B dx + i A B dx
77 11 16 itgcl φ A B dx
78 31 34 itgcl φ A B dx
79 mulcl i A B dx i A B dx
80 30 78 79 sylancr φ i A B dx
81 6 77 80 adddid φ C A B dx + i A B dx = C A B dx + C i A B dx
82 6 11 16 27 5 11 itgmulc2nclem2 φ C A B dx = A C B dx
83 6 71 78 mul12d φ C i A B dx = i C A B dx
84 6 31 34 41 5 31 itgmulc2nclem2 φ C A B dx = A C B dx
85 84 oveq2d φ i C A B dx = i A C B dx
86 83 85 eqtrd φ C i A B dx = i A C B dx
87 82 86 oveq12d φ C A B dx + C i A B dx = A C B dx + i A C B dx
88 76 81 87 3eqtrd φ C A B dx = A C B dx + i A C B dx
89 75 oveq2d φ i C A B dx = i C A B dx + i A B dx
90 72 77 80 adddid φ i C A B dx + i A B dx = i C A B dx + i C i A B dx
91 71 47 77 mulassd φ i C A B dx = i C A B dx
92 47 11 16 65 46 11 itgmulc2nclem2 φ C A B dx = A C B dx
93 92 oveq2d φ i C A B dx = i A C B dx
94 91 93 eqtrd φ i C A B dx = i A C B dx
95 71 47 71 78 mul4d φ i C i A B dx = i i C A B dx
96 ixi i i = 1
97 96 oveq1i i i C A B dx = -1 C A B dx
98 47 78 mulcld φ C A B dx
99 98 mulm1d φ -1 C A B dx = C A B dx
100 97 99 syl5eq φ i i C A B dx = C A B dx
101 47 78 mulneg1d φ C A B dx = C A B dx
102 48 31 34 56 54 31 itgmulc2nclem2 φ C A B dx = A C B dx
103 101 102 eqtr3d φ C A B dx = A C B dx
104 95 100 103 3eqtrd φ i C i A B dx = A C B dx
105 94 104 oveq12d φ i C A B dx + i C i A B dx = i A C B dx + A C B dx
106 69 58 addcomd φ i A C B dx + A C B dx = A C B dx + i A C B dx
107 105 106 eqtrd φ i C A B dx + i C i A B dx = A C B dx + i A C B dx
108 89 90 107 3eqtrd φ i C A B dx = A C B dx + i A C B dx
109 88 108 oveq12d φ C A B dx + i C A B dx = A C B dx + i A C B dx + A C B dx + i A C B dx
110 74 109 eqtrd φ C + i C A B dx = A C B dx + i A C B dx + A C B dx + i A C B dx
111 59 32 mulcld φ x A C B
112 18 59 31 62 35 offval2 φ A × C × f x A B = x A C B
113 38 46 39 mbfmulc2re φ A × C × f x A B MblFn
114 112 113 eqeltrrd φ x A C B MblFn
115 47 31 34 114 iblmulc2nc φ x A C B 𝐿 1
116 1 adantr φ x A C
117 116 10 mulcld φ x A C B
118 eqidd φ x A C B = x A C B
119 ref :
120 119 a1i φ :
121 120 feqmptd φ = k k
122 fveq2 k = C B k = C B
123 117 118 121 122 fmptco φ x A C B = x A C B
124 116 10 remuld φ x A C B = C B C B
125 124 mpteq2dva φ x A C B = x A C B C B
126 123 125 eqtrd φ x A C B = x A C B C B
127 117 fmpttd φ x A C B : A
128 ismbfcn x A C B : A x A C B MblFn x A C B MblFn x A C B MblFn
129 127 128 syl φ x A C B MblFn x A C B MblFn x A C B MblFn
130 4 129 mpbid φ x A C B MblFn x A C B MblFn
131 130 simpld φ x A C B MblFn
132 126 131 eqeltrrd φ x A C B C B MblFn
133 13 28 111 115 132 itgsubnc φ A C B C B dx = A C B dx A C B dx
134 124 itgeq2dv φ A C B dx = A C B C B dx
135 111 115 itgneg φ A C B dx = A C B dx
136 59 32 mulneg1d φ x A C B = C B
137 136 itgeq2dv φ A C B dx = A C B dx
138 135 137 eqtr4d φ A C B dx = A C B dx
139 138 oveq2d φ A C B dx + A C B dx = A C B dx + A C B dx
140 111 115 itgcl φ A C B dx
141 29 140 negsubd φ A C B dx + A C B dx = A C B dx A C B dx
142 139 141 eqtr3d φ A C B dx + A C B dx = A C B dx A C B dx
143 133 134 142 3eqtr4d φ A C B dx = A C B dx + A C B dx
144 116 10 immuld φ x A C B = C B + C B
145 144 itgeq2dv φ A C B dx = A C B + C B dx
146 imf :
147 146 a1i φ :
148 147 feqmptd φ = k k
149 fveq2 k = C B k = C B
150 117 118 148 149 fmptco φ x A C B = x A C B
151 144 mpteq2dva φ x A C B = x A C B + C B
152 150 151 eqtrd φ x A C B = x A C B + C B
153 130 simprd φ x A C B MblFn
154 152 153 eqeltrrd φ x A C B + C B MblFn
155 33 42 60 66 154 itgaddnc φ A C B + C B dx = A C B dx + A C B dx
156 145 155 eqtrd φ A C B dx = A C B dx + A C B dx
157 156 oveq2d φ i A C B dx = i A C B dx + A C B dx
158 71 43 67 adddid φ i A C B dx + A C B dx = i A C B dx + i A C B dx
159 157 158 eqtrd φ i A C B dx = i A C B dx + i A C B dx
160 143 159 oveq12d φ A C B dx + i A C B dx = A C B dx + A C B dx + i A C B dx + i A C B dx
161 70 110 160 3eqtr4d φ C + i C A B dx = A C B dx + i A C B dx
162 1 replimd φ C = C + i C
163 162 oveq1d φ C A B dx = C + i C A B dx
164 1 2 3 4 iblmulc2nc φ x A C B 𝐿 1
165 117 164 itgcnval φ A C B dx = A C B dx + i A C B dx
166 161 163 165 3eqtr4d φ C A B dx = A C B dx