Theorem fprodsplitf

Description: Split a finite product into two parts. A version of fprodsplit using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	fprodsplitf.kph	⊢ Ⅎ 𝑘 𝜑
	fprodsplitf.in	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
	fprodsplitf.un	⊢ ( 𝜑 → 𝑈 = ( 𝐴 ∪ 𝐵 ) )
	fprodsplitf.fi	⊢ ( 𝜑 → 𝑈 ∈ Fin )
	fprodsplitf.c	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → 𝐶 ∈ ℂ )
Assertion	fprodsplitf	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑈 𝐶 = ( ∏ 𝑘 ∈ 𝐴 𝐶 · ∏ 𝑘 ∈ 𝐵 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		fprodsplitf.kph	⊢ Ⅎ 𝑘 𝜑
2		fprodsplitf.in	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
3		fprodsplitf.un	⊢ ( 𝜑 → 𝑈 = ( 𝐴 ∪ 𝐵 ) )
4		fprodsplitf.fi	⊢ ( 𝜑 → 𝑈 ∈ Fin )
5		fprodsplitf.c	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → 𝐶 ∈ ℂ )
6		nfv	⊢ Ⅎ 𝑘 𝑗 ∈ 𝑈
7	1 6	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑈 )
8		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐶
9	8	nfel1	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ℂ
10	7 9	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑈 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ℂ )
11		eleq1w	⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝑈 ↔ 𝑗 ∈ 𝑈 ) )
12	11	anbi2d	⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑈 ) ) )
13		csbeq1a	⊢ ( 𝑘 = 𝑗 → 𝐶 = ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
14	13	eleq1d	⊢ ( 𝑘 = 𝑗 → ( 𝐶 ∈ ℂ ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ℂ ) )
15	12 14	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → 𝐶 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑈 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ℂ ) ) )
16	10 15 5	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑈 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ∈ ℂ )
17	2 3 4 16	fprodsplit	⊢ ( 𝜑 → ∏ 𝑗 ∈ 𝑈 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 = ( ∏ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 · ∏ 𝑗 ∈ 𝐵 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 ) )
18		nfcv	⊢ Ⅎ 𝑗 𝐶
19	18 8 13	cbvprodi	⊢ ∏ 𝑘 ∈ 𝑈 𝐶 = ∏ 𝑗 ∈ 𝑈 ⦋ 𝑗 / 𝑘 ⦌ 𝐶
20	18 8 13	cbvprodi	⊢ ∏ 𝑘 ∈ 𝐴 𝐶 = ∏ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐶
21	18 8 13	cbvprodi	⊢ ∏ 𝑘 ∈ 𝐵 𝐶 = ∏ 𝑗 ∈ 𝐵 ⦋ 𝑗 / 𝑘 ⦌ 𝐶
22	20 21	oveq12i	⊢ ( ∏ 𝑘 ∈ 𝐴 𝐶 · ∏ 𝑘 ∈ 𝐵 𝐶 ) = ( ∏ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 · ∏ 𝑗 ∈ 𝐵 ⦋ 𝑗 / 𝑘 ⦌ 𝐶 )
23	17 19 22	3eqtr4g	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑈 𝐶 = ( ∏ 𝑘 ∈ 𝐴 𝐶 · ∏ 𝑘 ∈ 𝐵 𝐶 ) )