Users' Mathboxes Mathbox for Gino Giotto < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cbvproddavw2 Structured version   Visualization version   GIF version

Theorem cbvproddavw2 36275
Description: Change bound variable and the set of integers in a product. Deduction form. (Contributed by GG, 14-Aug-2025.)
Hypotheses
Ref Expression
cbvproddavw2.1 (𝜑𝐴 = 𝐵)
cbvproddavw2.2 ((𝜑𝑗 = 𝑘) → 𝐶 = 𝐷)
Assertion
Ref Expression
cbvproddavw2 (𝜑 → ∏𝑗𝐴 𝐶 = ∏𝑘𝐵 𝐷)
Distinct variable groups:   𝜑,𝑗,𝑘   𝐴,𝑘   𝐵,𝑗   𝐶,𝑘   𝐷,𝑗
Allowed substitution hints:   𝐴(𝑗)   𝐵(𝑘)   𝐶(𝑗)   𝐷(𝑘)

Proof of Theorem cbvproddavw2
Dummy variables 𝑥 𝑦 𝑚 𝑛 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cbvproddavw2.1 . . . . . . 7 (𝜑𝐴 = 𝐵)
21sseq1d 4014 . . . . . 6 (𝜑 → (𝐴 ⊆ (ℤ𝑚) ↔ 𝐵 ⊆ (ℤ𝑚)))
3 simpr 484 . . . . . . . . . . . . . 14 ((𝜑𝑗 = 𝑘) → 𝑗 = 𝑘)
41adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑗 = 𝑘) → 𝐴 = 𝐵)
53, 4eleq12d 2834 . . . . . . . . . . . . 13 ((𝜑𝑗 = 𝑘) → (𝑗𝐴𝑘𝐵))
6 cbvproddavw2.2 . . . . . . . . . . . . 13 ((𝜑𝑗 = 𝑘) → 𝐶 = 𝐷)
75, 6ifbieq1d 4548 . . . . . . . . . . . 12 ((𝜑𝑗 = 𝑘) → if(𝑗𝐴, 𝐶, 1) = if(𝑘𝐵, 𝐷, 1))
87cbvmptdavw 36246 . . . . . . . . . . 11 (𝜑 → (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1)))
98seqeq3d 14046 . . . . . . . . . 10 (𝜑 → seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) = seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))))
109breq1d 5151 . . . . . . . . 9 (𝜑 → (seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑦 ↔ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑦))
1110anbi2d 630 . . . . . . . 8 (𝜑 → ((𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑦) ↔ (𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑦)))
1211exbidv 1921 . . . . . . 7 (𝜑 → (∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑦) ↔ ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑦)))
1312rexbidv 3178 . . . . . 6 (𝜑 → (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑦) ↔ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑦)))
148seqeq3d 14046 . . . . . . 7 (𝜑 → seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) = seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))))
1514breq1d 5151 . . . . . 6 (𝜑 → (seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑥 ↔ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑥))
162, 13, 153anbi123d 1438 . . . . 5 (𝜑 → ((𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑥) ↔ (𝐵 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑥)))
1716rexbidv 3178 . . . 4 (𝜑 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑥)))
181f1oeq3d 6843 . . . . . . 7 (𝜑 → (𝑓:(1...𝑚)–1-1-onto𝐴𝑓:(1...𝑚)–1-1-onto𝐵))
196cbvcsbdavw 36238 . . . . . . . . . . 11 (𝜑(𝑓𝑛) / 𝑗𝐶 = (𝑓𝑛) / 𝑘𝐷)
2019mpteq2dv 5242 . . . . . . . . . 10 (𝜑 → (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐶) = (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐷))
2120seqeq3d 14046 . . . . . . . . 9 (𝜑 → seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐶)) = seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐷)))
2221fveq1d 6906 . . . . . . . 8 (𝜑 → (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐶))‘𝑚) = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐷))‘𝑚))
2322eqeq2d 2747 . . . . . . 7 (𝜑 → (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐶))‘𝑚) ↔ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐷))‘𝑚)))
2418, 23anbi12d 632 . . . . . 6 (𝜑 → ((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐶))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐷))‘𝑚))))
2524exbidv 1921 . . . . 5 (𝜑 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐶))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐷))‘𝑚))))
2625rexbidv 3178 . . . 4 (𝜑 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐶))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐷))‘𝑚))))
2717, 26orbi12d 919 . . 3 (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐶))‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐷))‘𝑚)))))
2827iotabidv 6543 . 2 (𝜑 → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐶))‘𝑚)))) = (℩𝑥(∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐷))‘𝑚)))))
29 df-prod 15936 . 2 𝑗𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐶))‘𝑚))))
30 df-prod 15936 . 2 𝑘𝐵 𝐷 = (℩𝑥(∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐷))‘𝑚))))
3128, 29, 303eqtr4g 2801 1 (𝜑 → ∏𝑗𝐴 𝐶 = ∏𝑘𝐵 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wo 848  w3a 1087   = wceq 1540  wex 1779  wcel 2108  wne 2939  wrex 3069  csb 3898  wss 3950  ifcif 4524   class class class wbr 5141  cmpt 5223  cio 6510  1-1-ontowf1o 6558  cfv 6559  (class class class)co 7429  0cc0 11151  1c1 11152   · cmul 11156  cn 12262  cz 12609  cuz 12874  ...cfz 13543  seqcseq 14038  cli 15516  cprod 15935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4906  df-br 5142  df-opab 5204  df-mpt 5224  df-xp 5689  df-cnv 5691  df-co 5692  df-dm 5693  df-rn 5694  df-res 5695  df-ima 5696  df-pred 6319  df-iota 6512  df-f 6563  df-f1 6564  df-fo 6565  df-f1o 6566  df-fv 6567  df-ov 7432  df-oprab 7433  df-mpo 7434  df-frecs 8302  df-wrecs 8333  df-recs 8407  df-rdg 8446  df-seq 14039  df-prod 15936
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator