Metamath Proof Explorer

Theorem prodmolem2a

Description: Lemma for prodmo . (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Hypotheses prodmo.1 
|- F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )
prodmo.2 
|- ( ( ph /\ k e. A ) -> B e. CC )
prodmo.3 
|- G = ( j e. NN |-> [_ ( f ` j ) / k ]_ B )
prodmolem2.4 
|- H = ( j e. NN |-> [_ ( K ` j ) / k ]_ B )
prodmolem2.5 
|- ( ph -> N e. NN )
prodmolem2.6 
|- ( ph -> M e. ZZ )
prodmolem2.7 
|- ( ph -> A C_ ( ZZ>= ` M ) )
prodmolem2.8 
|- ( ph -> f : ( 1 ... N ) -1-1-onto-> A )
prodmolem2.9 
|- ( ph -> K Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
Assertion prodmolem2a 
|- ( ph -> seq M ( x. , F ) ~~> ( seq 1 ( x. , G ) ` N ) )

Proof

Step Hyp Ref Expression
1 prodmo.1 
 |-  F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )
2 prodmo.2 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
3 prodmo.3 
 |-  G = ( j e. NN |-> [_ ( f ` j ) / k ]_ B )
4 prodmolem2.4 
 |-  H = ( j e. NN |-> [_ ( K ` j ) / k ]_ B )
5 prodmolem2.5 
 |-  ( ph -> N e. NN )
6 prodmolem2.6 
 |-  ( ph -> M e. ZZ )
7 prodmolem2.7 
 |-  ( ph -> A C_ ( ZZ>= ` M ) )
8 prodmolem2.8 
 |-  ( ph -> f : ( 1 ... N ) -1-1-onto-> A )
9 prodmolem2.9 
 |-  ( ph -> K Isom < , < ( ( 1 ... ( # ` A ) ) , A ) )
10 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
11 10 8 hasheqf1od 
 |-  ( ph -> ( # ` ( 1 ... N ) ) = ( # ` A ) )
12 5 nnnn0d 
 |-  ( ph -> N e. NN0 )
13 hashfz1 
 |-  ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
14 12 13 syl 
 |-  ( ph -> ( # ` ( 1 ... N ) ) = N )
15 11 14 eqtr3d 
 |-  ( ph -> ( # ` A ) = N )
16 15 oveq2d 
 |-  ( ph -> ( 1 ... ( # ` A ) ) = ( 1 ... N ) )
17 isoeq4 
 |-  ( ( 1 ... ( # ` A ) ) = ( 1 ... N ) -> ( K Isom < , < ( ( 1 ... ( # ` A ) ) , A ) <-> K Isom < , < ( ( 1 ... N ) , A ) ) )
18 16 17 syl 
 |-  ( ph -> ( K Isom < , < ( ( 1 ... ( # ` A ) ) , A ) <-> K Isom < , < ( ( 1 ... N ) , A ) ) )
19 9 18 mpbid 
 |-  ( ph -> K Isom < , < ( ( 1 ... N ) , A ) )
20 isof1o 
 |-  ( K Isom < , < ( ( 1 ... N ) , A ) -> K : ( 1 ... N ) -1-1-onto-> A )
21 f1of 
 |-  ( K : ( 1 ... N ) -1-1-onto-> A -> K : ( 1 ... N ) --> A )
22 19 20 21 3syl 
 |-  ( ph -> K : ( 1 ... N ) --> A )
23 nnuz 
 |-  NN = ( ZZ>= ` 1 )
24 5 23 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 1 ) )
25 eluzfz2 
 |-  ( N e. ( ZZ>= ` 1 ) -> N e. ( 1 ... N ) )
26 24 25 syl 
 |-  ( ph -> N e. ( 1 ... N ) )
27 22 26 ffvelrnd 
 |-  ( ph -> ( K ` N ) e. A )
28 7 27 sseldd 
 |-  ( ph -> ( K ` N ) e. ( ZZ>= ` M ) )
29 7 sselda 
 |-  ( ( ph /\ j e. A ) -> j e. ( ZZ>= ` M ) )
30 19 20 syl 
 |-  ( ph -> K : ( 1 ... N ) -1-1-onto-> A )
31 f1ocnvfv2 
 |-  ( ( K : ( 1 ... N ) -1-1-onto-> A /\ j e. A ) -> ( K ` ( `' K ` j ) ) = j )
32 30 31 sylan 
 |-  ( ( ph /\ j e. A ) -> ( K ` ( `' K ` j ) ) = j )
33 f1ocnv 
 |-  ( K : ( 1 ... N ) -1-1-onto-> A -> `' K : A -1-1-onto-> ( 1 ... N ) )
34 f1of 
 |-  ( `' K : A -1-1-onto-> ( 1 ... N ) -> `' K : A --> ( 1 ... N ) )
35 30 33 34 3syl 
 |-  ( ph -> `' K : A --> ( 1 ... N ) )
36 35 ffvelrnda 
 |-  ( ( ph /\ j e. A ) -> ( `' K ` j ) e. ( 1 ... N ) )
37 elfzle2 
 |-  ( ( `' K ` j ) e. ( 1 ... N ) -> ( `' K ` j ) <_ N )
38 36 37 syl 
 |-  ( ( ph /\ j e. A ) -> ( `' K ` j ) <_ N )
39 19 adantr 
 |-  ( ( ph /\ j e. A ) -> K Isom < , < ( ( 1 ... N ) , A ) )
40 fzssuz 
 |-  ( 1 ... N ) C_ ( ZZ>= ` 1 )
41 uzssz 
 |-  ( ZZ>= ` 1 ) C_ ZZ
42 zssre 
 |-  ZZ C_ RR
43 41 42 sstri 
 |-  ( ZZ>= ` 1 ) C_ RR
44 40 43 sstri 
 |-  ( 1 ... N ) C_ RR
45 ressxr 
 |-  RR C_ RR*
46 44 45 sstri 
 |-  ( 1 ... N ) C_ RR*
47 46 a1i 
 |-  ( ( ph /\ j e. A ) -> ( 1 ... N ) C_ RR* )
48 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
49 48 42 sstri 
 |-  ( ZZ>= ` M ) C_ RR
50 49 45 sstri 
 |-  ( ZZ>= ` M ) C_ RR*
51 7 50 sstrdi 
 |-  ( ph -> A C_ RR* )
52 51 adantr 
 |-  ( ( ph /\ j e. A ) -> A C_ RR* )
53 26 adantr 
 |-  ( ( ph /\ j e. A ) -> N e. ( 1 ... N ) )
54 leisorel 
 |-  ( ( K Isom < , < ( ( 1 ... N ) , A ) /\ ( ( 1 ... N ) C_ RR* /\ A C_ RR* ) /\ ( ( `' K ` j ) e. ( 1 ... N ) /\ N e. ( 1 ... N ) ) ) -> ( ( `' K ` j ) <_ N <-> ( K ` ( `' K ` j ) ) <_ ( K ` N ) ) )
55 39 47 52 36 53 54 syl122anc 
 |-  ( ( ph /\ j e. A ) -> ( ( `' K ` j ) <_ N <-> ( K ` ( `' K ` j ) ) <_ ( K ` N ) ) )
56 38 55 mpbid 
 |-  ( ( ph /\ j e. A ) -> ( K ` ( `' K ` j ) ) <_ ( K ` N ) )
57 32 56 eqbrtrrd 
 |-  ( ( ph /\ j e. A ) -> j <_ ( K ` N ) )
58 7 48 sstrdi 
 |-  ( ph -> A C_ ZZ )
59 58 sselda 
 |-  ( ( ph /\ j e. A ) -> j e. ZZ )
60 eluzelz 
 |-  ( ( K ` N ) e. ( ZZ>= ` M ) -> ( K ` N ) e. ZZ )
61 28 60 syl 
 |-  ( ph -> ( K ` N ) e. ZZ )
62 61 adantr 
 |-  ( ( ph /\ j e. A ) -> ( K ` N ) e. ZZ )
63 eluz 
 |-  ( ( j e. ZZ /\ ( K ` N ) e. ZZ ) -> ( ( K ` N ) e. ( ZZ>= ` j ) <-> j <_ ( K ` N ) ) )
64 59 62 63 syl2anc 
 |-  ( ( ph /\ j e. A ) -> ( ( K ` N ) e. ( ZZ>= ` j ) <-> j <_ ( K ` N ) ) )
65 57 64 mpbird 
 |-  ( ( ph /\ j e. A ) -> ( K ` N ) e. ( ZZ>= ` j ) )
66 elfzuzb 
 |-  ( j e. ( M ... ( K ` N ) ) <-> ( j e. ( ZZ>= ` M ) /\ ( K ` N ) e. ( ZZ>= ` j ) ) )
67 29 65 66 sylanbrc 
 |-  ( ( ph /\ j e. A ) -> j e. ( M ... ( K ` N ) ) )
68 67 ex 
 |-  ( ph -> ( j e. A -> j e. ( M ... ( K ` N ) ) ) )
69 68 ssrdv 
 |-  ( ph -> A C_ ( M ... ( K ` N ) ) )
70 1 2 28 69 fprodcvg 
 |-  ( ph -> seq M ( x. , F ) ~~> ( seq M ( x. , F ) ` ( K ` N ) ) )
71 mulid2 
 |-  ( m e. CC -> ( 1 x. m ) = m )
72 71 adantl 
 |-  ( ( ph /\ m e. CC ) -> ( 1 x. m ) = m )
73 mulid1 
 |-  ( m e. CC -> ( m x. 1 ) = m )
74 73 adantl 
 |-  ( ( ph /\ m e. CC ) -> ( m x. 1 ) = m )
75 mulcl 
 |-  ( ( m e. CC /\ x e. CC ) -> ( m x. x ) e. CC )
76 75 adantl 
 |-  ( ( ph /\ ( m e. CC /\ x e. CC ) ) -> ( m x. x ) e. CC )
77 1cnd 
 |-  ( ph -> 1 e. CC )
78 26 16 eleqtrrd 
 |-  ( ph -> N e. ( 1 ... ( # ` A ) ) )
79 iftrue 
 |-  ( k e. A -> if ( k e. A , B , 1 ) = B )
80 79 adantl 
 |-  ( ( ph /\ k e. A ) -> if ( k e. A , B , 1 ) = B )
81 80 2 eqeltrd 
 |-  ( ( ph /\ k e. A ) -> if ( k e. A , B , 1 ) e. CC )
82 81 ex 
 |-  ( ph -> ( k e. A -> if ( k e. A , B , 1 ) e. CC ) )
83 iffalse 
 |-  ( -. k e. A -> if ( k e. A , B , 1 ) = 1 )
84 ax-1cn 
 |-  1 e. CC
85 83 84 eqeltrdi 
 |-  ( -. k e. A -> if ( k e. A , B , 1 ) e. CC )
86 82 85 pm2.61d1 
 |-  ( ph -> if ( k e. A , B , 1 ) e. CC )
87 86 adantr 
 |-  ( ( ph /\ k e. ZZ ) -> if ( k e. A , B , 1 ) e. CC )
88 87 1 fmptd 
 |-  ( ph -> F : ZZ --> CC )
89 elfzelz 
 |-  ( m e. ( M ... ( K ` ( # ` A ) ) ) -> m e. ZZ )
90 ffvelrn 
 |-  ( ( F : ZZ --> CC /\ m e. ZZ ) -> ( F ` m ) e. CC )
91 88 89 90 syl2an 
 |-  ( ( ph /\ m e. ( M ... ( K ` ( # ` A ) ) ) ) -> ( F ` m ) e. CC )
92 fveqeq2 
 |-  ( k = m -> ( ( F ` k ) = 1 <-> ( F ` m ) = 1 ) )
93 fzssz 
 |-  ( M ... ( K ` ( # ` A ) ) ) C_ ZZ
94 eldifi 
 |-  ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> k e. ( M ... ( K ` ( # ` A ) ) ) )
95 93 94 sseldi 
 |-  ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> k e. ZZ )
96 eldifn 
 |-  ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> -. k e. A )
97 96 83 syl 
 |-  ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> if ( k e. A , B , 1 ) = 1 )
98 97 84 eqeltrdi 
 |-  ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> if ( k e. A , B , 1 ) e. CC )
99 1 fvmpt2 
 |-  ( ( k e. ZZ /\ if ( k e. A , B , 1 ) e. CC ) -> ( F ` k ) = if ( k e. A , B , 1 ) )
100 95 98 99 syl2anc 
 |-  ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> ( F ` k ) = if ( k e. A , B , 1 ) )
101 100 97 eqtrd 
 |-  ( k e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> ( F ` k ) = 1 )
102 92 101 vtoclga 
 |-  ( m e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) -> ( F ` m ) = 1 )
103 102 adantl 
 |-  ( ( ph /\ m e. ( ( M ... ( K ` ( # ` A ) ) ) \ A ) ) -> ( F ` m ) = 1 )
104 isof1o 
 |-  ( K Isom < , < ( ( 1 ... ( # ` A ) ) , A ) -> K : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
105 f1of 
 |-  ( K : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> K : ( 1 ... ( # ` A ) ) --> A )
106 9 104 105 3syl 
 |-  ( ph -> K : ( 1 ... ( # ` A ) ) --> A )
107 106 ffvelrnda 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> ( K ` x ) e. A )
108 107 iftrued 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 1 ) = [_ ( K ` x ) / k ]_ B )
109 58 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> A C_ ZZ )
110 109 107 sseldd 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> ( K ` x ) e. ZZ )
111 nfv 
 |-  F/ k ph
112 nfv 
 |-  F/ k ( K ` x ) e. A
113 nfcsb1v 
 |-  F/_ k [_ ( K ` x ) / k ]_ B
114 nfcv 
 |-  F/_ k 1
115 112 113 114 nfif 
 |-  F/_ k if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 1 )
116 115 nfel1 
 |-  F/ k if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 1 ) e. CC
117 111 116 nfim 
 |-  F/ k ( ph -> if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 1 ) e. CC )
118 fvex 
 |-  ( K ` x ) e. _V
119 eleq1 
 |-  ( k = ( K ` x ) -> ( k e. A <-> ( K ` x ) e. A ) )
120 csbeq1a 
 |-  ( k = ( K ` x ) -> B = [_ ( K ` x ) / k ]_ B )
121 119 120 ifbieq1d 
 |-  ( k = ( K ` x ) -> if ( k e. A , B , 1 ) = if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 1 ) )
122 121 eleq1d 
 |-  ( k = ( K ` x ) -> ( if ( k e. A , B , 1 ) e. CC <-> if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 1 ) e. CC ) )
123 122 imbi2d 
 |-  ( k = ( K ` x ) -> ( ( ph -> if ( k e. A , B , 1 ) e. CC ) <-> ( ph -> if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 1 ) e. CC ) ) )
124 117 118 123 86 vtoclf 
 |-  ( ph -> if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 1 ) e. CC )
125 124 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 1 ) e. CC )
126 eleq1 
 |-  ( n = ( K ` x ) -> ( n e. A <-> ( K ` x ) e. A ) )
127 csbeq1 
 |-  ( n = ( K ` x ) -> [_ n / k ]_ B = [_ ( K ` x ) / k ]_ B )
128 126 127 ifbieq1d 
 |-  ( n = ( K ` x ) -> if ( n e. A , [_ n / k ]_ B , 1 ) = if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 1 ) )
129 nfcv 
 |-  F/_ n if ( k e. A , B , 1 )
130 nfv 
 |-  F/ k n e. A
131 nfcsb1v 
 |-  F/_ k [_ n / k ]_ B
132 130 131 114 nfif 
 |-  F/_ k if ( n e. A , [_ n / k ]_ B , 1 )
133 eleq1 
 |-  ( k = n -> ( k e. A <-> n e. A ) )
134 csbeq1a 
 |-  ( k = n -> B = [_ n / k ]_ B )
135 133 134 ifbieq1d 
 |-  ( k = n -> if ( k e. A , B , 1 ) = if ( n e. A , [_ n / k ]_ B , 1 ) )
136 129 132 135 cbvmpt 
 |-  ( k e. ZZ |-> if ( k e. A , B , 1 ) ) = ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 1 ) )
137 1 136 eqtri 
 |-  F = ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 1 ) )
138 128 137 fvmptg 
 |-  ( ( ( K ` x ) e. ZZ /\ if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 1 ) e. CC ) -> ( F ` ( K ` x ) ) = if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 1 ) )
139 110 125 138 syl2anc 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> ( F ` ( K ` x ) ) = if ( ( K ` x ) e. A , [_ ( K ` x ) / k ]_ B , 1 ) )
140 elfznn 
 |-  ( x e. ( 1 ... ( # ` A ) ) -> x e. NN )
141 108 125 eqeltrrd 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> [_ ( K ` x ) / k ]_ B e. CC )
142 fveq2 
 |-  ( j = x -> ( K ` j ) = ( K ` x ) )
143 142 csbeq1d 
 |-  ( j = x -> [_ ( K ` j ) / k ]_ B = [_ ( K ` x ) / k ]_ B )
144 143 4 fvmptg 
 |-  ( ( x e. NN /\ [_ ( K ` x ) / k ]_ B e. CC ) -> ( H ` x ) = [_ ( K ` x ) / k ]_ B )
145 140 141 144 syl2an2 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> ( H ` x ) = [_ ( K ` x ) / k ]_ B )
146 108 139 145 3eqtr4rd 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` A ) ) ) -> ( H ` x ) = ( F ` ( K ` x ) ) )
147 72 74 76 77 9 78 7 91 103 146 seqcoll 
 |-  ( ph -> ( seq M ( x. , F ) ` ( K ` N ) ) = ( seq 1 ( x. , H ) ` N ) )
148 5 5 jca 
 |-  ( ph -> ( N e. NN /\ N e. NN ) )
149 1 2 3 4 148 8 30 prodmolem3 
 |-  ( ph -> ( seq 1 ( x. , G ) ` N ) = ( seq 1 ( x. , H ) ` N ) )
150 147 149 eqtr4d 
 |-  ( ph -> ( seq M ( x. , F ) ` ( K ` N ) ) = ( seq 1 ( x. , G ) ` N ) )
151 70 150 breqtrd 
 |-  ( ph -> seq M ( x. , F ) ~~> ( seq 1 ( x. , G ) ` N ) )