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 ) |