prodeq2w

Description: Equality theorem for product, when the class expressions B and C are equal everywhere. Proved using only Extensionality. (Contributed by Scott Fenton, 4-Dec-2017)

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

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ℤ = ℤ$
2		ifeq1	$⊢ B = C \to if (k \in A, B, 1) = if (k \in A, C, 1)$
3	2	alimi	$⊢ \forall k B = C \to \forall k if (k \in A, B, 1) = if (k \in A, C, 1)$
4		alral	$⊢ \forall k if (k \in A, B, 1) = if (k \in A, C, 1) \to \forall k \in ℤ if (k \in A, B, 1) = if (k \in A, C, 1)$
5	3 4	syl	$⊢ \forall k B = C \to \forall k \in ℤ if (k \in A, B, 1) = if (k \in A, C, 1)$
6		mpteq12	$⊢ (ℤ = ℤ \land \forall k \in ℤ if (k \in A, B, 1) = if (k \in A, C, 1)) \to (k \in ℤ ⟼ if (k \in A, B, 1)) = (k \in ℤ ⟼ if (k \in A, C, 1))$
7	1 5 6	sylancr	$⊢ \forall k B = C \to (k \in ℤ ⟼ if (k \in A, B, 1)) = (k \in ℤ ⟼ if (k \in A, C, 1))$
8	7	seqeq3d	$⊢ \forall k B = C \to seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) = seq n (\times (k \in ℤ ⟼ if (k \in A, C, 1)))$
9	8	breq1d	$⊢ \forall k B = C \to (seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y \leftrightarrow seq n (\times (k \in ℤ ⟼ if (k \in A, C, 1))) ⇝ y)$
10	9	anbi2d	$⊢ \forall k B = C \to ((y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y) \leftrightarrow (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, C, 1))) ⇝ y))$
11	10	exbidv	$⊢ \forall k B = C \to (\exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y) \leftrightarrow \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \in A, C, 1))) ⇝ y))$
12	11	rexbidv	$⊢ \forall k B = C \to (\exists n \in ℤ_{\geq m} \exists y (y \neq 0 \land seq n (\times (k \in ℤ ⟼ if (k \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))$
13	7	seqeq3d	$⊢ \forall k B = C \to seq m (\times (k \in ℤ ⟼ if (k \in A, B, 1))) = seq m (\times (k \in ℤ ⟼ if (k \in A, C, 1)))$
14	13	breq1d	$⊢ \forall k B = C \to (seq m (\times (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ x \leftrightarrow seq m (\times (k \in ℤ ⟼ if (k \in A, C, 1))) ⇝ x)$
15	12 14	3anbi23d	$⊢ \forall k B = C \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, B, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \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))$
16	15	rexbidv	$⊢ \forall k B = C \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, B, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \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))$
17		csbeq2	$⊢ \forall k B = C \to ⦋ f (n) / k ⦌ B = ⦋ f (n) / k ⦌ C$
18	17	mpteq2dv	$⊢ \forall k B = C \to (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B) = (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)$
19	18	seqeq3d	$⊢ \forall k B = C \to seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C))$
20	19	fveq1d	$⊢ \forall k B = C \to seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m)$
21	20	eqeq2d	$⊢ \forall k B = C \to (x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m) \leftrightarrow x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m))$
22	21	anbi2d	$⊢ \forall k B = C \to ((f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m)) \leftrightarrow (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m)))$
23	22	exbidv	$⊢ \forall k B = C \to (\exists f (f : (1 \dots m) \underset{1-1 onto}{⟶} A \land x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ 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)))$
24	23	rexbidv	$⊢ \forall k B = C \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 ⦌ 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)))$
25	16 24	orbi12d	$⊢ \forall k B = C \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, B, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \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) / k ⦌ 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))))$
26	25	iotabidv	$⊢ \forall k B = C \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, B, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \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) / k ⦌ 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))))$
27		df-prod	$⊢ \prod_{k \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 (k \in ℤ ⟼ if (k \in A, B, 1))) ⇝ y) \land seq m (\times (k \in ℤ ⟼ if (k \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) / k ⦌ B)) (m))))$
28		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))))$
29	26 27 28	3eqtr4g	$⊢ \forall k B = C \to \prod_{k \in A} B = \prod_{k \in A} C$

Metamath Proof Explorer

Theorem prodeq2w

Proof