This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fprodsplit1

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

Ref Expression
Hypotheses fprodsplit1.a ⊢ φ → A ∈ Fin
fprodsplit1.b ⊢ φ ∧ k ∈ A → B ∈ ℂ
fprodsplit1.c ⊢ φ → C ∈ A
fprodsplit1.d ⊢ φ ∧ k = C → B = D
Assertion fprodsplit1 ⊢ φ → ∏ k ∈ A B = D ⁢ ∏ k ∈ A ∖ C B

Proof

Step Hyp Ref Expression
1 fprodsplit1.a ⊢ φ → A ∈ Fin
2 fprodsplit1.b ⊢ φ ∧ k ∈ A → B ∈ ℂ
3 fprodsplit1.c ⊢ φ → C ∈ A
4 fprodsplit1.d ⊢ φ ∧ k = C → B = D
5 nfv ⊢ Ⅎ k φ
6 nfcvd ⊢ φ → Ⅎ _ k D
7 5 6 1 2 3 4 fprodsplit1f ⊢ φ → ∏ k ∈ A B = D ⁢ ∏ k ∈ A ∖ C B