fprodsplitf

Description: Split a finite product into two parts. A version of fprodsplit using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	fprodsplitf.kph	$⊢ Ⅎ k φ$
	fprodsplitf.in	$⊢ φ \to A \cap B = \emptyset$
	fprodsplitf.un	$⊢ φ \to U = A \cup B$
	fprodsplitf.fi	$⊢ φ \to U \in Fin$
	fprodsplitf.c	$⊢ (φ \land k \in U) \to C \in ℂ$
Assertion	fprodsplitf	$⊢ φ \to \prod_{k \in U} C = \prod_{k \in A} C \prod_{k \in B} C$

Proof

Step	Hyp	Ref	Expression
1		fprodsplitf.kph	$⊢ Ⅎ k φ$
2		fprodsplitf.in	$⊢ φ \to A \cap B = \emptyset$
3		fprodsplitf.un	$⊢ φ \to U = A \cup B$
4		fprodsplitf.fi	$⊢ φ \to U \in Fin$
5		fprodsplitf.c	$⊢ (φ \land k \in U) \to C \in ℂ$
6		nfv	$⊢ Ⅎ k j \in U$
7	1 6	nfan	$⊢ Ⅎ k (φ \land j \in U)$
8		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ C$
9	8	nfel1	$⊢ Ⅎ k ⦋ j / k ⦌ C \in ℂ$
10	7 9	nfim	$⊢ Ⅎ k ((φ \land j \in U) \to ⦋ j / k ⦌ C \in ℂ)$
11		eleq1w	$⊢ k = j \to (k \in U \leftrightarrow j \in U)$
12	11	anbi2d	$⊢ k = j \to ((φ \land k \in U) \leftrightarrow (φ \land j \in U))$
13		csbeq1a	$⊢ k = j \to C = ⦋ j / k ⦌ C$
14	13	eleq1d	$⊢ k = j \to (C \in ℂ \leftrightarrow ⦋ j / k ⦌ C \in ℂ)$
15	12 14	imbi12d	$⊢ k = j \to (((φ \land k \in U) \to C \in ℂ) \leftrightarrow ((φ \land j \in U) \to ⦋ j / k ⦌ C \in ℂ))$
16	10 15 5	chvarfv	$⊢ (φ \land j \in U) \to ⦋ j / k ⦌ C \in ℂ$
17	2 3 4 16	fprodsplit	$⊢ φ \to \prod_{j \in U} ⦋ j / k ⦌ C = \prod_{j \in A} ⦋ j / k ⦌ C \prod_{j \in B} ⦋ j / k ⦌ C$
18		nfcv	$⊢ \underline{Ⅎ} j C$
19	18 8 13	cbvprodi	$⊢ \prod_{k \in U} C = \prod_{j \in U} ⦋ j / k ⦌ C$
20	18 8 13	cbvprodi	$⊢ \prod_{k \in A} C = \prod_{j \in A} ⦋ j / k ⦌ C$
21	18 8 13	cbvprodi	$⊢ \prod_{k \in B} C = \prod_{j \in B} ⦋ j / k ⦌ C$
22	20 21	oveq12i	$⊢ \prod_{k \in A} C \prod_{k \in B} C = \prod_{j \in A} ⦋ j / k ⦌ C \prod_{j \in B} ⦋ j / k ⦌ C$
23	17 19 22	3eqtr4g	$⊢ φ \to \prod_{k \in U} C = \prod_{k \in A} C \prod_{k \in B} C$

Metamath Proof Explorer

Theorem fprodsplitf

Proof