Metamath Proof Explorer


Theorem fprodrev

Description: Reversal of a finite product. (Contributed by Scott Fenton, 5-Jan-2018)

Ref Expression
Hypotheses fprodshft.1 ( 𝜑𝐾 ∈ ℤ )
fprodshft.2 ( 𝜑𝑀 ∈ ℤ )
fprodshft.3 ( 𝜑𝑁 ∈ ℤ )
fprodshft.4 ( ( 𝜑𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
fprodrev.5 ( 𝑗 = ( 𝐾𝑘 ) → 𝐴 = 𝐵 )
Assertion fprodrev ( 𝜑 → ∏ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ∏ 𝑘 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) 𝐵 )

Proof

Step Hyp Ref Expression
1 fprodshft.1 ( 𝜑𝐾 ∈ ℤ )
2 fprodshft.2 ( 𝜑𝑀 ∈ ℤ )
3 fprodshft.3 ( 𝜑𝑁 ∈ ℤ )
4 fprodshft.4 ( ( 𝜑𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
5 fprodrev.5 ( 𝑗 = ( 𝐾𝑘 ) → 𝐴 = 𝐵 )
6 fzfid ( 𝜑 → ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ∈ Fin )
7 eqid ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ↦ ( 𝐾𝑗 ) ) = ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ↦ ( 𝐾𝑗 ) )
8 1 adantr ( ( 𝜑𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ) → 𝐾 ∈ ℤ )
9 elfzelz ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) → 𝑗 ∈ ℤ )
10 9 adantl ( ( 𝜑𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ) → 𝑗 ∈ ℤ )
11 8 10 zsubcld ( ( 𝜑𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ) → ( 𝐾𝑗 ) ∈ ℤ )
12 1 adantr ( ( 𝜑𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐾 ∈ ℤ )
13 elfzelz ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ℤ )
14 13 adantl ( ( 𝜑𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑘 ∈ ℤ )
15 12 14 zsubcld ( ( 𝜑𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐾𝑘 ) ∈ ℤ )
16 simprr ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ∧ 𝑘 = ( 𝐾𝑗 ) ) ) → 𝑘 = ( 𝐾𝑗 ) )
17 simprl ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ∧ 𝑘 = ( 𝐾𝑗 ) ) ) → 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) )
18 2 adantr ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ∧ 𝑘 = ( 𝐾𝑗 ) ) ) → 𝑀 ∈ ℤ )
19 3 adantr ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ∧ 𝑘 = ( 𝐾𝑗 ) ) ) → 𝑁 ∈ ℤ )
20 1 adantr ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ∧ 𝑘 = ( 𝐾𝑗 ) ) ) → 𝐾 ∈ ℤ )
21 9 ad2antrl ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ∧ 𝑘 = ( 𝐾𝑗 ) ) ) → 𝑗 ∈ ℤ )
22 fzrev ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ↔ ( 𝐾𝑗 ) ∈ ( 𝑀 ... 𝑁 ) ) )
23 18 19 20 21 22 syl22anc ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ∧ 𝑘 = ( 𝐾𝑗 ) ) ) → ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ↔ ( 𝐾𝑗 ) ∈ ( 𝑀 ... 𝑁 ) ) )
24 17 23 mpbid ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ∧ 𝑘 = ( 𝐾𝑗 ) ) ) → ( 𝐾𝑗 ) ∈ ( 𝑀 ... 𝑁 ) )
25 16 24 eqeltrd ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ∧ 𝑘 = ( 𝐾𝑗 ) ) ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
26 oveq2 ( 𝑘 = ( 𝐾𝑗 ) → ( 𝐾𝑘 ) = ( 𝐾 − ( 𝐾𝑗 ) ) )
27 26 ad2antll ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ∧ 𝑘 = ( 𝐾𝑗 ) ) ) → ( 𝐾𝑘 ) = ( 𝐾 − ( 𝐾𝑗 ) ) )
28 1 zcnd ( 𝜑𝐾 ∈ ℂ )
29 28 adantr ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ∧ 𝑘 = ( 𝐾𝑗 ) ) ) → 𝐾 ∈ ℂ )
30 9 zcnd ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) → 𝑗 ∈ ℂ )
31 30 ad2antrl ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ∧ 𝑘 = ( 𝐾𝑗 ) ) ) → 𝑗 ∈ ℂ )
32 29 31 nncand ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ∧ 𝑘 = ( 𝐾𝑗 ) ) ) → ( 𝐾 − ( 𝐾𝑗 ) ) = 𝑗 )
33 27 32 eqtr2d ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ∧ 𝑘 = ( 𝐾𝑗 ) ) ) → 𝑗 = ( 𝐾𝑘 ) )
34 25 33 jca ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ∧ 𝑘 = ( 𝐾𝑗 ) ) ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾𝑘 ) ) )
35 simprr ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾𝑘 ) ) ) → 𝑗 = ( 𝐾𝑘 ) )
36 simprl ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾𝑘 ) ) ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
37 2 adantr ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾𝑘 ) ) ) → 𝑀 ∈ ℤ )
38 3 adantr ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾𝑘 ) ) ) → 𝑁 ∈ ℤ )
39 1 adantr ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾𝑘 ) ) ) → 𝐾 ∈ ℤ )
40 13 ad2antrl ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾𝑘 ) ) ) → 𝑘 ∈ ℤ )
41 fzrev2 ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐾𝑘 ) ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ) )
42 37 38 39 40 41 syl22anc ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾𝑘 ) ) ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐾𝑘 ) ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ) )
43 36 42 mpbid ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾𝑘 ) ) ) → ( 𝐾𝑘 ) ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) )
44 35 43 eqeltrd ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾𝑘 ) ) ) → 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) )
45 oveq2 ( 𝑗 = ( 𝐾𝑘 ) → ( 𝐾𝑗 ) = ( 𝐾 − ( 𝐾𝑘 ) ) )
46 45 ad2antll ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾𝑘 ) ) ) → ( 𝐾𝑗 ) = ( 𝐾 − ( 𝐾𝑘 ) ) )
47 28 adantr ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾𝑘 ) ) ) → 𝐾 ∈ ℂ )
48 13 zcnd ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ℂ )
49 48 ad2antrl ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾𝑘 ) ) ) → 𝑘 ∈ ℂ )
50 47 49 nncand ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾𝑘 ) ) ) → ( 𝐾 − ( 𝐾𝑘 ) ) = 𝑘 )
51 46 50 eqtr2d ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾𝑘 ) ) ) → 𝑘 = ( 𝐾𝑗 ) )
52 44 51 jca ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾𝑘 ) ) ) → ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ∧ 𝑘 = ( 𝐾𝑗 ) ) )
53 34 52 impbida ( 𝜑 → ( ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ∧ 𝑘 = ( 𝐾𝑗 ) ) ↔ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝐾𝑘 ) ) ) )
54 7 11 15 53 f1od ( 𝜑 → ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ↦ ( 𝐾𝑗 ) ) : ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) –1-1-onto→ ( 𝑀 ... 𝑁 ) )
55 oveq2 ( 𝑗 = 𝑘 → ( 𝐾𝑗 ) = ( 𝐾𝑘 ) )
56 ovex ( 𝐾𝑘 ) ∈ V
57 55 7 56 fvmpt ( 𝑘 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) → ( ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ↦ ( 𝐾𝑗 ) ) ‘ 𝑘 ) = ( 𝐾𝑘 ) )
58 57 adantl ( ( 𝜑𝑘 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ) → ( ( 𝑗 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) ↦ ( 𝐾𝑗 ) ) ‘ 𝑘 ) = ( 𝐾𝑘 ) )
59 5 6 54 58 4 fprodf1o ( 𝜑 → ∏ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ∏ 𝑘 ∈ ( ( 𝐾𝑁 ) ... ( 𝐾𝑀 ) ) 𝐵 )