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

Theorem prodeq1f 11382
 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 3127 . . . . . . 7 (𝐴 = 𝐵 → (𝐴 ⊆ (ℤ𝑚) ↔ 𝐵 ⊆ (ℤ𝑚)))
2 eleq2 2205 . . . . . . . . 9 (𝐴 = 𝐵 → (𝑗𝐴𝑗𝐵))
32dcbid 824 . . . . . . . 8 (𝐴 = 𝐵 → (DECID 𝑗𝐴DECID 𝑗𝐵))
43ralbidv 2440 . . . . . . 7 (𝐴 = 𝐵 → (∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ↔ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐵))
51, 4anbi12d 465 . . . . . 6 (𝐴 = 𝐵 → ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ↔ (𝐵 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐵)))
6 prodeq1f.1 . . . . . . . . . . . . . 14 𝑘𝐴
7 prodeq1f.2 . . . . . . . . . . . . . 14 𝑘𝐵
86, 7nfeq 2291 . . . . . . . . . . . . 13 𝑘 𝐴 = 𝐵
9 eleq2 2205 . . . . . . . . . . . . . . 15 (𝐴 = 𝐵 → (𝑘𝐴𝑘𝐵))
109ifbid 3500 . . . . . . . . . . . . . 14 (𝐴 = 𝐵 → if(𝑘𝐴, 𝐶, 1) = if(𝑘𝐵, 𝐶, 1))
1110adantr 274 . . . . . . . . . . . . 13 ((𝐴 = 𝐵𝑘 ∈ ℤ) → if(𝑘𝐴, 𝐶, 1) = if(𝑘𝐵, 𝐶, 1))
128, 11mpteq2da 4027 . . . . . . . . . . . 12 (𝐴 = 𝐵 → (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1)))
1312seqeq3d 10286 . . . . . . . . . . 11 (𝐴 = 𝐵 → seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) = seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))))
1413breq1d 3949 . . . . . . . . . 10 (𝐴 = 𝐵 → (seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦 ↔ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑦))
1514anbi2d 460 . . . . . . . . 9 (𝐴 = 𝐵 → ((𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦) ↔ (𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑦)))
1615exbidv 1799 . . . . . . . 8 (𝐴 = 𝐵 → (∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦) ↔ ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑦)))
1716rexbidv 2441 . . . . . . 7 (𝐴 = 𝐵 → (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦) ↔ ∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑦)))
1812seqeq3d 10286 . . . . . . . 8 (𝐴 = 𝐵 → seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) = seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))))
1918breq1d 3949 . . . . . . 7 (𝐴 = 𝐵 → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑥 ↔ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑥))
2017, 19anbi12d 465 . . . . . 6 (𝐴 = 𝐵 → ((∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑥) ↔ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑥)))
215, 20anbi12d 465 . . . . 5 (𝐴 = 𝐵 → (((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑥)) ↔ ((𝐵 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐵) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑥))))
2221rexbidv 2441 . . . 4 (𝐴 = 𝐵 → (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑥)) ↔ ∃𝑚 ∈ ℤ ((𝐵 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐵) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑥))))
23 f1oeq3 5370 . . . . . . 7 (𝐴 = 𝐵 → (𝑓:(1...𝑚)–1-1-onto𝐴𝑓:(1...𝑚)–1-1-onto𝐵))
2423anbi1d 461 . . . . . 6 (𝐴 = 𝐵 → ((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))‘𝑚))))
2524exbidv 1799 . . . . 5 (𝐴 = 𝐵 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))‘𝑚))))
2625rexbidv 2441 . . . 4 (𝐴 = 𝐵 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))‘𝑚))))
2722, 26orbi12d 783 . . 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 5121 . 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 11381 . 2 𝑘𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐴, 𝐶, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))‘𝑚))))
30 df-proddc 11381 . 2 𝑘𝐵 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐵 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐵) ∧ (∃𝑛 ∈ (ℤ𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘𝐵, 𝐶, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐵𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 1)))‘𝑚))))
3128, 29, 303eqtr4g 2199 1 (𝐴 = 𝐵 → ∏𝑘𝐴 𝐶 = ∏𝑘𝐵 𝐶)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ∨ wo 698  DECID wdc 820   = wceq 1332  ∃wex 1469   ∈ wcel 1481  Ⅎwnfc 2270  ∀wral 2418  ∃wrex 2419  ⦋csb 3009   ⊆ wss 3078  ifcif 3481   class class class wbr 3939   ↦ cmpt 3999  ℩cio 5098  –1-1-onto→wf1o 5134  ‘cfv 5135  (class class class)co 5786  0cc0 7673  1c1 7674   · cmul 7678   ≤ cle 7854   # cap 8396  ℕcn 8773  ℤcz 9107  ℤ≥cuz 9379  ...cfz 9850  seqcseq 10278   ⇝ cli 11108  ∏cprod 11380 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 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2123 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1738  df-clab 2128  df-cleq 2134  df-clel 2137  df-nfc 2272  df-ral 2423  df-rex 2424  df-v 2693  df-un 3082  df-in 3084  df-ss 3091  df-if 3482  df-sn 3540  df-pr 3541  df-op 3543  df-uni 3747  df-br 3940  df-opab 4000  df-mpt 4001  df-cnv 4559  df-dm 4561  df-rn 4562  df-res 4563  df-iota 5100  df-f 5139  df-f1 5140  df-fo 5141  df-f1o 5142  df-fv 5143  df-ov 5789  df-oprab 5790  df-mpo 5791  df-recs 6214  df-frec 6300  df-seqfrec 10279  df-proddc 11381 This theorem is referenced by:  prodeq1  11383
 Copyright terms: Public domain W3C validator