Metamath Proof Explorer


Theorem fprod2d

Description: Write a double product as a product over a two-dimensional region. Compare fsum2d . (Contributed by Scott Fenton, 30-Jan-2018)

Ref Expression
Hypotheses fprod2d.1 z=jkD=C
fprod2d.2 φAFin
fprod2d.3 φjABFin
fprod2d.4 φjAkBC
Assertion fprod2d φjAkBC=zjAj×BD

Proof

Step Hyp Ref Expression
1 fprod2d.1 z=jkD=C
2 fprod2d.2 φAFin
3 fprod2d.3 φjABFin
4 fprod2d.4 φjAkBC
5 ssid AA
6 sseq1 w=wAA
7 prodeq1 w=jwkBC=jkBC
8 iuneq1 w=jwj×B=jj×B
9 0iun jj×B=
10 8 9 eqtrdi w=jwj×B=
11 10 prodeq1d w=zjwj×BD=zD
12 7 11 eqeq12d w=jwkBC=zjwj×BDjkBC=zD
13 6 12 imbi12d w=wAjwkBC=zjwj×BDAjkBC=zD
14 13 imbi2d w=φwAjwkBC=zjwj×BDφAjkBC=zD
15 sseq1 w=xwAxA
16 prodeq1 w=xjwkBC=jxkBC
17 iuneq1 w=xjwj×B=jxj×B
18 17 prodeq1d w=xzjwj×BD=zjxj×BD
19 16 18 eqeq12d w=xjwkBC=zjwj×BDjxkBC=zjxj×BD
20 15 19 imbi12d w=xwAjwkBC=zjwj×BDxAjxkBC=zjxj×BD
21 20 imbi2d w=xφwAjwkBC=zjwj×BDφxAjxkBC=zjxj×BD
22 sseq1 w=xywAxyA
23 prodeq1 w=xyjwkBC=jxykBC
24 iuneq1 w=xyjwj×B=jxyj×B
25 24 prodeq1d w=xyzjwj×BD=zjxyj×BD
26 23 25 eqeq12d w=xyjwkBC=zjwj×BDjxykBC=zjxyj×BD
27 22 26 imbi12d w=xywAjwkBC=zjwj×BDxyAjxykBC=zjxyj×BD
28 27 imbi2d w=xyφwAjwkBC=zjwj×BDφxyAjxykBC=zjxyj×BD
29 sseq1 w=AwAAA
30 prodeq1 w=AjwkBC=jAkBC
31 iuneq1 w=Ajwj×B=jAj×B
32 31 prodeq1d w=Azjwj×BD=zjAj×BD
33 30 32 eqeq12d w=AjwkBC=zjwj×BDjAkBC=zjAj×BD
34 29 33 imbi12d w=AwAjwkBC=zjwj×BDAAjAkBC=zjAj×BD
35 34 imbi2d w=AφwAjwkBC=zjwj×BDφAAjAkBC=zjAj×BD
36 prod0 jkBC=1
37 prod0 zD=1
38 36 37 eqtr4i jkBC=zD
39 38 2a1i φAjkBC=zD
40 ssun1 xxy
41 sstr xxyxyAxA
42 40 41 mpan xyAxA
43 42 imim1i xAjxkBC=zjxj×BDxyAjxkBC=zjxj×BD
44 2 ad2antrr φ¬yxxyAAFin
45 3 ad4ant14 φ¬yxxyAjABFin
46 4 ad4ant14 φ¬yxxyAjAkBC
47 simplr φ¬yxxyA¬yx
48 simpr φ¬yxxyAxyA
49 biid jxkBC=zjxj×BDjxkBC=zjxj×BD
50 1 44 45 46 47 48 49 fprod2dlem φ¬yxxyAjxkBC=zjxj×BDjxykBC=zjxyj×BD
51 50 exp31 φ¬yxxyAjxkBC=zjxj×BDjxykBC=zjxyj×BD
52 51 a2d φ¬yxxyAjxkBC=zjxj×BDxyAjxykBC=zjxyj×BD
53 43 52 syl5 φ¬yxxAjxkBC=zjxj×BDxyAjxykBC=zjxyj×BD
54 53 expcom ¬yxφxAjxkBC=zjxj×BDxyAjxykBC=zjxyj×BD
55 54 a2d ¬yxφxAjxkBC=zjxj×BDφxyAjxykBC=zjxyj×BD
56 55 adantl xFin¬yxφxAjxkBC=zjxj×BDφxyAjxykBC=zjxyj×BD
57 14 21 28 35 39 56 findcard2s AFinφAAjAkBC=zjAj×BD
58 2 57 mpcom φAAjAkBC=zjAj×BD
59 5 58 mpi φjAkBC=zjAj×BD