Theorem fprodsplitsn

Description: Separate out a term in a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	fprodsplitsn.ph	⊢ Ⅎ 𝑘 𝜑
	fprodsplitsn.kd	⊢ Ⅎ 𝑘 𝐷
	fprodsplitsn.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fprodsplitsn.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	fprodsplitsn.ba	⊢ ( 𝜑 → ¬ 𝐵 ∈ 𝐴 )
	fprodsplitsn.c	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
	fprodsplitsn.d	⊢ ( 𝑘 = 𝐵 → 𝐶 = 𝐷 )
	fprodsplitsn.dcn	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
Assertion	fprodsplitsn	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) 𝐶 = ( ∏ 𝑘 ∈ 𝐴 𝐶 · 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		fprodsplitsn.ph	⊢ Ⅎ 𝑘 𝜑
2		fprodsplitsn.kd	⊢ Ⅎ 𝑘 𝐷
3		fprodsplitsn.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
4		fprodsplitsn.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
5		fprodsplitsn.ba	⊢ ( 𝜑 → ¬ 𝐵 ∈ 𝐴 )
6		fprodsplitsn.c	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
7		fprodsplitsn.d	⊢ ( 𝑘 = 𝐵 → 𝐶 = 𝐷 )
8		fprodsplitsn.dcn	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
9		disjsn	⊢ ( ( 𝐴 ∩ { 𝐵 } ) = ∅ ↔ ¬ 𝐵 ∈ 𝐴 )
10	5 9	sylibr	⊢ ( 𝜑 → ( 𝐴 ∩ { 𝐵 } ) = ∅ )
11		eqidd	⊢ ( 𝜑 → ( 𝐴 ∪ { 𝐵 } ) = ( 𝐴 ∪ { 𝐵 } ) )
12		snfi	⊢ { 𝐵 } ∈ Fin
13		unfi	⊢ ( ( 𝐴 ∈ Fin ∧ { 𝐵 } ∈ Fin ) → ( 𝐴 ∪ { 𝐵 } ) ∈ Fin )
14	3 12 13	sylancl	⊢ ( 𝜑 → ( 𝐴 ∪ { 𝐵 } ) ∈ Fin )
15	6	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
16		elunnel1	⊢ ( ( 𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) ∧ ¬ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ { 𝐵 } )
17		elsni	⊢ ( 𝑘 ∈ { 𝐵 } → 𝑘 = 𝐵 )
18	16 17	syl	⊢ ( ( 𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) ∧ ¬ 𝑘 ∈ 𝐴 ) → 𝑘 = 𝐵 )
19	18	adantll	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) ) ∧ ¬ 𝑘 ∈ 𝐴 ) → 𝑘 = 𝐵 )
20	19 7	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) ) ∧ ¬ 𝑘 ∈ 𝐴 ) → 𝐶 = 𝐷 )
21	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) ) ∧ ¬ 𝑘 ∈ 𝐴 ) → 𝐷 ∈ ℂ )
22	20 21	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) ) ∧ ¬ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
23	15 22	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) ) → 𝐶 ∈ ℂ )
24	1 10 11 14 23	fprodsplitf	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) 𝐶 = ( ∏ 𝑘 ∈ 𝐴 𝐶 · ∏ 𝑘 ∈ { 𝐵 } 𝐶 ) )
25	2 7	prodsnf	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ ℂ ) → ∏ 𝑘 ∈ { 𝐵 } 𝐶 = 𝐷 )
26	4 8 25	syl2anc	⊢ ( 𝜑 → ∏ 𝑘 ∈ { 𝐵 } 𝐶 = 𝐷 )
27	26	oveq2d	⊢ ( 𝜑 → ( ∏ 𝑘 ∈ 𝐴 𝐶 · ∏ 𝑘 ∈ { 𝐵 } 𝐶 ) = ( ∏ 𝑘 ∈ 𝐴 𝐶 · 𝐷 ) )
28	24 27	eqtrd	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝐴 ∪ { 𝐵 } ) 𝐶 = ( ∏ 𝑘 ∈ 𝐴 𝐶 · 𝐷 ) )