prodss

Description: Change the index set to a subset in an upper integer product. (Contributed by Scott Fenton, 11-Dec-2017)

	Ref	Expression
Hypotheses	prodss.1	$⊢ φ \to A \subseteq B$
	prodss.2	$⊢ (φ \land k \in A) \to C \in ℂ$
	prodss.3	$⊢ φ \to \exists n \in ℤ_{\geq M} \exists y (y \neq 0 \land seq n (\times (k \in ℤ_{\geq M} ⟼ if (k \in B, C, 1))) ⇝ y)$
	prodss.4	$⊢ (φ \land k \in (B ∖ A)) \to C = 1$
	prodss.5	$⊢ φ \to B \subseteq ℤ_{\geq M}$
Assertion	prodss	$⊢ φ \to \prod_{k \in A} C = \prod_{k \in B} C$

Proof

Step	Hyp	Ref	Expression
1		prodss.1	$⊢ φ \to A \subseteq B$
2		prodss.2	$⊢ (φ \land k \in A) \to C \in ℂ$
3		prodss.3	$⊢ φ \to \exists n \in ℤ_{\geq M} \exists y (y \neq 0 \land seq n (\times (k \in ℤ_{\geq M} ⟼ if (k \in B, C, 1))) ⇝ y)$
4		prodss.4	$⊢ (φ \land k \in (B ∖ A)) \to C = 1$
5		prodss.5	$⊢ φ \to B \subseteq ℤ_{\geq M}$
6		eqid	$⊢ ℤ_{\geq M} = ℤ_{\geq M}$
7		simpr	$⊢ (φ \land M \in ℤ) \to M \in ℤ$
8	3	adantr	$⊢ (φ \land M \in ℤ) \to \exists n \in ℤ_{\geq M} \exists y (y \neq 0 \land seq n (\times (k \in ℤ_{\geq M} ⟼ if (k \in B, C, 1))) ⇝ y)$
9	1 5	sstrd	$⊢ φ \to A \subseteq ℤ_{\geq M}$
10	9	adantr	$⊢ (φ \land M \in ℤ) \to A \subseteq ℤ_{\geq M}$
11		simpr	$⊢ ((φ \land M \in ℤ) \land m \in ℤ_{\geq M}) \to m \in ℤ_{\geq M}$
12		iftrue	$⊢ m \in B \to if (m \in B, ⦋ m / k ⦌ C, 1) = ⦋ m / k ⦌ C$
13	12	adantl	$⊢ (φ \land m \in B) \to if (m \in B, ⦋ m / k ⦌ C, 1) = ⦋ m / k ⦌ C$
14	2	ex	$⊢ φ \to (k \in A \to C \in ℂ)$
15	14	adantr	$⊢ (φ \land k \in B) \to (k \in A \to C \in ℂ)$
16		eldif	$⊢ k \in (B ∖ A) \leftrightarrow (k \in B \land \neg k \in A)$
17		ax-1cn	$⊢ 1 \in ℂ$
18	4 17	eqeltrdi	$⊢ (φ \land k \in (B ∖ A)) \to C \in ℂ$
19	16 18	sylan2br	$⊢ (φ \land (k \in B \land \neg k \in A)) \to C \in ℂ$
20	19	expr	$⊢ (φ \land k \in B) \to (\neg k \in A \to C \in ℂ)$
21	15 20	pm2.61d	$⊢ (φ \land k \in B) \to C \in ℂ$
22	21	ralrimiva	$⊢ φ \to \forall k \in B C \in ℂ$
23		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ m / k ⦌ C$
24	23	nfel1	$⊢ Ⅎ k ⦋ m / k ⦌ C \in ℂ$
25		csbeq1a	$⊢ k = m \to C = ⦋ m / k ⦌ C$
26	25	eleq1d	$⊢ k = m \to (C \in ℂ \leftrightarrow ⦋ m / k ⦌ C \in ℂ)$
27	24 26	rspc	$⊢ m \in B \to (\forall k \in B C \in ℂ \to ⦋ m / k ⦌ C \in ℂ)$
28	22 27	mpan9	$⊢ (φ \land m \in B) \to ⦋ m / k ⦌ C \in ℂ$
29	13 28	eqeltrd	$⊢ (φ \land m \in B) \to if (m \in B, ⦋ m / k ⦌ C, 1) \in ℂ$
30		iffalse	$⊢ \neg m \in B \to if (m \in B, ⦋ m / k ⦌ C, 1) = 1$
31	30 17	eqeltrdi	$⊢ \neg m \in B \to if (m \in B, ⦋ m / k ⦌ C, 1) \in ℂ$
32	31	adantl	$⊢ (φ \land \neg m \in B) \to if (m \in B, ⦋ m / k ⦌ C, 1) \in ℂ$
33	29 32	pm2.61dan	$⊢ φ \to if (m \in B, ⦋ m / k ⦌ C, 1) \in ℂ$
34	33	adantr	$⊢ (φ \land M \in ℤ) \to if (m \in B, ⦋ m / k ⦌ C, 1) \in ℂ$
35	34	adantr	$⊢ ((φ \land M \in ℤ) \land m \in ℤ_{\geq M}) \to if (m \in B, ⦋ m / k ⦌ C, 1) \in ℂ$
36		nfcv	$⊢ \underline{Ⅎ} k m$
37		nfv	$⊢ Ⅎ k m \in B$
38		nfcv	$⊢ \underline{Ⅎ} k 1$
39	37 23 38	nfif	$⊢ \underline{Ⅎ} k if (m \in B, ⦋ m / k ⦌ C, 1)$
40		eleq1w	$⊢ k = m \to (k \in B \leftrightarrow m \in B)$
41	40 25	ifbieq1d	$⊢ k = m \to if (k \in B, C, 1) = if (m \in B, ⦋ m / k ⦌ C, 1)$
42		eqid	$⊢ (k \in ℤ_{\geq M} ⟼ if (k \in B, C, 1)) = (k \in ℤ_{\geq M} ⟼ if (k \in B, C, 1))$
43	36 39 41 42	fvmptf	$⊢ (m \in ℤ_{\geq M} \land if (m \in B, ⦋ m / k ⦌ C, 1) \in ℂ) \to (k \in ℤ_{\geq M} ⟼ if (k \in B, C, 1)) (m) = if (m \in B, ⦋ m / k ⦌ C, 1)$
44	11 35 43	syl2anc	$⊢ ((φ \land M \in ℤ) \land m \in ℤ_{\geq M}) \to (k \in ℤ_{\geq M} ⟼ if (k \in B, C, 1)) (m) = if (m \in B, ⦋ m / k ⦌ C, 1)$
45		iftrue	$⊢ m \in A \to if (m \in A, (k \in A ⟼ C) (m), 1) = (k \in A ⟼ C) (m)$
46	45	adantl	$⊢ ((φ \land M \in ℤ) \land m \in A) \to if (m \in A, (k \in A ⟼ C) (m), 1) = (k \in A ⟼ C) (m)$
47		simpr	$⊢ ((φ \land M \in ℤ) \land m \in A) \to m \in A$
48	1	adantr	$⊢ (φ \land M \in ℤ) \to A \subseteq B$
49	48	sselda	$⊢ ((φ \land M \in ℤ) \land m \in A) \to m \in B$
50	28	adantlr	$⊢ ((φ \land M \in ℤ) \land m \in B) \to ⦋ m / k ⦌ C \in ℂ$
51	49 50	syldan	$⊢ ((φ \land M \in ℤ) \land m \in A) \to ⦋ m / k ⦌ C \in ℂ$
52		eqid	$⊢ (k \in A ⟼ C) = (k \in A ⟼ C)$
53	52	fvmpts	$⊢ (m \in A \land ⦋ m / k ⦌ C \in ℂ) \to (k \in A ⟼ C) (m) = ⦋ m / k ⦌ C$
54	47 51 53	syl2anc	$⊢ ((φ \land M \in ℤ) \land m \in A) \to (k \in A ⟼ C) (m) = ⦋ m / k ⦌ C$
55	46 54	eqtrd	$⊢ ((φ \land M \in ℤ) \land m \in A) \to if (m \in A, (k \in A ⟼ C) (m), 1) = ⦋ m / k ⦌ C$
56	55	ex	$⊢ (φ \land M \in ℤ) \to (m \in A \to if (m \in A, (k \in A ⟼ C) (m), 1) = ⦋ m / k ⦌ C)$
57	56	adantr	$⊢ ((φ \land M \in ℤ) \land m \in B) \to (m \in A \to if (m \in A, (k \in A ⟼ C) (m), 1) = ⦋ m / k ⦌ C)$
58		iffalse	$⊢ \neg m \in A \to if (m \in A, (k \in A ⟼ C) (m), 1) = 1$
59	58	adantl	$⊢ (m \in B \land \neg m \in A) \to if (m \in A, (k \in A ⟼ C) (m), 1) = 1$
60	59	adantl	$⊢ ((φ \land M \in ℤ) \land (m \in B \land \neg m \in A)) \to if (m \in A, (k \in A ⟼ C) (m), 1) = 1$
61		eldif	$⊢ m \in (B ∖ A) \leftrightarrow (m \in B \land \neg m \in A)$
62	4	ralrimiva	$⊢ φ \to \forall k \in (B ∖ A) C = 1$
63	62	adantr	$⊢ (φ \land M \in ℤ) \to \forall k \in (B ∖ A) C = 1$
64	23	nfeq1	$⊢ Ⅎ k ⦋ m / k ⦌ C = 1$
65	25	eqeq1d	$⊢ k = m \to (C = 1 \leftrightarrow ⦋ m / k ⦌ C = 1)$
66	64 65	rspc	$⊢ m \in (B ∖ A) \to (\forall k \in (B ∖ A) C = 1 \to ⦋ m / k ⦌ C = 1)$
67	63 66	mpan9	$⊢ ((φ \land M \in ℤ) \land m \in (B ∖ A)) \to ⦋ m / k ⦌ C = 1$
68	61 67	sylan2br	$⊢ ((φ \land M \in ℤ) \land (m \in B \land \neg m \in A)) \to ⦋ m / k ⦌ C = 1$
69	60 68	eqtr4d	$⊢ ((φ \land M \in ℤ) \land (m \in B \land \neg m \in A)) \to if (m \in A, (k \in A ⟼ C) (m), 1) = ⦋ m / k ⦌ C$
70	69	expr	$⊢ ((φ \land M \in ℤ) \land m \in B) \to (\neg m \in A \to if (m \in A, (k \in A ⟼ C) (m), 1) = ⦋ m / k ⦌ C)$
71	57 70	pm2.61d	$⊢ ((φ \land M \in ℤ) \land m \in B) \to if (m \in A, (k \in A ⟼ C) (m), 1) = ⦋ m / k ⦌ C$
72	12	adantl	$⊢ ((φ \land M \in ℤ) \land m \in B) \to if (m \in B, ⦋ m / k ⦌ C, 1) = ⦋ m / k ⦌ C$
73	71 72	eqtr4d	$⊢ ((φ \land M \in ℤ) \land m \in B) \to if (m \in A, (k \in A ⟼ C) (m), 1) = if (m \in B, ⦋ m / k ⦌ C, 1)$
74	48	ssneld	$⊢ (φ \land M \in ℤ) \to (\neg m \in B \to \neg m \in A)$
75	74	imp	$⊢ ((φ \land M \in ℤ) \land \neg m \in B) \to \neg m \in A$
76	75 58	syl	$⊢ ((φ \land M \in ℤ) \land \neg m \in B) \to if (m \in A, (k \in A ⟼ C) (m), 1) = 1$
77	30	adantl	$⊢ ((φ \land M \in ℤ) \land \neg m \in B) \to if (m \in B, ⦋ m / k ⦌ C, 1) = 1$
78	76 77	eqtr4d	$⊢ ((φ \land M \in ℤ) \land \neg m \in B) \to if (m \in A, (k \in A ⟼ C) (m), 1) = if (m \in B, ⦋ m / k ⦌ C, 1)$
79	73 78	pm2.61dan	$⊢ (φ \land M \in ℤ) \to if (m \in A, (k \in A ⟼ C) (m), 1) = if (m \in B, ⦋ m / k ⦌ C, 1)$
80	79	adantr	$⊢ ((φ \land M \in ℤ) \land m \in ℤ_{\geq M}) \to if (m \in A, (k \in A ⟼ C) (m), 1) = if (m \in B, ⦋ m / k ⦌ C, 1)$
81	44 80	eqtr4d	$⊢ ((φ \land M \in ℤ) \land m \in ℤ_{\geq M}) \to (k \in ℤ_{\geq M} ⟼ if (k \in B, C, 1)) (m) = if (m \in A, (k \in A ⟼ C) (m), 1)$
82	2	fmpttd	$⊢ φ \to (k \in A ⟼ C) : A ⟶ ℂ$
83	82	adantr	$⊢ (φ \land M \in ℤ) \to (k \in A ⟼ C) : A ⟶ ℂ$
84	83	ffvelcdmda	$⊢ ((φ \land M \in ℤ) \land m \in A) \to (k \in A ⟼ C) (m) \in ℂ$
85	6 7 8 10 81 84	zprod	$⊢ (φ \land M \in ℤ) \to \prod_{m \in A} (k \in A ⟼ C) (m) = ⇝ (seq M (\times (k \in ℤ_{\geq M} ⟼ if (k \in B, C, 1))))$
86	5	adantr	$⊢ (φ \land M \in ℤ) \to B \subseteq ℤ_{\geq M}$
87	43	ancoms	$⊢ (if (m \in B, ⦋ m / k ⦌ C, 1) \in ℂ \land m \in ℤ_{\geq M}) \to (k \in ℤ_{\geq M} ⟼ if (k \in B, C, 1)) (m) = if (m \in B, ⦋ m / k ⦌ C, 1)$
88	34 87	sylan	$⊢ ((φ \land M \in ℤ) \land m \in ℤ_{\geq M}) \to (k \in ℤ_{\geq M} ⟼ if (k \in B, C, 1)) (m) = if (m \in B, ⦋ m / k ⦌ C, 1)$
89		simpr	$⊢ ((φ \land M \in ℤ) \land m \in B) \to m \in B$
90		eqid	$⊢ (k \in B ⟼ C) = (k \in B ⟼ C)$
91	90	fvmpts	$⊢ (m \in B \land ⦋ m / k ⦌ C \in ℂ) \to (k \in B ⟼ C) (m) = ⦋ m / k ⦌ C$
92	89 50 91	syl2anc	$⊢ ((φ \land M \in ℤ) \land m \in B) \to (k \in B ⟼ C) (m) = ⦋ m / k ⦌ C$
93	92	ifeq1d	$⊢ ((φ \land M \in ℤ) \land m \in B) \to if (m \in B, (k \in B ⟼ C) (m), 1) = if (m \in B, ⦋ m / k ⦌ C, 1)$
94	93	adantlr	$⊢ (((φ \land M \in ℤ) \land m \in ℤ_{\geq M}) \land m \in B) \to if (m \in B, (k \in B ⟼ C) (m), 1) = if (m \in B, ⦋ m / k ⦌ C, 1)$
95		iffalse	$⊢ \neg m \in B \to if (m \in B, (k \in B ⟼ C) (m), 1) = 1$
96	95 30	eqtr4d	$⊢ \neg m \in B \to if (m \in B, (k \in B ⟼ C) (m), 1) = if (m \in B, ⦋ m / k ⦌ C, 1)$
97	96	adantl	$⊢ (((φ \land M \in ℤ) \land m \in ℤ_{\geq M}) \land \neg m \in B) \to if (m \in B, (k \in B ⟼ C) (m), 1) = if (m \in B, ⦋ m / k ⦌ C, 1)$
98	94 97	pm2.61dan	$⊢ ((φ \land M \in ℤ) \land m \in ℤ_{\geq M}) \to if (m \in B, (k \in B ⟼ C) (m), 1) = if (m \in B, ⦋ m / k ⦌ C, 1)$
99	88 98	eqtr4d	$⊢ ((φ \land M \in ℤ) \land m \in ℤ_{\geq M}) \to (k \in ℤ_{\geq M} ⟼ if (k \in B, C, 1)) (m) = if (m \in B, (k \in B ⟼ C) (m), 1)$
100	21	fmpttd	$⊢ φ \to (k \in B ⟼ C) : B ⟶ ℂ$
101	100	adantr	$⊢ (φ \land M \in ℤ) \to (k \in B ⟼ C) : B ⟶ ℂ$
102	101	ffvelcdmda	$⊢ ((φ \land M \in ℤ) \land m \in B) \to (k \in B ⟼ C) (m) \in ℂ$
103	6 7 8 86 99 102	zprod	$⊢ (φ \land M \in ℤ) \to \prod_{m \in B} (k \in B ⟼ C) (m) = ⇝ (seq M (\times (k \in ℤ_{\geq M} ⟼ if (k \in B, C, 1))))$
104	85 103	eqtr4d	$⊢ (φ \land M \in ℤ) \to \prod_{m \in A} (k \in A ⟼ C) (m) = \prod_{m \in B} (k \in B ⟼ C) (m)$
105		prodfc	$⊢ \prod_{m \in A} (k \in A ⟼ C) (m) = \prod_{k \in A} C$
106		prodfc	$⊢ \prod_{m \in B} (k \in B ⟼ C) (m) = \prod_{k \in B} C$
107	104 105 106	3eqtr3g	$⊢ (φ \land M \in ℤ) \to \prod_{k \in A} C = \prod_{k \in B} C$
108	1	adantr	$⊢ (φ \land \neg M \in ℤ) \to A \subseteq B$
109	5	adantr	$⊢ (φ \land \neg M \in ℤ) \to B \subseteq ℤ_{\geq M}$
110		uzf	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ$
111	110	fdmi	$⊢ dom ℤ_{\geq} = ℤ$
112	111	eleq2i	$⊢ M \in dom ℤ_{\geq} \leftrightarrow M \in ℤ$
113		ndmfv	$⊢ \neg M \in dom ℤ_{\geq} \to ℤ_{\geq M} = \emptyset$
114	112 113	sylnbir	$⊢ \neg M \in ℤ \to ℤ_{\geq M} = \emptyset$
115	114	adantl	$⊢ (φ \land \neg M \in ℤ) \to ℤ_{\geq M} = \emptyset$
116	109 115	sseqtrd	$⊢ (φ \land \neg M \in ℤ) \to B \subseteq \emptyset$
117	108 116	sstrd	$⊢ (φ \land \neg M \in ℤ) \to A \subseteq \emptyset$
118		ss0	$⊢ A \subseteq \emptyset \to A = \emptyset$
119	117 118	syl	$⊢ (φ \land \neg M \in ℤ) \to A = \emptyset$
120		ss0	$⊢ B \subseteq \emptyset \to B = \emptyset$
121	116 120	syl	$⊢ (φ \land \neg M \in ℤ) \to B = \emptyset$
122	119 121	eqtr4d	$⊢ (φ \land \neg M \in ℤ) \to A = B$
123	122	prodeq1d	$⊢ (φ \land \neg M \in ℤ) \to \prod_{k \in A} C = \prod_{k \in B} C$
124	107 123	pm2.61dan	$⊢ φ \to \prod_{k \in A} C = \prod_{k \in B} C$

Metamath Proof Explorer

Theorem prodss

Proof