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 ( 𝑘 = 𝐺𝐵 = 𝐷 )
fprodf1o.2 ( 𝜑𝐶 ∈ Fin )
fprodf1o.3 ( 𝜑𝐹 : 𝐶1-1-onto𝐴 )
fprodf1o.4 ( ( 𝜑𝑛𝐶 ) → ( 𝐹𝑛 ) = 𝐺 )
fprodf1o.5 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ )
Assertion fprodf1o ( 𝜑 → ∏ 𝑘𝐴 𝐵 = ∏ 𝑛𝐶 𝐷 )

Proof

Step Hyp Ref Expression
1 fprodf1o.1 ( 𝑘 = 𝐺𝐵 = 𝐷 )
2 fprodf1o.2 ( 𝜑𝐶 ∈ Fin )
3 fprodf1o.3 ( 𝜑𝐹 : 𝐶1-1-onto𝐴 )
4 fprodf1o.4 ( ( 𝜑𝑛𝐶 ) → ( 𝐹𝑛 ) = 𝐺 )
5 fprodf1o.5 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ )
6 prod0 𝑘 ∈ ∅ 𝐵 = 1
7 3 adantr ( ( 𝜑𝐶 = ∅ ) → 𝐹 : 𝐶1-1-onto𝐴 )
8 f1oeq2 ( 𝐶 = ∅ → ( 𝐹 : 𝐶1-1-onto𝐴𝐹 : ∅ –1-1-onto𝐴 ) )
9 8 adantl ( ( 𝜑𝐶 = ∅ ) → ( 𝐹 : 𝐶1-1-onto𝐴𝐹 : ∅ –1-1-onto𝐴 ) )
10 7 9 mpbid ( ( 𝜑𝐶 = ∅ ) → 𝐹 : ∅ –1-1-onto𝐴 )
11 f1ofo ( 𝐹 : ∅ –1-1-onto𝐴𝐹 : ∅ –onto𝐴 )
12 10 11 syl ( ( 𝜑𝐶 = ∅ ) → 𝐹 : ∅ –onto𝐴 )
13 fo00 ( 𝐹 : ∅ –onto𝐴 ↔ ( 𝐹 = ∅ ∧ 𝐴 = ∅ ) )
14 13 simprbi ( 𝐹 : ∅ –onto𝐴𝐴 = ∅ )
15 12 14 syl ( ( 𝜑𝐶 = ∅ ) → 𝐴 = ∅ )
16 15 prodeq1d ( ( 𝜑𝐶 = ∅ ) → ∏ 𝑘𝐴 𝐵 = ∏ 𝑘 ∈ ∅ 𝐵 )
17 prodeq1 ( 𝐶 = ∅ → ∏ 𝑛𝐶 𝐷 = ∏ 𝑛 ∈ ∅ 𝐷 )
18 prod0 𝑛 ∈ ∅ 𝐷 = 1
19 17 18 eqtrdi ( 𝐶 = ∅ → ∏ 𝑛𝐶 𝐷 = 1 )
20 19 adantl ( ( 𝜑𝐶 = ∅ ) → ∏ 𝑛𝐶 𝐷 = 1 )
21 6 16 20 3eqtr4a ( ( 𝜑𝐶 = ∅ ) → ∏ 𝑘𝐴 𝐵 = ∏ 𝑛𝐶 𝐷 )
22 21 ex ( 𝜑 → ( 𝐶 = ∅ → ∏ 𝑘𝐴 𝐵 = ∏ 𝑛𝐶 𝐷 ) )
23 2fveq3 ( 𝑚 = ( 𝑓𝑛 ) → ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑚 ) ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹 ‘ ( 𝑓𝑛 ) ) ) )
24 simprl ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) → ( ♯ ‘ 𝐶 ) ∈ ℕ )
25 simprr ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 )
26 f1of ( 𝐹 : 𝐶1-1-onto𝐴𝐹 : 𝐶𝐴 )
27 3 26 syl ( 𝜑𝐹 : 𝐶𝐴 )
28 27 ffvelrnda ( ( 𝜑𝑚𝐶 ) → ( 𝐹𝑚 ) ∈ 𝐴 )
29 5 fmpttd ( 𝜑 → ( 𝑘𝐴𝐵 ) : 𝐴 ⟶ ℂ )
30 29 ffvelrnda ( ( 𝜑 ∧ ( 𝐹𝑚 ) ∈ 𝐴 ) → ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑚 ) ) ∈ ℂ )
31 28 30 syldan ( ( 𝜑𝑚𝐶 ) → ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑚 ) ) ∈ ℂ )
32 31 adantlr ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) ∧ 𝑚𝐶 ) → ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑚 ) ) ∈ ℂ )
33 simpr ( ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 )
34 f1oco ( ( 𝐹 : 𝐶1-1-onto𝐴𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) → ( 𝐹𝑓 ) : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐴 )
35 3 33 34 syl2an ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) → ( 𝐹𝑓 ) : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐴 )
36 f1of ( ( 𝐹𝑓 ) : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐴 → ( 𝐹𝑓 ) : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐴 )
37 35 36 syl ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) → ( 𝐹𝑓 ) : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐴 )
38 fvco3 ( ( ( 𝐹𝑓 ) : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐴𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( ( ( 𝑘𝐴𝐵 ) ∘ ( 𝐹𝑓 ) ) ‘ 𝑛 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( ( 𝐹𝑓 ) ‘ 𝑛 ) ) )
39 37 38 sylan ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( ( ( 𝑘𝐴𝐵 ) ∘ ( 𝐹𝑓 ) ) ‘ 𝑛 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( ( 𝐹𝑓 ) ‘ 𝑛 ) ) )
40 f1of ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐶 )
41 40 adantl ( ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐶 )
42 41 adantl ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐶 )
43 fvco3 ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐶𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( ( 𝐹𝑓 ) ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝑓𝑛 ) ) )
44 42 43 sylan ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( ( 𝐹𝑓 ) ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝑓𝑛 ) ) )
45 44 fveq2d ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( ( 𝑘𝐴𝐵 ) ‘ ( ( 𝐹𝑓 ) ‘ 𝑛 ) ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹 ‘ ( 𝑓𝑛 ) ) ) )
46 39 45 eqtrd ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( ( ( 𝑘𝐴𝐵 ) ∘ ( 𝐹𝑓 ) ) ‘ 𝑛 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹 ‘ ( 𝑓𝑛 ) ) ) )
47 23 24 25 32 46 fprod ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) → ∏ 𝑚𝐶 ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑚 ) ) = ( seq 1 ( · , ( ( 𝑘𝐴𝐵 ) ∘ ( 𝐹𝑓 ) ) ) ‘ ( ♯ ‘ 𝐶 ) ) )
48 27 ffvelrnda ( ( 𝜑𝑛𝐶 ) → ( 𝐹𝑛 ) ∈ 𝐴 )
49 4 48 eqeltrrd ( ( 𝜑𝑛𝐶 ) → 𝐺𝐴 )
50 eqid ( 𝑘𝐴𝐵 ) = ( 𝑘𝐴𝐵 )
51 1 50 fvmpti ( 𝐺𝐴 → ( ( 𝑘𝐴𝐵 ) ‘ 𝐺 ) = ( I ‘ 𝐷 ) )
52 49 51 syl ( ( 𝜑𝑛𝐶 ) → ( ( 𝑘𝐴𝐵 ) ‘ 𝐺 ) = ( I ‘ 𝐷 ) )
53 4 fveq2d ( ( 𝜑𝑛𝐶 ) → ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑛 ) ) = ( ( 𝑘𝐴𝐵 ) ‘ 𝐺 ) )
54 eqid ( 𝑛𝐶𝐷 ) = ( 𝑛𝐶𝐷 )
55 54 fvmpt2i ( 𝑛𝐶 → ( ( 𝑛𝐶𝐷 ) ‘ 𝑛 ) = ( I ‘ 𝐷 ) )
56 55 adantl ( ( 𝜑𝑛𝐶 ) → ( ( 𝑛𝐶𝐷 ) ‘ 𝑛 ) = ( I ‘ 𝐷 ) )
57 52 53 56 3eqtr4rd ( ( 𝜑𝑛𝐶 ) → ( ( 𝑛𝐶𝐷 ) ‘ 𝑛 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑛 ) ) )
58 57 ralrimiva ( 𝜑 → ∀ 𝑛𝐶 ( ( 𝑛𝐶𝐷 ) ‘ 𝑛 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑛 ) ) )
59 nffvmpt1 𝑛 ( ( 𝑛𝐶𝐷 ) ‘ 𝑚 )
60 59 nfeq1 𝑛 ( ( 𝑛𝐶𝐷 ) ‘ 𝑚 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑚 ) )
61 fveq2 ( 𝑛 = 𝑚 → ( ( 𝑛𝐶𝐷 ) ‘ 𝑛 ) = ( ( 𝑛𝐶𝐷 ) ‘ 𝑚 ) )
62 2fveq3 ( 𝑛 = 𝑚 → ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑛 ) ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑚 ) ) )
63 61 62 eqeq12d ( 𝑛 = 𝑚 → ( ( ( 𝑛𝐶𝐷 ) ‘ 𝑛 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑛 ) ) ↔ ( ( 𝑛𝐶𝐷 ) ‘ 𝑚 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑚 ) ) ) )
64 60 63 rspc ( 𝑚𝐶 → ( ∀ 𝑛𝐶 ( ( 𝑛𝐶𝐷 ) ‘ 𝑛 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑛 ) ) → ( ( 𝑛𝐶𝐷 ) ‘ 𝑚 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑚 ) ) ) )
65 58 64 mpan9 ( ( 𝜑𝑚𝐶 ) → ( ( 𝑛𝐶𝐷 ) ‘ 𝑚 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑚 ) ) )
66 65 adantlr ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) ∧ 𝑚𝐶 ) → ( ( 𝑛𝐶𝐷 ) ‘ 𝑚 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑚 ) ) )
67 66 prodeq2dv ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) → ∏ 𝑚𝐶 ( ( 𝑛𝐶𝐷 ) ‘ 𝑚 ) = ∏ 𝑚𝐶 ( ( 𝑘𝐴𝐵 ) ‘ ( 𝐹𝑚 ) ) )
68 fveq2 ( 𝑚 = ( ( 𝐹𝑓 ) ‘ 𝑛 ) → ( ( 𝑘𝐴𝐵 ) ‘ 𝑚 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( ( 𝐹𝑓 ) ‘ 𝑛 ) ) )
69 29 adantr ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) → ( 𝑘𝐴𝐵 ) : 𝐴 ⟶ ℂ )
70 69 ffvelrnda ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) ∧ 𝑚𝐴 ) → ( ( 𝑘𝐴𝐵 ) ‘ 𝑚 ) ∈ ℂ )
71 68 24 35 70 39 fprod ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) → ∏ 𝑚𝐴 ( ( 𝑘𝐴𝐵 ) ‘ 𝑚 ) = ( seq 1 ( · , ( ( 𝑘𝐴𝐵 ) ∘ ( 𝐹𝑓 ) ) ) ‘ ( ♯ ‘ 𝐶 ) ) )
72 47 67 71 3eqtr4rd ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) → ∏ 𝑚𝐴 ( ( 𝑘𝐴𝐵 ) ‘ 𝑚 ) = ∏ 𝑚𝐶 ( ( 𝑛𝐶𝐷 ) ‘ 𝑚 ) )
73 prodfc 𝑚𝐴 ( ( 𝑘𝐴𝐵 ) ‘ 𝑚 ) = ∏ 𝑘𝐴 𝐵
74 prodfc 𝑚𝐶 ( ( 𝑛𝐶𝐷 ) ‘ 𝑚 ) = ∏ 𝑛𝐶 𝐷
75 72 73 74 3eqtr3g ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) → ∏ 𝑘𝐴 𝐵 = ∏ 𝑛𝐶 𝐷 )
76 75 expr ( ( 𝜑 ∧ ( ♯ ‘ 𝐶 ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 → ∏ 𝑘𝐴 𝐵 = ∏ 𝑛𝐶 𝐷 ) )
77 76 exlimdv ( ( 𝜑 ∧ ( ♯ ‘ 𝐶 ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 → ∏ 𝑘𝐴 𝐵 = ∏ 𝑛𝐶 𝐷 ) )
78 77 expimpd ( 𝜑 → ( ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) → ∏ 𝑘𝐴 𝐵 = ∏ 𝑛𝐶 𝐷 ) )
79 fz1f1o ( 𝐶 ∈ Fin → ( 𝐶 = ∅ ∨ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) )
80 2 79 syl ( 𝜑 → ( 𝐶 = ∅ ∨ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto𝐶 ) ) )
81 22 78 80 mpjaod ( 𝜑 → ∏ 𝑘𝐴 𝐵 = ∏ 𝑛𝐶 𝐷 )