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 )