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

Theorem cbvprodvw2 36226
Description: Change bound variable and the set of integers in a product, using implicit substitution. (Contributed by GG, 1-Sep-2025.)
Hypotheses
Ref Expression
cbvprodvw2.1 𝐴 = 𝐵
cbvprodvw2.2 (𝑗 = 𝑘𝐶 = 𝐷)
Assertion
Ref Expression
cbvprodvw2 𝑗𝐴 𝐶 = ∏𝑘𝐵 𝐷
Distinct variable groups:   𝑗,𝑘   𝐷,𝑗   𝐶,𝑘   𝐴,𝑘   𝐵,𝑗
Allowed substitution hints:   𝐴(𝑗)   𝐵(𝑘)   𝐶(𝑗)   𝐷(𝑘)

Proof of Theorem cbvprodvw2
Dummy variables 𝑥 𝑦 𝑚 𝑛 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cbvprodvw2.1 . . . . . . 7 𝐴 = 𝐵
21sseq1i 4011 . . . . . 6 (𝐴 ⊆ (ℤ𝑚) ↔ 𝐵 ⊆ (ℤ𝑚))
31eleq2i 2832 . . . . . . . . . . . . . 14 (𝑗𝐴𝑗𝐵)
4 eleq1w 2823 . . . . . . . . . . . . . 14 (𝑗 = 𝑘 → (𝑗𝐵𝑘𝐵))
53, 4bitrid 283 . . . . . . . . . . . . 13 (𝑗 = 𝑘 → (𝑗𝐴𝑘𝐵))
6 cbvprodvw2.2 . . . . . . . . . . . . 13 (𝑗 = 𝑘𝐶 = 𝐷)
75, 6ifbieq1d 4548 . . . . . . . . . . . 12 (𝑗 = 𝑘 → if(𝑗𝐴, 𝐶, 1) = if(𝑘𝐵, 𝐷, 1))
87cbvmptv 5253 . . . . . . . . . . 11 (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))
9 seqeq3 14043 . . . . . . . . . . 11 ((𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1)) → seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) = seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))))
108, 9ax-mp 5 . . . . . . . . . 10 seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) = seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1)))
1110breq1i 5148 . . . . . . . . 9 (seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑦 ↔ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑦)
1211anbi2i 623 . . . . . . . 8 ((𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑦) ↔ (𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑦))
1312exbii 1848 . . . . . . 7 (∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑦) ↔ ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑦))
1413rexbii 3093 . . . . . 6 (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑦) ↔ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑦))
15 seqeq3 14043 . . . . . . . 8 ((𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1)) → seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) = seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))))
168, 15ax-mp 5 . . . . . . 7 seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) = seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1)))
1716breq1i 5148 . . . . . 6 (seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑥 ↔ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑥)
182, 14, 173anbi123i 1156 . . . . 5 ((𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑥) ↔ (𝐵 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑥))
1918rexbii 3093 . . . 4 (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑥))
20 f1oeq3 6836 . . . . . . . 8 (𝐴 = 𝐵 → (𝑓:(1...𝑚)–1-1-onto𝐴𝑓:(1...𝑚)–1-1-onto𝐵))
211, 20ax-mp 5 . . . . . . 7 (𝑓:(1...𝑚)–1-1-onto𝐴𝑓:(1...𝑚)–1-1-onto𝐵)
226cbvcsbv 3910 . . . . . . . . . . 11 (𝑓𝑛) / 𝑗𝐶 = (𝑓𝑛) / 𝑘𝐷
2322mpteq2i 5245 . . . . . . . . . 10 (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐶) = (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐷)
24 seqeq3 14043 . . . . . . . . . 10 ((𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐶) = (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐷) → seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐶)) = seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐷)))
2523, 24ax-mp 5 . . . . . . . . 9 seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐶)) = seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐷))
2625fveq1i 6905 . . . . . . . 8 (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐶))‘𝑚) = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐷))‘𝑚)
2726eqeq2i 2749 . . . . . . 7 (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐶))‘𝑚) ↔ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐷))‘𝑚))
2821, 27anbi12i 628 . . . . . 6 ((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐶))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐷))‘𝑚)))
2928exbii 1848 . . . . 5 (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐶))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐷))‘𝑚)))
3029rexbii 3093 . . . 4 (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐶))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐷))‘𝑚)))
3119, 30orbi12i 915 . . 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( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐷))‘𝑚))))
3231iotabii 6544 . 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( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐷))‘𝑚))))
33 df-prod 15936 . 2 𝑗𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐶, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑗𝐶))‘𝑚))))
34 df-prod 15936 . 2 𝑘𝐵 𝐷 = (℩𝑥(∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ𝑚) ∧ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐷, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐷))‘𝑚))))
3532, 33, 343eqtr4i 2774 1 𝑗𝐴 𝐶 = ∏𝑘𝐵 𝐷
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  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