prodeq2ii

Description: Equality theorem for product, with the class expressions B and C guarded by _I to be always sets. (Contributed by Scott Fenton, 4-Dec-2017)

		Ref	Expression
	Assertion	prodeq2ii	$⊢ \forall k \in A I (B) = I (C) \to \prod_{k \in A} B = \prod_{k \in A} C$

Proof

Step	Hyp	Ref	Expression
1		eluzelz	$⊢ n \in ℤ_{\geq m} \to n \in ℤ$
2	1	adantl	$⊢ (\forall k \in A I (B) = I (C) \land n \in ℤ_{\geq m}) \to n \in ℤ$
3		nfra1	$⊢ Ⅎ k \forall k \in A I (B) = I (C)$
4		rsp	$⊢ \forall k \in A I (B) = I (C) \to (k \in A \to I (B) = I (C))$
5	4	adantr	$⊢ (\forall k \in A I (B) = I (C) \land k \in ℤ) \to (k \in A \to I (B) = I (C))$
6		ifeq1	$⊢ I (B) = I (C) \to if (k \in A, I (B), I (1)) = if (k \in A, I (C), I (1))$
7	5 6	syl6	$⊢ (\forall k \in A I (B) = I (C) \land k \in ℤ) \to (k \in A \to if (k \in A, I (B), I (1)) = if (k \in A, I (C), I (1)))$
8		iffalse	$⊢ \neg k \in A \to if (k \in A, I (B), I (1)) = I (1)$
9		iffalse	$⊢ \neg k \in A \to if (k \in A, I (C), I (1)) = I (1)$
10	8 9	eqtr4d	$⊢ \neg k \in A \to if (k \in A, I (B), I (1)) = if (k \in A, I (C), I (1))$
11	7 10	pm2.61d1	$⊢ (\forall k \in A I (B) = I (C) \land k \in ℤ) \to if (k \in A, I (B), I (1)) = if (k \in A, I (C), I (1))$
12		fvif	$⊢ I (if (k \in A, B, 1)) = if (k \in A, I (B), I (1))$
13		fvif	$⊢ I (if (k \in A, C, 1)) = if (k \in A, I (C), I (1))$
14	11 12 13	3eqtr4g	$⊢ (\forall k \in A I (B) = I (C) \land k \in ℤ) \to I (if (k \in A, B, 1)) = I (if (k \in A, C, 1))$
15	3 14	mpteq2da	$⊢ \forall k \in A I (B) = I (C) \to (k \in ℤ ⟼ I (if (k \in A, B, 1))) = (k \in ℤ ⟼ I (if (k \in A, C, 1)))$
16	15	adantr	$⊢ (\forall k \in A I (B) = I (C) \land x \in ℤ_{\geq n}) \to (k \in ℤ ⟼ I (if (k \in A, B, 1))) = (k \in ℤ ⟼ I (if (k \in A, C, 1)))$
17	16	fveq1d	$⊢ (\forall k \in A I (B) = I (C) \land x \in ℤ_{\geq n}) \to (k \in ℤ ⟼ I (if (k \in A, B, 1))) (x) = (k \in ℤ ⟼ I (if (k \in A, C, 1))) (x)$
18	17	adantlr	$⊢ ((\forall k \in A I (B) = I (C) \land n \in ℤ_{\geq m}) \land x \in ℤ_{\geq n}) \to (k \in ℤ ⟼ I (if (k \in A, B, 1))) (x) = (k \in ℤ ⟼ I (if (k \in A, C, 1))) (x)$
19		eqid	$⊢ (k \in ℤ ⟼ if (k \in A, B, 1)) = (k \in ℤ ⟼ if (k \in A, B, 1))$
20		eqid	$⊢ (k \in ℤ ⟼ I (if (k \in A, B, 1))) = (k \in ℤ ⟼ I (if (k \in A, B, 1)))$
21	19 20	fvmptex	$⊢ (k \in ℤ ⟼ if (k \in A, B, 1)) (x) = (k \in ℤ ⟼ I (if (k \in A, B, 1))) (x)$
22		eqid	$⊢ (k \in ℤ ⟼ if (k \in A, C, 1)) = (k \in ℤ ⟼ if (k \in A, C, 1))$
23		eqid	$⊢ (k \in ℤ ⟼ I (if (k \in A, C, 1))) = (k \in ℤ ⟼ I (if (k \in A, C, 1)))$
24	22 23	fvmptex	$⊢ (k \in ℤ ⟼ if (k \in A, C, 1)) (x) = (k \in ℤ ⟼ I (if (k \in A, C, 1))) (x)$
25	18 21 24	3eqtr4g	$⊢ ((\forall k \in A I (B) = I (C) \land n \in ℤ_{\geq m}) \land x \in ℤ_{\geq n}) \to (k \in ℤ ⟼ if (k \in A, B, 1)) (x) = (k \in ℤ ⟼ if (k \in A, C, 1)) (x)$
26	2 25	seqfeq	$⊢ (\forall k \in A I (B) = I (C) \land n \in ℤ_{\geq m}) \to seq n (\times (k \in ℤ ⟼ if (k \in A, B, 1))) = seq n (\times (k \in ℤ ⟼ if (k \in A, C, 1)))$
27	26	breq1d	$⊢ (\forall k \in A I (B) = I (C) \land n \in ℤ_{\geq m}) \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)$
28	27	anbi2d	$⊢ (\forall k \in A I (B) = I (C) \land n \in ℤ_{\geq m}) \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))$
29	28	exbidv	$⊢ (\forall k \in A I (B) = I (C) \land n \in ℤ_{\geq m}) \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))$
30	29	rexbidva	$⊢ \forall k \in A I (B) = I (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))$
31	30	adantr	$⊢ (\forall k \in A I (B) = I (C) \land m \in ℤ) \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))$
32		simpr	$⊢ (\forall k \in A I (B) = I (C) \land m \in ℤ) \to m \in ℤ$
33	15	adantr	$⊢ (\forall k \in A I (B) = I (C) \land x \in ℤ_{\geq m}) \to (k \in ℤ ⟼ I (if (k \in A, B, 1))) = (k \in ℤ ⟼ I (if (k \in A, C, 1)))$
34	33	fveq1d	$⊢ (\forall k \in A I (B) = I (C) \land x \in ℤ_{\geq m}) \to (k \in ℤ ⟼ I (if (k \in A, B, 1))) (x) = (k \in ℤ ⟼ I (if (k \in A, C, 1))) (x)$
35	34 21 24	3eqtr4g	$⊢ (\forall k \in A I (B) = I (C) \land x \in ℤ_{\geq m}) \to (k \in ℤ ⟼ if (k \in A, B, 1)) (x) = (k \in ℤ ⟼ if (k \in A, C, 1)) (x)$
36	35	adantlr	$⊢ ((\forall k \in A I (B) = I (C) \land m \in ℤ) \land x \in ℤ_{\geq m}) \to (k \in ℤ ⟼ if (k \in A, B, 1)) (x) = (k \in ℤ ⟼ if (k \in A, C, 1)) (x)$
37	32 36	seqfeq	$⊢ (\forall k \in A I (B) = I (C) \land m \in ℤ) \to seq m (\times (k \in ℤ ⟼ if (k \in A, B, 1))) = seq m (\times (k \in ℤ ⟼ if (k \in A, C, 1)))$
38	37	breq1d	$⊢ (\forall k \in A I (B) = I (C) \land m \in ℤ) \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)$
39	31 38	3anbi23d	$⊢ (\forall k \in A I (B) = I (C) \land m \in ℤ) \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))$
40	39	rexbidva	$⊢ \forall k \in A I (B) = I (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))$
41		simplr	$⊢ ((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to m \in ℕ$
42		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
43	41 42	eleqtrdi	$⊢ ((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to m \in ℤ_{\geq 1}$
44		f1of	$⊢ f : (1 \dots m) \underset{1-1 onto}{⟶} A \to f : (1 \dots m) ⟶ A$
45	44	ad2antlr	$⊢ (((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land x \in (1 \dots m)) \to f : (1 \dots m) ⟶ A$
46		ffvelcdm	$⊢ (f : (1 \dots m) ⟶ A \land x \in (1 \dots m)) \to f (x) \in A$
47	45 46	sylancom	$⊢ (((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land x \in (1 \dots m)) \to f (x) \in A$
48		simplll	$⊢ (((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land x \in (1 \dots m)) \to \forall k \in A I (B) = I (C)$
49		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ f (x) / k ⦌ I (B)$
50		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ f (x) / k ⦌ I (C)$
51	49 50	nfeq	$⊢ Ⅎ k ⦋ f (x) / k ⦌ I (B) = ⦋ f (x) / k ⦌ I (C)$
52		csbeq1a	$⊢ k = f (x) \to I (B) = ⦋ f (x) / k ⦌ I (B)$
53		csbeq1a	$⊢ k = f (x) \to I (C) = ⦋ f (x) / k ⦌ I (C)$
54	52 53	eqeq12d	$⊢ k = f (x) \to (I (B) = I (C) \leftrightarrow ⦋ f (x) / k ⦌ I (B) = ⦋ f (x) / k ⦌ I (C))$
55	51 54	rspc	$⊢ f (x) \in A \to (\forall k \in A I (B) = I (C) \to ⦋ f (x) / k ⦌ I (B) = ⦋ f (x) / k ⦌ I (C))$
56	47 48 55	sylc	$⊢ (((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land x \in (1 \dots m)) \to ⦋ f (x) / k ⦌ I (B) = ⦋ f (x) / k ⦌ I (C)$
57		fvex	$⊢ f (x) \in V$
58		csbfv2g	$⊢ f (x) \in V \to ⦋ f (x) / k ⦌ I (B) = I (⦋ f (x) / k ⦌ B)$
59	57 58	ax-mp	$⊢ ⦋ f (x) / k ⦌ I (B) = I (⦋ f (x) / k ⦌ B)$
60		csbfv2g	$⊢ f (x) \in V \to ⦋ f (x) / k ⦌ I (C) = I (⦋ f (x) / k ⦌ C)$
61	57 60	ax-mp	$⊢ ⦋ f (x) / k ⦌ I (C) = I (⦋ f (x) / k ⦌ C)$
62	56 59 61	3eqtr3g	$⊢ (((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land x \in (1 \dots m)) \to I (⦋ f (x) / k ⦌ B) = I (⦋ f (x) / k ⦌ C)$
63		elfznn	$⊢ x \in (1 \dots m) \to x \in ℕ$
64	63	adantl	$⊢ (((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land x \in (1 \dots m)) \to x \in ℕ$
65		fveq2	$⊢ n = x \to f (n) = f (x)$
66	65	csbeq1d	$⊢ n = x \to ⦋ f (n) / k ⦌ B = ⦋ f (x) / k ⦌ B$
67		eqid	$⊢ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B) = (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)$
68	66 67	fvmpti	$⊢ x \in ℕ \to (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B) (x) = I (⦋ f (x) / k ⦌ B)$
69	64 68	syl	$⊢ (((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land x \in (1 \dots m)) \to (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B) (x) = I (⦋ f (x) / k ⦌ B)$
70	65	csbeq1d	$⊢ n = x \to ⦋ f (n) / k ⦌ C = ⦋ f (x) / k ⦌ C$
71		eqid	$⊢ (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C) = (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)$
72	70 71	fvmpti	$⊢ x \in ℕ \to (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C) (x) = I (⦋ f (x) / k ⦌ C)$
73	64 72	syl	$⊢ (((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land x \in (1 \dots m)) \to (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C) (x) = I (⦋ f (x) / k ⦌ C)$
74	62 69 73	3eqtr4d	$⊢ (((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \land x \in (1 \dots m)) \to (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B) (x) = (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C) (x)$
75	43 74	seqfveq	$⊢ ((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m) = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m)$
76	75	eqeq2d	$⊢ ((\forall k \in A I (B) = I (C) \land m \in ℕ) \land f : (1 \dots m) \underset{1-1 onto}{⟶} A) \to (x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)) (m) \leftrightarrow x = seq 1 (\times (n \in ℕ ⟼ ⦋ f (n) / k ⦌ C)) (m))$
77	76	pm5.32da	$⊢ (\forall k \in A I (B) = I (C) \land m \in ℕ) \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)))$
78	77	exbidv	$⊢ (\forall k \in A I (B) = I (C) \land m \in ℕ) \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)))$
79	78	rexbidva	$⊢ \forall k \in A I (B) = I (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)))$
80	40 79	orbi12d	$⊢ \forall k \in A I (B) = I (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))))$
81	80	iotabidv	$⊢ \forall k \in A I (B) = I (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))))$
82		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))))$
83		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))))$
84	81 82 83	3eqtr4g	$⊢ \forall k \in A I (B) = I (C) \to \prod_{k \in A} B = \prod_{k \in A} C$

Metamath Proof Explorer

Theorem prodeq2ii

Proof