fprodmul

Description: The product of two finite products. (Contributed by Scott Fenton, 14-Dec-2017)

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

Proof

Step	Hyp	Ref	Expression
1		fprodmul.1	$⊢ φ \to A \in Fin$
2		fprodmul.2	$⊢ (φ \land k \in A) \to B \in ℂ$
3		fprodmul.3	$⊢ (φ \land k \in A) \to C \in ℂ$
4		1t1e1	$⊢ 1 \cdot 1 = 1$
5		prod0	$⊢ \prod_{k \in \emptyset} B = 1$
6		prod0	$⊢ \prod_{k \in \emptyset} C = 1$
7	5 6	oveq12i	$⊢ \prod_{k \in \emptyset} B \prod_{k \in \emptyset} C = 1 \cdot 1$
8		prod0	$⊢ \prod_{k \in \emptyset} B C = 1$
9	4 7 8	3eqtr4ri	$⊢ \prod_{k \in \emptyset} B C = \prod_{k \in \emptyset} B \prod_{k \in \emptyset} C$
10		prodeq1	$⊢ A = \emptyset \to \prod_{k \in A} B C = \prod_{k \in \emptyset} B C$
11		prodeq1	$⊢ A = \emptyset \to \prod_{k \in A} B = \prod_{k \in \emptyset} B$
12		prodeq1	$⊢ A = \emptyset \to \prod_{k \in A} C = \prod_{k \in \emptyset} C$
13	11 12	oveq12d	$⊢ A = \emptyset \to \prod_{k \in A} B \prod_{k \in A} C = \prod_{k \in \emptyset} B \prod_{k \in \emptyset} C$
14	9 10 13	3eqtr4a	$⊢ A = \emptyset \to \prod_{k \in A} B C = \prod_{k \in A} B \prod_{k \in A} C$
15	14	a1i	$⊢ φ \to (A = \emptyset \to \prod_{k \in A} B C = \prod_{k \in A} B \prod_{k \in A} C)$
16		simprl	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \|A\| \in ℕ$
17		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
18	16 17	eleqtrdi	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \|A\| \in ℤ_{\geq 1}$
19	2	fmpttd	$⊢ φ \to (k \in A ⟼ B) : A ⟶ ℂ$
20	19	adantr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (k \in A ⟼ B) : A ⟶ ℂ$
21		f1of	$⊢ f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to f : (1 \dots \|A\|) ⟶ A$
22	21	ad2antll	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to f : (1 \dots \|A\|) ⟶ A$
23		fco	$⊢ ((k \in A ⟼ B) : A ⟶ ℂ \land f : (1 \dots \|A\|) ⟶ A) \to ((k \in A ⟼ B) \circ f) : (1 \dots \|A\|) ⟶ ℂ$
24	20 22 23	syl2anc	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to ((k \in A ⟼ B) \circ f) : (1 \dots \|A\|) ⟶ ℂ$
25	24	ffvelrnda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ B) \circ f) (n) \in ℂ$
26	3	fmpttd	$⊢ φ \to (k \in A ⟼ C) : A ⟶ ℂ$
27	26	adantr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (k \in A ⟼ C) : A ⟶ ℂ$
28		fco	$⊢ ((k \in A ⟼ C) : A ⟶ ℂ \land f : (1 \dots \|A\|) ⟶ A) \to ((k \in A ⟼ C) \circ f) : (1 \dots \|A\|) ⟶ ℂ$
29	27 22 28	syl2anc	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to ((k \in A ⟼ C) \circ f) : (1 \dots \|A\|) ⟶ ℂ$
30	29	ffvelrnda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ C) \circ f) (n) \in ℂ$
31	22	ffvelrnda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to f (n) \in A$
32		simpr	$⊢ (φ \land k \in A) \to k \in A$
33	2 3	mulcld	$⊢ (φ \land k \in A) \to B C \in ℂ$
34		eqid	$⊢ (k \in A ⟼ B C) = (k \in A ⟼ B C)$
35	34	fvmpt2	$⊢ (k \in A \land B C \in ℂ) \to (k \in A ⟼ B C) (k) = B C$
36	32 33 35	syl2anc	$⊢ (φ \land k \in A) \to (k \in A ⟼ B C) (k) = B C$
37		eqid	$⊢ (k \in A ⟼ B) = (k \in A ⟼ B)$
38	37	fvmpt2	$⊢ (k \in A \land B \in ℂ) \to (k \in A ⟼ B) (k) = B$
39	32 2 38	syl2anc	$⊢ (φ \land k \in A) \to (k \in A ⟼ B) (k) = B$
40		eqid	$⊢ (k \in A ⟼ C) = (k \in A ⟼ C)$
41	40	fvmpt2	$⊢ (k \in A \land C \in ℂ) \to (k \in A ⟼ C) (k) = C$
42	32 3 41	syl2anc	$⊢ (φ \land k \in A) \to (k \in A ⟼ C) (k) = C$
43	39 42	oveq12d	$⊢ (φ \land k \in A) \to (k \in A ⟼ B) (k) (k \in A ⟼ C) (k) = B C$
44	36 43	eqtr4d	$⊢ (φ \land k \in A) \to (k \in A ⟼ B C) (k) = (k \in A ⟼ B) (k) (k \in A ⟼ C) (k)$
45	44	ralrimiva	$⊢ φ \to \forall k \in A (k \in A ⟼ B C) (k) = (k \in A ⟼ B) (k) (k \in A ⟼ C) (k)$
46	45	ad2antrr	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to \forall k \in A (k \in A ⟼ B C) (k) = (k \in A ⟼ B) (k) (k \in A ⟼ C) (k)$
47		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in A ⟼ B C) (f (n))$
48		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in A ⟼ B) (f (n))$
49		nfcv	$⊢ \underline{Ⅎ} k \times$
50		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in A ⟼ C) (f (n))$
51	48 49 50	nfov	$⊢ \underline{Ⅎ} k (k \in A ⟼ B) (f (n)) (k \in A ⟼ C) (f (n))$
52	47 51	nfeq	$⊢ Ⅎ k (k \in A ⟼ B C) (f (n)) = (k \in A ⟼ B) (f (n)) (k \in A ⟼ C) (f (n))$
53		fveq2	$⊢ k = f (n) \to (k \in A ⟼ B C) (k) = (k \in A ⟼ B C) (f (n))$
54		fveq2	$⊢ k = f (n) \to (k \in A ⟼ B) (k) = (k \in A ⟼ B) (f (n))$
55		fveq2	$⊢ k = f (n) \to (k \in A ⟼ C) (k) = (k \in A ⟼ C) (f (n))$
56	54 55	oveq12d	$⊢ k = f (n) \to (k \in A ⟼ B) (k) (k \in A ⟼ C) (k) = (k \in A ⟼ B) (f (n)) (k \in A ⟼ C) (f (n))$
57	53 56	eqeq12d	$⊢ k = f (n) \to ((k \in A ⟼ B C) (k) = (k \in A ⟼ B) (k) (k \in A ⟼ C) (k) \leftrightarrow (k \in A ⟼ B C) (f (n)) = (k \in A ⟼ B) (f (n)) (k \in A ⟼ C) (f (n)))$
58	52 57	rspc	$⊢ f (n) \in A \to (\forall k \in A (k \in A ⟼ B C) (k) = (k \in A ⟼ B) (k) (k \in A ⟼ C) (k) \to (k \in A ⟼ B C) (f (n)) = (k \in A ⟼ B) (f (n)) (k \in A ⟼ C) (f (n)))$
59	31 46 58	sylc	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to (k \in A ⟼ B C) (f (n)) = (k \in A ⟼ B) (f (n)) (k \in A ⟼ C) (f (n))$
60		fvco3	$⊢ (f : (1 \dots \|A\|) ⟶ A \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ B C) \circ f) (n) = (k \in A ⟼ B C) (f (n))$
61	22 60	sylan	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ B C) \circ f) (n) = (k \in A ⟼ B C) (f (n))$
62		fvco3	$⊢ (f : (1 \dots \|A\|) ⟶ A \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ B) \circ f) (n) = (k \in A ⟼ B) (f (n))$
63	22 62	sylan	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ B) \circ f) (n) = (k \in A ⟼ B) (f (n))$
64		fvco3	$⊢ (f : (1 \dots \|A\|) ⟶ A \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ C) \circ f) (n) = (k \in A ⟼ C) (f (n))$
65	22 64	sylan	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ C) \circ f) (n) = (k \in A ⟼ C) (f (n))$
66	63 65	oveq12d	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ B) \circ f) (n) ((k \in A ⟼ C) \circ f) (n) = (k \in A ⟼ B) (f (n)) (k \in A ⟼ C) (f (n))$
67	59 61 66	3eqtr4d	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ B C) \circ f) (n) = ((k \in A ⟼ B) \circ f) (n) ((k \in A ⟼ C) \circ f) (n)$
68	18 25 30 67	prodfmul	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to seq 1 (\times ((k \in A ⟼ B C) \circ f)) (\|A\|) = seq 1 (\times ((k \in A ⟼ B) \circ f)) (\|A\|) seq 1 (\times ((k \in A ⟼ C) \circ f)) (\|A\|)$
69		fveq2	$⊢ m = f (n) \to (k \in A ⟼ B C) (m) = (k \in A ⟼ B C) (f (n))$
70		simprr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
71	33	fmpttd	$⊢ φ \to (k \in A ⟼ B C) : A ⟶ ℂ$
72	71	adantr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (k \in A ⟼ B C) : A ⟶ ℂ$
73	72	ffvelrnda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land m \in A) \to (k \in A ⟼ B C) (m) \in ℂ$
74	69 16 70 73 61	fprod	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \prod_{m \in A} (k \in A ⟼ B C) (m) = seq 1 (\times ((k \in A ⟼ B C) \circ f)) (\|A\|)$
75		fveq2	$⊢ m = f (n) \to (k \in A ⟼ B) (m) = (k \in A ⟼ B) (f (n))$
76	20	ffvelrnda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land m \in A) \to (k \in A ⟼ B) (m) \in ℂ$
77	75 16 70 76 63	fprod	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \prod_{m \in A} (k \in A ⟼ B) (m) = seq 1 (\times ((k \in A ⟼ B) \circ f)) (\|A\|)$
78		fveq2	$⊢ m = f (n) \to (k \in A ⟼ C) (m) = (k \in A ⟼ C) (f (n))$
79	27	ffvelrnda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land m \in A) \to (k \in A ⟼ C) (m) \in ℂ$
80	78 16 70 79 65	fprod	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \prod_{m \in A} (k \in A ⟼ C) (m) = seq 1 (\times ((k \in A ⟼ C) \circ f)) (\|A\|)$
81	77 80	oveq12d	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \prod_{m \in A} (k \in A ⟼ B) (m) \prod_{m \in A} (k \in A ⟼ C) (m) = seq 1 (\times ((k \in A ⟼ B) \circ f)) (\|A\|) seq 1 (\times ((k \in A ⟼ C) \circ f)) (\|A\|)$
82	68 74 81	3eqtr4d	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \prod_{m \in A} (k \in A ⟼ B C) (m) = \prod_{m \in A} (k \in A ⟼ B) (m) \prod_{m \in A} (k \in A ⟼ C) (m)$
83		prodfc	$⊢ \prod_{m \in A} (k \in A ⟼ B C) (m) = \prod_{k \in A} B C$
84		prodfc	$⊢ \prod_{m \in A} (k \in A ⟼ B) (m) = \prod_{k \in A} B$
85		prodfc	$⊢ \prod_{m \in A} (k \in A ⟼ C) (m) = \prod_{k \in A} C$
86	84 85	oveq12i	$⊢ \prod_{m \in A} (k \in A ⟼ B) (m) \prod_{m \in A} (k \in A ⟼ C) (m) = \prod_{k \in A} B \prod_{k \in A} C$
87	82 83 86	3eqtr3g	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \prod_{k \in A} B C = \prod_{k \in A} B \prod_{k \in A} C$
88	87	expr	$⊢ (φ \land \|A\| \in ℕ) \to (f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to \prod_{k \in A} B C = \prod_{k \in A} B \prod_{k \in A} C)$
89	88	exlimdv	$⊢ (φ \land \|A\| \in ℕ) \to (\exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to \prod_{k \in A} B C = \prod_{k \in A} B \prod_{k \in A} C)$
90	89	expimpd	$⊢ φ \to ((\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to \prod_{k \in A} B C = \prod_{k \in A} B \prod_{k \in A} C)$
91		fz1f1o	$⊢ A \in Fin \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
92	1 91	syl	$⊢ φ \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
93	15 90 92	mpjaod	$⊢ φ \to \prod_{k \in A} B C = \prod_{k \in A} B \prod_{k \in A} C$

Metamath Proof Explorer

Theorem fprodmul

Proof