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 )