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 ⊢ Ⅎ k φ
fprodsplit1f.fk ⊢ φ → Ⅎ _ k D
fprodsplit1f.a ⊢ φ → A ∈ Fin
fprodsplit1f.b ⊢ φ ∧ k ∈ A → B ∈ ℂ
fprodsplit1f.c ⊢ φ → C ∈ A
fprodsplit1f.d ⊢ φ ∧ k = C → B = D
Assertion fprodsplit1f ⊢ φ → ∏ k ∈ A B = D ⁢ ∏ k ∈ A ∖ C B

Proof

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