MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fprodf1o Structured version   Visualization version   GIF version

Theorem fprodf1o 14670
Description: Re-index a finite product using a bijection. (Contributed by Scott Fenton, 7-Dec-2017.)
Hypotheses
Ref Expression
fprodf1o.1 (𝑘 = 𝐺𝐵 = 𝐷)
fprodf1o.2 (𝜑𝐶 ∈ Fin)
fprodf1o.3 (𝜑𝐹:𝐶1-1-onto𝐴)
fprodf1o.4 ((𝜑𝑛𝐶) → (𝐹𝑛) = 𝐺)
fprodf1o.5 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
Assertion
Ref Expression
fprodf1o (𝜑 → ∏𝑘𝐴 𝐵 = ∏𝑛𝐶 𝐷)
Distinct variable groups:   𝐴,𝑘,𝑛   𝐵,𝑛   𝐶,𝑛   𝐷,𝑘   𝑛,𝐹   𝑘,𝐺   𝑘,𝑛,𝜑
Allowed substitution hints:   𝐵(𝑘)   𝐶(𝑘)   𝐷(𝑛)   𝐹(𝑘)   𝐺(𝑛)

Proof of Theorem fprodf1o
Dummy variables 𝑓 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prod0 14667 . . . 4 𝑘 ∈ ∅ 𝐵 = 1
2 fprodf1o.3 . . . . . . . . 9 (𝜑𝐹:𝐶1-1-onto𝐴)
32adantr 481 . . . . . . . 8 ((𝜑𝐶 = ∅) → 𝐹:𝐶1-1-onto𝐴)
4 f1oeq2 6126 . . . . . . . . 9 (𝐶 = ∅ → (𝐹:𝐶1-1-onto𝐴𝐹:∅–1-1-onto𝐴))
54adantl 482 . . . . . . . 8 ((𝜑𝐶 = ∅) → (𝐹:𝐶1-1-onto𝐴𝐹:∅–1-1-onto𝐴))
63, 5mpbid 222 . . . . . . 7 ((𝜑𝐶 = ∅) → 𝐹:∅–1-1-onto𝐴)
7 f1ofo 6142 . . . . . . 7 (𝐹:∅–1-1-onto𝐴𝐹:∅–onto𝐴)
86, 7syl 17 . . . . . 6 ((𝜑𝐶 = ∅) → 𝐹:∅–onto𝐴)
9 fo00 6170 . . . . . . 7 (𝐹:∅–onto𝐴 ↔ (𝐹 = ∅ ∧ 𝐴 = ∅))
109simprbi 480 . . . . . 6 (𝐹:∅–onto𝐴𝐴 = ∅)
118, 10syl 17 . . . . 5 ((𝜑𝐶 = ∅) → 𝐴 = ∅)
1211prodeq1d 14645 . . . 4 ((𝜑𝐶 = ∅) → ∏𝑘𝐴 𝐵 = ∏𝑘 ∈ ∅ 𝐵)
13 prodeq1 14633 . . . . . 6 (𝐶 = ∅ → ∏𝑛𝐶 𝐷 = ∏𝑛 ∈ ∅ 𝐷)
14 prod0 14667 . . . . . 6 𝑛 ∈ ∅ 𝐷 = 1
1513, 14syl6eq 2671 . . . . 5 (𝐶 = ∅ → ∏𝑛𝐶 𝐷 = 1)
1615adantl 482 . . . 4 ((𝜑𝐶 = ∅) → ∏𝑛𝐶 𝐷 = 1)
171, 12, 163eqtr4a 2681 . . 3 ((𝜑𝐶 = ∅) → ∏𝑘𝐴 𝐵 = ∏𝑛𝐶 𝐷)
1817ex 450 . 2 (𝜑 → (𝐶 = ∅ → ∏𝑘𝐴 𝐵 = ∏𝑛𝐶 𝐷))
19 fveq2 6189 . . . . . . . . 9 (𝑚 = (𝑓𝑛) → (𝐹𝑚) = (𝐹‘(𝑓𝑛)))
2019fveq2d 6193 . . . . . . . 8 (𝑚 = (𝑓𝑛) → ((𝑘𝐴𝐵)‘(𝐹𝑚)) = ((𝑘𝐴𝐵)‘(𝐹‘(𝑓𝑛))))
21 simprl 794 . . . . . . . 8 ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto𝐶)) → (#‘𝐶) ∈ ℕ)
22 simprr 796 . . . . . . . 8 ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto𝐶)) → 𝑓:(1...(#‘𝐶))–1-1-onto𝐶)
23 f1of 6135 . . . . . . . . . . . 12 (𝐹:𝐶1-1-onto𝐴𝐹:𝐶𝐴)
242, 23syl 17 . . . . . . . . . . 11 (𝜑𝐹:𝐶𝐴)
2524ffvelrnda 6357 . . . . . . . . . 10 ((𝜑𝑚𝐶) → (𝐹𝑚) ∈ 𝐴)
26 fprodf1o.5 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
27 eqid 2621 . . . . . . . . . . . 12 (𝑘𝐴𝐵) = (𝑘𝐴𝐵)
2826, 27fmptd 6383 . . . . . . . . . . 11 (𝜑 → (𝑘𝐴𝐵):𝐴⟶ℂ)
2928ffvelrnda 6357 . . . . . . . . . 10 ((𝜑 ∧ (𝐹𝑚) ∈ 𝐴) → ((𝑘𝐴𝐵)‘(𝐹𝑚)) ∈ ℂ)
3025, 29syldan 487 . . . . . . . . 9 ((𝜑𝑚𝐶) → ((𝑘𝐴𝐵)‘(𝐹𝑚)) ∈ ℂ)
3130adantlr 751 . . . . . . . 8 (((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto𝐶)) ∧ 𝑚𝐶) → ((𝑘𝐴𝐵)‘(𝐹𝑚)) ∈ ℂ)
32 simpr 477 . . . . . . . . . . . 12 (((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto𝐶) → 𝑓:(1...(#‘𝐶))–1-1-onto𝐶)
33 f1oco 6157 . . . . . . . . . . . 12 ((𝐹:𝐶1-1-onto𝐴𝑓:(1...(#‘𝐶))–1-1-onto𝐶) → (𝐹𝑓):(1...(#‘𝐶))–1-1-onto𝐴)
342, 32, 33syl2an 494 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto𝐶)) → (𝐹𝑓):(1...(#‘𝐶))–1-1-onto𝐴)
35 f1of 6135 . . . . . . . . . . 11 ((𝐹𝑓):(1...(#‘𝐶))–1-1-onto𝐴 → (𝐹𝑓):(1...(#‘𝐶))⟶𝐴)
3634, 35syl 17 . . . . . . . . . 10 ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto𝐶)) → (𝐹𝑓):(1...(#‘𝐶))⟶𝐴)
37 fvco3 6273 . . . . . . . . . 10 (((𝐹𝑓):(1...(#‘𝐶))⟶𝐴𝑛 ∈ (1...(#‘𝐶))) → (((𝑘𝐴𝐵) ∘ (𝐹𝑓))‘𝑛) = ((𝑘𝐴𝐵)‘((𝐹𝑓)‘𝑛)))
3836, 37sylan 488 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto𝐶)) ∧ 𝑛 ∈ (1...(#‘𝐶))) → (((𝑘𝐴𝐵) ∘ (𝐹𝑓))‘𝑛) = ((𝑘𝐴𝐵)‘((𝐹𝑓)‘𝑛)))
39 f1of 6135 . . . . . . . . . . . . 13 (𝑓:(1...(#‘𝐶))–1-1-onto𝐶𝑓:(1...(#‘𝐶))⟶𝐶)
4039adantl 482 . . . . . . . . . . . 12 (((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto𝐶) → 𝑓:(1...(#‘𝐶))⟶𝐶)
4140adantl 482 . . . . . . . . . . 11 ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto𝐶)) → 𝑓:(1...(#‘𝐶))⟶𝐶)
42 fvco3 6273 . . . . . . . . . . 11 ((𝑓:(1...(#‘𝐶))⟶𝐶𝑛 ∈ (1...(#‘𝐶))) → ((𝐹𝑓)‘𝑛) = (𝐹‘(𝑓𝑛)))
4341, 42sylan 488 . . . . . . . . . 10 (((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto𝐶)) ∧ 𝑛 ∈ (1...(#‘𝐶))) → ((𝐹𝑓)‘𝑛) = (𝐹‘(𝑓𝑛)))
4443fveq2d 6193 . . . . . . . . 9 (((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto𝐶)) ∧ 𝑛 ∈ (1...(#‘𝐶))) → ((𝑘𝐴𝐵)‘((𝐹𝑓)‘𝑛)) = ((𝑘𝐴𝐵)‘(𝐹‘(𝑓𝑛))))
4538, 44eqtrd 2655 . . . . . . . 8 (((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto𝐶)) ∧ 𝑛 ∈ (1...(#‘𝐶))) → (((𝑘𝐴𝐵) ∘ (𝐹𝑓))‘𝑛) = ((𝑘𝐴𝐵)‘(𝐹‘(𝑓𝑛))))
4620, 21, 22, 31, 45fprod 14665 . . . . . . 7 ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto𝐶)) → ∏𝑚𝐶 ((𝑘𝐴𝐵)‘(𝐹𝑚)) = (seq1( · , ((𝑘𝐴𝐵) ∘ (𝐹𝑓)))‘(#‘𝐶)))
47 fprodf1o.4 . . . . . . . . . . . . . 14 ((𝜑𝑛𝐶) → (𝐹𝑛) = 𝐺)
4824ffvelrnda 6357 . . . . . . . . . . . . . 14 ((𝜑𝑛𝐶) → (𝐹𝑛) ∈ 𝐴)
4947, 48eqeltrrd 2701 . . . . . . . . . . . . 13 ((𝜑𝑛𝐶) → 𝐺𝐴)
50 fprodf1o.1 . . . . . . . . . . . . . 14 (𝑘 = 𝐺𝐵 = 𝐷)
5150, 27fvmpti 6279 . . . . . . . . . . . . 13 (𝐺𝐴 → ((𝑘𝐴𝐵)‘𝐺) = ( I ‘𝐷))
5249, 51syl 17 . . . . . . . . . . . 12 ((𝜑𝑛𝐶) → ((𝑘𝐴𝐵)‘𝐺) = ( I ‘𝐷))
5347fveq2d 6193 . . . . . . . . . . . 12 ((𝜑𝑛𝐶) → ((𝑘𝐴𝐵)‘(𝐹𝑛)) = ((𝑘𝐴𝐵)‘𝐺))
54 eqid 2621 . . . . . . . . . . . . . 14 (𝑛𝐶𝐷) = (𝑛𝐶𝐷)
5554fvmpt2i 6288 . . . . . . . . . . . . 13 (𝑛𝐶 → ((𝑛𝐶𝐷)‘𝑛) = ( I ‘𝐷))
5655adantl 482 . . . . . . . . . . . 12 ((𝜑𝑛𝐶) → ((𝑛𝐶𝐷)‘𝑛) = ( I ‘𝐷))
5752, 53, 563eqtr4rd 2666 . . . . . . . . . . 11 ((𝜑𝑛𝐶) → ((𝑛𝐶𝐷)‘𝑛) = ((𝑘𝐴𝐵)‘(𝐹𝑛)))
5857ralrimiva 2965 . . . . . . . . . 10 (𝜑 → ∀𝑛𝐶 ((𝑛𝐶𝐷)‘𝑛) = ((𝑘𝐴𝐵)‘(𝐹𝑛)))
59 nffvmpt1 6197 . . . . . . . . . . . 12 𝑛((𝑛𝐶𝐷)‘𝑚)
6059nfeq1 2777 . . . . . . . . . . 11 𝑛((𝑛𝐶𝐷)‘𝑚) = ((𝑘𝐴𝐵)‘(𝐹𝑚))
61 fveq2 6189 . . . . . . . . . . . 12 (𝑛 = 𝑚 → ((𝑛𝐶𝐷)‘𝑛) = ((𝑛𝐶𝐷)‘𝑚))
62 fveq2 6189 . . . . . . . . . . . . 13 (𝑛 = 𝑚 → (𝐹𝑛) = (𝐹𝑚))
6362fveq2d 6193 . . . . . . . . . . . 12 (𝑛 = 𝑚 → ((𝑘𝐴𝐵)‘(𝐹𝑛)) = ((𝑘𝐴𝐵)‘(𝐹𝑚)))
6461, 63eqeq12d 2636 . . . . . . . . . . 11 (𝑛 = 𝑚 → (((𝑛𝐶𝐷)‘𝑛) = ((𝑘𝐴𝐵)‘(𝐹𝑛)) ↔ ((𝑛𝐶𝐷)‘𝑚) = ((𝑘𝐴𝐵)‘(𝐹𝑚))))
6560, 64rspc 3301 . . . . . . . . . 10 (𝑚𝐶 → (∀𝑛𝐶 ((𝑛𝐶𝐷)‘𝑛) = ((𝑘𝐴𝐵)‘(𝐹𝑛)) → ((𝑛𝐶𝐷)‘𝑚) = ((𝑘𝐴𝐵)‘(𝐹𝑚))))
6658, 65mpan9 486 . . . . . . . . 9 ((𝜑𝑚𝐶) → ((𝑛𝐶𝐷)‘𝑚) = ((𝑘𝐴𝐵)‘(𝐹𝑚)))
6766adantlr 751 . . . . . . . 8 (((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto𝐶)) ∧ 𝑚𝐶) → ((𝑛𝐶𝐷)‘𝑚) = ((𝑘𝐴𝐵)‘(𝐹𝑚)))
6867prodeq2dv 14647 . . . . . . 7 ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto𝐶)) → ∏𝑚𝐶 ((𝑛𝐶𝐷)‘𝑚) = ∏𝑚𝐶 ((𝑘𝐴𝐵)‘(𝐹𝑚)))
69 fveq2 6189 . . . . . . . 8 (𝑚 = ((𝐹𝑓)‘𝑛) → ((𝑘𝐴𝐵)‘𝑚) = ((𝑘𝐴𝐵)‘((𝐹𝑓)‘𝑛)))
7028adantr 481 . . . . . . . . 9 ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto𝐶)) → (𝑘𝐴𝐵):𝐴⟶ℂ)
7170ffvelrnda 6357 . . . . . . . 8 (((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto𝐶)) ∧ 𝑚𝐴) → ((𝑘𝐴𝐵)‘𝑚) ∈ ℂ)
7269, 21, 34, 71, 38fprod 14665 . . . . . . 7 ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto𝐶)) → ∏𝑚𝐴 ((𝑘𝐴𝐵)‘𝑚) = (seq1( · , ((𝑘𝐴𝐵) ∘ (𝐹𝑓)))‘(#‘𝐶)))
7346, 68, 723eqtr4rd 2666 . . . . . 6 ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto𝐶)) → ∏𝑚𝐴 ((𝑘𝐴𝐵)‘𝑚) = ∏𝑚𝐶 ((𝑛𝐶𝐷)‘𝑚))
74 prodfc 14669 . . . . . 6 𝑚𝐴 ((𝑘𝐴𝐵)‘𝑚) = ∏𝑘𝐴 𝐵
75 prodfc 14669 . . . . . 6 𝑚𝐶 ((𝑛𝐶𝐷)‘𝑚) = ∏𝑛𝐶 𝐷
7673, 74, 753eqtr3g 2678 . . . . 5 ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto𝐶)) → ∏𝑘𝐴 𝐵 = ∏𝑛𝐶 𝐷)
7776expr 643 . . . 4 ((𝜑 ∧ (#‘𝐶) ∈ ℕ) → (𝑓:(1...(#‘𝐶))–1-1-onto𝐶 → ∏𝑘𝐴 𝐵 = ∏𝑛𝐶 𝐷))
7877exlimdv 1860 . . 3 ((𝜑 ∧ (#‘𝐶) ∈ ℕ) → (∃𝑓 𝑓:(1...(#‘𝐶))–1-1-onto𝐶 → ∏𝑘𝐴 𝐵 = ∏𝑛𝐶 𝐷))
7978expimpd 629 . 2 (𝜑 → (((#‘𝐶) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝐶))–1-1-onto𝐶) → ∏𝑘𝐴 𝐵 = ∏𝑛𝐶 𝐷))
80 fprodf1o.2 . . 3 (𝜑𝐶 ∈ Fin)
81 fz1f1o 14435 . . 3 (𝐶 ∈ Fin → (𝐶 = ∅ ∨ ((#‘𝐶) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝐶))–1-1-onto𝐶)))
8280, 81syl 17 . 2 (𝜑 → (𝐶 = ∅ ∨ ((#‘𝐶) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝐶))–1-1-onto𝐶)))
8318, 79, 82mpjaod 396 1 (𝜑 → ∏𝑘𝐴 𝐵 = ∏𝑛𝐶 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383  wa 384   = wceq 1482  wex 1703  wcel 1989  wral 2911  c0 3913  cmpt 4727   I cid 5021  ccom 5116  wf 5882  ontowfo 5884  1-1-ontowf1o 5885  cfv 5886  (class class class)co 6647  Fincfn 7952  cc 9931  1c1 9934   · cmul 9938  cn 11017  ...cfz 12323  seqcseq 12796  #chash 13112  cprod 14629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-rep 4769  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946  ax-inf2 8535  ax-cnex 9989  ax-resscn 9990  ax-1cn 9991  ax-icn 9992  ax-addcl 9993  ax-addrcl 9994  ax-mulcl 9995  ax-mulrcl 9996  ax-mulcom 9997  ax-addass 9998  ax-mulass 9999  ax-distr 10000  ax-i2m1 10001  ax-1ne0 10002  ax-1rid 10003  ax-rnegex 10004  ax-rrecex 10005  ax-cnre 10006  ax-pre-lttri 10007  ax-pre-lttrn 10008  ax-pre-ltadd 10009  ax-pre-mulgt0 10010  ax-pre-sup 10011
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-fal 1488  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-nel 2897  df-ral 2916  df-rex 2917  df-reu 2918  df-rmo 2919  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-int 4474  df-iun 4520  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-se 5072  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-isom 5895  df-riota 6608  df-ov 6650  df-oprab 6651  df-mpt2 6652  df-om 7063  df-1st 7165  df-2nd 7166  df-wrecs 7404  df-recs 7465  df-rdg 7503  df-1o 7557  df-oadd 7561  df-er 7739  df-en 7953  df-dom 7954  df-sdom 7955  df-fin 7956  df-sup 8345  df-oi 8412  df-card 8762  df-pnf 10073  df-mnf 10074  df-xr 10075  df-ltxr 10076  df-le 10077  df-sub 10265  df-neg 10266  df-div 10682  df-nn 11018  df-2 11076  df-3 11077  df-n0 11290  df-z 11375  df-uz 11685  df-rp 11830  df-fz 12324  df-fzo 12462  df-seq 12797  df-exp 12856  df-hash 13113  df-cj 13833  df-re 13834  df-im 13835  df-sqrt 13969  df-abs 13970  df-clim 14213  df-prod 14630
This theorem is referenced by:  fprodss  14672  fprodshft  14700  fprodrev  14701  fprod2dlem  14704  fprodcnv  14707  gausslemma2dlem1  25085  hgt750lemg  30717
  Copyright terms: Public domain W3C validator