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	$⊢ \underline{Ⅎ} k D$
	fprodsplitsn.a	$⊢ φ \to A \in Fin$
	fprodsplitsn.b	$⊢ φ \to B \in V$
	fprodsplitsn.ba	$⊢ φ \to \neg B \in A$
	fprodsplitsn.c	$⊢ (φ \land k \in A) \to C \in ℂ$
	fprodsplitsn.d	$⊢ k = B \to C = D$
	fprodsplitsn.dcn	$⊢ φ \to D \in ℂ$
Assertion	fprodsplitsn	$⊢ φ \to \prod_{k \in A \cup \{B\}} C = \prod_{k \in A} C D$

Proof

Step	Hyp	Ref	Expression
1		fprodsplitsn.ph	$⊢ Ⅎ k φ$
2		fprodsplitsn.kd	$⊢ \underline{Ⅎ} k D$
3		fprodsplitsn.a	$⊢ φ \to A \in Fin$
4		fprodsplitsn.b	$⊢ φ \to B \in V$
5		fprodsplitsn.ba	$⊢ φ \to \neg B \in A$
6		fprodsplitsn.c	$⊢ (φ \land k \in A) \to C \in ℂ$
7		fprodsplitsn.d	$⊢ k = B \to C = D$
8		fprodsplitsn.dcn	$⊢ φ \to D \in ℂ$
9		disjsn	$⊢ A \cap \{B\} = \emptyset \leftrightarrow \neg B \in A$
10	5 9	sylibr	$⊢ φ \to A \cap \{B\} = \emptyset$
11		eqidd	$⊢ φ \to A \cup \{B\} = A \cup \{B\}$
12		snfi	$⊢ \{B\} \in Fin$
13		unfi	$⊢ (A \in Fin \land \{B\} \in Fin) \to A \cup \{B\} \in Fin$
14	3 12 13	sylancl	$⊢ φ \to A \cup \{B\} \in Fin$
15	6	adantlr	$⊢ ((φ \land k \in (A \cup \{B\})) \land k \in A) \to C \in ℂ$
16		elunnel1	$⊢ (k \in (A \cup \{B\}) \land \neg k \in A) \to k \in \{B\}$
17		elsni	$⊢ k \in \{B\} \to k = B$
18	16 17	syl	$⊢ (k \in (A \cup \{B\}) \land \neg k \in A) \to k = B$
19	18	adantll	$⊢ ((φ \land k \in (A \cup \{B\})) \land \neg k \in A) \to k = B$
20	19 7	syl	$⊢ ((φ \land k \in (A \cup \{B\})) \land \neg k \in A) \to C = D$
21	8	ad2antrr	$⊢ ((φ \land k \in (A \cup \{B\})) \land \neg k \in A) \to D \in ℂ$
22	20 21	eqeltrd	$⊢ ((φ \land k \in (A \cup \{B\})) \land \neg k \in A) \to C \in ℂ$
23	15 22	pm2.61dan	$⊢ (φ \land k \in (A \cup \{B\})) \to C \in ℂ$
24	1 10 11 14 23	fprodsplitf	$⊢ φ \to \prod_{k \in A \cup \{B\}} C = \prod_{k \in A} C \prod_{k \in \{B\}} C$
25	2 7	prodsnf	$⊢ (B \in V \land D \in ℂ) \to \prod_{k \in \{B\}} C = D$
26	4 8 25	syl2anc	$⊢ φ \to \prod_{k \in \{B\}} C = D$
27	26	oveq2d	$⊢ φ \to \prod_{k \in A} C \prod_{k \in \{B\}} C = \prod_{k \in A} C D$
28	24 27	eqtrd	$⊢ φ \to \prod_{k \in A \cup \{B\}} C = \prod_{k \in A} C D$

Metamath Proof Explorer

Theorem fprodsplitsn

Proof