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 φAB=
fprodsplit.2 φU=AB
fprodsplit.3 φUFin
fprodsplit.4 φkUC
Assertion fprodsplit φkUC=kACkBC

Proof

Step Hyp Ref Expression
1 fprodsplit.1 φAB=
2 fprodsplit.2 φU=AB
3 fprodsplit.3 φUFin
4 fprodsplit.4 φkUC
5 iftrue kAifkAC1=C
6 5 prodeq2i kAifkAC1=kAC
7 ssun1 AAB
8 7 2 sseqtrrid φAU
9 5 adantl φkAifkAC1=C
10 8 sselda φkAkU
11 10 4 syldan φkAC
12 9 11 eqeltrd φkAifkAC1
13 eldifn kUA¬kA
14 13 iffalsed kUAifkAC1=1
15 14 adantl φkUAifkAC1=1
16 8 12 15 3 fprodss φkAifkAC1=kUifkAC1
17 6 16 eqtr3id φkAC=kUifkAC1
18 iftrue kBifkBC1=C
19 18 prodeq2i kBifkBC1=kBC
20 ssun2 BAB
21 20 2 sseqtrrid φBU
22 18 adantl φkBifkBC1=C
23 21 sselda φkBkU
24 23 4 syldan φkBC
25 22 24 eqeltrd φkBifkBC1
26 eldifn kUB¬kB
27 26 iffalsed kUBifkBC1=1
28 27 adantl φkUBifkBC1=1
29 21 25 28 3 fprodss φkBifkBC1=kUifkBC1
30 19 29 eqtr3id φkBC=kUifkBC1
31 17 30 oveq12d φkACkBC=kUifkAC1kUifkBC1
32 ax-1cn 1
33 ifcl C1ifkAC1
34 4 32 33 sylancl φkUifkAC1
35 ifcl C1ifkBC1
36 4 32 35 sylancl φkUifkBC1
37 3 34 36 fprodmul φkUifkAC1ifkBC1=kUifkAC1kUifkBC1
38 2 eleq2d φkUkAB
39 elun kABkAkB
40 38 39 bitrdi φkUkAkB
41 40 biimpa φkUkAkB
42 disjel AB=kA¬kB
43 1 42 sylan φkA¬kB
44 43 iffalsed φkAifkBC1=1
45 9 44 oveq12d φkAifkAC1ifkBC1=C1
46 11 mulid1d φkAC1=C
47 45 46 eqtrd φkAifkAC1ifkBC1=C
48 43 ex φkA¬kB
49 48 con2d φkB¬kA
50 49 imp φkB¬kA
51 50 iffalsed φkBifkAC1=1
52 51 22 oveq12d φkBifkAC1ifkBC1=1C
53 24 mulid2d φkB1C=C
54 52 53 eqtrd φkBifkAC1ifkBC1=C
55 47 54 jaodan φkAkBifkAC1ifkBC1=C
56 41 55 syldan φkUifkAC1ifkBC1=C
57 56 prodeq2dv φkUifkAC1ifkBC1=kUC
58 31 37 57 3eqtr2rd φkUC=kACkBC