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

Theorem prodeq1f 11502
Description: Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.)
Hypotheses
Ref Expression
prodeq1f.1 𝑘𝐴
prodeq1f.2 𝑘𝐵
Assertion
Ref Expression
prodeq1f (𝐴 = 𝐵 → ∏𝑘𝐴 𝐶 = ∏𝑘𝐵 𝐶)

Proof of Theorem prodeq1f
Dummy variables 𝑓 𝑗 𝑚 𝑛 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sseq1 3170 . . . . . . 7 (𝐴 = 𝐵 → (𝐴 ⊆ (ℤ𝑚) ↔ 𝐵 ⊆ (ℤ𝑚)))
2 eleq2 2234 . . . . . . . . 9 (𝐴 = 𝐵 → (𝑗𝐴𝑗𝐵))
32dcbid 833 . . . . . . . 8 (𝐴 = 𝐵 → (DECID 𝑗𝐴DECID 𝑗𝐵))
43ralbidv 2470 . . . . . . 7 (𝐴 = 𝐵 → (∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ↔ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐵))
51, 4anbi12d 470 . . . . . 6 (𝐴 = 𝐵 → ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ↔ (𝐵 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐵)))
6 prodeq1f.1 . . . . . . . . . . . . . 14 𝑘𝐴
7 prodeq1f.2 . . . . . . . . . . . . . 14 𝑘𝐵
86, 7nfeq 2320 . . . . . . . . . . . . 13 𝑘 𝐴 = 𝐵
9 eleq2 2234 . . . . . . . . . . . . . . 15 (𝐴 = 𝐵 → (𝑘𝐴𝑘𝐵))
109ifbid 3546 . . . . . . . . . . . . . 14 (𝐴 = 𝐵 → if(𝑘𝐴, 𝐶, 1) = if(𝑘𝐵, 𝐶, 1))
1110adantr 274 . . . . . . . . . . . . 13 ((𝐴 = 𝐵𝑘 ∈ ℤ) → if(𝑘𝐴, 𝐶, 1) = if(𝑘𝐵, 𝐶, 1))
128, 11mpteq2da 4076 . . . . . . . . . . . 12 (𝐴 = 𝐵 → (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1)))
1312seqeq3d 10396 . . . . . . . . . . 11 (𝐴 = 𝐵 → seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) = seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))))
1413breq1d 3997 . . . . . . . . . 10 (𝐴 = 𝐵 → (seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦 ↔ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑦))
1514anbi2d 461 . . . . . . . . 9 (𝐴 = 𝐵 → ((𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦) ↔ (𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑦)))
1615exbidv 1818 . . . . . . . 8 (𝐴 = 𝐵 → (∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦) ↔ ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑦)))
1716rexbidv 2471 . . . . . . 7 (𝐴 = 𝐵 → (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦) ↔ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑦)))
1812seqeq3d 10396 . . . . . . . 8 (𝐴 = 𝐵 → seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) = seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))))
1918breq1d 3997 . . . . . . 7 (𝐴 = 𝐵 → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑥 ↔ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑥))
2017, 19anbi12d 470 . . . . . 6 (𝐴 = 𝐵 → ((∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑥) ↔ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑥)))
215, 20anbi12d 470 . . . . 5 (𝐴 = 𝐵 → (((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑥)) ↔ ((𝐵 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐵) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑥))))
2221rexbidv 2471 . . . 4 (𝐴 = 𝐵 → (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑥)) ↔ ∃𝑚 ∈ ℤ ((𝐵 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐵) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑥))))
23 f1oeq3 5431 . . . . . . 7 (𝐴 = 𝐵 → (𝑓:(1...𝑚)–1-1-onto𝐴𝑓:(1...𝑚)–1-1-onto𝐵))
2423anbi1d 462 . . . . . 6 (𝐴 = 𝐵 → ((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))‘𝑚))))
2524exbidv 1818 . . . . 5 (𝐴 = 𝐵 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))‘𝑚))))
2625rexbidv 2471 . . . 4 (𝐴 = 𝐵 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))‘𝑚))))
2722, 26orbi12d 788 . . 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)))‘𝑚)))))
2827iotabidv 5179 . 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)))‘𝑚)))))
29 df-proddc 11501 . 2 𝑘𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))‘𝑚))))
30 df-proddc 11501 . 2 𝑘𝐵 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐵 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐵) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))‘𝑚))))
3128, 29, 303eqtr4g 2228 1 (𝐴 = 𝐵 → ∏𝑘𝐴 𝐶 = ∏𝑘𝐵 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wo 703  DECID wdc 829   = wceq 1348  wex 1485  wcel 2141  wnfc 2299  wral 2448  wrex 2449  csb 3049  wss 3121  ifcif 3525   class class class wbr 3987  cmpt 4048  cio 5156  1-1-ontowf1o 5195  cfv 5196  (class class class)co 5850  0cc0 7761  1c1 7762   · cmul 7766  cle 7942   # cap 8487  cn 8865  cz 9199  cuz 9474  ...cfz 9952  seqcseq 10388  cli 11228  cprod 11500
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-dc 830  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-if 3526  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-br 3988  df-opab 4049  df-mpt 4050  df-cnv 4617  df-dm 4619  df-rn 4620  df-res 4621  df-iota 5158  df-f 5200  df-f1 5201  df-fo 5202  df-f1o 5203  df-fv 5204  df-ov 5853  df-oprab 5854  df-mpo 5855  df-recs 6281  df-frec 6367  df-seqfrec 10389  df-proddc 11501
This theorem is referenced by:  prodeq1  11503
  Copyright terms: Public domain W3C validator