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