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 = <. j , k >. -> D = C )
fprod2d.2
|- ( ph -> A e. Fin )
fprod2d.3
|- ( ( ph /\ j e. A ) -> B e. Fin )
fprod2d.4
|- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )
Assertion fprod2d
|- ( ph -> prod_ j e. A prod_ k e. B C = prod_ z e. U_ j e. A ( { j } X. B ) D )

Proof

Step Hyp Ref Expression
1 fprod2d.1
 |-  ( z = <. j , k >. -> D = C )
2 fprod2d.2
 |-  ( ph -> A e. Fin )
3 fprod2d.3
 |-  ( ( ph /\ j e. A ) -> B e. Fin )
4 fprod2d.4
 |-  ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )
5 ssid
 |-  A C_ A
6 sseq1
 |-  ( w = (/) -> ( w C_ A <-> (/) C_ A ) )
7 prodeq1
 |-  ( w = (/) -> prod_ j e. w prod_ k e. B C = prod_ j e. (/) prod_ k e. B C )
8 iuneq1
 |-  ( w = (/) -> U_ j e. w ( { j } X. B ) = U_ j e. (/) ( { j } X. B ) )
9 0iun
 |-  U_ j e. (/) ( { j } X. B ) = (/)
10 8 9 eqtrdi
 |-  ( w = (/) -> U_ j e. w ( { j } X. B ) = (/) )
11 10 prodeq1d
 |-  ( w = (/) -> prod_ z e. U_ j e. w ( { j } X. B ) D = prod_ z e. (/) D )
12 7 11 eqeq12d
 |-  ( w = (/) -> ( prod_ j e. w prod_ k e. B C = prod_ z e. U_ j e. w ( { j } X. B ) D <-> prod_ j e. (/) prod_ k e. B C = prod_ z e. (/) D ) )
13 6 12 imbi12d
 |-  ( w = (/) -> ( ( w C_ A -> prod_ j e. w prod_ k e. B C = prod_ z e. U_ j e. w ( { j } X. B ) D ) <-> ( (/) C_ A -> prod_ j e. (/) prod_ k e. B C = prod_ z e. (/) D ) ) )
14 13 imbi2d
 |-  ( w = (/) -> ( ( ph -> ( w C_ A -> prod_ j e. w prod_ k e. B C = prod_ z e. U_ j e. w ( { j } X. B ) D ) ) <-> ( ph -> ( (/) C_ A -> prod_ j e. (/) prod_ k e. B C = prod_ z e. (/) D ) ) ) )
15 sseq1
 |-  ( w = x -> ( w C_ A <-> x C_ A ) )
16 prodeq1
 |-  ( w = x -> prod_ j e. w prod_ k e. B C = prod_ j e. x prod_ k e. B C )
17 iuneq1
 |-  ( w = x -> U_ j e. w ( { j } X. B ) = U_ j e. x ( { j } X. B ) )
18 17 prodeq1d
 |-  ( w = x -> prod_ z e. U_ j e. w ( { j } X. B ) D = prod_ z e. U_ j e. x ( { j } X. B ) D )
19 16 18 eqeq12d
 |-  ( w = x -> ( prod_ j e. w prod_ k e. B C = prod_ z e. U_ j e. w ( { j } X. B ) D <-> prod_ j e. x prod_ k e. B C = prod_ z e. U_ j e. x ( { j } X. B ) D ) )
20 15 19 imbi12d
 |-  ( w = x -> ( ( w C_ A -> prod_ j e. w prod_ k e. B C = prod_ z e. U_ j e. w ( { j } X. B ) D ) <-> ( x C_ A -> prod_ j e. x prod_ k e. B C = prod_ z e. U_ j e. x ( { j } X. B ) D ) ) )
21 20 imbi2d
 |-  ( w = x -> ( ( ph -> ( w C_ A -> prod_ j e. w prod_ k e. B C = prod_ z e. U_ j e. w ( { j } X. B ) D ) ) <-> ( ph -> ( x C_ A -> prod_ j e. x prod_ k e. B C = prod_ z e. U_ j e. x ( { j } X. B ) D ) ) ) )
22 sseq1
 |-  ( w = ( x u. { y } ) -> ( w C_ A <-> ( x u. { y } ) C_ A ) )
23 prodeq1
 |-  ( w = ( x u. { y } ) -> prod_ j e. w prod_ k e. B C = prod_ j e. ( x u. { y } ) prod_ k e. B C )
24 iuneq1
 |-  ( w = ( x u. { y } ) -> U_ j e. w ( { j } X. B ) = U_ j e. ( x u. { y } ) ( { j } X. B ) )
25 24 prodeq1d
 |-  ( w = ( x u. { y } ) -> prod_ z e. U_ j e. w ( { j } X. B ) D = prod_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D )
26 23 25 eqeq12d
 |-  ( w = ( x u. { y } ) -> ( prod_ j e. w prod_ k e. B C = prod_ z e. U_ j e. w ( { j } X. B ) D <-> prod_ j e. ( x u. { y } ) prod_ k e. B C = prod_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D ) )
27 22 26 imbi12d
 |-  ( w = ( x u. { y } ) -> ( ( w C_ A -> prod_ j e. w prod_ k e. B C = prod_ z e. U_ j e. w ( { j } X. B ) D ) <-> ( ( x u. { y } ) C_ A -> prod_ j e. ( x u. { y } ) prod_ k e. B C = prod_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D ) ) )
28 27 imbi2d
 |-  ( w = ( x u. { y } ) -> ( ( ph -> ( w C_ A -> prod_ j e. w prod_ k e. B C = prod_ z e. U_ j e. w ( { j } X. B ) D ) ) <-> ( ph -> ( ( x u. { y } ) C_ A -> prod_ j e. ( x u. { y } ) prod_ k e. B C = prod_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D ) ) ) )
29 sseq1
 |-  ( w = A -> ( w C_ A <-> A C_ A ) )
30 prodeq1
 |-  ( w = A -> prod_ j e. w prod_ k e. B C = prod_ j e. A prod_ k e. B C )
31 iuneq1
 |-  ( w = A -> U_ j e. w ( { j } X. B ) = U_ j e. A ( { j } X. B ) )
32 31 prodeq1d
 |-  ( w = A -> prod_ z e. U_ j e. w ( { j } X. B ) D = prod_ z e. U_ j e. A ( { j } X. B ) D )
33 30 32 eqeq12d
 |-  ( w = A -> ( prod_ j e. w prod_ k e. B C = prod_ z e. U_ j e. w ( { j } X. B ) D <-> prod_ j e. A prod_ k e. B C = prod_ z e. U_ j e. A ( { j } X. B ) D ) )
34 29 33 imbi12d
 |-  ( w = A -> ( ( w C_ A -> prod_ j e. w prod_ k e. B C = prod_ z e. U_ j e. w ( { j } X. B ) D ) <-> ( A C_ A -> prod_ j e. A prod_ k e. B C = prod_ z e. U_ j e. A ( { j } X. B ) D ) ) )
35 34 imbi2d
 |-  ( w = A -> ( ( ph -> ( w C_ A -> prod_ j e. w prod_ k e. B C = prod_ z e. U_ j e. w ( { j } X. B ) D ) ) <-> ( ph -> ( A C_ A -> prod_ j e. A prod_ k e. B C = prod_ z e. U_ j e. A ( { j } X. B ) D ) ) ) )
36 prod0
 |-  prod_ j e. (/) prod_ k e. B C = 1
37 prod0
 |-  prod_ z e. (/) D = 1
38 36 37 eqtr4i
 |-  prod_ j e. (/) prod_ k e. B C = prod_ z e. (/) D
39 38 2a1i
 |-  ( ph -> ( (/) C_ A -> prod_ j e. (/) prod_ k e. B C = prod_ z e. (/) D ) )
40 ssun1
 |-  x C_ ( x u. { y } )
41 sstr
 |-  ( ( x C_ ( x u. { y } ) /\ ( x u. { y } ) C_ A ) -> x C_ A )
42 40 41 mpan
 |-  ( ( x u. { y } ) C_ A -> x C_ A )
43 42 imim1i
 |-  ( ( x C_ A -> prod_ j e. x prod_ k e. B C = prod_ z e. U_ j e. x ( { j } X. B ) D ) -> ( ( x u. { y } ) C_ A -> prod_ j e. x prod_ k e. B C = prod_ z e. U_ j e. x ( { j } X. B ) D ) )
44 2 ad2antrr
 |-  ( ( ( ph /\ -. y e. x ) /\ ( x u. { y } ) C_ A ) -> A e. Fin )
45 3 ad4ant14
 |-  ( ( ( ( ph /\ -. y e. x ) /\ ( x u. { y } ) C_ A ) /\ j e. A ) -> B e. Fin )
46 4 ad4ant14
 |-  ( ( ( ( ph /\ -. y e. x ) /\ ( x u. { y } ) C_ A ) /\ ( j e. A /\ k e. B ) ) -> C e. CC )
47 simplr
 |-  ( ( ( ph /\ -. y e. x ) /\ ( x u. { y } ) C_ A ) -> -. y e. x )
48 simpr
 |-  ( ( ( ph /\ -. y e. x ) /\ ( x u. { y } ) C_ A ) -> ( x u. { y } ) C_ A )
49 biid
 |-  ( prod_ j e. x prod_ k e. B C = prod_ z e. U_ j e. x ( { j } X. B ) D <-> prod_ j e. x prod_ k e. B C = prod_ z e. U_ j e. x ( { j } X. B ) D )
50 1 44 45 46 47 48 49 fprod2dlem
 |-  ( ( ( ( ph /\ -. y e. x ) /\ ( x u. { y } ) C_ A ) /\ prod_ j e. x prod_ k e. B C = prod_ z e. U_ j e. x ( { j } X. B ) D ) -> prod_ j e. ( x u. { y } ) prod_ k e. B C = prod_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D )
51 50 exp31
 |-  ( ( ph /\ -. y e. x ) -> ( ( x u. { y } ) C_ A -> ( prod_ j e. x prod_ k e. B C = prod_ z e. U_ j e. x ( { j } X. B ) D -> prod_ j e. ( x u. { y } ) prod_ k e. B C = prod_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D ) ) )
52 51 a2d
 |-  ( ( ph /\ -. y e. x ) -> ( ( ( x u. { y } ) C_ A -> prod_ j e. x prod_ k e. B C = prod_ z e. U_ j e. x ( { j } X. B ) D ) -> ( ( x u. { y } ) C_ A -> prod_ j e. ( x u. { y } ) prod_ k e. B C = prod_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D ) ) )
53 43 52 syl5
 |-  ( ( ph /\ -. y e. x ) -> ( ( x C_ A -> prod_ j e. x prod_ k e. B C = prod_ z e. U_ j e. x ( { j } X. B ) D ) -> ( ( x u. { y } ) C_ A -> prod_ j e. ( x u. { y } ) prod_ k e. B C = prod_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D ) ) )
54 53 expcom
 |-  ( -. y e. x -> ( ph -> ( ( x C_ A -> prod_ j e. x prod_ k e. B C = prod_ z e. U_ j e. x ( { j } X. B ) D ) -> ( ( x u. { y } ) C_ A -> prod_ j e. ( x u. { y } ) prod_ k e. B C = prod_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D ) ) ) )
55 54 a2d
 |-  ( -. y e. x -> ( ( ph -> ( x C_ A -> prod_ j e. x prod_ k e. B C = prod_ z e. U_ j e. x ( { j } X. B ) D ) ) -> ( ph -> ( ( x u. { y } ) C_ A -> prod_ j e. ( x u. { y } ) prod_ k e. B C = prod_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D ) ) ) )
56 55 adantl
 |-  ( ( x e. Fin /\ -. y e. x ) -> ( ( ph -> ( x C_ A -> prod_ j e. x prod_ k e. B C = prod_ z e. U_ j e. x ( { j } X. B ) D ) ) -> ( ph -> ( ( x u. { y } ) C_ A -> prod_ j e. ( x u. { y } ) prod_ k e. B C = prod_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D ) ) ) )
57 14 21 28 35 39 56 findcard2s
 |-  ( A e. Fin -> ( ph -> ( A C_ A -> prod_ j e. A prod_ k e. B C = prod_ z e. U_ j e. A ( { j } X. B ) D ) ) )
58 2 57 mpcom
 |-  ( ph -> ( A C_ A -> prod_ j e. A prod_ k e. B C = prod_ z e. U_ j e. A ( { j } X. B ) D ) )
59 5 58 mpi
 |-  ( ph -> prod_ j e. A prod_ k e. B C = prod_ z e. U_ j e. A ( { j } X. B ) D )