Metamath Proof Explorer

Theorem i1fmul

Description: The pointwise product of two simple functions is a simple function. (Contributed by Mario Carneiro, 5-Sep-2014)

Ref Expression
Hypotheses i1fadd.1 
|- ( ph -> F e. dom S.1 )
i1fadd.2 
|- ( ph -> G e. dom S.1 )
Assertion i1fmul 
|- ( ph -> ( F oF x. G ) e. dom S.1 )

Proof

Step Hyp Ref Expression
1 i1fadd.1 
 |-  ( ph -> F e. dom S.1 )
2 i1fadd.2 
 |-  ( ph -> G e. dom S.1 )
3 remulcl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x x. y ) e. RR )
4 3 adantl 
 |-  ( ( ph /\ ( x e. RR /\ y e. RR ) ) -> ( x x. y ) e. RR )
5 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
6 1 5 syl 
 |-  ( ph -> F : RR --> RR )
7 i1ff 
 |-  ( G e. dom S.1 -> G : RR --> RR )
8 2 7 syl 
 |-  ( ph -> G : RR --> RR )
9 reex 
 |-  RR e. _V
10 9 a1i 
 |-  ( ph -> RR e. _V )
11 inidm 
 |-  ( RR i^i RR ) = RR
12 4 6 8 10 10 11 off 
 |-  ( ph -> ( F oF x. G ) : RR --> RR )
13 i1frn 
 |-  ( F e. dom S.1 -> ran F e. Fin )
14 1 13 syl 
 |-  ( ph -> ran F e. Fin )
15 i1frn 
 |-  ( G e. dom S.1 -> ran G e. Fin )
16 2 15 syl 
 |-  ( ph -> ran G e. Fin )
17 xpfi 
 |-  ( ( ran F e. Fin /\ ran G e. Fin ) -> ( ran F X. ran G ) e. Fin )
18 14 16 17 syl2anc 
 |-  ( ph -> ( ran F X. ran G ) e. Fin )
19 eqid 
 |-  ( u e. ran F , v e. ran G |-> ( u x. v ) ) = ( u e. ran F , v e. ran G |-> ( u x. v ) )
20 ovex 
 |-  ( u x. v ) e. _V
21 19 20 fnmpoi 
 |-  ( u e. ran F , v e. ran G |-> ( u x. v ) ) Fn ( ran F X. ran G )
22 dffn4 
 |-  ( ( u e. ran F , v e. ran G |-> ( u x. v ) ) Fn ( ran F X. ran G ) <-> ( u e. ran F , v e. ran G |-> ( u x. v ) ) : ( ran F X. ran G ) -onto-> ran ( u e. ran F , v e. ran G |-> ( u x. v ) ) )
23 21 22 mpbi 
 |-  ( u e. ran F , v e. ran G |-> ( u x. v ) ) : ( ran F X. ran G ) -onto-> ran ( u e. ran F , v e. ran G |-> ( u x. v ) )
24 fofi 
 |-  ( ( ( ran F X. ran G ) e. Fin /\ ( u e. ran F , v e. ran G |-> ( u x. v ) ) : ( ran F X. ran G ) -onto-> ran ( u e. ran F , v e. ran G |-> ( u x. v ) ) ) -> ran ( u e. ran F , v e. ran G |-> ( u x. v ) ) e. Fin )
25 18 23 24 sylancl 
 |-  ( ph -> ran ( u e. ran F , v e. ran G |-> ( u x. v ) ) e. Fin )
26 eqid 
 |-  ( x x. y ) = ( x x. y )
27 rspceov 
 |-  ( ( x e. ran F /\ y e. ran G /\ ( x x. y ) = ( x x. y ) ) -> E. u e. ran F E. v e. ran G ( x x. y ) = ( u x. v ) )
28 26 27 mp3an3 
 |-  ( ( x e. ran F /\ y e. ran G ) -> E. u e. ran F E. v e. ran G ( x x. y ) = ( u x. v ) )
29 ovex 
 |-  ( x x. y ) e. _V
30 eqeq1 
 |-  ( w = ( x x. y ) -> ( w = ( u x. v ) <-> ( x x. y ) = ( u x. v ) ) )
31 30 2rexbidv 
 |-  ( w = ( x x. y ) -> ( E. u e. ran F E. v e. ran G w = ( u x. v ) <-> E. u e. ran F E. v e. ran G ( x x. y ) = ( u x. v ) ) )
32 29 31 elab 
 |-  ( ( x x. y ) e. { w | E. u e. ran F E. v e. ran G w = ( u x. v ) } <-> E. u e. ran F E. v e. ran G ( x x. y ) = ( u x. v ) )
33 28 32 sylibr 
 |-  ( ( x e. ran F /\ y e. ran G ) -> ( x x. y ) e. { w | E. u e. ran F E. v e. ran G w = ( u x. v ) } )
34 33 adantl 
 |-  ( ( ph /\ ( x e. ran F /\ y e. ran G ) ) -> ( x x. y ) e. { w | E. u e. ran F E. v e. ran G w = ( u x. v ) } )
35 6 ffnd 
 |-  ( ph -> F Fn RR )
36 dffn3 
 |-  ( F Fn RR <-> F : RR --> ran F )
37 35 36 sylib 
 |-  ( ph -> F : RR --> ran F )
38 8 ffnd 
 |-  ( ph -> G Fn RR )
39 dffn3 
 |-  ( G Fn RR <-> G : RR --> ran G )
40 38 39 sylib 
 |-  ( ph -> G : RR --> ran G )
41 34 37 40 10 10 11 off 
 |-  ( ph -> ( F oF x. G ) : RR --> { w | E. u e. ran F E. v e. ran G w = ( u x. v ) } )
42 41 frnd 
 |-  ( ph -> ran ( F oF x. G ) C_ { w | E. u e. ran F E. v e. ran G w = ( u x. v ) } )
43 19 rnmpo 
 |-  ran ( u e. ran F , v e. ran G |-> ( u x. v ) ) = { w | E. u e. ran F E. v e. ran G w = ( u x. v ) }
44 42 43 sseqtrrdi 
 |-  ( ph -> ran ( F oF x. G ) C_ ran ( u e. ran F , v e. ran G |-> ( u x. v ) ) )
45 25 44 ssfid 
 |-  ( ph -> ran ( F oF x. G ) e. Fin )
46 12 frnd 
 |-  ( ph -> ran ( F oF x. G ) C_ RR )
47 ax-resscn 
 |-  RR C_ CC
48 46 47 sstrdi 
 |-  ( ph -> ran ( F oF x. G ) C_ CC )
49 48 ssdifd 
 |-  ( ph -> ( ran ( F oF x. G ) \ { 0 } ) C_ ( CC \ { 0 } ) )
50 49 sselda 
 |-  ( ( ph /\ y e. ( ran ( F oF x. G ) \ { 0 } ) ) -> y e. ( CC \ { 0 } ) )
51 1 2 i1fmullem 
 |-  ( ( ph /\ y e. ( CC \ { 0 } ) ) -> ( `' ( F oF x. G ) " { y } ) = U_ z e. ( ran G \ { 0 } ) ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) )
52 50 51 syldan 
 |-  ( ( ph /\ y e. ( ran ( F oF x. G ) \ { 0 } ) ) -> ( `' ( F oF x. G ) " { y } ) = U_ z e. ( ran G \ { 0 } ) ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) )
53 difss 
 |-  ( ran G \ { 0 } ) C_ ran G
54 ssfi 
 |-  ( ( ran G e. Fin /\ ( ran G \ { 0 } ) C_ ran G ) -> ( ran G \ { 0 } ) e. Fin )
55 16 53 54 sylancl 
 |-  ( ph -> ( ran G \ { 0 } ) e. Fin )
56 i1fima 
 |-  ( F e. dom S.1 -> ( `' F " { ( y / z ) } ) e. dom vol )
57 1 56 syl 
 |-  ( ph -> ( `' F " { ( y / z ) } ) e. dom vol )
58 i1fima 
 |-  ( G e. dom S.1 -> ( `' G " { z } ) e. dom vol )
59 2 58 syl 
 |-  ( ph -> ( `' G " { z } ) e. dom vol )
60 inmbl 
 |-  ( ( ( `' F " { ( y / z ) } ) e. dom vol /\ ( `' G " { z } ) e. dom vol ) -> ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) e. dom vol )
61 57 59 60 syl2anc 
 |-  ( ph -> ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) e. dom vol )
62 61 ralrimivw 
 |-  ( ph -> A. z e. ( ran G \ { 0 } ) ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) e. dom vol )
63 finiunmbl 
 |-  ( ( ( ran G \ { 0 } ) e. Fin /\ A. z e. ( ran G \ { 0 } ) ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) e. dom vol ) -> U_ z e. ( ran G \ { 0 } ) ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) e. dom vol )
64 55 62 63 syl2anc 
 |-  ( ph -> U_ z e. ( ran G \ { 0 } ) ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) e. dom vol )
65 64 adantr 
 |-  ( ( ph /\ y e. ( ran ( F oF x. G ) \ { 0 } ) ) -> U_ z e. ( ran G \ { 0 } ) ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) e. dom vol )
66 52 65 eqeltrd 
 |-  ( ( ph /\ y e. ( ran ( F oF x. G ) \ { 0 } ) ) -> ( `' ( F oF x. G ) " { y } ) e. dom vol )
67 mblvol 
 |-  ( ( `' ( F oF x. G ) " { y } ) e. dom vol -> ( vol ` ( `' ( F oF x. G ) " { y } ) ) = ( vol* ` ( `' ( F oF x. G ) " { y } ) ) )
68 66 67 syl 
 |-  ( ( ph /\ y e. ( ran ( F oF x. G ) \ { 0 } ) ) -> ( vol ` ( `' ( F oF x. G ) " { y } ) ) = ( vol* ` ( `' ( F oF x. G ) " { y } ) ) )
69 mblss 
 |-  ( ( `' ( F oF x. G ) " { y } ) e. dom vol -> ( `' ( F oF x. G ) " { y } ) C_ RR )
70 66 69 syl 
 |-  ( ( ph /\ y e. ( ran ( F oF x. G ) \ { 0 } ) ) -> ( `' ( F oF x. G ) " { y } ) C_ RR )
71 55 adantr 
 |-  ( ( ph /\ y e. ( ran ( F oF x. G ) \ { 0 } ) ) -> ( ran G \ { 0 } ) e. Fin )
72 inss2 
 |-  ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) C_ ( `' G " { z } )
73 72 a1i 
 |-  ( ( ( ph /\ y e. ( ran ( F oF x. G ) \ { 0 } ) ) /\ z e. ( ran G \ { 0 } ) ) -> ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) C_ ( `' G " { z } ) )
74 59 ad2antrr 
 |-  ( ( ( ph /\ y e. ( ran ( F oF x. G ) \ { 0 } ) ) /\ z e. ( ran G \ { 0 } ) ) -> ( `' G " { z } ) e. dom vol )
75 mblss 
 |-  ( ( `' G " { z } ) e. dom vol -> ( `' G " { z } ) C_ RR )
76 74 75 syl 
 |-  ( ( ( ph /\ y e. ( ran ( F oF x. G ) \ { 0 } ) ) /\ z e. ( ran G \ { 0 } ) ) -> ( `' G " { z } ) C_ RR )
77 mblvol 
 |-  ( ( `' G " { z } ) e. dom vol -> ( vol ` ( `' G " { z } ) ) = ( vol* ` ( `' G " { z } ) ) )
78 74 77 syl 
 |-  ( ( ( ph /\ y e. ( ran ( F oF x. G ) \ { 0 } ) ) /\ z e. ( ran G \ { 0 } ) ) -> ( vol ` ( `' G " { z } ) ) = ( vol* ` ( `' G " { z } ) ) )
79 2 adantr 
 |-  ( ( ph /\ y e. ( ran ( F oF x. G ) \ { 0 } ) ) -> G e. dom S.1 )
80 i1fima2sn 
 |-  ( ( G e. dom S.1 /\ z e. ( ran G \ { 0 } ) ) -> ( vol ` ( `' G " { z } ) ) e. RR )
81 79 80 sylan 
 |-  ( ( ( ph /\ y e. ( ran ( F oF x. G ) \ { 0 } ) ) /\ z e. ( ran G \ { 0 } ) ) -> ( vol ` ( `' G " { z } ) ) e. RR )
82 78 81 eqeltrrd 
 |-  ( ( ( ph /\ y e. ( ran ( F oF x. G ) \ { 0 } ) ) /\ z e. ( ran G \ { 0 } ) ) -> ( vol* ` ( `' G " { z } ) ) e. RR )
83 ovolsscl 
 |-  ( ( ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) C_ ( `' G " { z } ) /\ ( `' G " { z } ) C_ RR /\ ( vol* ` ( `' G " { z } ) ) e. RR ) -> ( vol* ` ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) ) e. RR )
84 73 76 82 83 syl3anc 
 |-  ( ( ( ph /\ y e. ( ran ( F oF x. G ) \ { 0 } ) ) /\ z e. ( ran G \ { 0 } ) ) -> ( vol* ` ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) ) e. RR )
85 71 84 fsumrecl 
 |-  ( ( ph /\ y e. ( ran ( F oF x. G ) \ { 0 } ) ) -> sum_ z e. ( ran G \ { 0 } ) ( vol* ` ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) ) e. RR )
86 52 fveq2d 
 |-  ( ( ph /\ y e. ( ran ( F oF x. G ) \ { 0 } ) ) -> ( vol* ` ( `' ( F oF x. G ) " { y } ) ) = ( vol* ` U_ z e. ( ran G \ { 0 } ) ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) ) )
87 mblss 
 |-  ( ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) e. dom vol -> ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) C_ RR )
88 61 87 syl 
 |-  ( ph -> ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) C_ RR )
89 88 ad2antrr 
 |-  ( ( ( ph /\ y e. ( ran ( F oF x. G ) \ { 0 } ) ) /\ z e. ( ran G \ { 0 } ) ) -> ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) C_ RR )
90 89 84 jca 
 |-  ( ( ( ph /\ y e. ( ran ( F oF x. G ) \ { 0 } ) ) /\ z e. ( ran G \ { 0 } ) ) -> ( ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) C_ RR /\ ( vol* ` ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) ) e. RR ) )
91 90 ralrimiva 
 |-  ( ( ph /\ y e. ( ran ( F oF x. G ) \ { 0 } ) ) -> A. z e. ( ran G \ { 0 } ) ( ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) C_ RR /\ ( vol* ` ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) ) e. RR ) )
92 ovolfiniun 
 |-  ( ( ( ran G \ { 0 } ) e. Fin /\ A. z e. ( ran G \ { 0 } ) ( ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) C_ RR /\ ( vol* ` ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) ) e. RR ) ) -> ( vol* ` U_ z e. ( ran G \ { 0 } ) ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) ) <_ sum_ z e. ( ran G \ { 0 } ) ( vol* ` ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) ) )
93 71 91 92 syl2anc 
 |-  ( ( ph /\ y e. ( ran ( F oF x. G ) \ { 0 } ) ) -> ( vol* ` U_ z e. ( ran G \ { 0 } ) ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) ) <_ sum_ z e. ( ran G \ { 0 } ) ( vol* ` ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) ) )
94 86 93 eqbrtrd 
 |-  ( ( ph /\ y e. ( ran ( F oF x. G ) \ { 0 } ) ) -> ( vol* ` ( `' ( F oF x. G ) " { y } ) ) <_ sum_ z e. ( ran G \ { 0 } ) ( vol* ` ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) ) )
95 ovollecl 
 |-  ( ( ( `' ( F oF x. G ) " { y } ) C_ RR /\ sum_ z e. ( ran G \ { 0 } ) ( vol* ` ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) ) e. RR /\ ( vol* ` ( `' ( F oF x. G ) " { y } ) ) <_ sum_ z e. ( ran G \ { 0 } ) ( vol* ` ( ( `' F " { ( y / z ) } ) i^i ( `' G " { z } ) ) ) ) -> ( vol* ` ( `' ( F oF x. G ) " { y } ) ) e. RR )
96 70 85 94 95 syl3anc 
 |-  ( ( ph /\ y e. ( ran ( F oF x. G ) \ { 0 } ) ) -> ( vol* ` ( `' ( F oF x. G ) " { y } ) ) e. RR )
97 68 96 eqeltrd 
 |-  ( ( ph /\ y e. ( ran ( F oF x. G ) \ { 0 } ) ) -> ( vol ` ( `' ( F oF x. G ) " { y } ) ) e. RR )
98 12 45 66 97 i1fd 
 |-  ( ph -> ( F oF x. G ) e. dom S.1 )