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

Metamath Proof Explorer

Theorem fprodsplitsn

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

Ref Expression
Hypotheses fprodsplitsn.ph ⊢ Ⅎ k φ
fprodsplitsn.kd ⊢ Ⅎ _ k D
fprodsplitsn.a ⊢ φ → A ∈ Fin
fprodsplitsn.b ⊢ φ → B ∈ V
fprodsplitsn.ba ⊢ φ → ¬ B ∈ A
fprodsplitsn.c ⊢ φ ∧ k ∈ A → C ∈ ℂ
fprodsplitsn.d ⊢ k = B → C = D
fprodsplitsn.dcn ⊢ φ → D ∈ ℂ
Assertion fprodsplitsn ⊢ φ → ∏ k ∈ A ∪ B C = ∏ k ∈ A C ⁢ D

Proof

Step Hyp Ref Expression
1 fprodsplitsn.ph ⊢ Ⅎ k φ
2 fprodsplitsn.kd ⊢ Ⅎ _ k D
3 fprodsplitsn.a ⊢ φ → A ∈ Fin
4 fprodsplitsn.b ⊢ φ → B ∈ V
5 fprodsplitsn.ba ⊢ φ → ¬ B ∈ A
6 fprodsplitsn.c ⊢ φ ∧ k ∈ A → C ∈ ℂ
7 fprodsplitsn.d ⊢ k = B → C = D
8 fprodsplitsn.dcn ⊢ φ → D ∈ ℂ
9 disjsn ⊢ A ∩ B = ∅ ↔ ¬ B ∈ A
10 5 9 sylibr ⊢ φ → A ∩ B = ∅
11 eqidd ⊢ φ → A ∪ B = A ∪ B
12 snfi ⊢ B ∈ Fin
13 unfi ⊢ A ∈ Fin ∧ B ∈ Fin → A ∪ B ∈ Fin
14 3 12 13 sylancl ⊢ φ → A ∪ B ∈ Fin
15 6 adantlr ⊢ φ ∧ k ∈ A ∪ B ∧ k ∈ A → C ∈ ℂ
16 elunnel1 ⊢ k ∈ A ∪ B ∧ ¬ k ∈ A → k ∈ B
17 elsni ⊢ k ∈ B → k = B
18 16 17 syl ⊢ k ∈ A ∪ B ∧ ¬ k ∈ A → k = B
19 18 adantll ⊢ φ ∧ k ∈ A ∪ B ∧ ¬ k ∈ A → k = B
20 19 7 syl ⊢ φ ∧ k ∈ A ∪ B ∧ ¬ k ∈ A → C = D
21 8 ad2antrr ⊢ φ ∧ k ∈ A ∪ B ∧ ¬ k ∈ A → D ∈ ℂ
22 20 21 eqeltrd ⊢ φ ∧ k ∈ A ∪ B ∧ ¬ k ∈ A → C ∈ ℂ
23 15 22 pm2.61dan ⊢ φ ∧ k ∈ A ∪ B → C ∈ ℂ
24 1 10 11 14 23 fprodsplitf ⊢ φ → ∏ k ∈ A ∪ B C = ∏ k ∈ A C ⁢ ∏ k ∈ B C
25 2 7 prodsnf ⊢ B ∈ V ∧ D ∈ ℂ → ∏ k ∈ B C = D
26 4 8 25 syl2anc ⊢ φ → ∏ k ∈ B C = D
27 26 oveq2d ⊢ φ → ∏ k ∈ A C ⁢ ∏ k ∈ B C = ∏ k ∈ A C ⁢ D
28 24 27 eqtrd ⊢ φ → ∏ k ∈ A ∪ B C = ∏ k ∈ A C ⁢ D