prodeq1

Description: Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017)

		Ref	Expression
	Assertion	prodeq1	$⊢ A = B \to \prod_{k \in A} C = \prod_{k \in B} C$

Proof

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

Metamath Proof Explorer

Theorem prodeq1

Proof