Theorem itgmulc2nclem2 28600

Description: Lemma for itgmulc2nc 28601; cf. itgmulc2lem2 21436. (Contributed by Brendan Leahy, 19-Nov-2017.)

Hypotheses

Ref	Expression
itgmulc2nc.1	|- ( ph -> C e. CC )
itgmulc2nc.2	|- ( ( ph /\ x e. A ) -> B e. V )
itgmulc2nc.3	|- ( ph -> ( x e. A |-> B ) e. L^1 )
itgmulc2nc.m	|- ( ph -> ( x e. A |-> ( C x. B ) ) e. MblFn )
itgmulc2nc.4	|- ( ph -> C e. RR )
itgmulc2nc.5	|- ( ( ph /\ x e. A ) -> B e. RR )

Assertion

Ref	Expression
itgmulc2nclem2	|- ( ph -> ( C x. S. A B _d x ) = S. A ( C x. B ) _d x )

Distinct variable groups:   x, A   x, C   ph, x   x, V

Allowed substitution hint:   B( x)

Proof of Theorem itgmulc2nclem2

Step	Hyp	Ref	Expression
1		itgmulc2nc.4	. . . . . . 7 |- ( ph -> C e. RR )
2		max0sub 11270	. . . . . . 7 |- ( C e. RR -> ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) = C )
3	1, 2	syl 16	. . . . . 6 |- ( ph -> ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) = C )
4	3	oveq1d 6208	. . . . 5 |- ( ph -> ( ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) x. B ) = ( C x. B ) )
5	4	adantr 465	. . . 4 |- ( ( ph /\ x e. A ) -> ( ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) x. B ) = ( C x. B ) )
6		0re 9490	. . . . . . . 8 |- 0 e. RR
7		ifcl 3932	. . . . . . . 8 |- ( ( C e. RR /\ 0 e. RR ) -> if ( 0 <_ C , C , 0 ) e. RR )
8	1, 6, 7	sylancl 662	. . . . . . 7 |- ( ph -> if ( 0 <_ C , C , 0 ) e. RR )
9	8	recnd 9516	. . . . . 6 |- ( ph -> if ( 0 <_ C , C , 0 ) e. CC )
10	9	adantr 465	. . . . 5 |- ( ( ph /\ x e. A ) -> if ( 0 <_ C , C , 0 ) e. CC )
11	1	renegcld 9879	. . . . . . . 8 |- ( ph -> -u C e. RR )
12		ifcl 3932	. . . . . . . 8 |- ( ( -u C e. RR /\ 0 e. RR ) -> if ( 0 <_ -u C , -u C , 0 ) e. RR )
13	11, 6, 12	sylancl 662	. . . . . . 7 |- ( ph -> if ( 0 <_ -u C , -u C , 0 ) e. RR )
14	13	recnd 9516	. . . . . 6 |- ( ph -> if ( 0 <_ -u C , -u C , 0 ) e. CC )
15	14	adantr 465	. . . . 5 |- ( ( ph /\ x e. A ) -> if ( 0 <_ -u C , -u C , 0 ) e. CC )
16		itgmulc2nc.5	. . . . . 6 |- ( ( ph /\ x e. A ) -> B e. RR )
17	16	recnd 9516	. . . . 5 |- ( ( ph /\ x e. A ) -> B e. CC )
18	10, 15, 17	subdird 9905	. . . 4 |- ( ( ph /\ x e. A ) -> ( ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) x. B ) = ( ( if ( 0 <_ C , C , 0 ) x. B ) - ( if ( 0 <_ -u C , -u C , 0 ) x. B ) ) )
19	5, 18	eqtr3d 2494	. . 3 |- ( ( ph /\ x e. A ) -> ( C x. B ) = ( ( if ( 0 <_ C , C , 0 ) x. B ) - ( if ( 0 <_ -u C , -u C , 0 ) x. B ) ) )
20	19	itgeq2dv 21385	. 2 |- ( ph -> S. A ( C x. B ) _d x = S. A ( ( if ( 0 <_ C , C , 0 ) x. B ) - ( if ( 0 <_ -u C , -u C , 0 ) x. B ) ) _d x )
21		ovex 6218	. . . 4 |- ( if ( 0 <_ C , C , 0 ) x. B ) e. _V
22	21	a1i 11	. . 3 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ C , C , 0 ) x. B ) e. _V )
23		itgmulc2nc.3	. . . 4 |- ( ph -> ( x e. A |-> B ) e. L^1 )
24		itgmulc2nc.m	. . . . . . 7 |- ( ph -> ( x e. A |-> ( C x. B ) ) e. MblFn )
25		ovex 6218	. . . . . . . 8 |- ( C x. B ) e. _V
26	25	a1i 11	. . . . . . 7 |- ( ( ph /\ x e. A ) -> ( C x. B ) e. _V )
27	24, 26	mbfdm2 21242	. . . . . 6 |- ( ph -> A e. dom vol )
28	8	adantr 465	. . . . . 6 |- ( ( ph /\ x e. A ) -> if ( 0 <_ C , C , 0 ) e. RR )
29		fconstmpt 4983	. . . . . . 7 |- ( A X. { if ( 0 <_ C , C , 0 ) } ) = ( x e. A |-> if ( 0 <_ C , C , 0 ) )
30	29	a1i 11	. . . . . 6 |- ( ph -> ( A X. { if ( 0 <_ C , C , 0 ) } ) = ( x e. A |-> if ( 0 <_ C , C , 0 ) ) )
31		eqidd 2452	. . . . . 6 |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> B ) )
32	27, 28, 16, 30, 31	offval2 6439	. . . . 5 |- ( ph -> ( ( A X. { if ( 0 <_ C , C , 0 ) } ) oF x. ( x e. A |-> B ) ) = ( x e. A |-> ( if ( 0 <_ C , C , 0 ) x. B ) ) )
33		iblmbf 21371	. . . . . . 7 |- ( ( x e. A |-> B ) e. L^1 -> ( x e. A |-> B ) e. MblFn )
34	23, 33	syl 16	. . . . . 6 |- ( ph -> ( x e. A |-> B ) e. MblFn )
35		eqid 2451	. . . . . . 7 |- ( x e. A |-> B ) = ( x e. A |-> B )
36	17, 35	fmptd 5969	. . . . . 6 |- ( ph -> ( x e. A |-> B ) : A --> CC )
37	34, 8, 36	mbfmulc2re 21252	. . . . 5 |- ( ph -> ( ( A X. { if ( 0 <_ C , C , 0 ) } ) oF x. ( x e. A |-> B ) ) e. MblFn )
38	32, 37	eqeltrrd 2540	. . . 4 |- ( ph -> ( x e. A |-> ( if ( 0 <_ C , C , 0 ) x. B ) ) e. MblFn )
39	9, 16, 23, 38	iblmulc2nc 28598	. . 3 |- ( ph -> ( x e. A |-> ( if ( 0 <_ C , C , 0 ) x. B ) ) e. L^1 )
40		ovex 6218	. . . 4 |- ( if ( 0 <_ -u C , -u C , 0 ) x. B ) e. _V
41	40	a1i 11	. . 3 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ -u C , -u C , 0 ) x. B ) e. _V )
42	13	adantr 465	. . . . . 6 |- ( ( ph /\ x e. A ) -> if ( 0 <_ -u C , -u C , 0 ) e. RR )
43		fconstmpt 4983	. . . . . . 7 |- ( A X. { if ( 0 <_ -u C , -u C , 0 ) } ) = ( x e. A |-> if ( 0 <_ -u C , -u C , 0 ) )
44	43	a1i 11	. . . . . 6 |- ( ph -> ( A X. { if ( 0 <_ -u C , -u C , 0 ) } ) = ( x e. A |-> if ( 0 <_ -u C , -u C , 0 ) ) )
45	27, 42, 16, 44, 31	offval2 6439	. . . . 5 |- ( ph -> ( ( A X. { if ( 0 <_ -u C , -u C , 0 ) } ) oF x. ( x e. A |-> B ) ) = ( x e. A |-> ( if ( 0 <_ -u C , -u C , 0 ) x. B ) ) )
46	34, 13, 36	mbfmulc2re 21252	. . . . 5 |- ( ph -> ( ( A X. { if ( 0 <_ -u C , -u C , 0 ) } ) oF x. ( x e. A |-> B ) ) e. MblFn )
47	45, 46	eqeltrrd 2540	. . . 4 |- ( ph -> ( x e. A |-> ( if ( 0 <_ -u C , -u C , 0 ) x. B ) ) e. MblFn )
48	14, 16, 23, 47	iblmulc2nc 28598	. . 3 |- ( ph -> ( x e. A |-> ( if ( 0 <_ -u C , -u C , 0 ) x. B ) ) e. L^1 )
49	19	mpteq2dva 4479	. . . 4 |- ( ph -> ( x e. A |-> ( C x. B ) ) = ( x e. A |-> ( ( if ( 0 <_ C , C , 0 ) x. B ) - ( if ( 0 <_ -u C , -u C , 0 ) x. B ) ) ) )
50	49, 24	eqeltrrd 2540	. . 3 |- ( ph -> ( x e. A |-> ( ( if ( 0 <_ C , C , 0 ) x. B ) - ( if ( 0 <_ -u C , -u C , 0 ) x. B ) ) ) e. MblFn )
51	22, 39, 41, 48, 50	itgsubnc 28595	. 2 |- ( ph -> S. A ( ( if ( 0 <_ C , C , 0 ) x. B ) - ( if ( 0 <_ -u C , -u C , 0 ) x. B ) ) _d x = ( S. A ( if ( 0 <_ C , C , 0 ) x. B ) _d x - S. A ( if ( 0 <_ -u C , -u C , 0 ) x. B ) _d x ) )
52		ovex 6218	. . . . . . 7 |- ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) e. _V
53	52	a1i 11	. . . . . 6 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) e. _V )
54		ifcl 3932	. . . . . . . 8 |- ( ( B e. RR /\ 0 e. RR ) -> if ( 0 <_ B , B , 0 ) e. RR )
55	16, 6, 54	sylancl 662	. . . . . . 7 |- ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. RR )
56	16	iblre 21397	. . . . . . . . 9 |- ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. L^1 /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. L^1 ) ) )
57	23, 56	mpbid 210	. . . . . . . 8 |- ( ph -> ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. L^1 /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. L^1 ) )
58	57	simpld 459	. . . . . . 7 |- ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. L^1 )
59		eqidd 2452	. . . . . . . . 9 |- ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) = ( x e. A |-> if ( 0 <_ B , B , 0 ) ) )
60	27, 28, 55, 30, 59	offval2 6439	. . . . . . . 8 |- ( ph -> ( ( A X. { if ( 0 <_ C , C , 0 ) } ) oF x. ( x e. A |-> if ( 0 <_ B , B , 0 ) ) ) = ( x e. A |-> ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) ) )
61	16, 34	mbfpos 21255	. . . . . . . . 9 |- ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn )
62	55	recnd 9516	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. CC )
63		eqid 2451	. . . . . . . . . 10 |- ( x e. A |-> if ( 0 <_ B , B , 0 ) ) = ( x e. A |-> if ( 0 <_ B , B , 0 ) )
64	62, 63	fmptd 5969	. . . . . . . . 9 |- ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) : A --> CC )
65	61, 8, 64	mbfmulc2re 21252	. . . . . . . 8 |- ( ph -> ( ( A X. { if ( 0 <_ C , C , 0 ) } ) oF x. ( x e. A |-> if ( 0 <_ B , B , 0 ) ) ) e. MblFn )
66	60, 65	eqeltrrd 2540	. . . . . . 7 |- ( ph -> ( x e. A |-> ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) ) e. MblFn )
67	9, 55, 58, 66	iblmulc2nc 28598	. . . . . 6 |- ( ph -> ( x e. A |-> ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) ) e. L^1 )
68		ovex 6218	. . . . . . 7 |- ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) e. _V
69	68	a1i 11	. . . . . 6 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) e. _V )
70	16	renegcld 9879	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> -u B e. RR )
71		ifcl 3932	. . . . . . . 8 |- ( ( -u B e. RR /\ 0 e. RR ) -> if ( 0 <_ -u B , -u B , 0 ) e. RR )
72	70, 6, 71	sylancl 662	. . . . . . 7 |- ( ( ph /\ x e. A ) -> if ( 0 <_ -u B , -u B , 0 ) e. RR )
73	57	simprd 463	. . . . . . 7 |- ( ph -> ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. L^1 )
74		eqidd 2452	. . . . . . . . 9 |- ( ph -> ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) = ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) )
75	27, 28, 72, 30, 74	offval2 6439	. . . . . . . 8 |- ( ph -> ( ( A X. { if ( 0 <_ C , C , 0 ) } ) oF x. ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) ) = ( x e. A |-> ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) )
76	16, 34	mbfneg 21254	. . . . . . . . . 10 |- ( ph -> ( x e. A |-> -u B ) e. MblFn )
77	70, 76	mbfpos 21255	. . . . . . . . 9 |- ( ph -> ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn )
78	72	recnd 9516	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> if ( 0 <_ -u B , -u B , 0 ) e. CC )
79		eqid 2451	. . . . . . . . . 10 |- ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) = ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) )
80	78, 79	fmptd 5969	. . . . . . . . 9 |- ( ph -> ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) : A --> CC )
81	77, 8, 80	mbfmulc2re 21252	. . . . . . . 8 |- ( ph -> ( ( A X. { if ( 0 <_ C , C , 0 ) } ) oF x. ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) ) e. MblFn )
82	75, 81	eqeltrrd 2540	. . . . . . 7 |- ( ph -> ( x e. A |-> ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) e. MblFn )
83	9, 72, 73, 82	iblmulc2nc 28598	. . . . . 6 |- ( ph -> ( x e. A |-> ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) e. L^1 )
84		max0sub 11270	. . . . . . . . . . . 12 |- ( B e. RR -> ( if ( 0 <_ B , B , 0 ) - if ( 0 <_ -u B , -u B , 0 ) ) = B )
85	16, 84	syl 16	. . . . . . . . . . 11 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) - if ( 0 <_ -u B , -u B , 0 ) ) = B )
86	85	oveq2d 6209	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ C , C , 0 ) x. ( if ( 0 <_ B , B , 0 ) - if ( 0 <_ -u B , -u B , 0 ) ) ) = ( if ( 0 <_ C , C , 0 ) x. B ) )
87	10, 62, 78	subdid 9904	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ C , C , 0 ) x. ( if ( 0 <_ B , B , 0 ) - if ( 0 <_ -u B , -u B , 0 ) ) ) = ( ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) - ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) )
88	86, 87	eqtr3d 2494	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ C , C , 0 ) x. B ) = ( ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) - ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) )
89	88	mpteq2dva 4479	. . . . . . . 8 |- ( ph -> ( x e. A |-> ( if ( 0 <_ C , C , 0 ) x. B ) ) = ( x e. A |-> ( ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) - ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) ) )
90	32, 89	eqtrd 2492	. . . . . . 7 |- ( ph -> ( ( A X. { if ( 0 <_ C , C , 0 ) } ) oF x. ( x e. A |-> B ) ) = ( x e. A |-> ( ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) - ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) ) )
91	90, 37	eqeltrrd 2540	. . . . . 6 |- ( ph -> ( x e. A |-> ( ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) - ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) ) e. MblFn )
92	53, 67, 69, 83, 91	itgsubnc 28595	. . . . 5 |- ( ph -> S. A ( ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) - ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) _d x = ( S. A ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) _d x - S. A ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) _d x ) )
93	88	itgeq2dv 21385	. . . . 5 |- ( ph -> S. A ( if ( 0 <_ C , C , 0 ) x. B ) _d x = S. A ( ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) - ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) _d x )
94	16, 23	itgreval 21400	. . . . . . 7 |- ( ph -> S. A B _d x = ( S. A if ( 0 <_ B , B , 0 ) _d x - S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) )
95	94	oveq2d 6209	. . . . . 6 |- ( ph -> ( if ( 0 <_ C , C , 0 ) x. S. A B _d x ) = ( if ( 0 <_ C , C , 0 ) x. ( S. A if ( 0 <_ B , B , 0 ) _d x - S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) ) )
96	55, 58	itgcl 21387	. . . . . . 7 |- ( ph -> S. A if ( 0 <_ B , B , 0 ) _d x e. CC )
97	72, 73	itgcl 21387	. . . . . . 7 |- ( ph -> S. A if ( 0 <_ -u B , -u B , 0 ) _d x e. CC )
98	9, 96, 97	subdid 9904	. . . . . 6 |- ( ph -> ( if ( 0 <_ C , C , 0 ) x. ( S. A if ( 0 <_ B , B , 0 ) _d x - S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) ) = ( ( if ( 0 <_ C , C , 0 ) x. S. A if ( 0 <_ B , B , 0 ) _d x ) - ( if ( 0 <_ C , C , 0 ) x. S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) ) )
99		max1 11261	. . . . . . . . 9 |- ( ( 0 e. RR /\ C e. RR ) -> 0 <_ if ( 0 <_ C , C , 0 ) )
100	6, 1, 99	sylancr 663	. . . . . . . 8 |- ( ph -> 0 <_ if ( 0 <_ C , C , 0 ) )
101		max1 11261	. . . . . . . . 9 |- ( ( 0 e. RR /\ B e. RR ) -> 0 <_ if ( 0 <_ B , B , 0 ) )
102	6, 16, 101	sylancr 663	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ B , B , 0 ) )
103	9, 55, 58, 66, 8, 55, 100, 102	itgmulc2nclem1 28599	. . . . . . 7 |- ( ph -> ( if ( 0 <_ C , C , 0 ) x. S. A if ( 0 <_ B , B , 0 ) _d x ) = S. A ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) _d x )
104		max1 11261	. . . . . . . . 9 |- ( ( 0 e. RR /\ -u B e. RR ) -> 0 <_ if ( 0 <_ -u B , -u B , 0 ) )
105	6, 70, 104	sylancr 663	. . . . . . . 8 |- ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ -u B , -u B , 0 ) )
106	9, 72, 73, 82, 8, 72, 100, 105	itgmulc2nclem1 28599	. . . . . . 7 |- ( ph -> ( if ( 0 <_ C , C , 0 ) x. S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) = S. A ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) _d x )
107	103, 106	oveq12d 6211	. . . . . 6 |- ( ph -> ( ( if ( 0 <_ C , C , 0 ) x. S. A if ( 0 <_ B , B , 0 ) _d x ) - ( if ( 0 <_ C , C , 0 ) x. S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) ) = ( S. A ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) _d x - S. A ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) _d x ) )
108	95, 98, 107	3eqtrd 2496	. . . . 5 |- ( ph -> ( if ( 0 <_ C , C , 0 ) x. S. A B _d x ) = ( S. A ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) _d x - S. A ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) _d x ) )
109	92, 93, 108	3eqtr4d 2502	. . . 4 |- ( ph -> S. A ( if ( 0 <_ C , C , 0 ) x. B ) _d x = ( if ( 0 <_ C , C , 0 ) x. S. A B _d x ) )
110		ovex 6218	. . . . . . 7 |- ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) e. _V
111	110	a1i 11	. . . . . 6 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) e. _V )
112	27, 42, 55, 44, 59	offval2 6439	. . . . . . . 8 |- ( ph -> ( ( A X. { if ( 0 <_ -u C , -u C , 0 ) } ) oF x. ( x e. A |-> if ( 0 <_ B , B , 0 ) ) ) = ( x e. A |-> ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) ) )
113	61, 13, 64	mbfmulc2re 21252	. . . . . . . 8 |- ( ph -> ( ( A X. { if ( 0 <_ -u C , -u C , 0 ) } ) oF x. ( x e. A |-> if ( 0 <_ B , B , 0 ) ) ) e. MblFn )
114	112, 113	eqeltrrd 2540	. . . . . . 7 |- ( ph -> ( x e. A |-> ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) ) e. MblFn )
115	14, 55, 58, 114	iblmulc2nc 28598	. . . . . 6 |- ( ph -> ( x e. A |-> ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) ) e. L^1 )
116		ovex 6218	. . . . . . 7 |- ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) e. _V
117	116	a1i 11	. . . . . 6 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) e. _V )
118	27, 42, 72, 44, 74	offval2 6439	. . . . . . . 8 |- ( ph -> ( ( A X. { if ( 0 <_ -u C , -u C , 0 ) } ) oF x. ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) ) = ( x e. A |-> ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) )
119	77, 13, 80	mbfmulc2re 21252	. . . . . . . 8 |- ( ph -> ( ( A X. { if ( 0 <_ -u C , -u C , 0 ) } ) oF x. ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) ) e. MblFn )
120	118, 119	eqeltrrd 2540	. . . . . . 7 |- ( ph -> ( x e. A |-> ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) e. MblFn )
121	14, 72, 73, 120	iblmulc2nc 28598	. . . . . 6 |- ( ph -> ( x e. A |-> ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) e. L^1 )
122	85	oveq2d 6209	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ -u C , -u C , 0 ) x. ( if ( 0 <_ B , B , 0 ) - if ( 0 <_ -u B , -u B , 0 ) ) ) = ( if ( 0 <_ -u C , -u C , 0 ) x. B ) )
123	15, 62, 78	subdid 9904	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ -u C , -u C , 0 ) x. ( if ( 0 <_ B , B , 0 ) - if ( 0 <_ -u B , -u B , 0 ) ) ) = ( ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) - ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) )
124	122, 123	eqtr3d 2494	. . . . . . . . 9 |- ( ( ph /\ x e. A ) -> ( if ( 0 <_ -u C , -u C , 0 ) x. B ) = ( ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) - ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) )
125	124	mpteq2dva 4479	. . . . . . . 8 |- ( ph -> ( x e. A |-> ( if ( 0 <_ -u C , -u C , 0 ) x. B ) ) = ( x e. A |-> ( ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) - ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) ) )
126	45, 125	eqtrd 2492	. . . . . . 7 |- ( ph -> ( ( A X. { if ( 0 <_ -u C , -u C , 0 ) } ) oF x. ( x e. A |-> B ) ) = ( x e. A |-> ( ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) - ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) ) )
127	126, 46	eqeltrrd 2540	. . . . . 6 |- ( ph -> ( x e. A |-> ( ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) - ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) ) e. MblFn )
128	111, 115, 117, 121, 127	itgsubnc 28595	. . . . 5 |- ( ph -> S. A ( ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) - ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) _d x = ( S. A ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) _d x - S. A ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) _d x ) )
129	124	itgeq2dv 21385	. . . . 5 |- ( ph -> S. A ( if ( 0 <_ -u C , -u C , 0 ) x. B ) _d x = S. A ( ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) - ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) _d x )
130	94	oveq2d 6209	. . . . . 6 |- ( ph -> ( if ( 0 <_ -u C , -u C , 0 ) x. S. A B _d x ) = ( if ( 0 <_ -u C , -u C , 0 ) x. ( S. A if ( 0 <_ B , B , 0 ) _d x - S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) ) )
131	14, 96, 97	subdid 9904	. . . . . 6 |- ( ph -> ( if ( 0 <_ -u C , -u C , 0 ) x. ( S. A if ( 0 <_ B , B , 0 ) _d x - S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) ) = ( ( if ( 0 <_ -u C , -u C , 0 ) x. S. A if ( 0 <_ B , B , 0 ) _d x ) - ( if ( 0 <_ -u C , -u C , 0 ) x. S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) ) )
132		max1 11261	. . . . . . . . 9 |- ( ( 0 e. RR /\ -u C e. RR ) -> 0 <_ if ( 0 <_ -u C , -u C , 0 ) )
133	6, 11, 132	sylancr 663	. . . . . . . 8 |- ( ph -> 0 <_ if ( 0 <_ -u C , -u C , 0 ) )
134	14, 55, 58, 114, 13, 55, 133, 102	itgmulc2nclem1 28599	. . . . . . 7 |- ( ph -> ( if ( 0 <_ -u C , -u C , 0 ) x. S. A if ( 0 <_ B , B , 0 ) _d x ) = S. A ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) _d x )
135	14, 72, 73, 120, 13, 72, 133, 105	itgmulc2nclem1 28599	. . . . . . 7 |- ( ph -> ( if ( 0 <_ -u C , -u C , 0 ) x. S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) = S. A ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) _d x )
136	134, 135	oveq12d 6211	. . . . . 6 |- ( ph -> ( ( if ( 0 <_ -u C , -u C , 0 ) x. S. A if ( 0 <_ B , B , 0 ) _d x ) - ( if ( 0 <_ -u C , -u C , 0 ) x. S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) ) = ( S. A ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) _d x - S. A ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) _d x ) )
137	130, 131, 136	3eqtrd 2496	. . . . 5 |- ( ph -> ( if ( 0 <_ -u C , -u C , 0 ) x. S. A B _d x ) = ( S. A ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) _d x - S. A ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) _d x ) )
138	128, 129, 137	3eqtr4d 2502	. . . 4 |- ( ph -> S. A ( if ( 0 <_ -u C , -u C , 0 ) x. B ) _d x = ( if ( 0 <_ -u C , -u C , 0 ) x. S. A B _d x ) )
139	109, 138	oveq12d 6211	. . 3 |- ( ph -> ( S. A ( if ( 0 <_ C , C , 0 ) x. B ) _d x - S. A ( if ( 0 <_ -u C , -u C , 0 ) x. B ) _d x ) = ( ( if ( 0 <_ C , C , 0 ) x. S. A B _d x ) - ( if ( 0 <_ -u C , -u C , 0 ) x. S. A B _d x ) ) )
140	16, 23	itgcl 21387	. . . 4 |- ( ph -> S. A B _d x e. CC )
141	9, 14, 140	subdird 9905	. . 3 |- ( ph -> ( ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) x. S. A B _d x ) = ( ( if ( 0 <_ C , C , 0 ) x. S. A B _d x ) - ( if ( 0 <_ -u C , -u C , 0 ) x. S. A B _d x ) ) )
142	3	oveq1d 6208	. . 3 |- ( ph -> ( ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) x. S. A B _d x ) = ( C x. S. A B _d x ) )
143	139, 141, 142	3eqtr2d 2498	. 2 |- ( ph -> ( S. A ( if ( 0 <_ C , C , 0 ) x. B ) _d x - S. A ( if ( 0 <_ -u C , -u C , 0 ) x. B ) _d x ) = ( C x. S. A B _d x ) )
144	20, 51, 143	3eqtrrd 2497	1 |- ( ph -> ( C x. S. A B _d x ) = S. A ( C x. B ) _d x )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1370   e. wcel 1758   _Vcvv 3071   ifcif 3892   {csn 3978   class class class wbr 4393   |-> cmpt 4451   X. cxp 4939   dom cdm 4941  (class class class)co 6193   oFcof 6421   CCcc 9384   RRcr 9385   0cc0 9386   x. cmul 9391   <_ cle 9523   - cmin 9699   -ucneg 9700   volcvol 21072  MblFncmbf 21220   L^1cibl 21223   S.citg 21224

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-rep 4504  ax-sep 4514  ax-nul 4522  ax-pow 4571  ax-pr 4632  ax-un 6475  ax-inf2 7951  ax-cnex 9442  ax-resscn 9443  ax-1cn 9444  ax-icn 9445  ax-addcl 9446  ax-addrcl 9447  ax-mulcl 9448  ax-mulrcl 9449  ax-mulcom 9450  ax-addass 9451  ax-mulass 9452  ax-distr 9453  ax-i2m1 9454  ax-1ne0 9455  ax-1rid 9456  ax-rnegex 9457  ax-rrecex 9458  ax-cnre 9459  ax-pre-lttri 9460  ax-pre-lttrn 9461  ax-pre-ltadd 9462  ax-pre-mulgt0 9463  ax-pre-sup 9464  ax-addf 9465

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-fal 1376  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-reu 2802  df-rmo 2803  df-rab 2804  df-v 3073  df-sbc 3288  df-csb 3390  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-pss 3445  df-nul 3739  df-if 3893  df-pw 3963  df-sn 3979  df-pr 3981  df-tp 3983  df-op 3985  df-uni 4193  df-int 4230  df-iun 4274  df-disj 4364  df-br 4394  df-opab 4452  df-mpt 4453  df-tr 4487  df-eprel 4733  df-id 4737  df-po 4742  df-so 4743  df-fr 4780  df-se 4781  df-we 4782  df-ord 4823  df-on 4824  df-lim 4825  df-suc 4826  df-xp 4947  df-rel 4948  df-cnv 4949  df-co 4950  df-dm 4951  df-rn 4952  df-res 4953  df-ima 4954  df-iota 5482  df-fun 5521  df-fn 5522  df-f 5523  df-f1 5524  df-fo 5525  df-f1o 5526  df-fv 5527  df-isom 5528  df-riota 6154  df-ov 6196  df-oprab 6197  df-mpt2 6198  df-of 6423  df-ofr 6424  df-om 6580  df-1st 6680  df-2nd 6681  df-recs 6935  df-rdg 6969  df-1o 7023  df-2o 7024  df-oadd 7027  df-er 7204  df-map 7319  df-pm 7320  df-en 7414  df-dom 7415  df-sdom 7416  df-fin 7417  df-fi 7765  df-sup 7795  df-oi 7828  df-card 8213  df-cda 8441  df-pnf 9524  df-mnf 9525  df-xr 9526  df-ltxr 9527  df-le 9528  df-sub 9701  df-neg 9702  df-div 10098  df-nn 10427  df-2 10484  df-3 10485  df-4 10486  df-n0 10684  df-z 10751  df-uz 10966  df-q 11058  df-rp 11096  df-xneg 11193  df-xadd 11194  df-xmul 11195  df-ioo 11408  df-ico 11410  df-icc 11411  df-fz 11548  df-fzo 11659  df-fl 11752  df-mod 11819  df-seq 11917  df-exp 11976  df-hash 12214  df-cj 12699  df-re 12700  df-im 12701  df-sqr 12835  df-abs 12836  df-clim 13077  df-sum 13275  df-rest 14472  df-topgen 14493  df-psmet 17927  df-xmet 17928  df-met 17929  df-bl 17930  df-mopn 17931  df-top 18628  df-bases 18630  df-topon 18631  df-cmp 19115  df-ovol 21073  df-vol 21074  df-mbf 21225  df-itg1 21226  df-itg2 21227  df-ibl 21228  df-itg 21229  df-0p 21274

This theorem is referenced by:  itgmulc2nc  28601