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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑈 𝐶 = ( ∏ 𝑘 ∈ 𝐴 𝐶 · ∏ 𝑘 ∈ 𝐵 𝐶 ) )