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 )