Theorem 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	⊢ Ⅎ 𝑘 𝜑
	fproddivf.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fproddivf.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
	fproddivf.c	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
	fproddivf.ne0	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ≠ 0 )
Assertion	fproddivf	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 ( 𝐵 / 𝐶 ) = ( ∏ 𝑘 ∈ 𝐴 𝐵 / ∏ 𝑘 ∈ 𝐴 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		fproddivf.kph	⊢ Ⅎ 𝑘 𝜑
2		fproddivf.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
3		fproddivf.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
4		fproddivf.c	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
5		fproddivf.ne0	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ≠ 0 )
6		nfcv	⊢ Ⅎ 𝑗 ( 𝐵 / 𝐶 )
7		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
8		nfcv	⊢ Ⅎ 𝑘 /
9		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐶
10	7 8 9	nfov	⊢ Ⅎ 𝑘 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 / ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
11		csbeq1a	⊢ ( 𝑘 = 𝑗 → 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
12		csbeq1a	⊢ ( 𝑘 = 𝑗 → 𝐶 = ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
13	11 12	oveq12d	⊢ ( 𝑘 = 𝑗 → ( 𝐵 / 𝐶 ) = ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 / ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) )
14	6 10 13	cbvprodi	⊢ ∏ 𝑘 ∈ 𝐴 ( 𝐵 / 𝐶 ) = ∏ 𝑗 ∈ 𝐴 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 / ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
15	14	a1i	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 ( 𝐵 / 𝐶 ) = ∏ 𝑗 ∈ 𝐴 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 / ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) )
16		nfvd	⊢ ( 𝜑 → Ⅎ 𝑘 𝑗 ∈ 𝐴 )
17	1 16	nfan1	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝐴 )
18	7	nfel1	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ
19	17 18	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ )
20		eleq1w	⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴 ) )
21	20	anbi2d	⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ) )
22	11	eleq1d	⊢ ( 𝑘 = 𝑗 → ( 𝐵 ∈ ℂ ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
23	21 22	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ ) ) )
24	19 23 3	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ )
25	9	nfel1	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ℂ
26	17 25	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ℂ )
27	12	eleq1d	⊢ ( 𝑘 = 𝑗 → ( 𝐶 ∈ ℂ ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ℂ ) )
28	21 27	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ℂ ) ) )
29	26 28 4	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ℂ )
30		nfcv	⊢ Ⅎ 𝑘 0
31	9 30	nfne	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ≠ 0
32	17 31	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ≠ 0 )
33	12	neeq1d	⊢ ( 𝑘 = 𝑗 → ( 𝐶 ≠ 0 ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ≠ 0 ) )
34	21 33	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ≠ 0 ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ≠ 0 ) ) )
35	32 34 5	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ≠ 0 )
36	2 24 29 35	fproddiv	⊢ ( 𝜑 → ∏ 𝑗 ∈ 𝐴 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 / ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) = ( ∏ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 / ∏ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) )
37		nfcv	⊢ Ⅎ 𝑗 𝐵
38	37 7 11	cbvprodi	⊢ ∏ 𝑘 ∈ 𝐴 𝐵 = ∏ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
39	38	eqcomi	⊢ ∏ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = ∏ 𝑘 ∈ 𝐴 𝐵
40	39	a1i	⊢ ( 𝜑 → ∏ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = ∏ 𝑘 ∈ 𝐴 𝐵 )
41		nfcv	⊢ Ⅎ 𝑗 𝐶
42	12	equcoms	⊢ ( 𝑗 = 𝑘 → 𝐶 = ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
43	42	eqcomd	⊢ ( 𝑗 = 𝑘 → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 = 𝐶 )
44	9 41 43	cbvprodi	⊢ ∏ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 = ∏ 𝑘 ∈ 𝐴 𝐶
45	44	a1i	⊢ ( 𝜑 → ∏ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 = ∏ 𝑘 ∈ 𝐴 𝐶 )
46	40 45	oveq12d	⊢ ( 𝜑 → ( ∏ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 / ∏ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) = ( ∏ 𝑘 ∈ 𝐴 𝐵 / ∏ 𝑘 ∈ 𝐴 𝐶 ) )
47	15 36 46	3eqtrd	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 ( 𝐵 / 𝐶 ) = ( ∏ 𝑘 ∈ 𝐴 𝐵 / ∏ 𝑘 ∈ 𝐴 𝐶 ) )