Theorem prodeq1 16000

Description: Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.)

Assertion

Ref	Expression
prodeq1	⊢ (𝐴 = 𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶)

Distinct variable groups:   𝐴,𝑘   𝐵,𝑘

Allowed substitution hint:   𝐶(𝑘)

Proof of Theorem prodeq1

Dummy variables 𝑥 𝑦 𝑚 𝑛 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sseq1 3959	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ (ℤ≥‘𝑚) ↔ 𝐵 ⊆ (ℤ≥‘𝑚)))
2		eleq2 2851	. . . . . . . . . . . . 13 ⊢ (𝐴 = 𝐵 → (𝑘 ∈ 𝐴 ↔ 𝑘 ∈ 𝐵))
3	2	ifbid 4509	. . . . . . . . . . . 12 ⊢ (𝐴 = 𝐵 → if(𝑘 ∈ 𝐴, 𝐶, 1) = if(𝑘 ∈ 𝐵, 𝐶, 1))
4	3	mpteq2dv 5203	. . . . . . . . . . 11 ⊢ (𝐴 = 𝐵 → (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐶, 1)))
5	4	seqeq3d 14077	. . . . . . . . . 10 ⊢ (𝐴 = 𝐵 → seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) = seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))))
6	5	breq1d 5117	. . . . . . . . 9 ⊢ (𝐴 = 𝐵 → (seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦 ↔ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))) ⇝ 𝑦))
7	6	anbi2d 642	. . . . . . . 8 ⊢ (𝐴 = 𝐵 → ((𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ↔ (𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))) ⇝ 𝑦)))
8	7	exbidv 1954	. . . . . . 7 ⊢ (𝐴 = 𝐵 → (∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ↔ ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))) ⇝ 𝑦)))
9	8	rexbidv 3188	. . . . . 6 ⊢ (𝐴 = 𝐵 → (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ↔ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))) ⇝ 𝑦)))
10	4	seqeq3d 14077	. . . . . . 7 ⊢ (𝐴 = 𝐵 → seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) = seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))))
11	10	breq1d 5117	. . . . . 6 ⊢ (𝐴 = 𝐵 → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥 ↔ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))) ⇝ 𝑥))
12	1, 9, 11	3anbi123d 1464	. . . . 5 ⊢ (𝐴 = 𝐵 → ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥) ↔ (𝐵 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))) ⇝ 𝑥)))
13	12	rexbidv 3188	. . . 4 ⊢ (𝐴 = 𝐵 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))) ⇝ 𝑥)))
14		f1oeq3 6811	. . . . . . 7 ⊢ (𝐴 = 𝐵 → (𝑓:(1...𝑚)–1-1-onto→𝐴 ↔ 𝑓:(1...𝑚)–1-1-onto→𝐵))
15	14	anbi1d 643	. . . . . 6 ⊢ (𝐴 = 𝐵 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐵 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
16	15	exbidv 1954	. . . . 5 ⊢ (𝐴 = 𝐵 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐵 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
17	16	rexbidv 3188	. . . 4 ⊢ (𝐴 = 𝐵 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐵 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
18	13, 17	orbi12d 932	. . 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( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)))))
19	18	iotabidv 6521	. 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( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)))))
20		df-prod 15997	. 2 ⊢ ∏𝑘 ∈ 𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
21		df-prod 15997	. 2 ⊢ ∏𝑘 ∈ 𝐵 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐵 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐵, 𝐶, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐵 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
22	19, 20, 21	3eqtr4g 2822	1 ⊢ (𝐴 = 𝐵 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2145   ≠ wne 2957  ∃wrex 3088  ⦋csb 3850   ⊆ wss 3902  ifcif 4485   class class class wbr 5107   ↦ cmpt 5190  ℩cio 6491  –1-1-onto→wf1o 6536  ‘cfv 6537  (class class class)co 7417  0cc0 11128  1c1 11129   · cmul 11133  ℕcn 12261  ℤcz 12619  ℤ_≥cuz 12891  ...cfz 13565  seqcseq 14069   ⇝ cli 15575  ∏cprod 15996

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-xp 5665  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-iota 6493  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7420  df-oprab 7421  df-mpo 7422  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-seq 14070  df-prod 15997

This theorem is used by:  prodeq1iOLD  16010  prodeq1d  16013  prod1  16037  fprodf1o  16039  fprodss  16041  fprodcllem  16044  fprodmul  16053  fproddiv  16054  fprodconst  16071  fprodn0  16072  fprod2d  16074  fprodmodd  16090  coprmprod  16757  coprmproddvds  16759  fprodexp  46432  fprodabs2  46433  mccl  46436  fprodcn  46438  fprodcncf  46736  dvmptfprod  46781  dvnprodlem3  46784  hoidmvval  47413  ovnhoi  47439  hspmbllem2  47463  fmtnorec2  48454