Metamath Proof Explorer

Theorem prodss

Description: Change the index set to a subset in an upper integer product. (Contributed by Scott Fenton, 11-Dec-2017)

Ref Expression
Hypotheses prodss.1 
|- ( ph -> A C_ B )
prodss.2 
|- ( ( ph /\ k e. A ) -> C e. CC )
prodss.3 
|- ( ph -> E. n e. ( ZZ>= ` M ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ( ZZ>= ` M ) |-> if ( k e. B , C , 1 ) ) ) ~~> y ) )
prodss.4 
|- ( ( ph /\ k e. ( B \ A ) ) -> C = 1 )
prodss.5 
|- ( ph -> B C_ ( ZZ>= ` M ) )
Assertion prodss 
|- ( ph -> prod_ k e. A C = prod_ k e. B C )

Proof

Step Hyp Ref Expression
1 prodss.1 
 |-  ( ph -> A C_ B )
2 prodss.2 
 |-  ( ( ph /\ k e. A ) -> C e. CC )
3 prodss.3 
 |-  ( ph -> E. n e. ( ZZ>= ` M ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ( ZZ>= ` M ) |-> if ( k e. B , C , 1 ) ) ) ~~> y ) )
4 prodss.4 
 |-  ( ( ph /\ k e. ( B \ A ) ) -> C = 1 )
5 prodss.5 
 |-  ( ph -> B C_ ( ZZ>= ` M ) )
6 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
7 simpr 
 |-  ( ( ph /\ M e. ZZ ) -> M e. ZZ )
8 3 adantr 
 |-  ( ( ph /\ M e. ZZ ) -> E. n e. ( ZZ>= ` M ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ( ZZ>= ` M ) |-> if ( k e. B , C , 1 ) ) ) ~~> y ) )
9 1 5 sstrd 
 |-  ( ph -> A C_ ( ZZ>= ` M ) )
10 9 adantr 
 |-  ( ( ph /\ M e. ZZ ) -> A C_ ( ZZ>= ` M ) )
11 simpr 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. ( ZZ>= ` M ) ) -> m e. ( ZZ>= ` M ) )
12 iftrue 
 |-  ( m e. B -> if ( m e. B , [_ m / k ]_ C , 1 ) = [_ m / k ]_ C )
13 12 adantl 
 |-  ( ( ph /\ m e. B ) -> if ( m e. B , [_ m / k ]_ C , 1 ) = [_ m / k ]_ C )
14 2 ex 
 |-  ( ph -> ( k e. A -> C e. CC ) )
15 14 adantr 
 |-  ( ( ph /\ k e. B ) -> ( k e. A -> C e. CC ) )
16 eldif 
 |-  ( k e. ( B \ A ) <-> ( k e. B /\ -. k e. A ) )
17 ax-1cn 
 |-  1 e. CC
18 4 17 eqeltrdi 
 |-  ( ( ph /\ k e. ( B \ A ) ) -> C e. CC )
19 16 18 sylan2br 
 |-  ( ( ph /\ ( k e. B /\ -. k e. A ) ) -> C e. CC )
20 19 expr 
 |-  ( ( ph /\ k e. B ) -> ( -. k e. A -> C e. CC ) )
21 15 20 pm2.61d 
 |-  ( ( ph /\ k e. B ) -> C e. CC )
22 21 ralrimiva 
 |-  ( ph -> A. k e. B C e. CC )
23 nfcsb1v 
 |-  F/_ k [_ m / k ]_ C
24 23 nfel1 
 |-  F/ k [_ m / k ]_ C e. CC
25 csbeq1a 
 |-  ( k = m -> C = [_ m / k ]_ C )
26 25 eleq1d 
 |-  ( k = m -> ( C e. CC <-> [_ m / k ]_ C e. CC ) )
27 24 26 rspc 
 |-  ( m e. B -> ( A. k e. B C e. CC -> [_ m / k ]_ C e. CC ) )
28 22 27 mpan9 
 |-  ( ( ph /\ m e. B ) -> [_ m / k ]_ C e. CC )
29 13 28 eqeltrd 
 |-  ( ( ph /\ m e. B ) -> if ( m e. B , [_ m / k ]_ C , 1 ) e. CC )
30 iffalse 
 |-  ( -. m e. B -> if ( m e. B , [_ m / k ]_ C , 1 ) = 1 )
31 30 17 eqeltrdi 
 |-  ( -. m e. B -> if ( m e. B , [_ m / k ]_ C , 1 ) e. CC )
32 31 adantl 
 |-  ( ( ph /\ -. m e. B ) -> if ( m e. B , [_ m / k ]_ C , 1 ) e. CC )
33 29 32 pm2.61dan 
 |-  ( ph -> if ( m e. B , [_ m / k ]_ C , 1 ) e. CC )
34 33 adantr 
 |-  ( ( ph /\ M e. ZZ ) -> if ( m e. B , [_ m / k ]_ C , 1 ) e. CC )
35 34 adantr 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. ( ZZ>= ` M ) ) -> if ( m e. B , [_ m / k ]_ C , 1 ) e. CC )
36 nfcv 
 |-  F/_ k m
37 nfv 
 |-  F/ k m e. B
38 nfcv 
 |-  F/_ k 1
39 37 23 38 nfif 
 |-  F/_ k if ( m e. B , [_ m / k ]_ C , 1 )
40 eleq1w 
 |-  ( k = m -> ( k e. B <-> m e. B ) )
41 40 25 ifbieq1d 
 |-  ( k = m -> if ( k e. B , C , 1 ) = if ( m e. B , [_ m / k ]_ C , 1 ) )
42 eqid 
 |-  ( k e. ( ZZ>= ` M ) |-> if ( k e. B , C , 1 ) ) = ( k e. ( ZZ>= ` M ) |-> if ( k e. B , C , 1 ) )
43 36 39 41 42 fvmptf 
 |-  ( ( m e. ( ZZ>= ` M ) /\ if ( m e. B , [_ m / k ]_ C , 1 ) e. CC ) -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. B , C , 1 ) ) ` m ) = if ( m e. B , [_ m / k ]_ C , 1 ) )
44 11 35 43 syl2anc 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. ( ZZ>= ` M ) ) -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. B , C , 1 ) ) ` m ) = if ( m e. B , [_ m / k ]_ C , 1 ) )
45 iftrue 
 |-  ( m e. A -> if ( m e. A , ( ( k e. A |-> C ) ` m ) , 1 ) = ( ( k e. A |-> C ) ` m ) )
46 45 adantl 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. A ) -> if ( m e. A , ( ( k e. A |-> C ) ` m ) , 1 ) = ( ( k e. A |-> C ) ` m ) )
47 simpr 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. A ) -> m e. A )
48 1 adantr 
 |-  ( ( ph /\ M e. ZZ ) -> A C_ B )
49 48 sselda 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. A ) -> m e. B )
50 28 adantlr 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. B ) -> [_ m / k ]_ C e. CC )
51 49 50 syldan 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. A ) -> [_ m / k ]_ C e. CC )
52 eqid 
 |-  ( k e. A |-> C ) = ( k e. A |-> C )
53 52 fvmpts 
 |-  ( ( m e. A /\ [_ m / k ]_ C e. CC ) -> ( ( k e. A |-> C ) ` m ) = [_ m / k ]_ C )
54 47 51 53 syl2anc 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. A ) -> ( ( k e. A |-> C ) ` m ) = [_ m / k ]_ C )
55 46 54 eqtrd 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. A ) -> if ( m e. A , ( ( k e. A |-> C ) ` m ) , 1 ) = [_ m / k ]_ C )
56 55 ex 
 |-  ( ( ph /\ M e. ZZ ) -> ( m e. A -> if ( m e. A , ( ( k e. A |-> C ) ` m ) , 1 ) = [_ m / k ]_ C ) )
57 56 adantr 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. B ) -> ( m e. A -> if ( m e. A , ( ( k e. A |-> C ) ` m ) , 1 ) = [_ m / k ]_ C ) )
58 iffalse 
 |-  ( -. m e. A -> if ( m e. A , ( ( k e. A |-> C ) ` m ) , 1 ) = 1 )
59 58 adantl 
 |-  ( ( m e. B /\ -. m e. A ) -> if ( m e. A , ( ( k e. A |-> C ) ` m ) , 1 ) = 1 )
60 59 adantl 
 |-  ( ( ( ph /\ M e. ZZ ) /\ ( m e. B /\ -. m e. A ) ) -> if ( m e. A , ( ( k e. A |-> C ) ` m ) , 1 ) = 1 )
61 eldif 
 |-  ( m e. ( B \ A ) <-> ( m e. B /\ -. m e. A ) )
62 4 ralrimiva 
 |-  ( ph -> A. k e. ( B \ A ) C = 1 )
63 62 adantr 
 |-  ( ( ph /\ M e. ZZ ) -> A. k e. ( B \ A ) C = 1 )
64 23 nfeq1 
 |-  F/ k [_ m / k ]_ C = 1
65 25 eqeq1d 
 |-  ( k = m -> ( C = 1 <-> [_ m / k ]_ C = 1 ) )
66 64 65 rspc 
 |-  ( m e. ( B \ A ) -> ( A. k e. ( B \ A ) C = 1 -> [_ m / k ]_ C = 1 ) )
67 63 66 mpan9 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. ( B \ A ) ) -> [_ m / k ]_ C = 1 )
68 61 67 sylan2br 
 |-  ( ( ( ph /\ M e. ZZ ) /\ ( m e. B /\ -. m e. A ) ) -> [_ m / k ]_ C = 1 )
69 60 68 eqtr4d 
 |-  ( ( ( ph /\ M e. ZZ ) /\ ( m e. B /\ -. m e. A ) ) -> if ( m e. A , ( ( k e. A |-> C ) ` m ) , 1 ) = [_ m / k ]_ C )
70 69 expr 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. B ) -> ( -. m e. A -> if ( m e. A , ( ( k e. A |-> C ) ` m ) , 1 ) = [_ m / k ]_ C ) )
71 57 70 pm2.61d 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. B ) -> if ( m e. A , ( ( k e. A |-> C ) ` m ) , 1 ) = [_ m / k ]_ C )
72 12 adantl 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. B ) -> if ( m e. B , [_ m / k ]_ C , 1 ) = [_ m / k ]_ C )
73 71 72 eqtr4d 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. B ) -> if ( m e. A , ( ( k e. A |-> C ) ` m ) , 1 ) = if ( m e. B , [_ m / k ]_ C , 1 ) )
74 48 ssneld 
 |-  ( ( ph /\ M e. ZZ ) -> ( -. m e. B -> -. m e. A ) )
75 74 imp 
 |-  ( ( ( ph /\ M e. ZZ ) /\ -. m e. B ) -> -. m e. A )
76 75 58 syl 
 |-  ( ( ( ph /\ M e. ZZ ) /\ -. m e. B ) -> if ( m e. A , ( ( k e. A |-> C ) ` m ) , 1 ) = 1 )
77 30 adantl 
 |-  ( ( ( ph /\ M e. ZZ ) /\ -. m e. B ) -> if ( m e. B , [_ m / k ]_ C , 1 ) = 1 )
78 76 77 eqtr4d 
 |-  ( ( ( ph /\ M e. ZZ ) /\ -. m e. B ) -> if ( m e. A , ( ( k e. A |-> C ) ` m ) , 1 ) = if ( m e. B , [_ m / k ]_ C , 1 ) )
79 73 78 pm2.61dan 
 |-  ( ( ph /\ M e. ZZ ) -> if ( m e. A , ( ( k e. A |-> C ) ` m ) , 1 ) = if ( m e. B , [_ m / k ]_ C , 1 ) )
80 79 adantr 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. ( ZZ>= ` M ) ) -> if ( m e. A , ( ( k e. A |-> C ) ` m ) , 1 ) = if ( m e. B , [_ m / k ]_ C , 1 ) )
81 44 80 eqtr4d 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. ( ZZ>= ` M ) ) -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. B , C , 1 ) ) ` m ) = if ( m e. A , ( ( k e. A |-> C ) ` m ) , 1 ) )
82 2 fmpttd 
 |-  ( ph -> ( k e. A |-> C ) : A --> CC )
83 82 adantr 
 |-  ( ( ph /\ M e. ZZ ) -> ( k e. A |-> C ) : A --> CC )
84 83 ffvelrnda 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. A ) -> ( ( k e. A |-> C ) ` m ) e. CC )
85 6 7 8 10 81 84 zprod 
 |-  ( ( ph /\ M e. ZZ ) -> prod_ m e. A ( ( k e. A |-> C ) ` m ) = ( ~~> ` seq M ( x. , ( k e. ( ZZ>= ` M ) |-> if ( k e. B , C , 1 ) ) ) ) )
86 5 adantr 
 |-  ( ( ph /\ M e. ZZ ) -> B C_ ( ZZ>= ` M ) )
87 43 ancoms 
 |-  ( ( if ( m e. B , [_ m / k ]_ C , 1 ) e. CC /\ m e. ( ZZ>= ` M ) ) -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. B , C , 1 ) ) ` m ) = if ( m e. B , [_ m / k ]_ C , 1 ) )
88 34 87 sylan 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. ( ZZ>= ` M ) ) -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. B , C , 1 ) ) ` m ) = if ( m e. B , [_ m / k ]_ C , 1 ) )
89 simpr 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. B ) -> m e. B )
90 eqid 
 |-  ( k e. B |-> C ) = ( k e. B |-> C )
91 90 fvmpts 
 |-  ( ( m e. B /\ [_ m / k ]_ C e. CC ) -> ( ( k e. B |-> C ) ` m ) = [_ m / k ]_ C )
92 89 50 91 syl2anc 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. B ) -> ( ( k e. B |-> C ) ` m ) = [_ m / k ]_ C )
93 92 ifeq1d 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. B ) -> if ( m e. B , ( ( k e. B |-> C ) ` m ) , 1 ) = if ( m e. B , [_ m / k ]_ C , 1 ) )
94 93 adantlr 
 |-  ( ( ( ( ph /\ M e. ZZ ) /\ m e. ( ZZ>= ` M ) ) /\ m e. B ) -> if ( m e. B , ( ( k e. B |-> C ) ` m ) , 1 ) = if ( m e. B , [_ m / k ]_ C , 1 ) )
95 iffalse 
 |-  ( -. m e. B -> if ( m e. B , ( ( k e. B |-> C ) ` m ) , 1 ) = 1 )
96 95 30 eqtr4d 
 |-  ( -. m e. B -> if ( m e. B , ( ( k e. B |-> C ) ` m ) , 1 ) = if ( m e. B , [_ m / k ]_ C , 1 ) )
97 96 adantl 
 |-  ( ( ( ( ph /\ M e. ZZ ) /\ m e. ( ZZ>= ` M ) ) /\ -. m e. B ) -> if ( m e. B , ( ( k e. B |-> C ) ` m ) , 1 ) = if ( m e. B , [_ m / k ]_ C , 1 ) )
98 94 97 pm2.61dan 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. ( ZZ>= ` M ) ) -> if ( m e. B , ( ( k e. B |-> C ) ` m ) , 1 ) = if ( m e. B , [_ m / k ]_ C , 1 ) )
99 88 98 eqtr4d 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. ( ZZ>= ` M ) ) -> ( ( k e. ( ZZ>= ` M ) |-> if ( k e. B , C , 1 ) ) ` m ) = if ( m e. B , ( ( k e. B |-> C ) ` m ) , 1 ) )
100 21 fmpttd 
 |-  ( ph -> ( k e. B |-> C ) : B --> CC )
101 100 adantr 
 |-  ( ( ph /\ M e. ZZ ) -> ( k e. B |-> C ) : B --> CC )
102 101 ffvelrnda 
 |-  ( ( ( ph /\ M e. ZZ ) /\ m e. B ) -> ( ( k e. B |-> C ) ` m ) e. CC )
103 6 7 8 86 99 102 zprod 
 |-  ( ( ph /\ M e. ZZ ) -> prod_ m e. B ( ( k e. B |-> C ) ` m ) = ( ~~> ` seq M ( x. , ( k e. ( ZZ>= ` M ) |-> if ( k e. B , C , 1 ) ) ) ) )
104 85 103 eqtr4d 
 |-  ( ( ph /\ M e. ZZ ) -> prod_ m e. A ( ( k e. A |-> C ) ` m ) = prod_ m e. B ( ( k e. B |-> C ) ` m ) )
105 prodfc 
 |-  prod_ m e. A ( ( k e. A |-> C ) ` m ) = prod_ k e. A C
106 prodfc 
 |-  prod_ m e. B ( ( k e. B |-> C ) ` m ) = prod_ k e. B C
107 104 105 106 3eqtr3g 
 |-  ( ( ph /\ M e. ZZ ) -> prod_ k e. A C = prod_ k e. B C )
108 1 adantr 
 |-  ( ( ph /\ -. M e. ZZ ) -> A C_ B )
109 5 adantr 
 |-  ( ( ph /\ -. M e. ZZ ) -> B C_ ( ZZ>= ` M ) )
110 uzf 
 |-  ZZ>= : ZZ --> ~P ZZ
111 110 fdmi 
 |-  dom ZZ>= = ZZ
112 111 eleq2i 
 |-  ( M e. dom ZZ>= <-> M e. ZZ )
113 ndmfv 
 |-  ( -. M e. dom ZZ>= -> ( ZZ>= ` M ) = (/) )
114 112 113 sylnbir 
 |-  ( -. M e. ZZ -> ( ZZ>= ` M ) = (/) )
115 114 adantl 
 |-  ( ( ph /\ -. M e. ZZ ) -> ( ZZ>= ` M ) = (/) )
116 109 115 sseqtrd 
 |-  ( ( ph /\ -. M e. ZZ ) -> B C_ (/) )
117 108 116 sstrd 
 |-  ( ( ph /\ -. M e. ZZ ) -> A C_ (/) )
118 ss0 
 |-  ( A C_ (/) -> A = (/) )
119 117 118 syl 
 |-  ( ( ph /\ -. M e. ZZ ) -> A = (/) )
120 ss0 
 |-  ( B C_ (/) -> B = (/) )
121 116 120 syl 
 |-  ( ( ph /\ -. M e. ZZ ) -> B = (/) )
122 119 121 eqtr4d 
 |-  ( ( ph /\ -. M e. ZZ ) -> A = B )
123 122 prodeq1d 
 |-  ( ( ph /\ -. M e. ZZ ) -> prod_ k e. A C = prod_ k e. B C )
124 107 123 pm2.61dan 
 |-  ( ph -> prod_ k e. A C = prod_ k e. B C )