Metamath Proof Explorer

Theorem itgabsnc

Description: Choice-free analogue of itgabs . (Contributed by Brendan Leahy, 19-Nov-2017) (Revised by Brendan Leahy, 19-Jun-2018)

Ref Expression
Hypotheses itgabsnc.1 
|- ( ( ph /\ x e. A ) -> B e. V )
itgabsnc.2 
|- ( ph -> ( x e. A |-> B ) e. L^1 )
itgabsnc.m1 
|- ( ph -> ( x e. A |-> ( abs ` B ) ) e. MblFn )
itgabsnc.m2 
|- ( ph -> ( y e. A |-> ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) e. MblFn )
Assertion itgabsnc 
|- ( ph -> ( abs ` S. A B _d x ) <_ S. A ( abs ` B ) _d x )

Proof

Step Hyp Ref Expression
1 itgabsnc.1 
 |-  ( ( ph /\ x e. A ) -> B e. V )
2 itgabsnc.2 
 |-  ( ph -> ( x e. A |-> B ) e. L^1 )
3 itgabsnc.m1 
 |-  ( ph -> ( x e. A |-> ( abs ` B ) ) e. MblFn )
4 itgabsnc.m2 
 |-  ( ph -> ( y e. A |-> ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) e. MblFn )
5 1 2 itgcl 
 |-  ( ph -> S. A B _d x e. CC )
6 5 cjcld 
 |-  ( ph -> ( * ` S. A B _d x ) e. CC )
7 iblmbf 
 |-  ( ( x e. A |-> B ) e. L^1 -> ( x e. A |-> B ) e. MblFn )
8 2 7 syl 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
9 8 1 mbfmptcl 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
10 9 ralrimiva 
 |-  ( ph -> A. x e. A B e. CC )
11 nfv 
 |-  F/ y B e. CC
12 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
13 12 nfel1 
 |-  F/ x [_ y / x ]_ B e. CC
14 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
15 14 eleq1d 
 |-  ( x = y -> ( B e. CC <-> [_ y / x ]_ B e. CC ) )
16 11 13 15 cbvralw 
 |-  ( A. x e. A B e. CC <-> A. y e. A [_ y / x ]_ B e. CC )
17 10 16 sylib 
 |-  ( ph -> A. y e. A [_ y / x ]_ B e. CC )
18 17 r19.21bi 
 |-  ( ( ph /\ y e. A ) -> [_ y / x ]_ B e. CC )
19 nfcv 
 |-  F/_ y B
20 19 12 14 cbvmpt 
 |-  ( x e. A |-> B ) = ( y e. A |-> [_ y / x ]_ B )
21 20 2 eqeltrrid 
 |-  ( ph -> ( y e. A |-> [_ y / x ]_ B ) e. L^1 )
22 6 18 21 4 iblmulc2nc 
 |-  ( ph -> ( y e. A |-> ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) e. L^1 )
23 6 adantr 
 |-  ( ( ph /\ y e. A ) -> ( * ` S. A B _d x ) e. CC )
24 23 18 mulcld 
 |-  ( ( ph /\ y e. A ) -> ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) e. CC )
25 24 iblcn 
 |-  ( ph -> ( ( y e. A |-> ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) e. L^1 <-> ( ( y e. A |-> ( Re ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) ) e. L^1 /\ ( y e. A |-> ( Im ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) ) e. L^1 ) ) )
26 22 25 mpbid 
 |-  ( ph -> ( ( y e. A |-> ( Re ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) ) e. L^1 /\ ( y e. A |-> ( Im ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) ) e. L^1 ) )
27 26 simpld 
 |-  ( ph -> ( y e. A |-> ( Re ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) ) e. L^1 )
28 23 18 absmuld 
 |-  ( ( ph /\ y e. A ) -> ( abs ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) = ( ( abs ` ( * ` S. A B _d x ) ) x. ( abs ` [_ y / x ]_ B ) ) )
29 28 mpteq2dva 
 |-  ( ph -> ( y e. A |-> ( abs ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) ) = ( y e. A |-> ( ( abs ` ( * ` S. A B _d x ) ) x. ( abs ` [_ y / x ]_ B ) ) ) )
30 8 1 mbfdm2 
 |-  ( ph -> A e. dom vol )
31 23 abscld 
 |-  ( ( ph /\ y e. A ) -> ( abs ` ( * ` S. A B _d x ) ) e. RR )
32 18 abscld 
 |-  ( ( ph /\ y e. A ) -> ( abs ` [_ y / x ]_ B ) e. RR )
33 fconstmpt 
 |-  ( A X. { ( abs ` ( * ` S. A B _d x ) ) } ) = ( y e. A |-> ( abs ` ( * ` S. A B _d x ) ) )
34 33 a1i 
 |-  ( ph -> ( A X. { ( abs ` ( * ` S. A B _d x ) ) } ) = ( y e. A |-> ( abs ` ( * ` S. A B _d x ) ) ) )
35 nfcv 
 |-  F/_ y ( abs ` B )
36 nfcv 
 |-  F/_ x abs
37 36 12 nffv 
 |-  F/_ x ( abs ` [_ y / x ]_ B )
38 14 fveq2d 
 |-  ( x = y -> ( abs ` B ) = ( abs ` [_ y / x ]_ B ) )
39 35 37 38 cbvmpt 
 |-  ( x e. A |-> ( abs ` B ) ) = ( y e. A |-> ( abs ` [_ y / x ]_ B ) )
40 39 a1i 
 |-  ( ph -> ( x e. A |-> ( abs ` B ) ) = ( y e. A |-> ( abs ` [_ y / x ]_ B ) ) )
41 30 31 32 34 40 offval2 
 |-  ( ph -> ( ( A X. { ( abs ` ( * ` S. A B _d x ) ) } ) oF x. ( x e. A |-> ( abs ` B ) ) ) = ( y e. A |-> ( ( abs ` ( * ` S. A B _d x ) ) x. ( abs ` [_ y / x ]_ B ) ) ) )
42 29 41 eqtr4d 
 |-  ( ph -> ( y e. A |-> ( abs ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) ) = ( ( A X. { ( abs ` ( * ` S. A B _d x ) ) } ) oF x. ( x e. A |-> ( abs ` B ) ) ) )
43 6 abscld 
 |-  ( ph -> ( abs ` ( * ` S. A B _d x ) ) e. RR )
44 9 abscld 
 |-  ( ( ph /\ x e. A ) -> ( abs ` B ) e. RR )
45 44 recnd 
 |-  ( ( ph /\ x e. A ) -> ( abs ` B ) e. CC )
46 45 fmpttd 
 |-  ( ph -> ( x e. A |-> ( abs ` B ) ) : A --> CC )
47 3 43 46 mbfmulc2re 
 |-  ( ph -> ( ( A X. { ( abs ` ( * ` S. A B _d x ) ) } ) oF x. ( x e. A |-> ( abs ` B ) ) ) e. MblFn )
48 42 47 eqeltrd 
 |-  ( ph -> ( y e. A |-> ( abs ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) ) e. MblFn )
49 24 22 48 iblabsnc 
 |-  ( ph -> ( y e. A |-> ( abs ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) ) e. L^1 )
50 24 recld 
 |-  ( ( ph /\ y e. A ) -> ( Re ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) e. RR )
51 24 abscld 
 |-  ( ( ph /\ y e. A ) -> ( abs ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) e. RR )
52 24 releabsd 
 |-  ( ( ph /\ y e. A ) -> ( Re ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) <_ ( abs ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) )
53 27 49 50 51 52 itgle 
 |-  ( ph -> S. A ( Re ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) _d y <_ S. A ( abs ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) _d y )
54 5 abscld 
 |-  ( ph -> ( abs ` S. A B _d x ) e. RR )
55 54 recnd 
 |-  ( ph -> ( abs ` S. A B _d x ) e. CC )
56 55 sqvald 
 |-  ( ph -> ( ( abs ` S. A B _d x ) ^ 2 ) = ( ( abs ` S. A B _d x ) x. ( abs ` S. A B _d x ) ) )
57 5 absvalsqd 
 |-  ( ph -> ( ( abs ` S. A B _d x ) ^ 2 ) = ( S. A B _d x x. ( * ` S. A B _d x ) ) )
58 5 6 mulcomd 
 |-  ( ph -> ( S. A B _d x x. ( * ` S. A B _d x ) ) = ( ( * ` S. A B _d x ) x. S. A B _d x ) )
59 14 19 12 cbvitg 
 |-  S. A B _d x = S. A [_ y / x ]_ B _d y
60 59 oveq2i 
 |-  ( ( * ` S. A B _d x ) x. S. A B _d x ) = ( ( * ` S. A B _d x ) x. S. A [_ y / x ]_ B _d y )
61 6 18 21 4 itgmulc2nc 
 |-  ( ph -> ( ( * ` S. A B _d x ) x. S. A [_ y / x ]_ B _d y ) = S. A ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) _d y )
62 60 61 syl5eq 
 |-  ( ph -> ( ( * ` S. A B _d x ) x. S. A B _d x ) = S. A ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) _d y )
63 57 58 62 3eqtrd 
 |-  ( ph -> ( ( abs ` S. A B _d x ) ^ 2 ) = S. A ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) _d y )
64 63 fveq2d 
 |-  ( ph -> ( Re ` ( ( abs ` S. A B _d x ) ^ 2 ) ) = ( Re ` S. A ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) _d y ) )
65 54 resqcld 
 |-  ( ph -> ( ( abs ` S. A B _d x ) ^ 2 ) e. RR )
66 65 rered 
 |-  ( ph -> ( Re ` ( ( abs ` S. A B _d x ) ^ 2 ) ) = ( ( abs ` S. A B _d x ) ^ 2 ) )
67 ovexd 
 |-  ( ( ph /\ y e. A ) -> ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) e. _V )
68 67 22 itgre 
 |-  ( ph -> ( Re ` S. A ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) _d y ) = S. A ( Re ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) _d y )
69 64 66 68 3eqtr3d 
 |-  ( ph -> ( ( abs ` S. A B _d x ) ^ 2 ) = S. A ( Re ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) _d y )
70 56 69 eqtr3d 
 |-  ( ph -> ( ( abs ` S. A B _d x ) x. ( abs ` S. A B _d x ) ) = S. A ( Re ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) _d y )
71 38 35 37 cbvitg 
 |-  S. A ( abs ` B ) _d x = S. A ( abs ` [_ y / x ]_ B ) _d y
72 71 oveq2i 
 |-  ( ( abs ` S. A B _d x ) x. S. A ( abs ` B ) _d x ) = ( ( abs ` S. A B _d x ) x. S. A ( abs ` [_ y / x ]_ B ) _d y )
73 1 2 3 iblabsnc 
 |-  ( ph -> ( x e. A |-> ( abs ` B ) ) e. L^1 )
74 39 73 eqeltrrid 
 |-  ( ph -> ( y e. A |-> ( abs ` [_ y / x ]_ B ) ) e. L^1 )
75 54 adantr 
 |-  ( ( ph /\ y e. A ) -> ( abs ` S. A B _d x ) e. RR )
76 fconstmpt 
 |-  ( A X. { ( abs ` S. A B _d x ) } ) = ( y e. A |-> ( abs ` S. A B _d x ) )
77 76 a1i 
 |-  ( ph -> ( A X. { ( abs ` S. A B _d x ) } ) = ( y e. A |-> ( abs ` S. A B _d x ) ) )
78 30 75 32 77 40 offval2 
 |-  ( ph -> ( ( A X. { ( abs ` S. A B _d x ) } ) oF x. ( x e. A |-> ( abs ` B ) ) ) = ( y e. A |-> ( ( abs ` S. A B _d x ) x. ( abs ` [_ y / x ]_ B ) ) ) )
79 3 54 46 mbfmulc2re 
 |-  ( ph -> ( ( A X. { ( abs ` S. A B _d x ) } ) oF x. ( x e. A |-> ( abs ` B ) ) ) e. MblFn )
80 78 79 eqeltrrd 
 |-  ( ph -> ( y e. A |-> ( ( abs ` S. A B _d x ) x. ( abs ` [_ y / x ]_ B ) ) ) e. MblFn )
81 55 32 74 80 itgmulc2nc 
 |-  ( ph -> ( ( abs ` S. A B _d x ) x. S. A ( abs ` [_ y / x ]_ B ) _d y ) = S. A ( ( abs ` S. A B _d x ) x. ( abs ` [_ y / x ]_ B ) ) _d y )
82 5 adantr 
 |-  ( ( ph /\ y e. A ) -> S. A B _d x e. CC )
83 82 abscjd 
 |-  ( ( ph /\ y e. A ) -> ( abs ` ( * ` S. A B _d x ) ) = ( abs ` S. A B _d x ) )
84 83 oveq1d 
 |-  ( ( ph /\ y e. A ) -> ( ( abs ` ( * ` S. A B _d x ) ) x. ( abs ` [_ y / x ]_ B ) ) = ( ( abs ` S. A B _d x ) x. ( abs ` [_ y / x ]_ B ) ) )
85 28 84 eqtrd 
 |-  ( ( ph /\ y e. A ) -> ( abs ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) = ( ( abs ` S. A B _d x ) x. ( abs ` [_ y / x ]_ B ) ) )
86 85 itgeq2dv 
 |-  ( ph -> S. A ( abs ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) _d y = S. A ( ( abs ` S. A B _d x ) x. ( abs ` [_ y / x ]_ B ) ) _d y )
87 81 86 eqtr4d 
 |-  ( ph -> ( ( abs ` S. A B _d x ) x. S. A ( abs ` [_ y / x ]_ B ) _d y ) = S. A ( abs ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) _d y )
88 72 87 syl5eq 
 |-  ( ph -> ( ( abs ` S. A B _d x ) x. S. A ( abs ` B ) _d x ) = S. A ( abs ` ( ( * ` S. A B _d x ) x. [_ y / x ]_ B ) ) _d y )
89 53 70 88 3brtr4d 
 |-  ( ph -> ( ( abs ` S. A B _d x ) x. ( abs ` S. A B _d x ) ) <_ ( ( abs ` S. A B _d x ) x. S. A ( abs ` B ) _d x ) )
90 89 adantr 
 |-  ( ( ph /\ 0 < ( abs ` S. A B _d x ) ) -> ( ( abs ` S. A B _d x ) x. ( abs ` S. A B _d x ) ) <_ ( ( abs ` S. A B _d x ) x. S. A ( abs ` B ) _d x ) )
91 54 adantr 
 |-  ( ( ph /\ 0 < ( abs ` S. A B _d x ) ) -> ( abs ` S. A B _d x ) e. RR )
92 44 73 itgrecl 
 |-  ( ph -> S. A ( abs ` B ) _d x e. RR )
93 92 adantr 
 |-  ( ( ph /\ 0 < ( abs ` S. A B _d x ) ) -> S. A ( abs ` B ) _d x e. RR )
94 simpr 
 |-  ( ( ph /\ 0 < ( abs ` S. A B _d x ) ) -> 0 < ( abs ` S. A B _d x ) )
95 lemul2 
 |-  ( ( ( abs ` S. A B _d x ) e. RR /\ S. A ( abs ` B ) _d x e. RR /\ ( ( abs ` S. A B _d x ) e. RR /\ 0 < ( abs ` S. A B _d x ) ) ) -> ( ( abs ` S. A B _d x ) <_ S. A ( abs ` B ) _d x <-> ( ( abs ` S. A B _d x ) x. ( abs ` S. A B _d x ) ) <_ ( ( abs ` S. A B _d x ) x. S. A ( abs ` B ) _d x ) ) )
96 91 93 91 94 95 syl112anc 
 |-  ( ( ph /\ 0 < ( abs ` S. A B _d x ) ) -> ( ( abs ` S. A B _d x ) <_ S. A ( abs ` B ) _d x <-> ( ( abs ` S. A B _d x ) x. ( abs ` S. A B _d x ) ) <_ ( ( abs ` S. A B _d x ) x. S. A ( abs ` B ) _d x ) ) )
97 90 96 mpbird 
 |-  ( ( ph /\ 0 < ( abs ` S. A B _d x ) ) -> ( abs ` S. A B _d x ) <_ S. A ( abs ` B ) _d x )
98 97 ex 
 |-  ( ph -> ( 0 < ( abs ` S. A B _d x ) -> ( abs ` S. A B _d x ) <_ S. A ( abs ` B ) _d x ) )
99 9 absge0d 
 |-  ( ( ph /\ x e. A ) -> 0 <_ ( abs ` B ) )
100 73 44 99 itgge0 
 |-  ( ph -> 0 <_ S. A ( abs ` B ) _d x )
101 breq1 
 |-  ( 0 = ( abs ` S. A B _d x ) -> ( 0 <_ S. A ( abs ` B ) _d x <-> ( abs ` S. A B _d x ) <_ S. A ( abs ` B ) _d x ) )
102 100 101 syl5ibcom 
 |-  ( ph -> ( 0 = ( abs ` S. A B _d x ) -> ( abs ` S. A B _d x ) <_ S. A ( abs ` B ) _d x ) )
103 5 absge0d 
 |-  ( ph -> 0 <_ ( abs ` S. A B _d x ) )
104 0re 
 |-  0 e. RR
105 leloe 
 |-  ( ( 0 e. RR /\ ( abs ` S. A B _d x ) e. RR ) -> ( 0 <_ ( abs ` S. A B _d x ) <-> ( 0 < ( abs ` S. A B _d x ) \/ 0 = ( abs ` S. A B _d x ) ) ) )
106 104 54 105 sylancr 
 |-  ( ph -> ( 0 <_ ( abs ` S. A B _d x ) <-> ( 0 < ( abs ` S. A B _d x ) \/ 0 = ( abs ` S. A B _d x ) ) ) )
107 103 106 mpbid 
 |-  ( ph -> ( 0 < ( abs ` S. A B _d x ) \/ 0 = ( abs ` S. A B _d x ) ) )
108 98 102 107 mpjaod 
 |-  ( ph -> ( abs ` S. A B _d x ) <_ S. A ( abs ` B ) _d x )