prodeq1f

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

	Ref	Expression
Hypotheses	prodeq1f.1	$⊢ \underline{Ⅎ} k A$
	prodeq1f.2	$⊢ \underline{Ⅎ} k B$
Assertion	prodeq1f	$⊢ A = B \to \prod_{k \in A} C = \prod_{k \in B} C$

Proof

Step	Hyp	Ref	Expression
1		prodeq1f.1	$⊢ \underline{Ⅎ} k A$
2		prodeq1f.2	$⊢ \underline{Ⅎ} k B$
3		sseq1	$⊢ A = B \to (A \subseteq ℤ_{\geq m} \leftrightarrow B \subseteq ℤ_{\geq m})$
4	1 2	nfeq	$⊢ Ⅎ k A = B$
5		eleq2	$⊢ A = B \to (k \in A \leftrightarrow k \in B)$
6	5	ifbid	$⊢ A = B \to if (k \in A, C, 1) = if (k \in B, C, 1)$
7	6	adantr	$⊢ (A = B \land k \in ℤ) \to if (k \in A, C, 1) = if (k \in B, C, 1)$
8	4 7	mpteq2da	$⊢ A = B \to (k \in ℤ ⟼ if (k \in A, C, 1)) = (k \in ℤ ⟼ if (k \in B, C, 1))$
9	8	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)))$
10	9	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)$
11	10	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))$
12	11	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))$
13	12	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))$
14	8	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)))$
15	14	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)$
16	3 13 15	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))$
17	16	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))$
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	18	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)))$
20	19	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)))$
21	20	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)))$
22	17 21	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))))$
23	22	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))))$
24		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))))$
25		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))))$
26	23 24 25	3eqtr4g	$⊢ A = B \to \prod_{k \in A} C = \prod_{k \in B} C$

Metamath Proof Explorer

Theorem prodeq1f

Proof