Theorem prodeq2w 12242

Description: Equality theorem for product, when the class expressions 𝐵 and 𝐶 are equal everywhere. Proved using only Extensionality. (Contributed by Scott Fenton, 4-Dec-2017.)

Assertion

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

Distinct variable group:   𝐴,𝑘

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

Proof of Theorem prodeq2w

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

Step	Hyp	Ref	Expression
1		eqid 2232	. . . . . . . . . . . . 13 ⊢ ℤ = ℤ
2		ifeq1 3625	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = 𝐶 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑘 ∈ 𝐴, 𝐶, 1))
3	2	alimi 1504	. . . . . . . . . . . . . 14 ⊢ (∀𝑘 𝐵 = 𝐶 → ∀𝑘if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑘 ∈ 𝐴, 𝐶, 1))
4		alral 2587	. . . . . . . . . . . . . 14 ⊢ (∀𝑘if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑘 ∈ 𝐴, 𝐶, 1) → ∀𝑘 ∈ ℤ if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑘 ∈ 𝐴, 𝐶, 1))
5	3, 4	syl 14	. . . . . . . . . . . . 13 ⊢ (∀𝑘 𝐵 = 𝐶 → ∀𝑘 ∈ ℤ if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑘 ∈ 𝐴, 𝐶, 1))
6		mpteq12 4193	. . . . . . . . . . . . 13 ⊢ ((ℤ = ℤ ∧ ∀𝑘 ∈ ℤ if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑘 ∈ 𝐴, 𝐶, 1)) → (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1)))
7	1, 5, 6	sylancr 414	. . . . . . . . . . . 12 ⊢ (∀𝑘 𝐵 = 𝐶 → (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1)))
8	7	seqeq3d 10817	. . . . . . . . . . 11 ⊢ (∀𝑘 𝐵 = 𝐶 → seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) = seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))))
9	8	breq1d 4119	. . . . . . . . . 10 ⊢ (∀𝑘 𝐵 = 𝐶 → (seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦 ↔ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦))
10	9	anbi2d 464	. . . . . . . . 9 ⊢ (∀𝑘 𝐵 = 𝐶 → ((𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ (𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦)))
11	10	exbidv 1874	. . . . . . . 8 ⊢ (∀𝑘 𝐵 = 𝐶 → (∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ ∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦)))
12	11	rexbidv 2543	. . . . . . 7 ⊢ (∀𝑘 𝐵 = 𝐶 → (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦)))
13	7	seqeq3d 10817	. . . . . . . 8 ⊢ (∀𝑘 𝐵 = 𝐶 → seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) = seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))))
14	13	breq1d 4119	. . . . . . 7 ⊢ (∀𝑘 𝐵 = 𝐶 → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥))
15	12, 14	anbi12d 473	. . . . . 6 ⊢ (∀𝑘 𝐵 = 𝐶 → ((∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ↔ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥)))
16	15	anbi2d 464	. . . . 5 ⊢ (∀𝑘 𝐵 = 𝐶 → (((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ↔ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥))))
17	16	rexbidv 2543	. . . 4 ⊢ (∀𝑘 𝐵 = 𝐶 → (∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ↔ ∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥))))
18		csbeq2 3162	. . . . . . . . . . . 12 ⊢ (∀𝑘 𝐵 = 𝐶 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑛) / 𝑘⦌𝐶)
19	18	ifeq1d 3640	. . . . . . . . . . 11 ⊢ (∀𝑘 𝐵 = 𝐶 → if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1) = if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐶, 1))
20	19	mpteq2dv 4201	. . . . . . . . . 10 ⊢ (∀𝑘 𝐵 = 𝐶 → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐶, 1)))
21	20	seqeq3d 10817	. . . . . . . . 9 ⊢ (∀𝑘 𝐵 = 𝐶 → seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1))) = seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐶, 1))))
22	21	fveq1d 5672	. . . . . . . 8 ⊢ (∀𝑘 𝐵 = 𝐶 → (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐶, 1)))‘𝑚))
23	22	eqeq2d 2244	. . . . . . 7 ⊢ (∀𝑘 𝐵 = 𝐶 → (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚) ↔ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐶, 1)))‘𝑚)))
24	23	anbi2d 464	. . . . . 6 ⊢ (∀𝑘 𝐵 = 𝐶 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐶, 1)))‘𝑚))))
25	24	exbidv 1874	. . . . 5 ⊢ (∀𝑘 𝐵 = 𝐶 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐶, 1)))‘𝑚))))
26	25	rexbidv 2543	. . . 4 ⊢ (∀𝑘 𝐵 = 𝐶 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐶, 1)))‘𝑚))))
27	17, 26	orbi12d 801	. . 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)))‘𝑚)))))
28	27	iotabidv 5335	. 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 12237	. 2 ⊢ ∏𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 1)))‘𝑚))))
30		df-proddc 12237	. 2 ⊢ ∏𝑘 ∈ 𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ≥‘𝑚)DECID 𝑗 ∈ 𝐴) ∧ (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 # 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐶, 1)))‘𝑚))))
31	28, 29, 30	3eqtr4g 2290	1 ⊢ (∀𝑘 𝐵 = 𝐶 → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   ∧ wa 104   ∨ wo 716  DECID wdc 842  ∀wal 1396   = wceq 1398  ∃wex 1541   ∈ wcel 2203  ∀wral 2520  ∃wrex 2521  ⦋csb 3138   ⊆ wss 3211  ifcif 3620   class class class wbr 4109   ↦ cmpt 4171  ℩cio 5310  –1-1-onto→wf1o 5351  ‘cfv 5352  (class class class)co 6050  0cc0 8127  1c1 8128   · cmul 8132   ≤ cle 8309   # cap 8855  ℕcn 9237  ℤcz 9577  ℤ_≥cuz 9853  ...cfz 10342  seqcseq 10809   ⇝ cli 11963  ∏cprod 12236

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-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-rab 2529  df-v 2815  df-sbc 3043  df-csb 3139  df-un 3215  df-in 3217  df-ss 3224  df-if 3621  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-opab 4172  df-mpt 4173  df-cnv 4757  df-dm 4759  df-rn 4760  df-res 4761  df-iota 5312  df-fv 5360  df-ov 6053  df-oprab 6054  df-mpo 6055  df-recs 6536  df-frec 6622  df-seqfrec 10810  df-proddc 12237

This theorem is referenced by: (None)