prodeq1i

Description: Equality inference for product. (Contributed by Scott Fenton, 4-Dec-2017) Remove DV conditions. (Revised by GG, 1-Sep-2025)

		Ref	Expression
	Hypothesis	prodeq1i.1	$⊢ A = B$
	Assertion	prodeq1i	$⊢ \prod_{k \in A} C = \prod_{k \in B} C$

Proof

Step	Hyp	Ref	Expression
1		prodeq1i.1	$⊢ A = B$
2	1	sseq1i	$⊢ A \subseteq ℤ_{\geq m} \leftrightarrow B \subseteq ℤ_{\geq m}$
3	1	eleq2i	$⊢ k \in A \leftrightarrow k \in B$
4		ifbi	$⊢ (k \in A \leftrightarrow k \in B) \to if (k \in A, C, 1) = if (k \in B, C, 1)$
5	3 4	ax-mp	$⊢ if (k \in A, C, 1) = if (k \in B, C, 1)$
6	5	mpteq2i	$⊢ (k \in ℤ ⟼ if (k \in A, C, 1)) = (k \in ℤ ⟼ if (k \in B, C, 1))$
7		seqeq3	$⊢ (k \in ℤ ⟼ if (k \in A, C, 1)) = (k \in ℤ ⟼ if (k \in B, C, 1)) \to seq n (\times (k \in ℤ ⟼ if (k \in A, C, 1))) = seq n (\times (k \in ℤ ⟼ if (k \in B, C, 1)))$
8	6 7	ax-mp	$⊢ seq n (\times (k \in ℤ ⟼ if (k \in A, C, 1))) = seq n (\times (k \in ℤ ⟼ if (k \in B, C, 1)))$
9	8	breq1i	$⊢ seq n (\times (k \in ℤ ⟼ if (k \in A, C, 1))) ⇝ y \leftrightarrow seq n (\times (k \in ℤ ⟼ if (k \in B, C, 1))) ⇝ y$
10	9	anbi2i	$⊢ (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, C, 1))) ⇝ y) \leftrightarrow (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in B, C, 1))) ⇝ y)$
11	10	exbii	$⊢ \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, C, 1))) ⇝ y) \leftrightarrow \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in B, C, 1))) ⇝ y)$
12	11	rexbii	$⊢ \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, C, 1))) ⇝ y) \leftrightarrow \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in B, C, 1))) ⇝ y)$
13		seqeq3	$⊢ (k \in ℤ ⟼ if (k \in A, C, 1)) = (k \in ℤ ⟼ if (k \in B, C, 1)) \to seq m (\times (k \in ℤ ⟼ if (k \in A, C, 1))) = seq m (\times (k \in ℤ ⟼ if (k \in B, C, 1)))$
14	6 13	ax-mp	$⊢ seq m (\times (k \in ℤ ⟼ if (k \in A, C, 1))) = seq m (\times (k \in ℤ ⟼ if (k \in B, C, 1)))$
15	14	breq1i	$⊢ seq m (\times (k \in ℤ ⟼ if (k \in A, C, 1))) ⇝ x \leftrightarrow seq m (\times (k \in ℤ ⟼ if (k \in B, C, 1))) ⇝ x$
16	2 12 15	3anbi123i	$⊢ (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) \leftrightarrow (B \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in B, C, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in B, C, 1))) ⇝ x)$
17	16	rexbii	$⊢ \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) \leftrightarrow \exists m \in ℤ (B \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in B, C, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in B, C, 1))) ⇝ x)$
18		f1oeq3	$⊢ A = B \to (f : (1 \dots m) \underset{1-1 onto}{⟶} A \leftrightarrow f : (1 \dots m) \underset{1-1 onto}{⟶} B)$
19	1 18	ax-mp	$⊢ f : (1 \dots m) \underset{1-1 onto}{⟶} A \leftrightarrow f : (1 \dots m) \underset{1-1 onto}{⟶} B$
20	19	anbi1i	$⊢ (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m)) \leftrightarrow (f : (1 \dots m) \underset{1-1 onto}{⟶} B \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m))$
21	20	exbii	$⊢ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m)) \leftrightarrow \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} B \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m))$
22	21	rexbii	$⊢ \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)) \leftrightarrow \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} B \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m))$
23	17 22	orbi12i	$⊢ (\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))) \leftrightarrow (\exists m \in ℤ (B \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in B, C, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in B, C, 1))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} B \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m)))$
24	23	iotabii	$⊢ (ι 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)))) = (ι x \| (\exists m \in ℤ (B \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in B, C, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in B, C, 1))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} B \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m))))$
25		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))))$
26		df-prod	$⊢ \prod_{k \in B} C = (ι x \| (\exists m \in ℤ (B \subseteq ℤ_{\geq m} \land \exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in B, C, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \in B, C, 1))) ⇝ x) \lor \exists m \in ℕ \exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} B \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m))))$
27	24 25 26	3eqtr4i	$⊢ \prod_{k \in A} C = \prod_{k \in B} C$

Metamath Proof Explorer

Theorem prodeq1i

Proof