Metamath Proof Explorer

Theorem i1fd

Description: A simplified set of assumptions to show that a given function is simple. (Contributed by Mario Carneiro, 26-Jun-2014)

Ref Expression
Hypotheses i1fd.1 
|- ( ph -> F : RR --> RR )
i1fd.2 
|- ( ph -> ran F e. Fin )
i1fd.3 
|- ( ( ph /\ x e. ( ran F \ { 0 } ) ) -> ( `' F " { x } ) e. dom vol )
i1fd.4 
|- ( ( ph /\ x e. ( ran F \ { 0 } ) ) -> ( vol ` ( `' F " { x } ) ) e. RR )
Assertion i1fd 
|- ( ph -> F e. dom S.1 )

Proof

Step Hyp Ref Expression
1 i1fd.1 
 |-  ( ph -> F : RR --> RR )
2 i1fd.2 
 |-  ( ph -> ran F e. Fin )
3 i1fd.3 
 |-  ( ( ph /\ x e. ( ran F \ { 0 } ) ) -> ( `' F " { x } ) e. dom vol )
4 i1fd.4 
 |-  ( ( ph /\ x e. ( ran F \ { 0 } ) ) -> ( vol ` ( `' F " { x } ) ) e. RR )
5 1 ad2antrr 
 |-  ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> F : RR --> RR )
6 ffun 
 |-  ( F : RR --> RR -> Fun F )
7 funcnvcnv 
 |-  ( Fun F -> Fun `' `' F )
8 imadif 
 |-  ( Fun `' `' F -> ( `' F " ( RR \ ( RR \ x ) ) ) = ( ( `' F " RR ) \ ( `' F " ( RR \ x ) ) ) )
9 5 6 7 8 4syl 
 |-  ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> ( `' F " ( RR \ ( RR \ x ) ) ) = ( ( `' F " RR ) \ ( `' F " ( RR \ x ) ) ) )
10 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
11 frn 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> ran (,) C_ ~P RR )
12 10 11 ax-mp 
 |-  ran (,) C_ ~P RR
13 12 sseli 
 |-  ( x e. ran (,) -> x e. ~P RR )
14 13 elpwid 
 |-  ( x e. ran (,) -> x C_ RR )
15 14 ad2antlr 
 |-  ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> x C_ RR )
16 dfss4 
 |-  ( x C_ RR <-> ( RR \ ( RR \ x ) ) = x )
17 15 16 sylib 
 |-  ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> ( RR \ ( RR \ x ) ) = x )
18 17 imaeq2d 
 |-  ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> ( `' F " ( RR \ ( RR \ x ) ) ) = ( `' F " x ) )
19 9 18 eqtr3d 
 |-  ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> ( ( `' F " RR ) \ ( `' F " ( RR \ x ) ) ) = ( `' F " x ) )
20 fimacnv 
 |-  ( F : RR --> RR -> ( `' F " RR ) = RR )
21 5 20 syl 
 |-  ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> ( `' F " RR ) = RR )
22 rembl 
 |-  RR e. dom vol
23 21 22 eqeltrdi 
 |-  ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> ( `' F " RR ) e. dom vol )
24 1 adantr 
 |-  ( ( ph /\ -. 0 e. y ) -> F : RR --> RR )
25 inpreima 
 |-  ( Fun F -> ( `' F " ( y i^i ran F ) ) = ( ( `' F " y ) i^i ( `' F " ran F ) ) )
26 iunid 
 |-  U_ x e. ( y i^i ran F ) { x } = ( y i^i ran F )
27 26 imaeq2i 
 |-  ( `' F " U_ x e. ( y i^i ran F ) { x } ) = ( `' F " ( y i^i ran F ) )
28 imaiun 
 |-  ( `' F " U_ x e. ( y i^i ran F ) { x } ) = U_ x e. ( y i^i ran F ) ( `' F " { x } )
29 27 28 eqtr3i 
 |-  ( `' F " ( y i^i ran F ) ) = U_ x e. ( y i^i ran F ) ( `' F " { x } )
30 cnvimass 
 |-  ( `' F " y ) C_ dom F
31 cnvimarndm 
 |-  ( `' F " ran F ) = dom F
32 30 31 sseqtrri 
 |-  ( `' F " y ) C_ ( `' F " ran F )
33 df-ss 
 |-  ( ( `' F " y ) C_ ( `' F " ran F ) <-> ( ( `' F " y ) i^i ( `' F " ran F ) ) = ( `' F " y ) )
34 32 33 mpbi 
 |-  ( ( `' F " y ) i^i ( `' F " ran F ) ) = ( `' F " y )
35 25 29 34 3eqtr3g 
 |-  ( Fun F -> U_ x e. ( y i^i ran F ) ( `' F " { x } ) = ( `' F " y ) )
36 24 6 35 3syl 
 |-  ( ( ph /\ -. 0 e. y ) -> U_ x e. ( y i^i ran F ) ( `' F " { x } ) = ( `' F " y ) )
37 2 adantr 
 |-  ( ( ph /\ -. 0 e. y ) -> ran F e. Fin )
38 inss2 
 |-  ( y i^i ran F ) C_ ran F
39 ssfi 
 |-  ( ( ran F e. Fin /\ ( y i^i ran F ) C_ ran F ) -> ( y i^i ran F ) e. Fin )
40 37 38 39 sylancl 
 |-  ( ( ph /\ -. 0 e. y ) -> ( y i^i ran F ) e. Fin )
41 simpll 
 |-  ( ( ( ph /\ -. 0 e. y ) /\ x e. ( y i^i ran F ) ) -> ph )
42 elinel1 
 |-  ( 0 e. ( y i^i ran F ) -> 0 e. y )
43 42 con3i 
 |-  ( -. 0 e. y -> -. 0 e. ( y i^i ran F ) )
44 43 adantl 
 |-  ( ( ph /\ -. 0 e. y ) -> -. 0 e. ( y i^i ran F ) )
45 disjsn 
 |-  ( ( ( y i^i ran F ) i^i { 0 } ) = (/) <-> -. 0 e. ( y i^i ran F ) )
46 44 45 sylibr 
 |-  ( ( ph /\ -. 0 e. y ) -> ( ( y i^i ran F ) i^i { 0 } ) = (/) )
47 reldisj 
 |-  ( ( y i^i ran F ) C_ ran F -> ( ( ( y i^i ran F ) i^i { 0 } ) = (/) <-> ( y i^i ran F ) C_ ( ran F \ { 0 } ) ) )
48 38 47 ax-mp 
 |-  ( ( ( y i^i ran F ) i^i { 0 } ) = (/) <-> ( y i^i ran F ) C_ ( ran F \ { 0 } ) )
49 46 48 sylib 
 |-  ( ( ph /\ -. 0 e. y ) -> ( y i^i ran F ) C_ ( ran F \ { 0 } ) )
50 49 sselda 
 |-  ( ( ( ph /\ -. 0 e. y ) /\ x e. ( y i^i ran F ) ) -> x e. ( ran F \ { 0 } ) )
51 41 50 3 syl2anc 
 |-  ( ( ( ph /\ -. 0 e. y ) /\ x e. ( y i^i ran F ) ) -> ( `' F " { x } ) e. dom vol )
52 51 ralrimiva 
 |-  ( ( ph /\ -. 0 e. y ) -> A. x e. ( y i^i ran F ) ( `' F " { x } ) e. dom vol )
53 finiunmbl 
 |-  ( ( ( y i^i ran F ) e. Fin /\ A. x e. ( y i^i ran F ) ( `' F " { x } ) e. dom vol ) -> U_ x e. ( y i^i ran F ) ( `' F " { x } ) e. dom vol )
54 40 52 53 syl2anc 
 |-  ( ( ph /\ -. 0 e. y ) -> U_ x e. ( y i^i ran F ) ( `' F " { x } ) e. dom vol )
55 36 54 eqeltrrd 
 |-  ( ( ph /\ -. 0 e. y ) -> ( `' F " y ) e. dom vol )
56 55 ex 
 |-  ( ph -> ( -. 0 e. y -> ( `' F " y ) e. dom vol ) )
57 56 alrimiv 
 |-  ( ph -> A. y ( -. 0 e. y -> ( `' F " y ) e. dom vol ) )
58 57 ad2antrr 
 |-  ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> A. y ( -. 0 e. y -> ( `' F " y ) e. dom vol ) )
59 elndif 
 |-  ( 0 e. x -> -. 0 e. ( RR \ x ) )
60 59 adantl 
 |-  ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> -. 0 e. ( RR \ x ) )
61 reex 
 |-  RR e. _V
62 61 difexi 
 |-  ( RR \ x ) e. _V
63 eleq2 
 |-  ( y = ( RR \ x ) -> ( 0 e. y <-> 0 e. ( RR \ x ) ) )
64 63 notbid 
 |-  ( y = ( RR \ x ) -> ( -. 0 e. y <-> -. 0 e. ( RR \ x ) ) )
65 imaeq2 
 |-  ( y = ( RR \ x ) -> ( `' F " y ) = ( `' F " ( RR \ x ) ) )
66 65 eleq1d 
 |-  ( y = ( RR \ x ) -> ( ( `' F " y ) e. dom vol <-> ( `' F " ( RR \ x ) ) e. dom vol ) )
67 64 66 imbi12d 
 |-  ( y = ( RR \ x ) -> ( ( -. 0 e. y -> ( `' F " y ) e. dom vol ) <-> ( -. 0 e. ( RR \ x ) -> ( `' F " ( RR \ x ) ) e. dom vol ) ) )
68 62 67 spcv 
 |-  ( A. y ( -. 0 e. y -> ( `' F " y ) e. dom vol ) -> ( -. 0 e. ( RR \ x ) -> ( `' F " ( RR \ x ) ) e. dom vol ) )
69 58 60 68 sylc 
 |-  ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> ( `' F " ( RR \ x ) ) e. dom vol )
70 difmbl 
 |-  ( ( ( `' F " RR ) e. dom vol /\ ( `' F " ( RR \ x ) ) e. dom vol ) -> ( ( `' F " RR ) \ ( `' F " ( RR \ x ) ) ) e. dom vol )
71 23 69 70 syl2anc 
 |-  ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> ( ( `' F " RR ) \ ( `' F " ( RR \ x ) ) ) e. dom vol )
72 19 71 eqeltrrd 
 |-  ( ( ( ph /\ x e. ran (,) ) /\ 0 e. x ) -> ( `' F " x ) e. dom vol )
73 eleq2 
 |-  ( y = x -> ( 0 e. y <-> 0 e. x ) )
74 73 notbid 
 |-  ( y = x -> ( -. 0 e. y <-> -. 0 e. x ) )
75 imaeq2 
 |-  ( y = x -> ( `' F " y ) = ( `' F " x ) )
76 75 eleq1d 
 |-  ( y = x -> ( ( `' F " y ) e. dom vol <-> ( `' F " x ) e. dom vol ) )
77 74 76 imbi12d 
 |-  ( y = x -> ( ( -. 0 e. y -> ( `' F " y ) e. dom vol ) <-> ( -. 0 e. x -> ( `' F " x ) e. dom vol ) ) )
78 77 spvv 
 |-  ( A. y ( -. 0 e. y -> ( `' F " y ) e. dom vol ) -> ( -. 0 e. x -> ( `' F " x ) e. dom vol ) )
79 57 78 syl 
 |-  ( ph -> ( -. 0 e. x -> ( `' F " x ) e. dom vol ) )
80 79 imp 
 |-  ( ( ph /\ -. 0 e. x ) -> ( `' F " x ) e. dom vol )
81 80 adantlr 
 |-  ( ( ( ph /\ x e. ran (,) ) /\ -. 0 e. x ) -> ( `' F " x ) e. dom vol )
82 72 81 pm2.61dan 
 |-  ( ( ph /\ x e. ran (,) ) -> ( `' F " x ) e. dom vol )
83 82 ralrimiva 
 |-  ( ph -> A. x e. ran (,) ( `' F " x ) e. dom vol )
84 ismbf 
 |-  ( F : RR --> RR -> ( F e. MblFn <-> A. x e. ran (,) ( `' F " x ) e. dom vol ) )
85 1 84 syl 
 |-  ( ph -> ( F e. MblFn <-> A. x e. ran (,) ( `' F " x ) e. dom vol ) )
86 83 85 mpbird 
 |-  ( ph -> F e. MblFn )
87 mblvol 
 |-  ( ( `' F " y ) e. dom vol -> ( vol ` ( `' F " y ) ) = ( vol* ` ( `' F " y ) ) )
88 55 87 syl 
 |-  ( ( ph /\ -. 0 e. y ) -> ( vol ` ( `' F " y ) ) = ( vol* ` ( `' F " y ) ) )
89 mblss 
 |-  ( ( `' F " y ) e. dom vol -> ( `' F " y ) C_ RR )
90 55 89 syl 
 |-  ( ( ph /\ -. 0 e. y ) -> ( `' F " y ) C_ RR )
91 mblvol 
 |-  ( ( `' F " { x } ) e. dom vol -> ( vol ` ( `' F " { x } ) ) = ( vol* ` ( `' F " { x } ) ) )
92 51 91 syl 
 |-  ( ( ( ph /\ -. 0 e. y ) /\ x e. ( y i^i ran F ) ) -> ( vol ` ( `' F " { x } ) ) = ( vol* ` ( `' F " { x } ) ) )
93 41 50 4 syl2anc 
 |-  ( ( ( ph /\ -. 0 e. y ) /\ x e. ( y i^i ran F ) ) -> ( vol ` ( `' F " { x } ) ) e. RR )
94 92 93 eqeltrrd 
 |-  ( ( ( ph /\ -. 0 e. y ) /\ x e. ( y i^i ran F ) ) -> ( vol* ` ( `' F " { x } ) ) e. RR )
95 40 94 fsumrecl 
 |-  ( ( ph /\ -. 0 e. y ) -> sum_ x e. ( y i^i ran F ) ( vol* ` ( `' F " { x } ) ) e. RR )
96 36 fveq2d 
 |-  ( ( ph /\ -. 0 e. y ) -> ( vol* ` U_ x e. ( y i^i ran F ) ( `' F " { x } ) ) = ( vol* ` ( `' F " y ) ) )
97 mblss 
 |-  ( ( `' F " { x } ) e. dom vol -> ( `' F " { x } ) C_ RR )
98 51 97 syl 
 |-  ( ( ( ph /\ -. 0 e. y ) /\ x e. ( y i^i ran F ) ) -> ( `' F " { x } ) C_ RR )
99 98 94 jca 
 |-  ( ( ( ph /\ -. 0 e. y ) /\ x e. ( y i^i ran F ) ) -> ( ( `' F " { x } ) C_ RR /\ ( vol* ` ( `' F " { x } ) ) e. RR ) )
100 99 ralrimiva 
 |-  ( ( ph /\ -. 0 e. y ) -> A. x e. ( y i^i ran F ) ( ( `' F " { x } ) C_ RR /\ ( vol* ` ( `' F " { x } ) ) e. RR ) )
101 ovolfiniun 
 |-  ( ( ( y i^i ran F ) e. Fin /\ A. x e. ( y i^i ran F ) ( ( `' F " { x } ) C_ RR /\ ( vol* ` ( `' F " { x } ) ) e. RR ) ) -> ( vol* ` U_ x e. ( y i^i ran F ) ( `' F " { x } ) ) <_ sum_ x e. ( y i^i ran F ) ( vol* ` ( `' F " { x } ) ) )
102 40 100 101 syl2anc 
 |-  ( ( ph /\ -. 0 e. y ) -> ( vol* ` U_ x e. ( y i^i ran F ) ( `' F " { x } ) ) <_ sum_ x e. ( y i^i ran F ) ( vol* ` ( `' F " { x } ) ) )
103 96 102 eqbrtrrd 
 |-  ( ( ph /\ -. 0 e. y ) -> ( vol* ` ( `' F " y ) ) <_ sum_ x e. ( y i^i ran F ) ( vol* ` ( `' F " { x } ) ) )
104 ovollecl 
 |-  ( ( ( `' F " y ) C_ RR /\ sum_ x e. ( y i^i ran F ) ( vol* ` ( `' F " { x } ) ) e. RR /\ ( vol* ` ( `' F " y ) ) <_ sum_ x e. ( y i^i ran F ) ( vol* ` ( `' F " { x } ) ) ) -> ( vol* ` ( `' F " y ) ) e. RR )
105 90 95 103 104 syl3anc 
 |-  ( ( ph /\ -. 0 e. y ) -> ( vol* ` ( `' F " y ) ) e. RR )
106 88 105 eqeltrd 
 |-  ( ( ph /\ -. 0 e. y ) -> ( vol ` ( `' F " y ) ) e. RR )
107 106 ex 
 |-  ( ph -> ( -. 0 e. y -> ( vol ` ( `' F " y ) ) e. RR ) )
108 107 alrimiv 
 |-  ( ph -> A. y ( -. 0 e. y -> ( vol ` ( `' F " y ) ) e. RR ) )
109 neldifsn 
 |-  -. 0 e. ( RR \ { 0 } )
110 61 difexi 
 |-  ( RR \ { 0 } ) e. _V
111 eleq2 
 |-  ( y = ( RR \ { 0 } ) -> ( 0 e. y <-> 0 e. ( RR \ { 0 } ) ) )
112 111 notbid 
 |-  ( y = ( RR \ { 0 } ) -> ( -. 0 e. y <-> -. 0 e. ( RR \ { 0 } ) ) )
113 imaeq2 
 |-  ( y = ( RR \ { 0 } ) -> ( `' F " y ) = ( `' F " ( RR \ { 0 } ) ) )
114 113 fveq2d 
 |-  ( y = ( RR \ { 0 } ) -> ( vol ` ( `' F " y ) ) = ( vol ` ( `' F " ( RR \ { 0 } ) ) ) )
115 114 eleq1d 
 |-  ( y = ( RR \ { 0 } ) -> ( ( vol ` ( `' F " y ) ) e. RR <-> ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) )
116 112 115 imbi12d 
 |-  ( y = ( RR \ { 0 } ) -> ( ( -. 0 e. y -> ( vol ` ( `' F " y ) ) e. RR ) <-> ( -. 0 e. ( RR \ { 0 } ) -> ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) ) )
117 110 116 spcv 
 |-  ( A. y ( -. 0 e. y -> ( vol ` ( `' F " y ) ) e. RR ) -> ( -. 0 e. ( RR \ { 0 } ) -> ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) )
118 108 109 117 mpisyl 
 |-  ( ph -> ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR )
119 1 2 118 3jca 
 |-  ( ph -> ( F : RR --> RR /\ ran F e. Fin /\ ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) )
120 isi1f 
 |-  ( F e. dom S.1 <-> ( F e. MblFn /\ ( F : RR --> RR /\ ran F e. Fin /\ ( vol ` ( `' F " ( RR \ { 0 } ) ) ) e. RR ) ) )
121 86 119 120 sylanbrc 
 |-  ( ph -> F e. dom S.1 )