Metamath Proof Explorer


Theorem fprodss

Description: Change the index set to a subset in a finite product. (Contributed by Scott Fenton, 16-Dec-2017)

Ref Expression
Hypotheses fprodss.1 φ A B
fprodss.2 φ k A C
fprodss.3 φ k B A C = 1
fprodss.4 φ B Fin
Assertion fprodss φ k A C = k B C

Proof

Step Hyp Ref Expression
1 fprodss.1 φ A B
2 fprodss.2 φ k A C
3 fprodss.3 φ k B A C = 1
4 fprodss.4 φ B Fin
5 sseq2 B = A B A
6 ss0 A A =
7 5 6 syl6bi B = A B A =
8 prodeq1 A = k A C = k C
9 prodeq1 B = k B C = k C
10 9 eqcomd B = k C = k B C
11 8 10 sylan9eq A = B = k A C = k B C
12 11 expcom B = A = k A C = k B C
13 7 12 syld B = A B k A C = k B C
14 1 13 syl5com φ B = k A C = k B C
15 cnvimass f -1 A dom f
16 simprr φ B f : 1 B 1-1 onto B f : 1 B 1-1 onto B
17 f1of f : 1 B 1-1 onto B f : 1 B B
18 16 17 syl φ B f : 1 B 1-1 onto B f : 1 B B
19 15 18 fssdm φ B f : 1 B 1-1 onto B f -1 A 1 B
20 f1ofn f : 1 B 1-1 onto B f Fn 1 B
21 elpreima f Fn 1 B n f -1 A n 1 B f n A
22 16 20 21 3syl φ B f : 1 B 1-1 onto B n f -1 A n 1 B f n A
23 18 ffvelrnda φ B f : 1 B 1-1 onto B n 1 B f n B
24 23 ex φ B f : 1 B 1-1 onto B n 1 B f n B
25 24 adantrd φ B f : 1 B 1-1 onto B n 1 B f n A f n B
26 22 25 sylbid φ B f : 1 B 1-1 onto B n f -1 A f n B
27 26 imp φ B f : 1 B 1-1 onto B n f -1 A f n B
28 2 ex φ k A C
29 28 adantr φ k B k A C
30 eldif k B A k B ¬ k A
31 ax-1cn 1
32 3 31 eqeltrdi φ k B A C
33 30 32 sylan2br φ k B ¬ k A C
34 33 expr φ k B ¬ k A C
35 29 34 pm2.61d φ k B C
36 35 adantlr φ B f : 1 B 1-1 onto B k B C
37 36 fmpttd φ B f : 1 B 1-1 onto B k B C : B
38 37 ffvelrnda φ B f : 1 B 1-1 onto B f n B k B C f n
39 27 38 syldan φ B f : 1 B 1-1 onto B n f -1 A k B C f n
40 eqid 1 = 1
41 simprl φ B f : 1 B 1-1 onto B B
42 nnuz = 1
43 41 42 eleqtrdi φ B f : 1 B 1-1 onto B B 1
44 ssidd φ B f : 1 B 1-1 onto B 1 B 1 B
45 40 43 44 fprodntriv φ B f : 1 B 1-1 onto B m 1 y y 0 seq m × n 1 if n 1 B k B C f n 1 y
46 eldifi n 1 B f -1 A n 1 B
47 46 23 sylan2 φ B f : 1 B 1-1 onto B n 1 B f -1 A f n B
48 eldifn n 1 B f -1 A ¬ n f -1 A
49 48 adantl φ B f : 1 B 1-1 onto B n 1 B f -1 A ¬ n f -1 A
50 46 adantl φ B f : 1 B 1-1 onto B n 1 B f -1 A n 1 B
51 22 adantr φ B f : 1 B 1-1 onto B n 1 B f -1 A n f -1 A n 1 B f n A
52 50 51 mpbirand φ B f : 1 B 1-1 onto B n 1 B f -1 A n f -1 A f n A
53 49 52 mtbid φ B f : 1 B 1-1 onto B n 1 B f -1 A ¬ f n A
54 47 53 eldifd φ B f : 1 B 1-1 onto B n 1 B f -1 A f n B A
55 difss B A B
56 resmpt B A B k B C B A = k B A C
57 55 56 ax-mp k B C B A = k B A C
58 57 fveq1i k B C B A f n = k B A C f n
59 fvres f n B A k B C B A f n = k B C f n
60 58 59 eqtr3id f n B A k B A C f n = k B C f n
61 54 60 syl φ B f : 1 B 1-1 onto B n 1 B f -1 A k B A C f n = k B C f n
62 1ex 1 V
63 62 elsn2 C 1 C = 1
64 3 63 sylibr φ k B A C 1
65 64 fmpttd φ k B A C : B A 1
66 65 ad2antrr φ B f : 1 B 1-1 onto B n 1 B f -1 A k B A C : B A 1
67 66 54 ffvelrnd φ B f : 1 B 1-1 onto B n 1 B f -1 A k B A C f n 1
68 elsni k B A C f n 1 k B A C f n = 1
69 67 68 syl φ B f : 1 B 1-1 onto B n 1 B f -1 A k B A C f n = 1
70 61 69 eqtr3d φ B f : 1 B 1-1 onto B n 1 B f -1 A k B C f n = 1
71 fzssuz 1 B 1
72 71 a1i φ B f : 1 B 1-1 onto B 1 B 1
73 19 39 45 70 72 prodss φ B f : 1 B 1-1 onto B n f -1 A k B C f n = n = 1 B k B C f n
74 1 adantr φ B f : 1 B 1-1 onto B A B
75 74 resmptd φ B f : 1 B 1-1 onto B k B C A = k A C
76 75 fveq1d φ B f : 1 B 1-1 onto B k B C A m = k A C m
77 fvres m A k B C A m = k B C m
78 76 77 sylan9req φ B f : 1 B 1-1 onto B m A k A C m = k B C m
79 78 prodeq2dv φ B f : 1 B 1-1 onto B m A k A C m = m A k B C m
80 fveq2 m = f n k B C m = k B C f n
81 fzfid φ B f : 1 B 1-1 onto B 1 B Fin
82 81 18 fisuppfi φ B f : 1 B 1-1 onto B f -1 A Fin
83 f1of1 f : 1 B 1-1 onto B f : 1 B 1-1 B
84 16 83 syl φ B f : 1 B 1-1 onto B f : 1 B 1-1 B
85 f1ores f : 1 B 1-1 B f -1 A 1 B f f -1 A : f -1 A 1-1 onto f f -1 A
86 84 19 85 syl2anc φ B f : 1 B 1-1 onto B f f -1 A : f -1 A 1-1 onto f f -1 A
87 f1ofo f : 1 B 1-1 onto B f : 1 B onto B
88 16 87 syl φ B f : 1 B 1-1 onto B f : 1 B onto B
89 foimacnv f : 1 B onto B A B f f -1 A = A
90 88 74 89 syl2anc φ B f : 1 B 1-1 onto B f f -1 A = A
91 90 f1oeq3d φ B f : 1 B 1-1 onto B f f -1 A : f -1 A 1-1 onto f f -1 A f f -1 A : f -1 A 1-1 onto A
92 86 91 mpbid φ B f : 1 B 1-1 onto B f f -1 A : f -1 A 1-1 onto A
93 fvres n f -1 A f f -1 A n = f n
94 93 adantl φ B f : 1 B 1-1 onto B n f -1 A f f -1 A n = f n
95 74 sselda φ B f : 1 B 1-1 onto B m A m B
96 37 ffvelrnda φ B f : 1 B 1-1 onto B m B k B C m
97 95 96 syldan φ B f : 1 B 1-1 onto B m A k B C m
98 80 82 92 94 97 fprodf1o φ B f : 1 B 1-1 onto B m A k B C m = n f -1 A k B C f n
99 79 98 eqtrd φ B f : 1 B 1-1 onto B m A k A C m = n f -1 A k B C f n
100 eqidd φ B f : 1 B 1-1 onto B n 1 B f n = f n
101 80 81 16 100 96 fprodf1o φ B f : 1 B 1-1 onto B m B k B C m = n = 1 B k B C f n
102 73 99 101 3eqtr4d φ B f : 1 B 1-1 onto B m A k A C m = m B k B C m
103 prodfc m A k A C m = k A C
104 prodfc m B k B C m = k B C
105 102 103 104 3eqtr3g φ B f : 1 B 1-1 onto B k A C = k B C
106 105 expr φ B f : 1 B 1-1 onto B k A C = k B C
107 106 exlimdv φ B f f : 1 B 1-1 onto B k A C = k B C
108 107 expimpd φ B f f : 1 B 1-1 onto B k A C = k B C
109 fz1f1o B Fin B = B f f : 1 B 1-1 onto B
110 4 109 syl φ B = B f f : 1 B 1-1 onto B
111 14 108 110 mpjaod φ k A C = k B C