Theorem fprodsplit1f

Description: Separate out a term in a finite product. A version of fprodsplit1 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	fprodsplit1f.kph	⊢ Ⅎ 𝑘 𝜑
	fprodsplit1f.fk	⊢ ( 𝜑 → Ⅎ 𝑘 𝐷 )
	fprodsplit1f.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fprodsplit1f.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
	fprodsplit1f.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
	fprodsplit1f.d	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐶 ) → 𝐵 = 𝐷 )
Assertion	fprodsplit1f	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 = ( 𝐷 · ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝐶 } ) 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fprodsplit1f.kph	⊢ Ⅎ 𝑘 𝜑
2		fprodsplit1f.fk	⊢ ( 𝜑 → Ⅎ 𝑘 𝐷 )
3		fprodsplit1f.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
4		fprodsplit1f.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
5		fprodsplit1f.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
6		fprodsplit1f.d	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐶 ) → 𝐵 = 𝐷 )
7		disjdif	⊢ ( { 𝐶 } ∩ ( 𝐴 ∖ { 𝐶 } ) ) = ∅
8	7	a1i	⊢ ( 𝜑 → ( { 𝐶 } ∩ ( 𝐴 ∖ { 𝐶 } ) ) = ∅ )
9	5	snssd	⊢ ( 𝜑 → { 𝐶 } ⊆ 𝐴 )
10		undif	⊢ ( { 𝐶 } ⊆ 𝐴 ↔ ( { 𝐶 } ∪ ( 𝐴 ∖ { 𝐶 } ) ) = 𝐴 )
11	9 10	sylib	⊢ ( 𝜑 → ( { 𝐶 } ∪ ( 𝐴 ∖ { 𝐶 } ) ) = 𝐴 )
12	11	eqcomd	⊢ ( 𝜑 → 𝐴 = ( { 𝐶 } ∪ ( 𝐴 ∖ { 𝐶 } ) ) )
13	1 8 12 3 4	fprodsplitf	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 = ( ∏ 𝑘 ∈ { 𝐶 } 𝐵 · ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝐶 } ) 𝐵 ) )
14	5	ancli	⊢ ( 𝜑 → ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) )
15		nfv	⊢ Ⅎ 𝑘 𝐶 ∈ 𝐴
16	1 15	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝐶 ∈ 𝐴 )
17		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝐶 / 𝑘 ⦌ 𝐵
18	17	nfel1	⊢ Ⅎ 𝑘 ⦋ 𝐶 / 𝑘 ⦌ 𝐵 ∈ ℂ
19	16 18	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ⦋ 𝐶 / 𝑘 ⦌ 𝐵 ∈ ℂ )
20		eleq1	⊢ ( 𝑘 = 𝐶 → ( 𝑘 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴 ) )
21	20	anbi2d	⊢ ( 𝑘 = 𝐶 → ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) ) )
22		csbeq1a	⊢ ( 𝑘 = 𝐶 → 𝐵 = ⦋ 𝐶 / 𝑘 ⦌ 𝐵 )
23	22	eleq1d	⊢ ( 𝑘 = 𝐶 → ( 𝐵 ∈ ℂ ↔ ⦋ 𝐶 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
24	21 23	imbi12d	⊢ ( 𝑘 = 𝐶 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ⦋ 𝐶 / 𝑘 ⦌ 𝐵 ∈ ℂ ) ) )
25	19 24 4	vtoclg1f	⊢ ( 𝐶 ∈ 𝐴 → ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ⦋ 𝐶 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
26	5 14 25	sylc	⊢ ( 𝜑 → ⦋ 𝐶 / 𝑘 ⦌ 𝐵 ∈ ℂ )
27		prodsns	⊢ ( ( 𝐶 ∈ 𝐴 ∧ ⦋ 𝐶 / 𝑘 ⦌ 𝐵 ∈ ℂ ) → ∏ 𝑘 ∈ { 𝐶 } 𝐵 = ⦋ 𝐶 / 𝑘 ⦌ 𝐵 )
28	5 26 27	syl2anc	⊢ ( 𝜑 → ∏ 𝑘 ∈ { 𝐶 } 𝐵 = ⦋ 𝐶 / 𝑘 ⦌ 𝐵 )
29	1 2 5 6	csbiedf	⊢ ( 𝜑 → ⦋ 𝐶 / 𝑘 ⦌ 𝐵 = 𝐷 )
30	28 29	eqtrd	⊢ ( 𝜑 → ∏ 𝑘 ∈ { 𝐶 } 𝐵 = 𝐷 )
31	30	oveq1d	⊢ ( 𝜑 → ( ∏ 𝑘 ∈ { 𝐶 } 𝐵 · ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝐶 } ) 𝐵 ) = ( 𝐷 · ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝐶 } ) 𝐵 ) )
32	13 31	eqtrd	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 = ( 𝐷 · ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝐶 } ) 𝐵 ) )