Theorem prodeq2 11700

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

Assertion

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

Distinct variable group:   𝐴,𝑘

Allowed substitution hints:   𝐵(𝑘)   𝐶(𝑘)

Proof of Theorem prodeq2

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

Step	Hyp	Ref	Expression
1		nfra1 2525	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘∀𝑘 ∈ 𝐴 𝐵 = 𝐶
2		nfv 1539	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘 𝑚 ∈ ℤ
3	1, 2	nfan 1576	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘(∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ)
4		nfv 1539	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘(𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)
5	3, 4	nfan 1576	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴))
6		nfv 1539	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘 𝑛 ∈ (ℤ≥‘𝑚)
7	5, 6	nfan 1576	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘(((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)) ∧ 𝑛 ∈ (ℤ≥‘𝑚))
8		simp-4l 541	. . . . . . . . . . . . . . . 16 ⊢ (((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶)
9		simpr 110	. . . . . . . . . . . . . . . 16 ⊢ (((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ 𝐴)
10		rsp 2541	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑘 ∈ 𝐴 𝐵 = 𝐶 → (𝑘 ∈ 𝐴 → 𝐵 = 𝐶))
11	8, 9, 10	sylc 62	. . . . . . . . . . . . . . 15 ⊢ (((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶)
12	11	adantllr 481	. . . . . . . . . . . . . 14 ⊢ ((((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)) ∧ 𝑛 ∈ (ℤ≥‘𝑚)) ∧ 𝑘 ∈ ℤ) ∧ 𝑘 ∈ 𝐴) → 𝐵 = 𝐶)
13		simpllr 534	. . . . . . . . . . . . . . . 16 ⊢ ((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)) ∧ 𝑘 ∈ ℤ) → 𝑚 ∈ ℤ)
14		simplrl 535	. . . . . . . . . . . . . . . 16 ⊢ ((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)) ∧ 𝑘 ∈ ℤ) → 𝐴 ⊆ (ℤ≥‘𝑚))
15		simplrr 536	. . . . . . . . . . . . . . . 16 ⊢ ((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)) ∧ 𝑘 ∈ ℤ) → ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)
16		simpr 110	. . . . . . . . . . . . . . . 16 ⊢ ((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)) ∧ 𝑘 ∈ ℤ) → 𝑘 ∈ ℤ)
17	13, 14, 15, 16	sumdc 11501	. . . . . . . . . . . . . . 15 ⊢ ((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)) ∧ 𝑘 ∈ ℤ) → DECID 𝑘 ∈ 𝐴)
18	17	adantlr 477	. . . . . . . . . . . . . 14 ⊢ (((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)) ∧ 𝑛 ∈ (ℤ≥‘𝑚)) ∧ 𝑘 ∈ ℤ) → DECID 𝑘 ∈ 𝐴)
19	12, 18	ifeq1dadc 3587	. . . . . . . . . . . . 13 ⊢ (((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)) ∧ 𝑛 ∈ (ℤ≥‘𝑚)) ∧ 𝑘 ∈ ℤ) → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑘 ∈ 𝐴, 𝐶, 1))
20	7, 19	mpteq2da 4118	. . . . . . . . . . . 12 ⊢ ((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)) ∧ 𝑛 ∈ (ℤ≥‘𝑚)) → (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1)))
21	20	seqeq3d 10526	. . . . . . . . . . 11 ⊢ ((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)) ∧ 𝑛 ∈ (ℤ≥‘𝑚)) → seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) = seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))))
22	21	breq1d 4039	. . . . . . . . . 10 ⊢ ((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)) ∧ 𝑛 ∈ (ℤ≥‘𝑚)) → (seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦 ↔ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦))
23	22	anbi2d 464	. . . . . . . . 9 ⊢ ((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)) ∧ 𝑛 ∈ (ℤ≥‘𝑚)) → ((𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ (𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦)))
24	23	exbidv 1836	. . . . . . . 8 ⊢ ((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)) ∧ 𝑛 ∈ (ℤ≥‘𝑚)) → (∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦)))
25	24	rexbidva 2491	. . . . . . 7 ⊢ (((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)) → (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦)))
26	11, 17	ifeq1dadc 3587	. . . . . . . . . 10 ⊢ ((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)) ∧ 𝑘 ∈ ℤ) → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑘 ∈ 𝐴, 𝐶, 1))
27	5, 26	mpteq2da 4118	. . . . . . . . 9 ⊢ (((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)) → (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1)))
28	27	seqeq3d 10526	. . . . . . . 8 ⊢ (((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)) → seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) = seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))))
29	28	breq1d 4039	. . . . . . 7 ⊢ (((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)) → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥))
30	25, 29	anbi12d 473	. . . . . 6 ⊢ (((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴)) → ((∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ↔ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥)))
31	30	pm5.32da 452	. . . . 5 ⊢ ((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℤ) → (((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ↔ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥))))
32	31	rexbidva 2491	. . . 4 ⊢ (∀𝑘 ∈ 𝐴 𝐵 = 𝐶 → (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ↔ ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥))))
33		f1of 5500	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(1...𝑚)–1-1-onto→𝐴 → 𝑓:(1...𝑚)⟶𝐴)
34	33	ad3antlr 493	. . . . . . . . . . . . . 14 ⊢ (((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ≤ 𝑚) → 𝑓:(1...𝑚)⟶𝐴)
35		simplr 528	. . . . . . . . . . . . . . 15 ⊢ (((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ≤ 𝑚) → 𝑛 ∈ ℕ)
36		simpr 110	. . . . . . . . . . . . . . 15 ⊢ (((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ≤ 𝑚) → 𝑛 ≤ 𝑚)
37		simp-4r 542	. . . . . . . . . . . . . . . . 17 ⊢ (((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ≤ 𝑚) → 𝑚 ∈ ℕ)
38	37	nnzd 9438	. . . . . . . . . . . . . . . 16 ⊢ (((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ≤ 𝑚) → 𝑚 ∈ ℤ)
39		fznn 10155	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ℤ → (𝑛 ∈ (1...𝑚) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑚)))
40	38, 39	syl 14	. . . . . . . . . . . . . . 15 ⊢ (((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ≤ 𝑚) → (𝑛 ∈ (1...𝑚) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑚)))
41	35, 36, 40	mpbir2and 946	. . . . . . . . . . . . . 14 ⊢ (((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ≤ 𝑚) → 𝑛 ∈ (1...𝑚))
42	34, 41	ffvelcdmd 5694	. . . . . . . . . . . . 13 ⊢ (((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ≤ 𝑚) → (𝑓‘𝑛) ∈ 𝐴)
43		simp-4l 541	. . . . . . . . . . . . 13 ⊢ (((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ≤ 𝑚) → ∀𝑘 ∈ 𝐴 𝐵 = 𝐶)
44		nfcsb1v 3113	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘⦋(𝑓‘𝑛) / 𝑘⦌𝐵
45		nfcsb1v 3113	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘⦋(𝑓‘𝑛) / 𝑘⦌𝐶
46	44, 45	nfeq 2344	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑛) / 𝑘⦌𝐶
47		csbeq1a 3089	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝑓‘𝑛) → 𝐵 = ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)
48		csbeq1a 3089	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝑓‘𝑛) → 𝐶 = ⦋(𝑓‘𝑛) / 𝑘⦌𝐶)
49	47, 48	eqeq12d 2208	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑓‘𝑛) → (𝐵 = 𝐶 ↔ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))
50	46, 49	rspc 2858	. . . . . . . . . . . . 13 ⊢ ((𝑓‘𝑛) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 = 𝐶 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))
51	42, 43, 50	sylc 62	. . . . . . . . . . . 12 ⊢ (((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ≤ 𝑚) → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑛) / 𝑘⦌𝐶)
52		simpr 110	. . . . . . . . . . . . . 14 ⊢ ((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
53	52	nnzd 9438	. . . . . . . . . . . . 13 ⊢ ((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℤ)
54		simpllr 534	. . . . . . . . . . . . . 14 ⊢ ((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) ∧ 𝑛 ∈ ℕ) → 𝑚 ∈ ℕ)
55	54	nnzd 9438	. . . . . . . . . . . . 13 ⊢ ((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) ∧ 𝑛 ∈ ℕ) → 𝑚 ∈ ℤ)
56		zdcle 9393	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ) → DECID 𝑛 ≤ 𝑚)
57	53, 55, 56	syl2anc 411	. . . . . . . . . . . 12 ⊢ ((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) ∧ 𝑛 ∈ ℕ) → DECID 𝑛 ≤ 𝑚)
58	51, 57	ifeq1dadc 3587	. . . . . . . . . . 11 ⊢ ((((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) ∧ 𝑛 ∈ ℕ) → if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1) = if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐶, 1))
59	58	mpteq2dva 4119	. . . . . . . . . 10 ⊢ (((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐶, 1)))
60	59	seqeq3d 10526	. . . . . . . . 9 ⊢ (((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1))) = seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐶, 1))))
61	60	fveq1d 5556	. . . . . . . 8 ⊢ (((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐶, 1)))‘𝑚))
62	61	eqeq2d 2205	. . . . . . 7 ⊢ (((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚) ↔ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐶, 1)))‘𝑚)))
63	62	pm5.32da 452	. . . . . 6 ⊢ ((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℕ) → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐶, 1)))‘𝑚))))
64	63	exbidv 1836	. . . . 5 ⊢ ((∀𝑘 ∈ 𝐴 𝐵 = 𝐶 ∧ 𝑚 ∈ ℕ) → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐶, 1)))‘𝑚))))
65	64	rexbidva 2491	. . . 4 ⊢ (∀𝑘 ∈ 𝐴 𝐵 = 𝐶 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐶, 1)))‘𝑚))))
66	32, 65	orbi12d 794	. . 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)))‘𝑚)))))
67	66	iotabidv 5237	. 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)))‘𝑚)))))
68		df-proddc 11694	. 2 ⊢ ∏𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))))
69		df-proddc 11694	. 2 ⊢ ∏𝑘 ∈ 𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐶, 1)))‘𝑚))))
70	67, 68, 69	3eqtr4g 2251	1 ⊢ (∀𝑘 ∈ 𝐴 𝐵 = 𝐶 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 709  DECID wdc 835   = wceq 1364  ∃wex 1503   ∈ wcel 2164  ∀wral 2472  ∃wrex 2473  ⦋csb 3080   ⊆ wss 3153  ifcif 3557   class class class wbr 4029   ↦ cmpt 4090  ℩cio 5213  ⟶wf 5250  –1-1-onto→wf1o 5253  ‘cfv 5254  (class class class)co 5918  0cc0 7872  1c1 7873   · cmul 7877   ≤ cle 8055   # cap 8600  ℕcn 8982  ℤcz 9317  ℤ_≥cuz 9592  ...cfz 10074  seqcseq 10518   ⇝ cli 11421  ∏cprod 11693

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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-setind 4569  ax-cnex 7963  ax-resscn 7964  ax-1cn 7965  ax-1re 7966  ax-icn 7967  ax-addcl 7968  ax-addrcl 7969  ax-mulcl 7970  ax-addcom 7972  ax-addass 7974  ax-distr 7976  ax-i2m1 7977  ax-0lt1 7978  ax-0id 7980  ax-rnegex 7981  ax-cnre 7983  ax-pre-ltirr 7984  ax-pre-ltwlin 7985  ax-pre-lttrn 7986  ax-pre-ltadd 7988

This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rab 2481  df-v 2762  df-sbc 2986  df-csb 3081  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-if 3558  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-int 3871  df-br 4030  df-opab 4091  df-mpt 4092  df-id 4324  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-rn 4670  df-res 4671  df-ima 4672  df-iota 5215  df-fun 5256  df-fn 5257  df-f 5258  df-f1 5259  df-f1o 5261  df-fv 5262  df-riota 5873  df-ov 5921  df-oprab 5922  df-mpo 5923  df-recs 6358  df-frec 6444  df-pnf 8056  df-mnf 8057  df-xr 8058  df-ltxr 8059  df-le 8060  df-sub 8192  df-neg 8193  df-inn 8983  df-n0 9241  df-z 9318  df-uz 9593  df-fz 10075  df-seqfrec 10519  df-proddc 11694

This theorem is referenced by:  prodeq2i  11705  prodeq2d  11708  gausslemma2dlem5a  15181