Metamath Proof Explorer

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 ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 = ( 𝐷 · ∏ 𝑘 ∈ ( 𝐴 ∖ { 𝐶 } ) 𝐵 ) )