Metamath Proof Explorer

Theorem fprodf1o

Description: Re-index a finite product using a bijection. (Contributed by Scott Fenton, 7-Dec-2017)

Ref Expression
Hypotheses fprodf1o.1 
|- ( k = G -> B = D )
fprodf1o.2 
|- ( ph -> C e. Fin )
fprodf1o.3 
|- ( ph -> F : C -1-1-onto-> A )
fprodf1o.4 
|- ( ( ph /\ n e. C ) -> ( F ` n ) = G )
fprodf1o.5 
|- ( ( ph /\ k e. A ) -> B e. CC )
Assertion fprodf1o 
|- ( ph -> prod_ k e. A B = prod_ n e. C D )

Proof

Step Hyp Ref Expression
1 fprodf1o.1 
 |-  ( k = G -> B = D )
2 fprodf1o.2 
 |-  ( ph -> C e. Fin )
3 fprodf1o.3 
 |-  ( ph -> F : C -1-1-onto-> A )
4 fprodf1o.4 
 |-  ( ( ph /\ n e. C ) -> ( F ` n ) = G )
5 fprodf1o.5 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
6 prod0 
 |-  prod_ k e. (/) B = 1
7 3 adantr 
 |-  ( ( ph /\ C = (/) ) -> F : C -1-1-onto-> A )
8 f1oeq2 
 |-  ( C = (/) -> ( F : C -1-1-onto-> A <-> F : (/) -1-1-onto-> A ) )
9 8 adantl 
 |-  ( ( ph /\ C = (/) ) -> ( F : C -1-1-onto-> A <-> F : (/) -1-1-onto-> A ) )
10 7 9 mpbid 
 |-  ( ( ph /\ C = (/) ) -> F : (/) -1-1-onto-> A )
11 f1ofo 
 |-  ( F : (/) -1-1-onto-> A -> F : (/) -onto-> A )
12 10 11 syl 
 |-  ( ( ph /\ C = (/) ) -> F : (/) -onto-> A )
13 fo00 
 |-  ( F : (/) -onto-> A <-> ( F = (/) /\ A = (/) ) )
14 13 simprbi 
 |-  ( F : (/) -onto-> A -> A = (/) )
15 12 14 syl 
 |-  ( ( ph /\ C = (/) ) -> A = (/) )
16 15 prodeq1d 
 |-  ( ( ph /\ C = (/) ) -> prod_ k e. A B = prod_ k e. (/) B )
17 prodeq1 
 |-  ( C = (/) -> prod_ n e. C D = prod_ n e. (/) D )
18 prod0 
 |-  prod_ n e. (/) D = 1
19 17 18 eqtrdi 
 |-  ( C = (/) -> prod_ n e. C D = 1 )
20 19 adantl 
 |-  ( ( ph /\ C = (/) ) -> prod_ n e. C D = 1 )
21 6 16 20 3eqtr4a 
 |-  ( ( ph /\ C = (/) ) -> prod_ k e. A B = prod_ n e. C D )
22 21 ex 
 |-  ( ph -> ( C = (/) -> prod_ k e. A B = prod_ n e. C D ) )
23 2fveq3 
 |-  ( m = ( f ` n ) -> ( ( k e. A |-> B ) ` ( F ` m ) ) = ( ( k e. A |-> B ) ` ( F ` ( f ` n ) ) ) )
24 simprl 
 |-  ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) -> ( # ` C ) e. NN )
25 simprr 
 |-  ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) -> f : ( 1 ... ( # ` C ) ) -1-1-onto-> C )
26 f1of 
 |-  ( F : C -1-1-onto-> A -> F : C --> A )
27 3 26 syl 
 |-  ( ph -> F : C --> A )
28 27 ffvelrnda 
 |-  ( ( ph /\ m e. C ) -> ( F ` m ) e. A )
29 5 fmpttd 
 |-  ( ph -> ( k e. A |-> B ) : A --> CC )
30 29 ffvelrnda 
 |-  ( ( ph /\ ( F ` m ) e. A ) -> ( ( k e. A |-> B ) ` ( F ` m ) ) e. CC )
31 28 30 syldan 
 |-  ( ( ph /\ m e. C ) -> ( ( k e. A |-> B ) ` ( F ` m ) ) e. CC )
32 31 adantlr 
 |-  ( ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) /\ m e. C ) -> ( ( k e. A |-> B ) ` ( F ` m ) ) e. CC )
33 simpr 
 |-  ( ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) -> f : ( 1 ... ( # ` C ) ) -1-1-onto-> C )
34 f1oco 
 |-  ( ( F : C -1-1-onto-> A /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) -> ( F o. f ) : ( 1 ... ( # ` C ) ) -1-1-onto-> A )
35 3 33 34 syl2an 
 |-  ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) -> ( F o. f ) : ( 1 ... ( # ` C ) ) -1-1-onto-> A )
36 f1of 
 |-  ( ( F o. f ) : ( 1 ... ( # ` C ) ) -1-1-onto-> A -> ( F o. f ) : ( 1 ... ( # ` C ) ) --> A )
37 35 36 syl 
 |-  ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) -> ( F o. f ) : ( 1 ... ( # ` C ) ) --> A )
38 fvco3 
 |-  ( ( ( F o. f ) : ( 1 ... ( # ` C ) ) --> A /\ n e. ( 1 ... ( # ` C ) ) ) -> ( ( ( k e. A |-> B ) o. ( F o. f ) ) ` n ) = ( ( k e. A |-> B ) ` ( ( F o. f ) ` n ) ) )
39 37 38 sylan 
 |-  ( ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) /\ n e. ( 1 ... ( # ` C ) ) ) -> ( ( ( k e. A |-> B ) o. ( F o. f ) ) ` n ) = ( ( k e. A |-> B ) ` ( ( F o. f ) ` n ) ) )
40 f1of 
 |-  ( f : ( 1 ... ( # ` C ) ) -1-1-onto-> C -> f : ( 1 ... ( # ` C ) ) --> C )
41 40 adantl 
 |-  ( ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) -> f : ( 1 ... ( # ` C ) ) --> C )
42 41 adantl 
 |-  ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) -> f : ( 1 ... ( # ` C ) ) --> C )
43 fvco3 
 |-  ( ( f : ( 1 ... ( # ` C ) ) --> C /\ n e. ( 1 ... ( # ` C ) ) ) -> ( ( F o. f ) ` n ) = ( F ` ( f ` n ) ) )
44 42 43 sylan 
 |-  ( ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) /\ n e. ( 1 ... ( # ` C ) ) ) -> ( ( F o. f ) ` n ) = ( F ` ( f ` n ) ) )
45 44 fveq2d 
 |-  ( ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) /\ n e. ( 1 ... ( # ` C ) ) ) -> ( ( k e. A |-> B ) ` ( ( F o. f ) ` n ) ) = ( ( k e. A |-> B ) ` ( F ` ( f ` n ) ) ) )
46 39 45 eqtrd 
 |-  ( ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) /\ n e. ( 1 ... ( # ` C ) ) ) -> ( ( ( k e. A |-> B ) o. ( F o. f ) ) ` n ) = ( ( k e. A |-> B ) ` ( F ` ( f ` n ) ) ) )
47 23 24 25 32 46 fprod 
 |-  ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) -> prod_ m e. C ( ( k e. A |-> B ) ` ( F ` m ) ) = ( seq 1 ( x. , ( ( k e. A |-> B ) o. ( F o. f ) ) ) ` ( # ` C ) ) )
48 27 ffvelrnda 
 |-  ( ( ph /\ n e. C ) -> ( F ` n ) e. A )
49 4 48 eqeltrrd 
 |-  ( ( ph /\ n e. C ) -> G e. A )
50 eqid 
 |-  ( k e. A |-> B ) = ( k e. A |-> B )
51 1 50 fvmpti 
 |-  ( G e. A -> ( ( k e. A |-> B ) ` G ) = ( _I ` D ) )
52 49 51 syl 
 |-  ( ( ph /\ n e. C ) -> ( ( k e. A |-> B ) ` G ) = ( _I ` D ) )
53 4 fveq2d 
 |-  ( ( ph /\ n e. C ) -> ( ( k e. A |-> B ) ` ( F ` n ) ) = ( ( k e. A |-> B ) ` G ) )
54 eqid 
 |-  ( n e. C |-> D ) = ( n e. C |-> D )
55 54 fvmpt2i 
 |-  ( n e. C -> ( ( n e. C |-> D ) ` n ) = ( _I ` D ) )
56 55 adantl 
 |-  ( ( ph /\ n e. C ) -> ( ( n e. C |-> D ) ` n ) = ( _I ` D ) )
57 52 53 56 3eqtr4rd 
 |-  ( ( ph /\ n e. C ) -> ( ( n e. C |-> D ) ` n ) = ( ( k e. A |-> B ) ` ( F ` n ) ) )
58 57 ralrimiva 
 |-  ( ph -> A. n e. C ( ( n e. C |-> D ) ` n ) = ( ( k e. A |-> B ) ` ( F ` n ) ) )
59 nffvmpt1 
 |-  F/_ n ( ( n e. C |-> D ) ` m )
60 59 nfeq1 
 |-  F/ n ( ( n e. C |-> D ) ` m ) = ( ( k e. A |-> B ) ` ( F ` m ) )
61 fveq2 
 |-  ( n = m -> ( ( n e. C |-> D ) ` n ) = ( ( n e. C |-> D ) ` m ) )
62 2fveq3 
 |-  ( n = m -> ( ( k e. A |-> B ) ` ( F ` n ) ) = ( ( k e. A |-> B ) ` ( F ` m ) ) )
63 61 62 eqeq12d 
 |-  ( n = m -> ( ( ( n e. C |-> D ) ` n ) = ( ( k e. A |-> B ) ` ( F ` n ) ) <-> ( ( n e. C |-> D ) ` m ) = ( ( k e. A |-> B ) ` ( F ` m ) ) ) )
64 60 63 rspc 
 |-  ( m e. C -> ( A. n e. C ( ( n e. C |-> D ) ` n ) = ( ( k e. A |-> B ) ` ( F ` n ) ) -> ( ( n e. C |-> D ) ` m ) = ( ( k e. A |-> B ) ` ( F ` m ) ) ) )
65 58 64 mpan9 
 |-  ( ( ph /\ m e. C ) -> ( ( n e. C |-> D ) ` m ) = ( ( k e. A |-> B ) ` ( F ` m ) ) )
66 65 adantlr 
 |-  ( ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) /\ m e. C ) -> ( ( n e. C |-> D ) ` m ) = ( ( k e. A |-> B ) ` ( F ` m ) ) )
67 66 prodeq2dv 
 |-  ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) -> prod_ m e. C ( ( n e. C |-> D ) ` m ) = prod_ m e. C ( ( k e. A |-> B ) ` ( F ` m ) ) )
68 fveq2 
 |-  ( m = ( ( F o. f ) ` n ) -> ( ( k e. A |-> B ) ` m ) = ( ( k e. A |-> B ) ` ( ( F o. f ) ` n ) ) )
69 29 adantr 
 |-  ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) -> ( k e. A |-> B ) : A --> CC )
70 69 ffvelrnda 
 |-  ( ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) /\ m e. A ) -> ( ( k e. A |-> B ) ` m ) e. CC )
71 68 24 35 70 39 fprod 
 |-  ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) -> prod_ m e. A ( ( k e. A |-> B ) ` m ) = ( seq 1 ( x. , ( ( k e. A |-> B ) o. ( F o. f ) ) ) ` ( # ` C ) ) )
72 47 67 71 3eqtr4rd 
 |-  ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) -> prod_ m e. A ( ( k e. A |-> B ) ` m ) = prod_ m e. C ( ( n e. C |-> D ) ` m ) )
73 prodfc 
 |-  prod_ m e. A ( ( k e. A |-> B ) ` m ) = prod_ k e. A B
74 prodfc 
 |-  prod_ m e. C ( ( n e. C |-> D ) ` m ) = prod_ n e. C D
75 72 73 74 3eqtr3g 
 |-  ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) -> prod_ k e. A B = prod_ n e. C D )
76 75 expr 
 |-  ( ( ph /\ ( # ` C ) e. NN ) -> ( f : ( 1 ... ( # ` C ) ) -1-1-onto-> C -> prod_ k e. A B = prod_ n e. C D ) )
77 76 exlimdv 
 |-  ( ( ph /\ ( # ` C ) e. NN ) -> ( E. f f : ( 1 ... ( # ` C ) ) -1-1-onto-> C -> prod_ k e. A B = prod_ n e. C D ) )
78 77 expimpd 
 |-  ( ph -> ( ( ( # ` C ) e. NN /\ E. f f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) -> prod_ k e. A B = prod_ n e. C D ) )
79 fz1f1o 
 |-  ( C e. Fin -> ( C = (/) \/ ( ( # ` C ) e. NN /\ E. f f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) )
80 2 79 syl 
 |-  ( ph -> ( C = (/) \/ ( ( # ` C ) e. NN /\ E. f f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) )
81 22 78 80 mpjaod 
 |-  ( ph -> prod_ k e. A B = prod_ n e. C D )