fprodf1o

Description: Re-index a finite product using a bijection. (Contributed by Scott Fenton, 7-Dec-2017)

	Ref	Expression
Hypotheses	fprodf1o.1	$⊢ k = G \to B = D$
	fprodf1o.2	$⊢ φ \to C \in Fin$
	fprodf1o.3	$⊢ φ \to F : C \underset{1-1 onto}{⟶} A$
	fprodf1o.4	$⊢ (φ \land n \in C) \to F (n) = G$
	fprodf1o.5	$⊢ (φ \land k \in A) \to B \in ℂ$
Assertion	fprodf1o	$⊢ φ \to \prod_{k \in A} B = \prod_{n \in C} D$

Proof

Step	Hyp	Ref	Expression
1		fprodf1o.1	$⊢ k = G \to B = D$
2		fprodf1o.2	$⊢ φ \to C \in Fin$
3		fprodf1o.3	$⊢ φ \to F : C \underset{1-1 onto}{⟶} A$
4		fprodf1o.4	$⊢ (φ \land n \in C) \to F (n) = G$
5		fprodf1o.5	$⊢ (φ \land k \in A) \to B \in ℂ$
6		prod0	$⊢ \prod_{k \in \emptyset} B = 1$
7	3	adantr	$⊢ (φ \land C = \emptyset) \to F : C \underset{1-1 onto}{⟶} A$
8		f1oeq2	$⊢ C = \emptyset \to (F : C \underset{1-1 onto}{⟶} A \leftrightarrow F : \emptyset \underset{1-1 onto}{⟶} A)$
9	8	adantl	$⊢ (φ \land C = \emptyset) \to (F : C \underset{1-1 onto}{⟶} A \leftrightarrow F : \emptyset \underset{1-1 onto}{⟶} A)$
10	7 9	mpbid	$⊢ (φ \land C = \emptyset) \to F : \emptyset \underset{1-1 onto}{⟶} A$
11		f1ofo	$⊢ F : \emptyset \underset{1-1 onto}{⟶} A \to F : \emptyset \underset{onto}{⟶} A$
12	10 11	syl	$⊢ (φ \land C = \emptyset) \to F : \emptyset \underset{onto}{⟶} A$
13		fo00	$⊢ F : \emptyset \underset{onto}{⟶} A \leftrightarrow (F = \emptyset \land A = \emptyset)$
14	13	simprbi	$⊢ F : \emptyset \underset{onto}{⟶} A \to A = \emptyset$
15	12 14	syl	$⊢ (φ \land C = \emptyset) \to A = \emptyset$
16	15	prodeq1d	$⊢ (φ \land C = \emptyset) \to \prod_{k \in A} B = \prod_{k \in \emptyset} B$
17		prodeq1	$⊢ C = \emptyset \to \prod_{n \in C} D = \prod_{n \in \emptyset} D$
18		prod0	$⊢ \prod_{n \in \emptyset} D = 1$
19	17 18	eqtrdi	$⊢ C = \emptyset \to \prod_{n \in C} D = 1$
20	19	adantl	$⊢ (φ \land C = \emptyset) \to \prod_{n \in C} D = 1$
21	6 16 20	3eqtr4a	$⊢ (φ \land C = \emptyset) \to \prod_{k \in A} B = \prod_{n \in C} D$
22	21	ex	$⊢ φ \to (C = \emptyset \to \prod_{k \in A} B = \prod_{n \in C} D)$
23		2fveq3	$⊢ m = f (n) \to (k \in A ⟼ B) (F (m)) = (k \in A ⟼ B) (F (f (n)))$
24		simprl	$⊢ (φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \to \|C\| \in ℕ$
25		simprr	$⊢ (φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \to f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C$
26		f1of	$⊢ F : C \underset{1-1 onto}{⟶} A \to F : C ⟶ A$
27	3 26	syl	$⊢ φ \to F : C ⟶ A$
28	27	ffvelrnda	$⊢ (φ \land m \in C) \to F (m) \in A$
29	5	fmpttd	$⊢ φ \to (k \in A ⟼ B) : A ⟶ ℂ$
30	29	ffvelrnda	$⊢ (φ \land F (m) \in A) \to (k \in A ⟼ B) (F (m)) \in ℂ$
31	28 30	syldan	$⊢ (φ \land m \in C) \to (k \in A ⟼ B) (F (m)) \in ℂ$
32	31	adantlr	$⊢ ((φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \land m \in C) \to (k \in A ⟼ B) (F (m)) \in ℂ$
33		simpr	$⊢ (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C) \to f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C$
34		f1oco	$⊢ (F : C \underset{1-1 onto}{⟶} A \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C) \to (F \circ f) : (1 \dots \|C\|) \underset{1-1 onto}{⟶} A$
35	3 33 34	syl2an	$⊢ (φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \to (F \circ f) : (1 \dots \|C\|) \underset{1-1 onto}{⟶} A$
36		f1of	$⊢ (F \circ f) : (1 \dots \|C\|) \underset{1-1 onto}{⟶} A \to (F \circ f) : (1 \dots \|C\|) ⟶ A$
37	35 36	syl	$⊢ (φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \to (F \circ f) : (1 \dots \|C\|) ⟶ A$
38		fvco3	$⊢ ((F \circ f) : (1 \dots \|C\|) ⟶ A \land n \in (1 \dots \|C\|)) \to ((k \in A ⟼ B) \circ (F \circ f)) (n) = (k \in A ⟼ B) ((F \circ f) (n))$
39	37 38	sylan	$⊢ ((φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \land n \in (1 \dots \|C\|)) \to ((k \in A ⟼ B) \circ (F \circ f)) (n) = (k \in A ⟼ B) ((F \circ f) (n))$
40		f1of	$⊢ f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C \to f : (1 \dots \|C\|) ⟶ C$
41	40	adantl	$⊢ (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C) \to f : (1 \dots \|C\|) ⟶ C$
42	41	adantl	$⊢ (φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \to f : (1 \dots \|C\|) ⟶ C$
43		fvco3	$⊢ (f : (1 \dots \|C\|) ⟶ C \land n \in (1 \dots \|C\|)) \to (F \circ f) (n) = F (f (n))$
44	42 43	sylan	$⊢ ((φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \land n \in (1 \dots \|C\|)) \to (F \circ f) (n) = F (f (n))$
45	44	fveq2d	$⊢ ((φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \land n \in (1 \dots \|C\|)) \to (k \in A ⟼ B) ((F \circ f) (n)) = (k \in A ⟼ B) (F (f (n)))$
46	39 45	eqtrd	$⊢ ((φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \land n \in (1 \dots \|C\|)) \to ((k \in A ⟼ B) \circ (F \circ f)) (n) = (k \in A ⟼ B) (F (f (n)))$
47	23 24 25 32 46	fprod	$⊢ (φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \to \prod_{m \in C} (k \in A ⟼ B) (F (m)) = seq 1 (\times ((k \in A ⟼ B) \circ (F \circ f))) (\|C\|)$
48	27	ffvelrnda	$⊢ (φ \land n \in C) \to F (n) \in A$
49	4 48	eqeltrrd	$⊢ (φ \land n \in C) \to G \in A$
50		eqid	$⊢ (k \in A ⟼ B) = (k \in A ⟼ B)$
51	1 50	fvmpti	$⊢ G \in A \to (k \in A ⟼ B) (G) = I (D)$
52	49 51	syl	$⊢ (φ \land n \in C) \to (k \in A ⟼ B) (G) = I (D)$
53	4	fveq2d	$⊢ (φ \land n \in C) \to (k \in A ⟼ B) (F (n)) = (k \in A ⟼ B) (G)$
54		eqid	$⊢ (n \in C ⟼ D) = (n \in C ⟼ D)$
55	54	fvmpt2i	$⊢ n \in C \to (n \in C ⟼ D) (n) = I (D)$
56	55	adantl	$⊢ (φ \land n \in C) \to (n \in C ⟼ D) (n) = I (D)$
57	52 53 56	3eqtr4rd	$⊢ (φ \land n \in C) \to (n \in C ⟼ D) (n) = (k \in A ⟼ B) (F (n))$
58	57	ralrimiva	$⊢ φ \to \forall n \in C (n \in C ⟼ D) (n) = (k \in A ⟼ B) (F (n))$
59		nffvmpt1	$⊢ \underline{Ⅎ} n (n \in C ⟼ D) (m)$
60	59	nfeq1	$⊢ Ⅎ n (n \in C ⟼ D) (m) = (k \in A ⟼ B) (F (m))$
61		fveq2	$⊢ n = m \to (n \in C ⟼ D) (n) = (n \in C ⟼ D) (m)$
62		2fveq3	$⊢ n = m \to (k \in A ⟼ B) (F (n)) = (k \in A ⟼ B) (F (m))$
63	61 62	eqeq12d	$⊢ n = m \to ((n \in C ⟼ D) (n) = (k \in A ⟼ B) (F (n)) \leftrightarrow (n \in C ⟼ D) (m) = (k \in A ⟼ B) (F (m)))$
64	60 63	rspc	$⊢ m \in C \to (\forall n \in C (n \in C ⟼ D) (n) = (k \in A ⟼ B) (F (n)) \to (n \in C ⟼ D) (m) = (k \in A ⟼ B) (F (m)))$
65	58 64	mpan9	$⊢ (φ \land m \in C) \to (n \in C ⟼ D) (m) = (k \in A ⟼ B) (F (m))$
66	65	adantlr	$⊢ ((φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \land m \in C) \to (n \in C ⟼ D) (m) = (k \in A ⟼ B) (F (m))$
67	66	prodeq2dv	$⊢ (φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \to \prod_{m \in C} (n \in C ⟼ D) (m) = \prod_{m \in C} (k \in A ⟼ B) (F (m))$
68		fveq2	$⊢ m = (F \circ f) (n) \to (k \in A ⟼ B) (m) = (k \in A ⟼ B) ((F \circ f) (n))$
69	29	adantr	$⊢ (φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \to (k \in A ⟼ B) : A ⟶ ℂ$
70	69	ffvelrnda	$⊢ ((φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \land m \in A) \to (k \in A ⟼ B) (m) \in ℂ$
71	68 24 35 70 39	fprod	$⊢ (φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \to \prod_{m \in A} (k \in A ⟼ B) (m) = seq 1 (\times ((k \in A ⟼ B) \circ (F \circ f))) (\|C\|)$
72	47 67 71	3eqtr4rd	$⊢ (φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \to \prod_{m \in A} (k \in A ⟼ B) (m) = \prod_{m \in C} (n \in C ⟼ D) (m)$
73		prodfc	$⊢ \prod_{m \in A} (k \in A ⟼ B) (m) = \prod_{k \in A} B$
74		prodfc	$⊢ \prod_{m \in C} (n \in C ⟼ D) (m) = \prod_{n \in C} D$
75	72 73 74	3eqtr3g	$⊢ (φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \to \prod_{k \in A} B = \prod_{n \in C} D$
76	75	expr	$⊢ (φ \land \|C\| \in ℕ) \to (f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C \to \prod_{k \in A} B = \prod_{n \in C} D)$
77	76	exlimdv	$⊢ (φ \land \|C\| \in ℕ) \to (\exists f f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C \to \prod_{k \in A} B = \prod_{n \in C} D)$
78	77	expimpd	$⊢ φ \to ((\|C\| \in ℕ \land \exists f f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C) \to \prod_{k \in A} B = \prod_{n \in C} D)$
79		fz1f1o	$⊢ C \in Fin \to (C = \emptyset \lor (\|C\| \in ℕ \land \exists f f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C))$
80	2 79	syl	$⊢ φ \to (C = \emptyset \lor (\|C\| \in ℕ \land \exists f f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C))$
81	22 78 80	mpjaod	$⊢ φ \to \prod_{k \in A} B = \prod_{n \in C} D$

Metamath Proof Explorer

Theorem fprodf1o

Proof