fprodss

Description: Change the index set to a subset in a finite product. (Contributed by Scott Fenton, 16-Dec-2017)

	Ref	Expression
Hypotheses	fprodss.1	$⊢ φ \to A \subseteq B$
	fprodss.2	$⊢ (φ \land k \in A) \to C \in ℂ$
	fprodss.3	$⊢ (φ \land k \in (B ∖ A)) \to C = 1$
	fprodss.4	$⊢ φ \to B \in Fin$
Assertion	fprodss	$⊢ φ \to \prod_{k \in A} C = \prod_{k \in B} C$

Proof

Step	Hyp	Ref	Expression
1		fprodss.1	$⊢ φ \to A \subseteq B$
2		fprodss.2	$⊢ (φ \land k \in A) \to C \in ℂ$
3		fprodss.3	$⊢ (φ \land k \in (B ∖ A)) \to C = 1$
4		fprodss.4	$⊢ φ \to B \in Fin$
5		sseq2	$⊢ B = \emptyset \to (A \subseteq B \leftrightarrow A \subseteq \emptyset)$
6		ss0	$⊢ A \subseteq \emptyset \to A = \emptyset$
7	5 6	syl6bi	$⊢ B = \emptyset \to (A \subseteq B \to A = \emptyset)$
8		prodeq1	$⊢ A = \emptyset \to \prod_{k \in A} C = \prod_{k \in \emptyset} C$
9		prodeq1	$⊢ B = \emptyset \to \prod_{k \in B} C = \prod_{k \in \emptyset} C$
10	9	eqcomd	$⊢ B = \emptyset \to \prod_{k \in \emptyset} C = \prod_{k \in B} C$
11	8 10	sylan9eq	$⊢ (A = \emptyset \land B = \emptyset) \to \prod_{k \in A} C = \prod_{k \in B} C$
12	11	expcom	$⊢ B = \emptyset \to (A = \emptyset \to \prod_{k \in A} C = \prod_{k \in B} C)$
13	7 12	syld	$⊢ B = \emptyset \to (A \subseteq B \to \prod_{k \in A} C = \prod_{k \in B} C)$
14	1 13	syl5com	$⊢ φ \to (B = \emptyset \to \prod_{k \in A} C = \prod_{k \in B} C)$
15		cnvimass	$⊢ f^{-1} [A] \subseteq dom f$
16		simprr	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B$
17		f1of	$⊢ f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B \to f : (1 \dots \|B\|) ⟶ B$
18	16 17	syl	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to f : (1 \dots \|B\|) ⟶ B$
19	15 18	fssdm	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to f^{-1} [A] \subseteq (1 \dots \|B\|)$
20		f1ofn	$⊢ f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B \to f Fn (1 \dots \|B\|)$
21		elpreima	$⊢ f Fn (1 \dots \|B\|) \to (n \in f^{-1} [A] \leftrightarrow (n \in (1 \dots \|B\|) \land f (n) \in A))$
22	16 20 21	3syl	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to (n \in f^{-1} [A] \leftrightarrow (n \in (1 \dots \|B\|) \land f (n) \in A))$
23	18	ffvelrnda	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in (1 \dots \|B\|)) \to f (n) \in B$
24	23	ex	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to (n \in (1 \dots \|B\|) \to f (n) \in B)$
25	24	adantrd	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to ((n \in (1 \dots \|B\|) \land f (n) \in A) \to f (n) \in B)$
26	22 25	sylbid	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to (n \in f^{-1} [A] \to f (n) \in B)$
27	26	imp	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in f^{-1} [A]) \to f (n) \in B$
28	2	ex	$⊢ φ \to (k \in A \to C \in ℂ)$
29	28	adantr	$⊢ (φ \land k \in B) \to (k \in A \to C \in ℂ)$
30		eldif	$⊢ k \in (B ∖ A) \leftrightarrow (k \in B \land \neg k \in A)$
31		ax-1cn	$⊢ 1 \in ℂ$
32	3 31	eqeltrdi	$⊢ (φ \land k \in (B ∖ A)) \to C \in ℂ$
33	30 32	sylan2br	$⊢ (φ \land (k \in B \land \neg k \in A)) \to C \in ℂ$
34	33	expr	$⊢ (φ \land k \in B) \to (\neg k \in A \to C \in ℂ)$
35	29 34	pm2.61d	$⊢ (φ \land k \in B) \to C \in ℂ$
36	35	adantlr	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land k \in B) \to C \in ℂ$
37	36	fmpttd	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to (k \in B ⟼ C) : B ⟶ ℂ$
38	37	ffvelrnda	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land f (n) \in B) \to (k \in B ⟼ C) (f (n)) \in ℂ$
39	27 38	syldan	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in f^{-1} [A]) \to (k \in B ⟼ C) (f (n)) \in ℂ$
40		eqid	$⊢ ℤ_{\geq 1} = ℤ_{\geq 1}$
41		simprl	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to \|B\| \in ℕ$
42		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
43	41 42	eleqtrdi	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to \|B\| \in ℤ_{\geq 1}$
44		ssidd	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to (1 \dots \|B\|) \subseteq (1 \dots \|B\|)$
45	40 43 44	fprodntriv	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to \exists m \in ℤ_{\geq 1} \exists y (y \neq 0 \land seq m (\times (n \in ℤ_{\geq 1} ⟼ if (n \in (1 \dots \|B\|), (k \in B ⟼ C) (f (n)), 1))) ⇝ y)$
46		eldifi	$⊢ n \in ((1 \dots \|B\|) ∖ f^{-1} [A]) \to n \in (1 \dots \|B\|)$
47	46 23	sylan2	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in ((1 \dots \|B\|) ∖ f^{-1} [A])) \to f (n) \in B$
48		eldifn	$⊢ n \in ((1 \dots \|B\|) ∖ f^{-1} [A]) \to \neg n \in f^{-1} [A]$
49	48	adantl	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in ((1 \dots \|B\|) ∖ f^{-1} [A])) \to \neg n \in f^{-1} [A]$
50	46	adantl	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in ((1 \dots \|B\|) ∖ f^{-1} [A])) \to n \in (1 \dots \|B\|)$
51	22	adantr	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in ((1 \dots \|B\|) ∖ f^{-1} [A])) \to (n \in f^{-1} [A] \leftrightarrow (n \in (1 \dots \|B\|) \land f (n) \in A))$
52	50 51	mpbirand	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in ((1 \dots \|B\|) ∖ f^{-1} [A])) \to (n \in f^{-1} [A] \leftrightarrow f (n) \in A)$
53	49 52	mtbid	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in ((1 \dots \|B\|) ∖ f^{-1} [A])) \to \neg f (n) \in A$
54	47 53	eldifd	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in ((1 \dots \|B\|) ∖ f^{-1} [A])) \to f (n) \in (B ∖ A)$
55		difss	$⊢ B ∖ A \subseteq B$
56		resmpt	$⊢ B ∖ A \subseteq B \to {(k \in B ⟼ C) ↾}_{(B ∖ A)} = (k \in (B ∖ A) ⟼ C)$
57	55 56	ax-mp	$⊢ {(k \in B ⟼ C) ↾}_{(B ∖ A)} = (k \in (B ∖ A) ⟼ C)$
58	57	fveq1i	$⊢ ({(k \in B ⟼ C) ↾}_{(B ∖ A)}) (f (n)) = (k \in (B ∖ A) ⟼ C) (f (n))$
59		fvres	$⊢ f (n) \in (B ∖ A) \to ({(k \in B ⟼ C) ↾}_{(B ∖ A)}) (f (n)) = (k \in B ⟼ C) (f (n))$
60	58 59	syl5eqr	$⊢ f (n) \in (B ∖ A) \to (k \in (B ∖ A) ⟼ C) (f (n)) = (k \in B ⟼ C) (f (n))$
61	54 60	syl	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in ((1 \dots \|B\|) ∖ f^{-1} [A])) \to (k \in (B ∖ A) ⟼ C) (f (n)) = (k \in B ⟼ C) (f (n))$
62		1ex	$⊢ 1 \in V$
63	62	elsn2	$⊢ C \in \{1\} \leftrightarrow C = 1$
64	3 63	sylibr	$⊢ (φ \land k \in (B ∖ A)) \to C \in \{1\}$
65	64	fmpttd	$⊢ φ \to (k \in (B ∖ A) ⟼ C) : B ∖ A ⟶ \{1\}$
66	65	ad2antrr	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in ((1 \dots \|B\|) ∖ f^{-1} [A])) \to (k \in (B ∖ A) ⟼ C) : B ∖ A ⟶ \{1\}$
67	66 54	ffvelrnd	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in ((1 \dots \|B\|) ∖ f^{-1} [A])) \to (k \in (B ∖ A) ⟼ C) (f (n)) \in \{1\}$
68		elsni	$⊢ (k \in (B ∖ A) ⟼ C) (f (n)) \in \{1\} \to (k \in (B ∖ A) ⟼ C) (f (n)) = 1$
69	67 68	syl	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in ((1 \dots \|B\|) ∖ f^{-1} [A])) \to (k \in (B ∖ A) ⟼ C) (f (n)) = 1$
70	61 69	eqtr3d	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in ((1 \dots \|B\|) ∖ f^{-1} [A])) \to (k \in B ⟼ C) (f (n)) = 1$
71		fzssuz	$⊢ (1 \dots \|B\|) \subseteq ℤ_{\geq 1}$
72	71	a1i	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to (1 \dots \|B\|) \subseteq ℤ_{\geq 1}$
73	19 39 45 70 72	prodss	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to \prod_{n \in f^{-1} [A]} (k \in B ⟼ C) (f (n)) = \prod_{n = 1}^{\|B\|} (k \in B ⟼ C) (f (n))$
74	1	adantr	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to A \subseteq B$
75	74	resmptd	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to {(k \in B ⟼ C) ↾}_{A} = (k \in A ⟼ C)$
76	75	fveq1d	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to ({(k \in B ⟼ C) ↾}_{A}) (m) = (k \in A ⟼ C) (m)$
77		fvres	$⊢ m \in A \to ({(k \in B ⟼ C) ↾}_{A}) (m) = (k \in B ⟼ C) (m)$
78	76 77	sylan9req	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land m \in A) \to (k \in A ⟼ C) (m) = (k \in B ⟼ C) (m)$
79	78	prodeq2dv	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to \prod_{m \in A} (k \in A ⟼ C) (m) = \prod_{m \in A} (k \in B ⟼ C) (m)$
80		fveq2	$⊢ m = f (n) \to (k \in B ⟼ C) (m) = (k \in B ⟼ C) (f (n))$
81		fzfid	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to (1 \dots \|B\|) \in Fin$
82	81 18	fisuppfi	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to f^{-1} [A] \in Fin$
83		f1of1	$⊢ f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B \to f : (1 \dots \|B\|) \underset{1-1}{⟶} B$
84	16 83	syl	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to f : (1 \dots \|B\|) \underset{1-1}{⟶} B$
85		f1ores	$⊢ (f : (1 \dots \|B\|) \underset{1-1}{⟶} B \land f^{-1} [A] \subseteq (1 \dots \|B\|)) \to ({f ↾}_{f^{-1} [A]}) : f^{-1} [A] \underset{1-1 onto}{⟶} f [f^{-1} [A]]$
86	84 19 85	syl2anc	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to ({f ↾}_{f^{-1} [A]}) : f^{-1} [A] \underset{1-1 onto}{⟶} f [f^{-1} [A]]$
87		f1ofo	$⊢ f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B \to f : (1 \dots \|B\|) \underset{onto}{⟶} B$
88	16 87	syl	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to f : (1 \dots \|B\|) \underset{onto}{⟶} B$
89		foimacnv	$⊢ (f : (1 \dots \|B\|) \underset{onto}{⟶} B \land A \subseteq B) \to f [f^{-1} [A]] = A$
90	88 74 89	syl2anc	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to f [f^{-1} [A]] = A$
91	90	f1oeq3d	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to (({f ↾}_{f^{-1} [A]}) : f^{-1} [A] \underset{1-1 onto}{⟶} f [f^{-1} [A]] \leftrightarrow ({f ↾}_{f^{-1} [A]}) : f^{-1} [A] \underset{1-1 onto}{⟶} A)$
92	86 91	mpbid	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to ({f ↾}_{f^{-1} [A]}) : f^{-1} [A] \underset{1-1 onto}{⟶} A$
93		fvres	$⊢ n \in f^{-1} [A] \to ({f ↾}_{f^{-1} [A]}) (n) = f (n)$
94	93	adantl	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in f^{-1} [A]) \to ({f ↾}_{f^{-1} [A]}) (n) = f (n)$
95	74	sselda	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land m \in A) \to m \in B$
96	37	ffvelrnda	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land m \in B) \to (k \in B ⟼ C) (m) \in ℂ$
97	95 96	syldan	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land m \in A) \to (k \in B ⟼ C) (m) \in ℂ$
98	80 82 92 94 97	fprodf1o	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to \prod_{m \in A} (k \in B ⟼ C) (m) = \prod_{n \in f^{-1} [A]} (k \in B ⟼ C) (f (n))$
99	79 98	eqtrd	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to \prod_{m \in A} (k \in A ⟼ C) (m) = \prod_{n \in f^{-1} [A]} (k \in B ⟼ C) (f (n))$
100		eqidd	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in (1 \dots \|B\|)) \to f (n) = f (n)$
101	80 81 16 100 96	fprodf1o	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to \prod_{m \in B} (k \in B ⟼ C) (m) = \prod_{n = 1}^{\|B\|} (k \in B ⟼ C) (f (n))$
102	73 99 101	3eqtr4d	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to \prod_{m \in A} (k \in A ⟼ C) (m) = \prod_{m \in B} (k \in B ⟼ C) (m)$
103		prodfc	$⊢ \prod_{m \in A} (k \in A ⟼ C) (m) = \prod_{k \in A} C$
104		prodfc	$⊢ \prod_{m \in B} (k \in B ⟼ C) (m) = \prod_{k \in B} C$
105	102 103 104	3eqtr3g	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to \prod_{k \in A} C = \prod_{k \in B} C$
106	105	expr	$⊢ (φ \land \|B\| \in ℕ) \to (f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B \to \prod_{k \in A} C = \prod_{k \in B} C)$
107	106	exlimdv	$⊢ (φ \land \|B\| \in ℕ) \to (\exists f f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B \to \prod_{k \in A} C = \prod_{k \in B} C)$
108	107	expimpd	$⊢ φ \to ((\|B\| \in ℕ \land \exists f f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B) \to \prod_{k \in A} C = \prod_{k \in B} C)$
109		fz1f1o	$⊢ B \in Fin \to (B = \emptyset \lor (\|B\| \in ℕ \land \exists f f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B))$
110	4 109	syl	$⊢ φ \to (B = \emptyset \lor (\|B\| \in ℕ \land \exists f f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B))$
111	14 108 110	mpjaod	$⊢ φ \to \prod_{k \in A} C = \prod_{k \in B} C$

Metamath Proof Explorer

Theorem fprodss

Proof