Metamath Proof Explorer

Theorem metakunt33

Description: Construction of one solution of the increment equation system. (Contributed by metakunt, 18-Jul-2024)

Ref Expression
Hypotheses metakunt33.1 
|- ( ph -> M e. NN )
metakunt33.2 
|- ( ph -> I e. NN )
metakunt33.3 
|- ( ph -> I <_ M )
metakunt33.4 
|- A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
metakunt33.5 
|- B = ( z e. ( 1 ... M ) |-> if ( z = M , M , if ( z < I , ( z + ( M - I ) ) , ( z + ( 1 - I ) ) ) ) )
metakunt33.6 
|- C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) )
metakunt33.7 
|- D = ( w e. ( 1 ... M ) |-> if ( w = I , w , if ( w < I , ( ( w + ( M - I ) ) + if ( I <_ ( w + ( M - I ) ) , 1 , 0 ) ) , ( ( w - I ) + if ( I <_ ( w - I ) , 1 , 0 ) ) ) ) )
Assertion metakunt33 
|- ( ph -> ( C o. ( B o. A ) ) = D )

Proof

Step Hyp Ref Expression
1 metakunt33.1 
 |-  ( ph -> M e. NN )
2 metakunt33.2 
 |-  ( ph -> I e. NN )
3 metakunt33.3 
 |-  ( ph -> I <_ M )
4 metakunt33.4 
 |-  A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
5 metakunt33.5 
 |-  B = ( z e. ( 1 ... M ) |-> if ( z = M , M , if ( z < I , ( z + ( M - I ) ) , ( z + ( 1 - I ) ) ) ) )
6 metakunt33.6 
 |-  C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) )
7 metakunt33.7 
 |-  D = ( w e. ( 1 ... M ) |-> if ( w = I , w , if ( w < I , ( ( w + ( M - I ) ) + if ( I <_ ( w + ( M - I ) ) , 1 , 0 ) ) , ( ( w - I ) + if ( I <_ ( w - I ) , 1 , 0 ) ) ) ) )
8 1 2 3 6 metakunt2 
 |-  ( ph -> C : ( 1 ... M ) --> ( 1 ... M ) )
9 1 2 3 5 metakunt25 
 |-  ( ph -> B : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
10 f1of 
 |-  ( B : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) -> B : ( 1 ... M ) --> ( 1 ... M ) )
11 9 10 syl 
 |-  ( ph -> B : ( 1 ... M ) --> ( 1 ... M ) )
12 1 2 3 4 metakunt1 
 |-  ( ph -> A : ( 1 ... M ) --> ( 1 ... M ) )
13 11 12 fcod 
 |-  ( ph -> ( B o. A ) : ( 1 ... M ) --> ( 1 ... M ) )
14 8 13 fcod 
 |-  ( ph -> ( C o. ( B o. A ) ) : ( 1 ... M ) --> ( 1 ... M ) )
15 14 ffnd 
 |-  ( ph -> ( C o. ( B o. A ) ) Fn ( 1 ... M ) )
16 nfv 
 |-  F/ w ph
17 elfzelz 
 |-  ( w e. ( 1 ... M ) -> w e. ZZ )
18 17 adantl 
 |-  ( ( ph /\ w e. ( 1 ... M ) ) -> w e. ZZ )
19 1 nnzd 
 |-  ( ph -> M e. ZZ )
20 19 adantr 
 |-  ( ( ph /\ w e. ( 1 ... M ) ) -> M e. ZZ )
21 2 nnzd 
 |-  ( ph -> I e. ZZ )
22 21 adantr 
 |-  ( ( ph /\ w e. ( 1 ... M ) ) -> I e. ZZ )
23 20 22 zsubcld 
 |-  ( ( ph /\ w e. ( 1 ... M ) ) -> ( M - I ) e. ZZ )
24 18 23 zaddcld 
 |-  ( ( ph /\ w e. ( 1 ... M ) ) -> ( w + ( M - I ) ) e. ZZ )
25 1zzd 
 |-  ( ( ph /\ w e. ( 1 ... M ) ) -> 1 e. ZZ )
26 0zd 
 |-  ( ( ph /\ w e. ( 1 ... M ) ) -> 0 e. ZZ )
27 25 26 ifcld 
 |-  ( ( ph /\ w e. ( 1 ... M ) ) -> if ( I <_ ( w + ( M - I ) ) , 1 , 0 ) e. ZZ )
28 24 27 zaddcld 
 |-  ( ( ph /\ w e. ( 1 ... M ) ) -> ( ( w + ( M - I ) ) + if ( I <_ ( w + ( M - I ) ) , 1 , 0 ) ) e. ZZ )
29 18 22 zsubcld 
 |-  ( ( ph /\ w e. ( 1 ... M ) ) -> ( w - I ) e. ZZ )
30 25 26 ifcld 
 |-  ( ( ph /\ w e. ( 1 ... M ) ) -> if ( I <_ ( w - I ) , 1 , 0 ) e. ZZ )
31 29 30 zaddcld 
 |-  ( ( ph /\ w e. ( 1 ... M ) ) -> ( ( w - I ) + if ( I <_ ( w - I ) , 1 , 0 ) ) e. ZZ )
32 28 31 ifcld 
 |-  ( ( ph /\ w e. ( 1 ... M ) ) -> if ( w < I , ( ( w + ( M - I ) ) + if ( I <_ ( w + ( M - I ) ) , 1 , 0 ) ) , ( ( w - I ) + if ( I <_ ( w - I ) , 1 , 0 ) ) ) e. ZZ )
33 18 32 ifcld 
 |-  ( ( ph /\ w e. ( 1 ... M ) ) -> if ( w = I , w , if ( w < I , ( ( w + ( M - I ) ) + if ( I <_ ( w + ( M - I ) ) , 1 , 0 ) ) , ( ( w - I ) + if ( I <_ ( w - I ) , 1 , 0 ) ) ) ) e. ZZ )
34 16 33 7 fnmptd 
 |-  ( ph -> D Fn ( 1 ... M ) )
35 13 adantr 
 |-  ( ( ph /\ a e. ( 1 ... M ) ) -> ( B o. A ) : ( 1 ... M ) --> ( 1 ... M ) )
36 simpr 
 |-  ( ( ph /\ a e. ( 1 ... M ) ) -> a e. ( 1 ... M ) )
37 35 36 fvco3d 
 |-  ( ( ph /\ a e. ( 1 ... M ) ) -> ( ( C o. ( B o. A ) ) ` a ) = ( C ` ( ( B o. A ) ` a ) ) )
38 12 adantr 
 |-  ( ( ph /\ a e. ( 1 ... M ) ) -> A : ( 1 ... M ) --> ( 1 ... M ) )
39 38 36 fvco3d 
 |-  ( ( ph /\ a e. ( 1 ... M ) ) -> ( ( B o. A ) ` a ) = ( B ` ( A ` a ) ) )
40 39 fveq2d 
 |-  ( ( ph /\ a e. ( 1 ... M ) ) -> ( C ` ( ( B o. A ) ` a ) ) = ( C ` ( B ` ( A ` a ) ) ) )
41 37 40 eqtrd 
 |-  ( ( ph /\ a e. ( 1 ... M ) ) -> ( ( C o. ( B o. A ) ) ` a ) = ( C ` ( B ` ( A ` a ) ) ) )
42 1 adantr 
 |-  ( ( ph /\ a e. ( 1 ... M ) ) -> M e. NN )
43 2 adantr 
 |-  ( ( ph /\ a e. ( 1 ... M ) ) -> I e. NN )
44 3 adantr 
 |-  ( ( ph /\ a e. ( 1 ... M ) ) -> I <_ M )
45 eqid 
 |-  if ( I <_ ( a + ( M - I ) ) , 1 , 0 ) = if ( I <_ ( a + ( M - I ) ) , 1 , 0 )
46 eqid 
 |-  if ( I <_ ( a - I ) , 1 , 0 ) = if ( I <_ ( a - I ) , 1 , 0 )
47 eqid 
 |-  if ( a = I , a , if ( a < I , ( ( a + ( M - I ) ) + if ( I <_ ( a + ( M - I ) ) , 1 , 0 ) ) , ( ( a - I ) + if ( I <_ ( a - I ) , 1 , 0 ) ) ) ) = if ( a = I , a , if ( a < I , ( ( a + ( M - I ) ) + if ( I <_ ( a + ( M - I ) ) , 1 , 0 ) ) , ( ( a - I ) + if ( I <_ ( a - I ) , 1 , 0 ) ) ) )
48 42 43 44 36 4 5 6 45 46 47 metakunt31 
 |-  ( ( ph /\ a e. ( 1 ... M ) ) -> ( C ` ( B ` ( A ` a ) ) ) = if ( a = I , a , if ( a < I , ( ( a + ( M - I ) ) + if ( I <_ ( a + ( M - I ) ) , 1 , 0 ) ) , ( ( a - I ) + if ( I <_ ( a - I ) , 1 , 0 ) ) ) ) )
49 42 43 44 36 7 45 46 47 metakunt32 
 |-  ( ( ph /\ a e. ( 1 ... M ) ) -> ( D ` a ) = if ( a = I , a , if ( a < I , ( ( a + ( M - I ) ) + if ( I <_ ( a + ( M - I ) ) , 1 , 0 ) ) , ( ( a - I ) + if ( I <_ ( a - I ) , 1 , 0 ) ) ) ) )
50 49 eqcomd 
 |-  ( ( ph /\ a e. ( 1 ... M ) ) -> if ( a = I , a , if ( a < I , ( ( a + ( M - I ) ) + if ( I <_ ( a + ( M - I ) ) , 1 , 0 ) ) , ( ( a - I ) + if ( I <_ ( a - I ) , 1 , 0 ) ) ) ) = ( D ` a ) )
51 48 50 eqtrd 
 |-  ( ( ph /\ a e. ( 1 ... M ) ) -> ( C ` ( B ` ( A ` a ) ) ) = ( D ` a ) )
52 41 51 eqtrd 
 |-  ( ( ph /\ a e. ( 1 ... M ) ) -> ( ( C o. ( B o. A ) ) ` a ) = ( D ` a ) )
53 15 34 52 eqfnfvd 
 |-  ( ph -> ( C o. ( B o. A ) ) = D )