Metamath Proof Explorer

Theorem prodmolem3

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 )
prodmolem3.4 
|- H = ( j e. NN |-> [_ ( K ` j ) / k ]_ B )
prodmolem3.5 
|- ( ph -> ( M e. NN /\ N e. NN ) )
prodmolem3.6 
|- ( ph -> f : ( 1 ... M ) -1-1-onto-> A )
prodmolem3.7 
|- ( ph -> K : ( 1 ... N ) -1-1-onto-> A )
Assertion prodmolem3 
|- ( ph -> ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , H ) ` 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 prodmolem3.4 
 |-  H = ( j e. NN |-> [_ ( K ` j ) / k ]_ B )
5 prodmolem3.5 
 |-  ( ph -> ( M e. NN /\ N e. NN ) )
6 prodmolem3.6 
 |-  ( ph -> f : ( 1 ... M ) -1-1-onto-> A )
7 prodmolem3.7 
 |-  ( ph -> K : ( 1 ... N ) -1-1-onto-> A )
8 mulcl 
 |-  ( ( m e. CC /\ j e. CC ) -> ( m x. j ) e. CC )
9 8 adantl 
 |-  ( ( ph /\ ( m e. CC /\ j e. CC ) ) -> ( m x. j ) e. CC )
10 mulcom 
 |-  ( ( m e. CC /\ j e. CC ) -> ( m x. j ) = ( j x. m ) )
11 10 adantl 
 |-  ( ( ph /\ ( m e. CC /\ j e. CC ) ) -> ( m x. j ) = ( j x. m ) )
12 mulass 
 |-  ( ( m e. CC /\ j e. CC /\ z e. CC ) -> ( ( m x. j ) x. z ) = ( m x. ( j x. z ) ) )
13 12 adantl 
 |-  ( ( ph /\ ( m e. CC /\ j e. CC /\ z e. CC ) ) -> ( ( m x. j ) x. z ) = ( m x. ( j x. z ) ) )
14 5 simpld 
 |-  ( ph -> M e. NN )
15 nnuz 
 |-  NN = ( ZZ>= ` 1 )
16 14 15 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 1 ) )
17 ssidd 
 |-  ( ph -> CC C_ CC )
18 f1ocnv 
 |-  ( f : ( 1 ... M ) -1-1-onto-> A -> `' f : A -1-1-onto-> ( 1 ... M ) )
19 6 18 syl 
 |-  ( ph -> `' f : A -1-1-onto-> ( 1 ... M ) )
20 f1oco 
 |-  ( ( `' f : A -1-1-onto-> ( 1 ... M ) /\ K : ( 1 ... N ) -1-1-onto-> A ) -> ( `' f o. K ) : ( 1 ... N ) -1-1-onto-> ( 1 ... M ) )
21 19 7 20 syl2anc 
 |-  ( ph -> ( `' f o. K ) : ( 1 ... N ) -1-1-onto-> ( 1 ... M ) )
22 ovex 
 |-  ( 1 ... N ) e. _V
23 22 f1oen 
 |-  ( ( `' f o. K ) : ( 1 ... N ) -1-1-onto-> ( 1 ... M ) -> ( 1 ... N ) ~~ ( 1 ... M ) )
24 21 23 syl 
 |-  ( ph -> ( 1 ... N ) ~~ ( 1 ... M ) )
25 fzfi 
 |-  ( 1 ... N ) e. Fin
26 fzfi 
 |-  ( 1 ... M ) e. Fin
27 hashen 
 |-  ( ( ( 1 ... N ) e. Fin /\ ( 1 ... M ) e. Fin ) -> ( ( # ` ( 1 ... N ) ) = ( # ` ( 1 ... M ) ) <-> ( 1 ... N ) ~~ ( 1 ... M ) ) )
28 25 26 27 mp2an 
 |-  ( ( # ` ( 1 ... N ) ) = ( # ` ( 1 ... M ) ) <-> ( 1 ... N ) ~~ ( 1 ... M ) )
29 24 28 sylibr 
 |-  ( ph -> ( # ` ( 1 ... N ) ) = ( # ` ( 1 ... M ) ) )
30 5 simprd 
 |-  ( ph -> N e. NN )
31 30 nnnn0d 
 |-  ( ph -> N e. NN0 )
32 hashfz1 
 |-  ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
33 31 32 syl 
 |-  ( ph -> ( # ` ( 1 ... N ) ) = N )
34 14 nnnn0d 
 |-  ( ph -> M e. NN0 )
35 hashfz1 
 |-  ( M e. NN0 -> ( # ` ( 1 ... M ) ) = M )
36 34 35 syl 
 |-  ( ph -> ( # ` ( 1 ... M ) ) = M )
37 29 33 36 3eqtr3rd 
 |-  ( ph -> M = N )
38 37 oveq2d 
 |-  ( ph -> ( 1 ... M ) = ( 1 ... N ) )
39 38 f1oeq2d 
 |-  ( ph -> ( ( `' f o. K ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) <-> ( `' f o. K ) : ( 1 ... N ) -1-1-onto-> ( 1 ... M ) ) )
40 21 39 mpbird 
 |-  ( ph -> ( `' f o. K ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
41 fveq2 
 |-  ( j = m -> ( f ` j ) = ( f ` m ) )
42 41 csbeq1d 
 |-  ( j = m -> [_ ( f ` j ) / k ]_ B = [_ ( f ` m ) / k ]_ B )
43 elfznn 
 |-  ( m e. ( 1 ... M ) -> m e. NN )
44 43 adantl 
 |-  ( ( ph /\ m e. ( 1 ... M ) ) -> m e. NN )
45 f1of 
 |-  ( f : ( 1 ... M ) -1-1-onto-> A -> f : ( 1 ... M ) --> A )
46 6 45 syl 
 |-  ( ph -> f : ( 1 ... M ) --> A )
47 46 ffvelrnda 
 |-  ( ( ph /\ m e. ( 1 ... M ) ) -> ( f ` m ) e. A )
48 2 ralrimiva 
 |-  ( ph -> A. k e. A B e. CC )
49 48 adantr 
 |-  ( ( ph /\ m e. ( 1 ... M ) ) -> A. k e. A B e. CC )
50 nfcsb1v 
 |-  F/_ k [_ ( f ` m ) / k ]_ B
51 50 nfel1 
 |-  F/ k [_ ( f ` m ) / k ]_ B e. CC
52 csbeq1a 
 |-  ( k = ( f ` m ) -> B = [_ ( f ` m ) / k ]_ B )
53 52 eleq1d 
 |-  ( k = ( f ` m ) -> ( B e. CC <-> [_ ( f ` m ) / k ]_ B e. CC ) )
54 51 53 rspc 
 |-  ( ( f ` m ) e. A -> ( A. k e. A B e. CC -> [_ ( f ` m ) / k ]_ B e. CC ) )
55 47 49 54 sylc 
 |-  ( ( ph /\ m e. ( 1 ... M ) ) -> [_ ( f ` m ) / k ]_ B e. CC )
56 3 42 44 55 fvmptd3 
 |-  ( ( ph /\ m e. ( 1 ... M ) ) -> ( G ` m ) = [_ ( f ` m ) / k ]_ B )
57 56 55 eqeltrd 
 |-  ( ( ph /\ m e. ( 1 ... M ) ) -> ( G ` m ) e. CC )
58 38 f1oeq2d 
 |-  ( ph -> ( K : ( 1 ... M ) -1-1-onto-> A <-> K : ( 1 ... N ) -1-1-onto-> A ) )
59 7 58 mpbird 
 |-  ( ph -> K : ( 1 ... M ) -1-1-onto-> A )
60 f1of 
 |-  ( K : ( 1 ... M ) -1-1-onto-> A -> K : ( 1 ... M ) --> A )
61 59 60 syl 
 |-  ( ph -> K : ( 1 ... M ) --> A )
62 fvco3 
 |-  ( ( K : ( 1 ... M ) --> A /\ i e. ( 1 ... M ) ) -> ( ( `' f o. K ) ` i ) = ( `' f ` ( K ` i ) ) )
63 61 62 sylan 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( `' f o. K ) ` i ) = ( `' f ` ( K ` i ) ) )
64 63 fveq2d 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( f ` ( ( `' f o. K ) ` i ) ) = ( f ` ( `' f ` ( K ` i ) ) ) )
65 6 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> f : ( 1 ... M ) -1-1-onto-> A )
66 61 ffvelrnda 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( K ` i ) e. A )
67 f1ocnvfv2 
 |-  ( ( f : ( 1 ... M ) -1-1-onto-> A /\ ( K ` i ) e. A ) -> ( f ` ( `' f ` ( K ` i ) ) ) = ( K ` i ) )
68 65 66 67 syl2anc 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( f ` ( `' f ` ( K ` i ) ) ) = ( K ` i ) )
69 64 68 eqtrd 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( f ` ( ( `' f o. K ) ` i ) ) = ( K ` i ) )
70 69 csbeq1d 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> [_ ( f ` ( ( `' f o. K ) ` i ) ) / k ]_ B = [_ ( K ` i ) / k ]_ B )
71 70 fveq2d 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( _I ` [_ ( f ` ( ( `' f o. K ) ` i ) ) / k ]_ B ) = ( _I ` [_ ( K ` i ) / k ]_ B ) )
72 f1of 
 |-  ( ( `' f o. K ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) -> ( `' f o. K ) : ( 1 ... M ) --> ( 1 ... M ) )
73 40 72 syl 
 |-  ( ph -> ( `' f o. K ) : ( 1 ... M ) --> ( 1 ... M ) )
74 73 ffvelrnda 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( `' f o. K ) ` i ) e. ( 1 ... M ) )
75 elfznn 
 |-  ( ( ( `' f o. K ) ` i ) e. ( 1 ... M ) -> ( ( `' f o. K ) ` i ) e. NN )
76 fveq2 
 |-  ( j = ( ( `' f o. K ) ` i ) -> ( f ` j ) = ( f ` ( ( `' f o. K ) ` i ) ) )
77 76 csbeq1d 
 |-  ( j = ( ( `' f o. K ) ` i ) -> [_ ( f ` j ) / k ]_ B = [_ ( f ` ( ( `' f o. K ) ` i ) ) / k ]_ B )
78 77 3 fvmpti 
 |-  ( ( ( `' f o. K ) ` i ) e. NN -> ( G ` ( ( `' f o. K ) ` i ) ) = ( _I ` [_ ( f ` ( ( `' f o. K ) ` i ) ) / k ]_ B ) )
79 74 75 78 3syl 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( G ` ( ( `' f o. K ) ` i ) ) = ( _I ` [_ ( f ` ( ( `' f o. K ) ` i ) ) / k ]_ B ) )
80 elfznn 
 |-  ( i e. ( 1 ... M ) -> i e. NN )
81 80 adantl 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> i e. NN )
82 fveq2 
 |-  ( j = i -> ( K ` j ) = ( K ` i ) )
83 82 csbeq1d 
 |-  ( j = i -> [_ ( K ` j ) / k ]_ B = [_ ( K ` i ) / k ]_ B )
84 83 4 fvmpti 
 |-  ( i e. NN -> ( H ` i ) = ( _I ` [_ ( K ` i ) / k ]_ B ) )
85 81 84 syl 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( H ` i ) = ( _I ` [_ ( K ` i ) / k ]_ B ) )
86 71 79 85 3eqtr4rd 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( H ` i ) = ( G ` ( ( `' f o. K ) ` i ) ) )
87 9 11 13 16 17 40 57 86 seqf1o 
 |-  ( ph -> ( seq 1 ( x. , H ) ` M ) = ( seq 1 ( x. , G ) ` M ) )
88 37 fveq2d 
 |-  ( ph -> ( seq 1 ( x. , H ) ` M ) = ( seq 1 ( x. , H ) ` N ) )
89 87 88 eqtr3d 
 |-  ( ph -> ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , H ) ` N ) )