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 φFdom1
i1fadd.2 φGdom1
Assertion i1fmul φF×fGdom1

Proof

Step Hyp Ref Expression
1 i1fadd.1 φFdom1
2 i1fadd.2 φGdom1
3 remulcl xyxy
4 3 adantl φxyxy
5 i1ff Fdom1F:
6 1 5 syl φF:
7 i1ff Gdom1G:
8 2 7 syl φG:
9 reex V
10 9 a1i φV
11 inidm =
12 4 6 8 10 10 11 off φF×fG:
13 i1frn Fdom1ranFFin
14 1 13 syl φranFFin
15 i1frn Gdom1ranGFin
16 2 15 syl φranGFin
17 xpfi ranFFinranGFinranF×ranGFin
18 14 16 17 syl2anc φranF×ranGFin
19 eqid uranF,vranGuv=uranF,vranGuv
20 ovex uvV
21 19 20 fnmpoi uranF,vranGuvFnranF×ranG
22 dffn4 uranF,vranGuvFnranF×ranGuranF,vranGuv:ranF×ranGontoranuranF,vranGuv
23 21 22 mpbi uranF,vranGuv:ranF×ranGontoranuranF,vranGuv
24 fofi ranF×ranGFinuranF,vranGuv:ranF×ranGontoranuranF,vranGuvranuranF,vranGuvFin
25 18 23 24 sylancl φranuranF,vranGuvFin
26 eqid xy=xy
27 rspceov xranFyranGxy=xyuranFvranGxy=uv
28 26 27 mp3an3 xranFyranGuranFvranGxy=uv
29 ovex xyV
30 eqeq1 w=xyw=uvxy=uv
31 30 2rexbidv w=xyuranFvranGw=uvuranFvranGxy=uv
32 29 31 elab xyw|uranFvranGw=uvuranFvranGxy=uv
33 28 32 sylibr xranFyranGxyw|uranFvranGw=uv
34 33 adantl φxranFyranGxyw|uranFvranGw=uv
35 6 ffnd φFFn
36 dffn3 FFnF:ranF
37 35 36 sylib φF:ranF
38 8 ffnd φGFn
39 dffn3 GFnG:ranG
40 38 39 sylib φG:ranG
41 34 37 40 10 10 11 off φF×fG:w|uranFvranGw=uv
42 41 frnd φranF×fGw|uranFvranGw=uv
43 19 rnmpo ranuranF,vranGuv=w|uranFvranGw=uv
44 42 43 sseqtrrdi φranF×fGranuranF,vranGuv
45 25 44 ssfid φranF×fGFin
46 12 frnd φranF×fG
47 ax-resscn
48 46 47 sstrdi φranF×fG
49 48 ssdifd φranF×fG00
50 49 sselda φyranF×fG0y0
51 1 2 i1fmullem φy0F×fG-1y=zranG0F-1yzG-1z
52 50 51 syldan φyranF×fG0F×fG-1y=zranG0F-1yzG-1z
53 difss ranG0ranG
54 ssfi ranGFinranG0ranGranG0Fin
55 16 53 54 sylancl φranG0Fin
56 i1fima Fdom1F-1yzdomvol
57 1 56 syl φF-1yzdomvol
58 i1fima Gdom1G-1zdomvol
59 2 58 syl φG-1zdomvol
60 inmbl F-1yzdomvolG-1zdomvolF-1yzG-1zdomvol
61 57 59 60 syl2anc φF-1yzG-1zdomvol
62 61 ralrimivw φzranG0F-1yzG-1zdomvol
63 finiunmbl ranG0FinzranG0F-1yzG-1zdomvolzranG0F-1yzG-1zdomvol
64 55 62 63 syl2anc φzranG0F-1yzG-1zdomvol
65 64 adantr φyranF×fG0zranG0F-1yzG-1zdomvol
66 52 65 eqeltrd φyranF×fG0F×fG-1ydomvol
67 mblvol F×fG-1ydomvolvolF×fG-1y=vol*F×fG-1y
68 66 67 syl φyranF×fG0volF×fG-1y=vol*F×fG-1y
69 mblss F×fG-1ydomvolF×fG-1y
70 66 69 syl φyranF×fG0F×fG-1y
71 55 adantr φyranF×fG0ranG0Fin
72 inss2 F-1yzG-1zG-1z
73 72 a1i φyranF×fG0zranG0F-1yzG-1zG-1z
74 59 ad2antrr φyranF×fG0zranG0G-1zdomvol
75 mblss G-1zdomvolG-1z
76 74 75 syl φyranF×fG0zranG0G-1z
77 mblvol G-1zdomvolvolG-1z=vol*G-1z
78 74 77 syl φyranF×fG0zranG0volG-1z=vol*G-1z
79 2 adantr φyranF×fG0Gdom1
80 i1fima2sn Gdom1zranG0volG-1z
81 79 80 sylan φyranF×fG0zranG0volG-1z
82 78 81 eqeltrrd φyranF×fG0zranG0vol*G-1z
83 ovolsscl F-1yzG-1zG-1zG-1zvol*G-1zvol*F-1yzG-1z
84 73 76 82 83 syl3anc φyranF×fG0zranG0vol*F-1yzG-1z
85 71 84 fsumrecl φyranF×fG0zranG0vol*F-1yzG-1z
86 52 fveq2d φyranF×fG0vol*F×fG-1y=vol*zranG0F-1yzG-1z
87 mblss F-1yzG-1zdomvolF-1yzG-1z
88 61 87 syl φF-1yzG-1z
89 88 ad2antrr φyranF×fG0zranG0F-1yzG-1z
90 89 84 jca φyranF×fG0zranG0F-1yzG-1zvol*F-1yzG-1z
91 90 ralrimiva φyranF×fG0zranG0F-1yzG-1zvol*F-1yzG-1z
92 ovolfiniun ranG0FinzranG0F-1yzG-1zvol*F-1yzG-1zvol*zranG0F-1yzG-1zzranG0vol*F-1yzG-1z
93 71 91 92 syl2anc φyranF×fG0vol*zranG0F-1yzG-1zzranG0vol*F-1yzG-1z
94 86 93 eqbrtrd φyranF×fG0vol*F×fG-1yzranG0vol*F-1yzG-1z
95 ovollecl F×fG-1yzranG0vol*F-1yzG-1zvol*F×fG-1yzranG0vol*F-1yzG-1zvol*F×fG-1y
96 70 85 94 95 syl3anc φyranF×fG0vol*F×fG-1y
97 68 96 eqeltrd φyranF×fG0volF×fG-1y
98 12 45 66 97 i1fd φF×fGdom1