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 φ A B =
fprodsplit.2 φ U = A B
fprodsplit.3 φ U Fin
fprodsplit.4 φ k U C
Assertion fprodsplit φ k U C = k A C k B C

Proof

Step Hyp Ref Expression
1 fprodsplit.1 φ A B =
2 fprodsplit.2 φ U = A B
3 fprodsplit.3 φ U Fin
4 fprodsplit.4 φ k U C
5 iftrue k A if k A C 1 = C
6 5 prodeq2i k A if k A C 1 = k A C
7 ssun1 A A B
8 7 2 sseqtrrid φ A U
9 5 adantl φ k A if k A C 1 = C
10 8 sselda φ k A k U
11 10 4 syldan φ k A C
12 9 11 eqeltrd φ k A if k A C 1
13 eldifn k U A ¬ k A
14 13 iffalsed k U A if k A C 1 = 1
15 14 adantl φ k U A if k A C 1 = 1
16 8 12 15 3 fprodss φ k A if k A C 1 = k U if k A C 1
17 6 16 eqtr3id φ k A C = k U if k A C 1
18 iftrue k B if k B C 1 = C
19 18 prodeq2i k B if k B C 1 = k B C
20 ssun2 B A B
21 20 2 sseqtrrid φ B U
22 18 adantl φ k B if k B C 1 = C
23 21 sselda φ k B k U
24 23 4 syldan φ k B C
25 22 24 eqeltrd φ k B if k B C 1
26 eldifn k U B ¬ k B
27 26 iffalsed k U B if k B C 1 = 1
28 27 adantl φ k U B if k B C 1 = 1
29 21 25 28 3 fprodss φ k B if k B C 1 = k U if k B C 1
30 19 29 eqtr3id φ k B C = k U if k B C 1
31 17 30 oveq12d φ k A C k B C = k U if k A C 1 k U if k B C 1
32 ax-1cn 1
33 ifcl C 1 if k A C 1
34 4 32 33 sylancl φ k U if k A C 1
35 ifcl C 1 if k B C 1
36 4 32 35 sylancl φ k U if k B C 1
37 3 34 36 fprodmul φ k U if k A C 1 if k B C 1 = k U if k A C 1 k U if k B C 1
38 2 eleq2d φ k U k A B
39 elun k A B k A k B
40 38 39 bitrdi φ k U k A k B
41 40 biimpa φ k U k A k B
42 disjel A B = k A ¬ k B
43 1 42 sylan φ k A ¬ k B
44 43 iffalsed φ k A if k B C 1 = 1
45 9 44 oveq12d φ k A if k A C 1 if k B C 1 = C 1
46 11 mulid1d φ k A C 1 = C
47 45 46 eqtrd φ k A if k A C 1 if k B C 1 = C
48 43 ex φ k A ¬ k B
49 48 con2d φ k B ¬ k A
50 49 imp φ k B ¬ k A
51 50 iffalsed φ k B if k A C 1 = 1
52 51 22 oveq12d φ k B if k A C 1 if k B C 1 = 1 C
53 24 mulid2d φ k B 1 C = C
54 52 53 eqtrd φ k B if k A C 1 if k B C 1 = C
55 47 54 jaodan φ k A k B if k A C 1 if k B C 1 = C
56 41 55 syldan φ k U if k A C 1 if k B C 1 = C
57 56 prodeq2dv φ k U if k A C 1 if k B C 1 = k U C
58 31 37 57 3eqtr2rd φ k U C = k A C k B C