cbvprod

Description: Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017)

	Ref	Expression
Hypotheses	cbvprod.1	$⊢ j = k \to B = C$
	cbvprod.2	$⊢ \underline{Ⅎ} k A$
	cbvprod.3	$⊢ \underline{Ⅎ} j A$
	cbvprod.4	$⊢ \underline{Ⅎ} k B$
	cbvprod.5	$⊢ \underline{Ⅎ} j C$
Assertion	cbvprod	$⊢ \prod_{j \in A} B = \prod_{k \in A} C$

Proof

Step	Hyp	Ref	Expression
1		cbvprod.1	$⊢ j = k \to B = C$
2		cbvprod.2	$⊢ \underline{Ⅎ} k A$
3		cbvprod.3	$⊢ \underline{Ⅎ} j A$
4		cbvprod.4	$⊢ \underline{Ⅎ} k B$
5		cbvprod.5	$⊢ \underline{Ⅎ} j C$
6		biid	$⊢ A \subseteq ℤ_{\geq m} \leftrightarrow A \subseteq ℤ_{\geq m}$
7	2	nfcri	$⊢ Ⅎ k j \in A$
8		nfcv	$⊢ \underline{Ⅎ} k 1$
9	7 4 8	nfif	$⊢ \underline{Ⅎ} k if (j \in A, B, 1)$
10	3	nfcri	$⊢ Ⅎ j k \in A$
11		nfcv	$⊢ \underline{Ⅎ} j 1$
12	10 5 11	nfif	$⊢ \underline{Ⅎ} j if (k \in A, C, 1)$
13		eleq1w	$⊢ j = k \to (j \in A \leftrightarrow k \in A)$
14	13 1	ifbieq1d	$⊢ j = k \to if (j \in A, B, 1) = if (k \in A, C, 1)$
15	9 12 14	cbvmpt	$⊢ (j \in ℤ ⟼ if (j \in A, B, 1)) = (k \in ℤ ⟼ if (k \in A, C, 1))$
16		seqeq3	$⊢ (j \in ℤ ⟼ if (j \in A, B, 1)) = (k \in ℤ ⟼ if (k \in A, C, 1)) \to seq n (\times (j \in ℤ ⟼ if (j \in A, B, 1))) = seq n (\times (k \in ℤ ⟼ if (k \in A, C, 1)))$
17	15 16	ax-mp	$⊢ seq n (\times (j \in ℤ ⟼ if (j \in A, B, 1))) = seq n (\times (k \in ℤ ⟼ if (k \in A, C, 1)))$
18	17	breq1i	$⊢ 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$
19	18	anbi2i	$⊢ (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)$
20	19	exbii	$⊢ \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)$
21	20	rexbii	$⊢ \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)$
22		seqeq3	$⊢ (j \in ℤ ⟼ if (j \in A, B, 1)) = (k \in ℤ ⟼ if (k \in A, C, 1)) \to seq m (\times (j \in ℤ ⟼ if (j \in A, B, 1))) = seq m (\times (k \in ℤ ⟼ if (k \in A, C, 1)))$
23	15 22	ax-mp	$⊢ seq m (\times (j \in ℤ ⟼ if (j \in A, B, 1))) = seq m (\times (k \in ℤ ⟼ if (k \in A, C, 1)))$
24	23	breq1i	$⊢ 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$
25	6 21 24	3anbi123i	$⊢ (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)$
26	25	rexbii	$⊢ \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)$
27	4 5 1	cbvcsbw	$⊢ ⦋ f (n) / j ⦌ B = ⦋ f (n) / k ⦌ C$
28	27	mpteq2i	$⊢ (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B) = (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)$
29		seqeq3	$⊢ (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B) = (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C) \to seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B)) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C))$
30	28 29	ax-mp	$⊢ seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B)) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C))$
31	30	fveq1i	$⊢ seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B)) (m) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m)$
32	31	eqeq2i	$⊢ x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / j ⦌ B)) (m) \leftrightarrow x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m)$
33	32	anbi2i	$⊢ (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))$
34	33	exbii	$⊢ \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))$
35	34	rexbii	$⊢ \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))$
36	26 35	orbi12i	$⊢ (\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)))$
37	36	iotabii	$⊢ (ι 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))))$
38		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))))$
39		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))))$
40	37 38 39	3eqtr4i	$⊢ \prod_{j \in A} B = \prod_{k \in A} C$

Metamath Proof Explorer

Theorem cbvprod

Proof