fproddivf

Description: The quotient of two finite products. A version of fproddiv using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	fproddivf.kph	$⊢ Ⅎ k φ$
	fproddivf.a	$⊢ φ \to A \in Fin$
	fproddivf.b	$⊢ (φ \land k \in A) \to B \in ℂ$
	fproddivf.c	$⊢ (φ \land k \in A) \to C \in ℂ$
	fproddivf.ne0	$⊢ (φ \land k \in A) \to C \neq 0$
Assertion	fproddivf	$⊢ φ \to \prod_{k \in A} (\frac{B}{C}) = \frac{\prod_{k \in A} B}{\prod_{k \in A} C}$

Proof

Step	Hyp	Ref	Expression
1		fproddivf.kph	$⊢ Ⅎ k φ$
2		fproddivf.a	$⊢ φ \to A \in Fin$
3		fproddivf.b	$⊢ (φ \land k \in A) \to B \in ℂ$
4		fproddivf.c	$⊢ (φ \land k \in A) \to C \in ℂ$
5		fproddivf.ne0	$⊢ (φ \land k \in A) \to C \neq 0$
6		nfcv	$⊢ \underline{Ⅎ} j (\frac{B}{C})$
7		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ B$
8		nfcv	$⊢ \underline{Ⅎ} k \div$
9		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ C$
10	7 8 9	nfov	$⊢ \underline{Ⅎ} k (\frac{⦋ j / k ⦌ B}{⦋ j / k ⦌ C})$
11		csbeq1a	$⊢ k = j \to B = ⦋ j / k ⦌ B$
12		csbeq1a	$⊢ k = j \to C = ⦋ j / k ⦌ C$
13	11 12	oveq12d	$⊢ k = j \to \frac{B}{C} = \frac{⦋ j / k ⦌ B}{⦋ j / k ⦌ C}$
14	6 10 13	cbvprodi	$⊢ \prod_{k \in A} (\frac{B}{C}) = \prod_{j \in A} (\frac{⦋ j / k ⦌ B}{⦋ j / k ⦌ C})$
15	14	a1i	$⊢ φ \to \prod_{k \in A} (\frac{B}{C}) = \prod_{j \in A} (\frac{⦋ j / k ⦌ B}{⦋ j / k ⦌ C})$
16		nfvd	$⊢ φ \to Ⅎ k j \in A$
17	1 16	nfan1	$⊢ Ⅎ k (φ \land j \in A)$
18	7	nfel1	$⊢ Ⅎ k ⦋ j / k ⦌ B \in ℂ$
19	17 18	nfim	$⊢ Ⅎ k ((φ \land j \in A) \to ⦋ j / k ⦌ B \in ℂ)$
20		eleq1w	$⊢ k = j \to (k \in A \leftrightarrow j \in A)$
21	20	anbi2d	$⊢ k = j \to ((φ \land k \in A) \leftrightarrow (φ \land j \in A))$
22	11	eleq1d	$⊢ k = j \to (B \in ℂ \leftrightarrow ⦋ j / k ⦌ B \in ℂ)$
23	21 22	imbi12d	$⊢ k = j \to (((φ \land k \in A) \to B \in ℂ) \leftrightarrow ((φ \land j \in A) \to ⦋ j / k ⦌ B \in ℂ))$
24	19 23 3	chvarfv	$⊢ (φ \land j \in A) \to ⦋ j / k ⦌ B \in ℂ$
25	9	nfel1	$⊢ Ⅎ k ⦋ j / k ⦌ C \in ℂ$
26	17 25	nfim	$⊢ Ⅎ k ((φ \land j \in A) \to ⦋ j / k ⦌ C \in ℂ)$
27	12	eleq1d	$⊢ k = j \to (C \in ℂ \leftrightarrow ⦋ j / k ⦌ C \in ℂ)$
28	21 27	imbi12d	$⊢ k = j \to (((φ \land k \in A) \to C \in ℂ) \leftrightarrow ((φ \land j \in A) \to ⦋ j / k ⦌ C \in ℂ))$
29	26 28 4	chvarfv	$⊢ (φ \land j \in A) \to ⦋ j / k ⦌ C \in ℂ$
30		nfcv	$⊢ \underline{Ⅎ} k 0$
31	9 30	nfne	$⊢ Ⅎ k ⦋ j / k ⦌ C \neq 0$
32	17 31	nfim	$⊢ Ⅎ k ((φ \land j \in A) \to ⦋ j / k ⦌ C \neq 0)$
33	12	neeq1d	$⊢ k = j \to (C \neq 0 \leftrightarrow ⦋ j / k ⦌ C \neq 0)$
34	21 33	imbi12d	$⊢ k = j \to (((φ \land k \in A) \to C \neq 0) \leftrightarrow ((φ \land j \in A) \to ⦋ j / k ⦌ C \neq 0))$
35	32 34 5	chvarfv	$⊢ (φ \land j \in A) \to ⦋ j / k ⦌ C \neq 0$
36	2 24 29 35	fproddiv	$⊢ φ \to \prod_{j \in A} (\frac{⦋ j / k ⦌ B}{⦋ j / k ⦌ C}) = \frac{\prod_{j \in A} ⦋ j / k ⦌ B}{\prod_{j \in A} ⦋ j / k ⦌ C}$
37		nfcv	$⊢ \underline{Ⅎ} j B$
38	37 7 11	cbvprodi	$⊢ \prod_{k \in A} B = \prod_{j \in A} ⦋ j / k ⦌ B$
39	38	eqcomi	$⊢ \prod_{j \in A} ⦋ j / k ⦌ B = \prod_{k \in A} B$
40	39	a1i	$⊢ φ \to \prod_{j \in A} ⦋ j / k ⦌ B = \prod_{k \in A} B$
41		nfcv	$⊢ \underline{Ⅎ} j C$
42	12	equcoms	$⊢ j = k \to C = ⦋ j / k ⦌ C$
43	42	eqcomd	$⊢ j = k \to ⦋ j / k ⦌ C = C$
44	9 41 43	cbvprodi	$⊢ \prod_{j \in A} ⦋ j / k ⦌ C = \prod_{k \in A} C$
45	44	a1i	$⊢ φ \to \prod_{j \in A} ⦋ j / k ⦌ C = \prod_{k \in A} C$
46	40 45	oveq12d	$⊢ φ \to \frac{\prod_{j \in A} ⦋ j / k ⦌ B}{\prod_{j \in A} ⦋ j / k ⦌ C} = \frac{\prod_{k \in A} B}{\prod_{k \in A} C}$
47	15 36 46	3eqtrd	$⊢ φ \to \prod_{k \in A} (\frac{B}{C}) = \frac{\prod_{k \in A} B}{\prod_{k \in A} C}$

Metamath Proof Explorer

Theorem fproddivf

Proof