Metamath Proof Explorer


Theorem i1fres

Description: The "restriction" of a simple function to a measurable subset is simple. (It's not actually a restriction because it is zero instead of undefined outside A .) (Contributed by Mario Carneiro, 29-Jun-2014)

Ref Expression
Hypothesis i1fres.1
|- G = ( x e. RR |-> if ( x e. A , ( F ` x ) , 0 ) )
Assertion i1fres
|- ( ( F e. dom S.1 /\ A e. dom vol ) -> G e. dom S.1 )

Proof

Step Hyp Ref Expression
1 i1fres.1
 |-  G = ( x e. RR |-> if ( x e. A , ( F ` x ) , 0 ) )
2 i1ff
 |-  ( F e. dom S.1 -> F : RR --> RR )
3 2 adantr
 |-  ( ( F e. dom S.1 /\ A e. dom vol ) -> F : RR --> RR )
4 3 ffnd
 |-  ( ( F e. dom S.1 /\ A e. dom vol ) -> F Fn RR )
5 fnfvelrn
 |-  ( ( F Fn RR /\ x e. RR ) -> ( F ` x ) e. ran F )
6 4 5 sylan
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ x e. RR ) -> ( F ` x ) e. ran F )
7 i1f0rn
 |-  ( F e. dom S.1 -> 0 e. ran F )
8 7 ad2antrr
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ x e. RR ) -> 0 e. ran F )
9 6 8 ifcld
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ x e. RR ) -> if ( x e. A , ( F ` x ) , 0 ) e. ran F )
10 9 1 fmptd
 |-  ( ( F e. dom S.1 /\ A e. dom vol ) -> G : RR --> ran F )
11 3 frnd
 |-  ( ( F e. dom S.1 /\ A e. dom vol ) -> ran F C_ RR )
12 10 11 fssd
 |-  ( ( F e. dom S.1 /\ A e. dom vol ) -> G : RR --> RR )
13 i1frn
 |-  ( F e. dom S.1 -> ran F e. Fin )
14 13 adantr
 |-  ( ( F e. dom S.1 /\ A e. dom vol ) -> ran F e. Fin )
15 10 frnd
 |-  ( ( F e. dom S.1 /\ A e. dom vol ) -> ran G C_ ran F )
16 14 15 ssfid
 |-  ( ( F e. dom S.1 /\ A e. dom vol ) -> ran G e. Fin )
17 eleq1w
 |-  ( x = z -> ( x e. A <-> z e. A ) )
18 fveq2
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
19 17 18 ifbieq1d
 |-  ( x = z -> if ( x e. A , ( F ` x ) , 0 ) = if ( z e. A , ( F ` z ) , 0 ) )
20 fvex
 |-  ( F ` z ) e. _V
21 c0ex
 |-  0 e. _V
22 20 21 ifex
 |-  if ( z e. A , ( F ` z ) , 0 ) e. _V
23 19 1 22 fvmpt
 |-  ( z e. RR -> ( G ` z ) = if ( z e. A , ( F ` z ) , 0 ) )
24 23 adantl
 |-  ( ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) /\ z e. RR ) -> ( G ` z ) = if ( z e. A , ( F ` z ) , 0 ) )
25 24 eqeq1d
 |-  ( ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) /\ z e. RR ) -> ( ( G ` z ) = y <-> if ( z e. A , ( F ` z ) , 0 ) = y ) )
26 eldifsni
 |-  ( y e. ( ran G \ { 0 } ) -> y =/= 0 )
27 26 ad2antlr
 |-  ( ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) /\ z e. RR ) -> y =/= 0 )
28 27 necomd
 |-  ( ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) /\ z e. RR ) -> 0 =/= y )
29 iffalse
 |-  ( -. z e. A -> if ( z e. A , ( F ` z ) , 0 ) = 0 )
30 29 neeq1d
 |-  ( -. z e. A -> ( if ( z e. A , ( F ` z ) , 0 ) =/= y <-> 0 =/= y ) )
31 28 30 syl5ibrcom
 |-  ( ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) /\ z e. RR ) -> ( -. z e. A -> if ( z e. A , ( F ` z ) , 0 ) =/= y ) )
32 31 necon4bd
 |-  ( ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) /\ z e. RR ) -> ( if ( z e. A , ( F ` z ) , 0 ) = y -> z e. A ) )
33 32 pm4.71rd
 |-  ( ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) /\ z e. RR ) -> ( if ( z e. A , ( F ` z ) , 0 ) = y <-> ( z e. A /\ if ( z e. A , ( F ` z ) , 0 ) = y ) ) )
34 25 33 bitrd
 |-  ( ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) /\ z e. RR ) -> ( ( G ` z ) = y <-> ( z e. A /\ if ( z e. A , ( F ` z ) , 0 ) = y ) ) )
35 iftrue
 |-  ( z e. A -> if ( z e. A , ( F ` z ) , 0 ) = ( F ` z ) )
36 35 eqeq1d
 |-  ( z e. A -> ( if ( z e. A , ( F ` z ) , 0 ) = y <-> ( F ` z ) = y ) )
37 36 pm5.32i
 |-  ( ( z e. A /\ if ( z e. A , ( F ` z ) , 0 ) = y ) <-> ( z e. A /\ ( F ` z ) = y ) )
38 34 37 bitrdi
 |-  ( ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) /\ z e. RR ) -> ( ( G ` z ) = y <-> ( z e. A /\ ( F ` z ) = y ) ) )
39 38 pm5.32da
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) -> ( ( z e. RR /\ ( G ` z ) = y ) <-> ( z e. RR /\ ( z e. A /\ ( F ` z ) = y ) ) ) )
40 an12
 |-  ( ( z e. RR /\ ( z e. A /\ ( F ` z ) = y ) ) <-> ( z e. A /\ ( z e. RR /\ ( F ` z ) = y ) ) )
41 39 40 bitrdi
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) -> ( ( z e. RR /\ ( G ` z ) = y ) <-> ( z e. A /\ ( z e. RR /\ ( F ` z ) = y ) ) ) )
42 10 ffnd
 |-  ( ( F e. dom S.1 /\ A e. dom vol ) -> G Fn RR )
43 42 adantr
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) -> G Fn RR )
44 fniniseg
 |-  ( G Fn RR -> ( z e. ( `' G " { y } ) <-> ( z e. RR /\ ( G ` z ) = y ) ) )
45 43 44 syl
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) -> ( z e. ( `' G " { y } ) <-> ( z e. RR /\ ( G ` z ) = y ) ) )
46 4 adantr
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) -> F Fn RR )
47 fniniseg
 |-  ( F Fn RR -> ( z e. ( `' F " { y } ) <-> ( z e. RR /\ ( F ` z ) = y ) ) )
48 46 47 syl
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) -> ( z e. ( `' F " { y } ) <-> ( z e. RR /\ ( F ` z ) = y ) ) )
49 48 anbi2d
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) -> ( ( z e. A /\ z e. ( `' F " { y } ) ) <-> ( z e. A /\ ( z e. RR /\ ( F ` z ) = y ) ) ) )
50 41 45 49 3bitr4d
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) -> ( z e. ( `' G " { y } ) <-> ( z e. A /\ z e. ( `' F " { y } ) ) ) )
51 elin
 |-  ( z e. ( A i^i ( `' F " { y } ) ) <-> ( z e. A /\ z e. ( `' F " { y } ) ) )
52 50 51 bitr4di
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) -> ( z e. ( `' G " { y } ) <-> z e. ( A i^i ( `' F " { y } ) ) ) )
53 52 eqrdv
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) -> ( `' G " { y } ) = ( A i^i ( `' F " { y } ) ) )
54 simplr
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) -> A e. dom vol )
55 i1fima
 |-  ( F e. dom S.1 -> ( `' F " { y } ) e. dom vol )
56 55 ad2antrr
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) -> ( `' F " { y } ) e. dom vol )
57 inmbl
 |-  ( ( A e. dom vol /\ ( `' F " { y } ) e. dom vol ) -> ( A i^i ( `' F " { y } ) ) e. dom vol )
58 54 56 57 syl2anc
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) -> ( A i^i ( `' F " { y } ) ) e. dom vol )
59 53 58 eqeltrd
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) -> ( `' G " { y } ) e. dom vol )
60 53 fveq2d
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) -> ( vol ` ( `' G " { y } ) ) = ( vol ` ( A i^i ( `' F " { y } ) ) ) )
61 mblvol
 |-  ( ( A i^i ( `' F " { y } ) ) e. dom vol -> ( vol ` ( A i^i ( `' F " { y } ) ) ) = ( vol* ` ( A i^i ( `' F " { y } ) ) ) )
62 58 61 syl
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) -> ( vol ` ( A i^i ( `' F " { y } ) ) ) = ( vol* ` ( A i^i ( `' F " { y } ) ) ) )
63 60 62 eqtrd
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) -> ( vol ` ( `' G " { y } ) ) = ( vol* ` ( A i^i ( `' F " { y } ) ) ) )
64 inss2
 |-  ( A i^i ( `' F " { y } ) ) C_ ( `' F " { y } )
65 mblss
 |-  ( ( `' F " { y } ) e. dom vol -> ( `' F " { y } ) C_ RR )
66 56 65 syl
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) -> ( `' F " { y } ) C_ RR )
67 mblvol
 |-  ( ( `' F " { y } ) e. dom vol -> ( vol ` ( `' F " { y } ) ) = ( vol* ` ( `' F " { y } ) ) )
68 56 67 syl
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) -> ( vol ` ( `' F " { y } ) ) = ( vol* ` ( `' F " { y } ) ) )
69 i1fima2sn
 |-  ( ( F e. dom S.1 /\ y e. ( ran G \ { 0 } ) ) -> ( vol ` ( `' F " { y } ) ) e. RR )
70 69 adantlr
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) -> ( vol ` ( `' F " { y } ) ) e. RR )
71 68 70 eqeltrrd
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) -> ( vol* ` ( `' F " { y } ) ) e. RR )
72 ovolsscl
 |-  ( ( ( A i^i ( `' F " { y } ) ) C_ ( `' F " { y } ) /\ ( `' F " { y } ) C_ RR /\ ( vol* ` ( `' F " { y } ) ) e. RR ) -> ( vol* ` ( A i^i ( `' F " { y } ) ) ) e. RR )
73 64 66 71 72 mp3an2i
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) -> ( vol* ` ( A i^i ( `' F " { y } ) ) ) e. RR )
74 63 73 eqeltrd
 |-  ( ( ( F e. dom S.1 /\ A e. dom vol ) /\ y e. ( ran G \ { 0 } ) ) -> ( vol ` ( `' G " { y } ) ) e. RR )
75 12 16 59 74 i1fd
 |-  ( ( F e. dom S.1 /\ A e. dom vol ) -> G e. dom S.1 )