Theorem fprodsplit

Description: Split a finite product into two parts. (Contributed by Scott Fenton, 16-Dec-2017)

	Ref	Expression
Hypotheses	fprodsplit.1	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
	fprodsplit.2	⊢ ( 𝜑 → 𝑈 = ( 𝐴 ∪ 𝐵 ) )
	fprodsplit.3	⊢ ( 𝜑 → 𝑈 ∈ Fin )
	fprodsplit.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → 𝐶 ∈ ℂ )
Assertion	fprodsplit	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑈 𝐶 = ( ∏ 𝑘 ∈ 𝐴 𝐶 · ∏ 𝑘 ∈ 𝐵 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		fprodsplit.1	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
2		fprodsplit.2	⊢ ( 𝜑 → 𝑈 = ( 𝐴 ∪ 𝐵 ) )
3		fprodsplit.3	⊢ ( 𝜑 → 𝑈 ∈ Fin )
4		fprodsplit.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → 𝐶 ∈ ℂ )
5		iftrue	⊢ ( 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) = 𝐶 )
6	5	prodeq2i	⊢ ∏ 𝑘 ∈ 𝐴 if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) = ∏ 𝑘 ∈ 𝐴 𝐶
7		ssun1	⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
8	7 2	sseqtrrid	⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 )
9	5	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) = 𝐶 )
10	8	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝑈 )
11	10 4	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
12	9 11	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ∈ ℂ )
13		eldifn	⊢ ( 𝑘 ∈ ( 𝑈 ∖ 𝐴 ) → ¬ 𝑘 ∈ 𝐴 )
14	13	iffalsed	⊢ ( 𝑘 ∈ ( 𝑈 ∖ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) = 1 )
15	14	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑈 ∖ 𝐴 ) ) → if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) = 1 )
16	8 12 15 3	fprodss	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) = ∏ 𝑘 ∈ 𝑈 if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) )
17	6 16	eqtr3id	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐶 = ∏ 𝑘 ∈ 𝑈 if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) )
18		iftrue	⊢ ( 𝑘 ∈ 𝐵 → if ( 𝑘 ∈ 𝐵 , 𝐶 , 1 ) = 𝐶 )
19	18	prodeq2i	⊢ ∏ 𝑘 ∈ 𝐵 if ( 𝑘 ∈ 𝐵 , 𝐶 , 1 ) = ∏ 𝑘 ∈ 𝐵 𝐶
20		ssun2	⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
21	20 2	sseqtrrid	⊢ ( 𝜑 → 𝐵 ⊆ 𝑈 )
22	18	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → if ( 𝑘 ∈ 𝐵 , 𝐶 , 1 ) = 𝐶 )
23	21	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝑘 ∈ 𝑈 )
24	23 4	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
25	22 24	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → if ( 𝑘 ∈ 𝐵 , 𝐶 , 1 ) ∈ ℂ )
26		eldifn	⊢ ( 𝑘 ∈ ( 𝑈 ∖ 𝐵 ) → ¬ 𝑘 ∈ 𝐵 )
27	26	iffalsed	⊢ ( 𝑘 ∈ ( 𝑈 ∖ 𝐵 ) → if ( 𝑘 ∈ 𝐵 , 𝐶 , 1 ) = 1 )
28	27	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑈 ∖ 𝐵 ) ) → if ( 𝑘 ∈ 𝐵 , 𝐶 , 1 ) = 1 )
29	21 25 28 3	fprodss	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐵 if ( 𝑘 ∈ 𝐵 , 𝐶 , 1 ) = ∏ 𝑘 ∈ 𝑈 if ( 𝑘 ∈ 𝐵 , 𝐶 , 1 ) )
30	19 29	eqtr3id	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐵 𝐶 = ∏ 𝑘 ∈ 𝑈 if ( 𝑘 ∈ 𝐵 , 𝐶 , 1 ) )
31	17 30	oveq12d	⊢ ( 𝜑 → ( ∏ 𝑘 ∈ 𝐴 𝐶 · ∏ 𝑘 ∈ 𝐵 𝐶 ) = ( ∏ 𝑘 ∈ 𝑈 if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) · ∏ 𝑘 ∈ 𝑈 if ( 𝑘 ∈ 𝐵 , 𝐶 , 1 ) ) )
32		ax-1cn	⊢ 1 ∈ ℂ
33		ifcl	⊢ ( ( 𝐶 ∈ ℂ ∧ 1 ∈ ℂ ) → if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ∈ ℂ )
34	4 32 33	sylancl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ∈ ℂ )
35		ifcl	⊢ ( ( 𝐶 ∈ ℂ ∧ 1 ∈ ℂ ) → if ( 𝑘 ∈ 𝐵 , 𝐶 , 1 ) ∈ ℂ )
36	4 32 35	sylancl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → if ( 𝑘 ∈ 𝐵 , 𝐶 , 1 ) ∈ ℂ )
37	3 34 36	fprodmul	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑈 ( if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) · if ( 𝑘 ∈ 𝐵 , 𝐶 , 1 ) ) = ( ∏ 𝑘 ∈ 𝑈 if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) · ∏ 𝑘 ∈ 𝑈 if ( 𝑘 ∈ 𝐵 , 𝐶 , 1 ) ) )
38	2	eleq2d	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑈 ↔ 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ) )
39		elun	⊢ ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵 ) )
40	38 39	bitrdi	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑈 ↔ ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵 ) ) )
41	40	biimpa	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵 ) )
42		disjel	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑘 ∈ 𝐴 ) → ¬ 𝑘 ∈ 𝐵 )
43	1 42	sylan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ¬ 𝑘 ∈ 𝐵 )
44	43	iffalsed	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐵 , 𝐶 , 1 ) = 1 )
45	9 44	oveq12d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) · if ( 𝑘 ∈ 𝐵 , 𝐶 , 1 ) ) = ( 𝐶 · 1 ) )
46	11	mulridd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐶 · 1 ) = 𝐶 )
47	45 46	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) · if ( 𝑘 ∈ 𝐵 , 𝐶 , 1 ) ) = 𝐶 )
48	43	ex	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 → ¬ 𝑘 ∈ 𝐵 ) )
49	48	con2d	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐵 → ¬ 𝑘 ∈ 𝐴 ) )
50	49	imp	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ¬ 𝑘 ∈ 𝐴 )
51	50	iffalsed	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) = 1 )
52	51 22	oveq12d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) · if ( 𝑘 ∈ 𝐵 , 𝐶 , 1 ) ) = ( 1 · 𝐶 ) )
53	24	mullidd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 1 · 𝐶 ) = 𝐶 )
54	52 53	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) · if ( 𝑘 ∈ 𝐵 , 𝐶 , 1 ) ) = 𝐶 )
55	47 54	jaodan	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵 ) ) → ( if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) · if ( 𝑘 ∈ 𝐵 , 𝐶 , 1 ) ) = 𝐶 )
56	41 55	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → ( if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) · if ( 𝑘 ∈ 𝐵 , 𝐶 , 1 ) ) = 𝐶 )
57	56	prodeq2dv	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑈 ( if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) · if ( 𝑘 ∈ 𝐵 , 𝐶 , 1 ) ) = ∏ 𝑘 ∈ 𝑈 𝐶 )
58	31 37 57	3eqtr2rd	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑈 𝐶 = ( ∏ 𝑘 ∈ 𝐴 𝐶 · ∏ 𝑘 ∈ 𝐵 𝐶 ) )