ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  cbvprod GIF version

Theorem cbvprod 11550
Description: Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.)
Hypotheses
Ref Expression
cbvprod.1 (𝑗 = 𝑘𝐵 = 𝐶)
cbvprod.2 𝑘𝐴
cbvprod.3 𝑗𝐴
cbvprod.4 𝑘𝐵
cbvprod.5 𝑗𝐶
Assertion
Ref Expression
cbvprod 𝑗𝐴 𝐵 = ∏𝑘𝐴 𝐶
Distinct variable group:   𝑗,𝑘
Allowed substitution hints:   𝐴(𝑗,𝑘)   𝐵(𝑗,𝑘)   𝐶(𝑗,𝑘)

Proof of Theorem cbvprod
Dummy variables 𝑓 𝑚 𝑛 𝑠 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cbvprod.2 . . . . . . . . . . . . . . 15 𝑘𝐴
21nfcri 2313 . . . . . . . . . . . . . 14 𝑘 𝑗𝐴
3 cbvprod.4 . . . . . . . . . . . . . 14 𝑘𝐵
4 nfcv 2319 . . . . . . . . . . . . . 14 𝑘1
52, 3, 4nfif 3562 . . . . . . . . . . . . 13 𝑘if(𝑗𝐴, 𝐵, 1)
6 cbvprod.3 . . . . . . . . . . . . . . 15 𝑗𝐴
76nfcri 2313 . . . . . . . . . . . . . 14 𝑗 𝑘𝐴
8 cbvprod.5 . . . . . . . . . . . . . 14 𝑗𝐶
9 nfcv 2319 . . . . . . . . . . . . . 14 𝑗1
107, 8, 9nfif 3562 . . . . . . . . . . . . 13 𝑗if(𝑘𝐴, 𝐶, 1)
11 eleq1w 2238 . . . . . . . . . . . . . 14 (𝑗 = 𝑘 → (𝑗𝐴𝑘𝐴))
12 cbvprod.1 . . . . . . . . . . . . . 14 (𝑗 = 𝑘𝐵 = 𝐶)
1311, 12ifbieq1d 3556 . . . . . . . . . . . . 13 (𝑗 = 𝑘 → if(𝑗𝐴, 𝐵, 1) = if(𝑘𝐴, 𝐶, 1))
145, 10, 13cbvmpt 4095 . . . . . . . . . . . 12 (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐵, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))
15 seqeq3 10436 . . . . . . . . . . . 12 ((𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐵, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1)) → seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐵, 1))) = seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))))
1614, 15ax-mp 5 . . . . . . . . . . 11 seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐵, 1))) = seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1)))
1716breq1i 4007 . . . . . . . . . 10 (seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐵, 1))) ⇝ 𝑦 ↔ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦)
1817anbi2i 457 . . . . . . . . 9 ((𝑦 # 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ (𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦))
1918exbii 1605 . . . . . . . 8 (∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦))
2019rexbii 2484 . . . . . . 7 (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦))
21 seqeq3 10436 . . . . . . . . 9 ((𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐵, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1)) → seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐵, 1))) = seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))))
2214, 21ax-mp 5 . . . . . . . 8 seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐵, 1))) = seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1)))
2322breq1i 4007 . . . . . . 7 (seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑥)
2420, 23anbi12i 460 . . . . . 6 ((∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐵, 1))) ⇝ 𝑥) ↔ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑥))
2524anbi2i 457 . . . . 5 (((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑠 ∈ (ℤ𝑚)DECID 𝑠𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐵, 1))) ⇝ 𝑥)) ↔ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑠 ∈ (ℤ𝑚)DECID 𝑠𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑥)))
2625rexbii 2484 . . . 4 (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑠 ∈ (ℤ𝑚)DECID 𝑠𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐵, 1))) ⇝ 𝑥)) ↔ ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑠 ∈ (ℤ𝑚)DECID 𝑠𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑥)))
273, 8, 12cbvcsbw 3061 . . . . . . . . . . . 12 (𝑓𝑛) / 𝑗𝐵 = (𝑓𝑛) / 𝑘𝐶
28 ifeq1 3537 . . . . . . . . . . . 12 ((𝑓𝑛) / 𝑗𝐵 = (𝑓𝑛) / 𝑘𝐶 → if(𝑛𝑚, (𝑓𝑛) / 𝑗𝐵, 1) = if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1))
2927, 28ax-mp 5 . . . . . . . . . . 11 if(𝑛𝑚, (𝑓𝑛) / 𝑗𝐵, 1) = if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)
3029mpteq2i 4087 . . . . . . . . . 10 (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑗𝐵, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1))
31 seqeq3 10436 . . . . . . . . . 10 ((𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑗𝐵, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)) → seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑗𝐵, 1))) = seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1))))
3230, 31ax-mp 5 . . . . . . . . 9 seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑗𝐵, 1))) = seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))
3332fveq1i 5512 . . . . . . . 8 (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑗𝐵, 1)))‘𝑚) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))‘𝑚)
3433eqeq2i 2188 . . . . . . 7 (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑗𝐵, 1)))‘𝑚) ↔ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))‘𝑚))
3534anbi2i 457 . . . . . 6 ((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑗𝐵, 1)))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))‘𝑚)))
3635exbii 1605 . . . . 5 (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑗𝐵, 1)))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))‘𝑚)))
3736rexbii 2484 . . . 4 (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑗𝐵, 1)))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))‘𝑚)))
3826, 37orbi12i 764 . . 3 ((∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑠 ∈ (ℤ𝑚)DECID 𝑠𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑗𝐵, 1)))‘𝑚))) ↔ (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑠 ∈ (ℤ𝑚)DECID 𝑠𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))‘𝑚))))
3938iotabii 5196 . 2 (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑠 ∈ (ℤ𝑚)DECID 𝑠𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑗𝐵, 1)))‘𝑚)))) = (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑠 ∈ (ℤ𝑚)DECID 𝑠𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))‘𝑚))))
40 df-proddc 11543 . 2 𝑗𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑠 ∈ (ℤ𝑚)DECID 𝑠𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑗𝐵, 1)))‘𝑚))))
41 df-proddc 11543 . 2 𝑘𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑠 ∈ (ℤ𝑚)DECID 𝑠𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))‘𝑚))))
4239, 40, 413eqtr4i 2208 1 𝑗𝐴 𝐵 = ∏𝑘𝐴 𝐶
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wo 708  DECID wdc 834   = wceq 1353  wex 1492  wcel 2148  wnfc 2306  wral 2455  wrex 2456  csb 3057  wss 3129  ifcif 3534   class class class wbr 4000  cmpt 4061  cio 5172  1-1-ontowf1o 5211  cfv 5212  (class class class)co 5869  0cc0 7802  1c1 7803   · cmul 7807  cle 7983   # cap 8528  cn 8908  cz 9242  cuz 9517  ...cfz 9995  seqcseq 10431  cli 11270  cprod 11542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-un 3133  df-in 3135  df-ss 3142  df-if 3535  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-opab 4062  df-mpt 4063  df-cnv 4631  df-dm 4633  df-rn 4634  df-res 4635  df-iota 5174  df-fv 5220  df-ov 5872  df-oprab 5873  df-mpo 5874  df-recs 6300  df-frec 6386  df-seqfrec 10432  df-proddc 11543
This theorem is referenced by:  cbvprodv  11551  cbvprodi  11552
  Copyright terms: Public domain W3C validator