prodeq12sdv

Description: Equality deduction for product. General version of prodeq2sdv . (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypotheses	prodeq12sdv.1	$⊢ φ \to A = B$
	prodeq12sdv.2	$⊢ φ \to C = D$
Assertion	prodeq12sdv	$⊢ φ \to \prod_{k \in A} C = \prod_{k \in B} D$

Proof

Step	Hyp	Ref	Expression
1		prodeq12sdv.1	$⊢ φ \to A = B$
2		prodeq12sdv.2	$⊢ φ \to C = D$
3	1	sseq1d	$⊢ φ \to (A \subseteq ℤ_{\geq m} \leftrightarrow B \subseteq ℤ_{\geq m})$
4	1	eleq2d	$⊢ φ \to (k \in A \leftrightarrow k \in B)$
5	4	ifbid	$⊢ φ \to if (k \in A, C, 1) = if (k \in B, C, 1)$
6	5	mpteq2dv	$⊢ φ \to (k \in ℤ ⟼ if (k \in A, C, 1)) = (k \in ℤ ⟼ if (k \in B, C, 1))$
7	6	seqeq3d	$⊢ φ \to seq n (\times (k \in ℤ ⟼ if (k \in A, C, 1))) = seq n (\times (k \in ℤ ⟼ if (k \in B, C, 1)))$
8	7	breq1d	$⊢ φ \to (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)$
9	8	anbi2d	$⊢ φ \to ((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))$
10	9	exbidv	$⊢ φ \to (\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))$
11	10	rexbidv	$⊢ φ \to (\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))$
12	6	seqeq3d	$⊢ φ \to seq m (\times (k \in ℤ ⟼ if (k \in A, C, 1))) = seq m (\times (k \in ℤ ⟼ if (k \in B, C, 1)))$
13	12	breq1d	$⊢ φ \to (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)$
14	3 11 13	3anbi123d	$⊢ φ \to ((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))$
15	14	rexbidv	$⊢ φ \to (\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))$
16	1	f1oeq3d	$⊢ φ \to (f : (1 \dots m) \underset{1-1 onto}{⟶} A \leftrightarrow f : (1 \dots m) \underset{1-1 onto}{⟶} B)$
17	16	anbi1d	$⊢ φ \to ((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)))$
18	17	exbidv	$⊢ φ \to (\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)))$
19	18	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) / 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)))$
20	15 19	orbi12d	$⊢ φ \to ((\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))))$
21	20	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 (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))))$
22		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))))$
23		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))))$
24	21 22 23	3eqtr4g	$⊢ φ \to \prod_{k \in A} C = \prod_{k \in B} C$
25	2	prodeq2sdv	$⊢ φ \to \prod_{k \in B} C = \prod_{k \in B} D$
26	24 25	eqtrd	$⊢ φ \to \prod_{k \in A} C = \prod_{k \in B} D$

Metamath Proof Explorer

Theorem prodeq12sdv

Proof