cbvproddavw

Description: Change bound variable in a product. Deduction form. (Contributed by GG, 14-Aug-2025)

		Ref	Expression
	Hypothesis	cbvproddavw.1	$⊢ (φ \land j = k) \to B = C$
	Assertion	cbvproddavw	$⊢ φ \to \prod_{j \in A} B = \prod_{k \in A} C$

Proof

Step	Hyp	Ref	Expression
1		cbvproddavw.1	$⊢ (φ \land j = k) \to B = C$
2		eleq1w	$⊢ j = k \to (j \in A \leftrightarrow k \in A)$
3	2	adantl	$⊢ (φ \land j = k) \to (j \in A \leftrightarrow k \in A)$
4	3 1	ifbieq1d	$⊢ (φ \land j = k) \to if (j \in A, B, 1) = if (k \in A, C, 1)$
5	4	cbvmptdavw	$⊢ φ \to (j \in ℤ ⟼ if (j \in A, B, 1)) = (k \in ℤ ⟼ if (k \in A, C, 1))$
6	5	seqeq3d	$⊢ φ \to seq n (\times (j \in ℤ ⟼ if (j \in A, B, 1))) = seq n (\times (k \in ℤ ⟼ if (k \in A, C, 1)))$
7	6	breq1d	$⊢ φ \to (seq n (\times (j \in ℤ ⟼ if (j \in A, B, 1))) ⇝ y \leftrightarrow seq n (\times (k \in ℤ ⟼ if (k \in A, C, 1))) ⇝ y)$
8	7	anbi2d	$⊢ φ \to ((y \neq 0 \land seq n (\times (j \in ℤ ⟼ if (j \in A, B, 1))) ⇝ y) \leftrightarrow (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, C, 1))) ⇝ y))$
9	8	exbidv	$⊢ φ \to (\exists y (y \neq 0 \land seq n (\times (j \in ℤ ⟼ if (j \in A, B, 1))) ⇝ y) \leftrightarrow \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, C, 1))) ⇝ y))$
10	9	rexbidv	$⊢ φ \to (\exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (j \in ℤ ⟼ if (j \in A, B, 1))) ⇝ y) \leftrightarrow \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, C, 1))) ⇝ y))$
11	5	seqeq3d	$⊢ φ \to seq m (\times (j \in ℤ ⟼ if (j \in A, B, 1))) = seq m (\times (k \in ℤ ⟼ if (k \in A, C, 1)))$
12	11	breq1d	$⊢ φ \to (seq m (\times (j \in ℤ ⟼ if (j \in A, B, 1))) ⇝ x \leftrightarrow seq m (\times (k \in ℤ ⟼ if (k \in A, C, 1))) ⇝ x)$
13	10 12	3anbi23d	$⊢ φ \to ((A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (j \in ℤ ⟼ if (j \in A, B, 1))) ⇝ y) \land seq m (\times (j \in ℤ ⟼ if (j \in A, B, 1))) ⇝ x) \leftrightarrow (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, C, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in A, C, 1))) ⇝ x))$
14	13	rexbidv	$⊢ φ \to (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (j \in ℤ ⟼ if (j \in A, B, 1))) ⇝ y) \land seq m (\times (j \in ℤ ⟼ if (j \in A, B, 1))) ⇝ x) \leftrightarrow \exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, C, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in A, C, 1))) ⇝ x))$
15	1	cbvcsbdavw	$⊢ φ \to ⦋ f (n) / j ⦌ B = ⦋ f (n) / k ⦌ C$
16	15	mpteq2dv	$⊢ φ \to (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B) = (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)$
17	16	seqeq3d	$⊢ φ \to seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B)) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C))$
18	17	fveq1d	$⊢ φ \to seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B)) (m) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m)$
19	18	eqeq2d	$⊢ φ \to (x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B)) (m) \leftrightarrow x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m))$
20	19	anbi2d	$⊢ φ \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B)) (m)) \leftrightarrow (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m)))$
21	20	exbidv	$⊢ φ \to (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B)) (m)) \leftrightarrow \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m)))$
22	21	rexbidv	$⊢ φ \to (\exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B)) (m)) \leftrightarrow \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m)))$
23	14 22	orbi12d	$⊢ φ \to ((\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (j \in ℤ ⟼ if (j \in A, B, 1))) ⇝ y) \land seq m (\times (j \in ℤ ⟼ if (j \in A, B, 1))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B)) (m))) \leftrightarrow (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, C, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in A, C, 1))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m))))$
24	23	iotabidv	$⊢ φ \to (ι x \| (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (j \in ℤ ⟼ if (j \in A, B, 1))) ⇝ y) \land seq m (\times (j \in ℤ ⟼ if (j \in A, B, 1))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B)) (m)))) = (ι x \| (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, C, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in A, C, 1))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m))))$
25		df-prod	$⊢ \prod_{j \in A} B = (ι x \| (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (j \in ℤ ⟼ if (j \in A, B, 1))) ⇝ y) \land seq m (\times (j \in ℤ ⟼ if (j \in A, B, 1))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B)) (m))))$
26		df-prod	$⊢ \prod_{k \in A} C = (ι x \| (\exists m \in ℤ (A \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, C, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in A, C, 1))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m))))$
27	24 25 26	3eqtr4g	$⊢ φ \to \prod_{j \in A} B = \prod_{k \in A} C$

Metamath Proof Explorer

Theorem cbvproddavw

Proof