# 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}\to {B}={D}$
fprodf1o.2 ${⊢}{\phi }\to {C}\in \mathrm{Fin}$
fprodf1o.3 ${⊢}{\phi }\to {F}:{C}\underset{1-1 onto}{⟶}{A}$
fprodf1o.4 ${⊢}\left({\phi }\wedge {n}\in {C}\right)\to {F}\left({n}\right)={G}$
fprodf1o.5 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
Assertion fprodf1o ${⊢}{\phi }\to \prod _{{k}\in {A}}{B}=\prod _{{n}\in {C}}{D}$

### Proof

Step Hyp Ref Expression
1 fprodf1o.1 ${⊢}{k}={G}\to {B}={D}$
2 fprodf1o.2 ${⊢}{\phi }\to {C}\in \mathrm{Fin}$
3 fprodf1o.3 ${⊢}{\phi }\to {F}:{C}\underset{1-1 onto}{⟶}{A}$
4 fprodf1o.4 ${⊢}\left({\phi }\wedge {n}\in {C}\right)\to {F}\left({n}\right)={G}$
5 fprodf1o.5 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
6 prod0 ${⊢}\prod _{{k}\in \varnothing }{B}=1$
7 3 adantr ${⊢}\left({\phi }\wedge {C}=\varnothing \right)\to {F}:{C}\underset{1-1 onto}{⟶}{A}$
8 f1oeq2 ${⊢}{C}=\varnothing \to \left({F}:{C}\underset{1-1 onto}{⟶}{A}↔{F}:\varnothing \underset{1-1 onto}{⟶}{A}\right)$
9 8 adantl ${⊢}\left({\phi }\wedge {C}=\varnothing \right)\to \left({F}:{C}\underset{1-1 onto}{⟶}{A}↔{F}:\varnothing \underset{1-1 onto}{⟶}{A}\right)$
10 7 9 mpbid ${⊢}\left({\phi }\wedge {C}=\varnothing \right)\to {F}:\varnothing \underset{1-1 onto}{⟶}{A}$
11 f1ofo ${⊢}{F}:\varnothing \underset{1-1 onto}{⟶}{A}\to {F}:\varnothing \underset{onto}{⟶}{A}$
12 10 11 syl ${⊢}\left({\phi }\wedge {C}=\varnothing \right)\to {F}:\varnothing \underset{onto}{⟶}{A}$
13 fo00 ${⊢}{F}:\varnothing \underset{onto}{⟶}{A}↔\left({F}=\varnothing \wedge {A}=\varnothing \right)$
14 13 simprbi ${⊢}{F}:\varnothing \underset{onto}{⟶}{A}\to {A}=\varnothing$
15 12 14 syl ${⊢}\left({\phi }\wedge {C}=\varnothing \right)\to {A}=\varnothing$
16 15 prodeq1d ${⊢}\left({\phi }\wedge {C}=\varnothing \right)\to \prod _{{k}\in {A}}{B}=\prod _{{k}\in \varnothing }{B}$
17 prodeq1 ${⊢}{C}=\varnothing \to \prod _{{n}\in {C}}{D}=\prod _{{n}\in \varnothing }{D}$
18 prod0 ${⊢}\prod _{{n}\in \varnothing }{D}=1$
19 17 18 eqtrdi ${⊢}{C}=\varnothing \to \prod _{{n}\in {C}}{D}=1$
20 19 adantl ${⊢}\left({\phi }\wedge {C}=\varnothing \right)\to \prod _{{n}\in {C}}{D}=1$
21 6 16 20 3eqtr4a ${⊢}\left({\phi }\wedge {C}=\varnothing \right)\to \prod _{{k}\in {A}}{B}=\prod _{{n}\in {C}}{D}$
22 21 ex ${⊢}{\phi }\to \left({C}=\varnothing \to \prod _{{k}\in {A}}{B}=\prod _{{n}\in {C}}{D}\right)$
23 2fveq3 ${⊢}{m}={f}\left({n}\right)\to \left({k}\in {A}⟼{B}\right)\left({F}\left({m}\right)\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({f}\left({n}\right)\right)\right)$
24 simprl ${⊢}\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\to \left|{C}\right|\in ℕ$
25 simprr ${⊢}\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\to {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}$
26 f1of ${⊢}{F}:{C}\underset{1-1 onto}{⟶}{A}\to {F}:{C}⟶{A}$
27 3 26 syl ${⊢}{\phi }\to {F}:{C}⟶{A}$
28 27 ffvelrnda ${⊢}\left({\phi }\wedge {m}\in {C}\right)\to {F}\left({m}\right)\in {A}$
29 5 fmpttd ${⊢}{\phi }\to \left({k}\in {A}⟼{B}\right):{A}⟶ℂ$
30 29 ffvelrnda ${⊢}\left({\phi }\wedge {F}\left({m}\right)\in {A}\right)\to \left({k}\in {A}⟼{B}\right)\left({F}\left({m}\right)\right)\in ℂ$
31 28 30 syldan ${⊢}\left({\phi }\wedge {m}\in {C}\right)\to \left({k}\in {A}⟼{B}\right)\left({F}\left({m}\right)\right)\in ℂ$
32 31 adantlr ${⊢}\left(\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\wedge {m}\in {C}\right)\to \left({k}\in {A}⟼{B}\right)\left({F}\left({m}\right)\right)\in ℂ$
33 simpr ${⊢}\left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\to {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}$
34 f1oco ${⊢}\left({F}:{C}\underset{1-1 onto}{⟶}{A}\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\to \left({F}\circ {f}\right):\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{A}$
35 3 33 34 syl2an ${⊢}\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\to \left({F}\circ {f}\right):\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{A}$
36 f1of ${⊢}\left({F}\circ {f}\right):\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{A}\to \left({F}\circ {f}\right):\left(1\dots \left|{C}\right|\right)⟶{A}$
37 35 36 syl ${⊢}\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\to \left({F}\circ {f}\right):\left(1\dots \left|{C}\right|\right)⟶{A}$
38 fvco3 ${⊢}\left(\left({F}\circ {f}\right):\left(1\dots \left|{C}\right|\right)⟶{A}\wedge {n}\in \left(1\dots \left|{C}\right|\right)\right)\to \left(\left({k}\in {A}⟼{B}\right)\circ \left({F}\circ {f}\right)\right)\left({n}\right)=\left({k}\in {A}⟼{B}\right)\left(\left({F}\circ {f}\right)\left({n}\right)\right)$
39 37 38 sylan ${⊢}\left(\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\wedge {n}\in \left(1\dots \left|{C}\right|\right)\right)\to \left(\left({k}\in {A}⟼{B}\right)\circ \left({F}\circ {f}\right)\right)\left({n}\right)=\left({k}\in {A}⟼{B}\right)\left(\left({F}\circ {f}\right)\left({n}\right)\right)$
40 f1of ${⊢}{f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\to {f}:\left(1\dots \left|{C}\right|\right)⟶{C}$
41 40 adantl ${⊢}\left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\to {f}:\left(1\dots \left|{C}\right|\right)⟶{C}$
42 41 adantl ${⊢}\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\to {f}:\left(1\dots \left|{C}\right|\right)⟶{C}$
43 fvco3 ${⊢}\left({f}:\left(1\dots \left|{C}\right|\right)⟶{C}\wedge {n}\in \left(1\dots \left|{C}\right|\right)\right)\to \left({F}\circ {f}\right)\left({n}\right)={F}\left({f}\left({n}\right)\right)$
44 42 43 sylan ${⊢}\left(\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\wedge {n}\in \left(1\dots \left|{C}\right|\right)\right)\to \left({F}\circ {f}\right)\left({n}\right)={F}\left({f}\left({n}\right)\right)$
45 44 fveq2d ${⊢}\left(\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\wedge {n}\in \left(1\dots \left|{C}\right|\right)\right)\to \left({k}\in {A}⟼{B}\right)\left(\left({F}\circ {f}\right)\left({n}\right)\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({f}\left({n}\right)\right)\right)$
46 39 45 eqtrd ${⊢}\left(\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\wedge {n}\in \left(1\dots \left|{C}\right|\right)\right)\to \left(\left({k}\in {A}⟼{B}\right)\circ \left({F}\circ {f}\right)\right)\left({n}\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({f}\left({n}\right)\right)\right)$
47 23 24 25 32 46 fprod ${⊢}\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\to \prod _{{m}\in {C}}\left({k}\in {A}⟼{B}\right)\left({F}\left({m}\right)\right)=seq1\left(×,\left(\left({k}\in {A}⟼{B}\right)\circ \left({F}\circ {f}\right)\right)\right)\left(\left|{C}\right|\right)$
48 27 ffvelrnda ${⊢}\left({\phi }\wedge {n}\in {C}\right)\to {F}\left({n}\right)\in {A}$
49 4 48 eqeltrrd ${⊢}\left({\phi }\wedge {n}\in {C}\right)\to {G}\in {A}$
50 eqid ${⊢}\left({k}\in {A}⟼{B}\right)=\left({k}\in {A}⟼{B}\right)$
51 1 50 fvmpti ${⊢}{G}\in {A}\to \left({k}\in {A}⟼{B}\right)\left({G}\right)=\mathrm{I}\left({D}\right)$
52 49 51 syl ${⊢}\left({\phi }\wedge {n}\in {C}\right)\to \left({k}\in {A}⟼{B}\right)\left({G}\right)=\mathrm{I}\left({D}\right)$
53 4 fveq2d ${⊢}\left({\phi }\wedge {n}\in {C}\right)\to \left({k}\in {A}⟼{B}\right)\left({F}\left({n}\right)\right)=\left({k}\in {A}⟼{B}\right)\left({G}\right)$
54 eqid ${⊢}\left({n}\in {C}⟼{D}\right)=\left({n}\in {C}⟼{D}\right)$
55 54 fvmpt2i ${⊢}{n}\in {C}\to \left({n}\in {C}⟼{D}\right)\left({n}\right)=\mathrm{I}\left({D}\right)$
56 55 adantl ${⊢}\left({\phi }\wedge {n}\in {C}\right)\to \left({n}\in {C}⟼{D}\right)\left({n}\right)=\mathrm{I}\left({D}\right)$
57 52 53 56 3eqtr4rd ${⊢}\left({\phi }\wedge {n}\in {C}\right)\to \left({n}\in {C}⟼{D}\right)\left({n}\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({n}\right)\right)$
58 57 ralrimiva ${⊢}{\phi }\to \forall {n}\in {C}\phantom{\rule{.4em}{0ex}}\left({n}\in {C}⟼{D}\right)\left({n}\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({n}\right)\right)$
59 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left({n}\in {C}⟼{D}\right)\left({m}\right)$
60 59 nfeq1 ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\left({n}\in {C}⟼{D}\right)\left({m}\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({m}\right)\right)$
61 fveq2 ${⊢}{n}={m}\to \left({n}\in {C}⟼{D}\right)\left({n}\right)=\left({n}\in {C}⟼{D}\right)\left({m}\right)$
62 2fveq3 ${⊢}{n}={m}\to \left({k}\in {A}⟼{B}\right)\left({F}\left({n}\right)\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({m}\right)\right)$
63 61 62 eqeq12d ${⊢}{n}={m}\to \left(\left({n}\in {C}⟼{D}\right)\left({n}\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({n}\right)\right)↔\left({n}\in {C}⟼{D}\right)\left({m}\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({m}\right)\right)\right)$
64 60 63 rspc ${⊢}{m}\in {C}\to \left(\forall {n}\in {C}\phantom{\rule{.4em}{0ex}}\left({n}\in {C}⟼{D}\right)\left({n}\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({n}\right)\right)\to \left({n}\in {C}⟼{D}\right)\left({m}\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({m}\right)\right)\right)$
65 58 64 mpan9 ${⊢}\left({\phi }\wedge {m}\in {C}\right)\to \left({n}\in {C}⟼{D}\right)\left({m}\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({m}\right)\right)$
66 65 adantlr ${⊢}\left(\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\wedge {m}\in {C}\right)\to \left({n}\in {C}⟼{D}\right)\left({m}\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({m}\right)\right)$
67 66 prodeq2dv ${⊢}\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\to \prod _{{m}\in {C}}\left({n}\in {C}⟼{D}\right)\left({m}\right)=\prod _{{m}\in {C}}\left({k}\in {A}⟼{B}\right)\left({F}\left({m}\right)\right)$
68 fveq2 ${⊢}{m}=\left({F}\circ {f}\right)\left({n}\right)\to \left({k}\in {A}⟼{B}\right)\left({m}\right)=\left({k}\in {A}⟼{B}\right)\left(\left({F}\circ {f}\right)\left({n}\right)\right)$
69 29 adantr ${⊢}\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\to \left({k}\in {A}⟼{B}\right):{A}⟶ℂ$
70 69 ffvelrnda ${⊢}\left(\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\wedge {m}\in {A}\right)\to \left({k}\in {A}⟼{B}\right)\left({m}\right)\in ℂ$
71 68 24 35 70 39 fprod ${⊢}\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\to \prod _{{m}\in {A}}\left({k}\in {A}⟼{B}\right)\left({m}\right)=seq1\left(×,\left(\left({k}\in {A}⟼{B}\right)\circ \left({F}\circ {f}\right)\right)\right)\left(\left|{C}\right|\right)$
72 47 67 71 3eqtr4rd ${⊢}\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\to \prod _{{m}\in {A}}\left({k}\in {A}⟼{B}\right)\left({m}\right)=\prod _{{m}\in {C}}\left({n}\in {C}⟼{D}\right)\left({m}\right)$
73 prodfc ${⊢}\prod _{{m}\in {A}}\left({k}\in {A}⟼{B}\right)\left({m}\right)=\prod _{{k}\in {A}}{B}$
74 prodfc ${⊢}\prod _{{m}\in {C}}\left({n}\in {C}⟼{D}\right)\left({m}\right)=\prod _{{n}\in {C}}{D}$
75 72 73 74 3eqtr3g ${⊢}\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\to \prod _{{k}\in {A}}{B}=\prod _{{n}\in {C}}{D}$
76 75 expr ${⊢}\left({\phi }\wedge \left|{C}\right|\in ℕ\right)\to \left({f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\to \prod _{{k}\in {A}}{B}=\prod _{{n}\in {C}}{D}\right)$
77 76 exlimdv ${⊢}\left({\phi }\wedge \left|{C}\right|\in ℕ\right)\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\to \prod _{{k}\in {A}}{B}=\prod _{{n}\in {C}}{D}\right)$
78 77 expimpd ${⊢}{\phi }\to \left(\left(\left|{C}\right|\in ℕ\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\to \prod _{{k}\in {A}}{B}=\prod _{{n}\in {C}}{D}\right)$
79 fz1f1o ${⊢}{C}\in \mathrm{Fin}\to \left({C}=\varnothing \vee \left(\left|{C}\right|\in ℕ\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)$
80 2 79 syl ${⊢}{\phi }\to \left({C}=\varnothing \vee \left(\left|{C}\right|\in ℕ\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)$
81 22 78 80 mpjaod ${⊢}{\phi }\to \prod _{{k}\in {A}}{B}=\prod _{{n}\in {C}}{D}$