Metamath Proof Explorer


Theorem mbfmullem

Description: Lemma for mbfmul . (Contributed by Mario Carneiro, 7-Sep-2014)

Ref Expression
Hypotheses mbfmul.1 φFMblFn
mbfmul.2 φGMblFn
mbfmul.3 φF:A
mbfmul.4 φG:A
Assertion mbfmullem φF×fGMblFn

Proof

Step Hyp Ref Expression
1 mbfmul.1 φFMblFn
2 mbfmul.2 φGMblFn
3 mbfmul.3 φF:A
4 mbfmul.4 φG:A
5 1 3 mbfi1flim φff:dom1yAnfnyFy
6 2 4 mbfi1flim φgg:dom1yAngnyGy
7 exdistrv fgf:dom1yAnfnyFyg:dom1yAngnyGyff:dom1yAnfnyFygg:dom1yAngnyGy
8 1 adantr φf:dom1yAnfnyFyg:dom1yAngnyGyFMblFn
9 2 adantr φf:dom1yAnfnyFyg:dom1yAngnyGyGMblFn
10 3 adantr φf:dom1yAnfnyFyg:dom1yAngnyGyF:A
11 4 adantr φf:dom1yAnfnyFyg:dom1yAngnyGyG:A
12 simprll φf:dom1yAnfnyFyg:dom1yAngnyGyf:dom1
13 simprlr φf:dom1yAnfnyFyg:dom1yAngnyGyyAnfnyFy
14 fveq2 y=xfny=fnx
15 14 mpteq2dv y=xnfny=nfnx
16 fveq2 n=mfn=fm
17 16 fveq1d n=mfnx=fmx
18 17 cbvmptv nfnx=mfmx
19 15 18 eqtrdi y=xnfny=mfmx
20 fveq2 y=xFy=Fx
21 19 20 breq12d y=xnfnyFymfmxFx
22 21 rspccva yAnfnyFyxAmfmxFx
23 13 22 sylan φf:dom1yAnfnyFyg:dom1yAngnyGyxAmfmxFx
24 simprrl φf:dom1yAnfnyFyg:dom1yAngnyGyg:dom1
25 simprrr φf:dom1yAnfnyFyg:dom1yAngnyGyyAngnyGy
26 fveq2 y=xgny=gnx
27 26 mpteq2dv y=xngny=ngnx
28 fveq2 n=mgn=gm
29 28 fveq1d n=mgnx=gmx
30 29 cbvmptv ngnx=mgmx
31 27 30 eqtrdi y=xngny=mgmx
32 fveq2 y=xGy=Gx
33 31 32 breq12d y=xngnyGymgmxGx
34 33 rspccva yAngnyGyxAmgmxGx
35 25 34 sylan φf:dom1yAnfnyFyg:dom1yAngnyGyxAmgmxGx
36 8 9 10 11 12 23 24 35 mbfmullem2 φf:dom1yAnfnyFyg:dom1yAngnyGyF×fGMblFn
37 36 ex φf:dom1yAnfnyFyg:dom1yAngnyGyF×fGMblFn
38 37 exlimdvv φfgf:dom1yAnfnyFyg:dom1yAngnyGyF×fGMblFn
39 7 38 syl5bir φff:dom1yAnfnyFygg:dom1yAngnyGyF×fGMblFn
40 5 6 39 mp2and φF×fGMblFn