Metamath Proof Explorer

Theorem metakunt19

Description: Domains on restrictions of functions. (Contributed by metakunt, 28-May-2024)

Ref Expression
Hypotheses metakunt19.1 
|- ( ph -> M e. NN )
metakunt19.2 
|- ( ph -> I e. NN )
metakunt19.3 
|- ( ph -> I <_ M )
metakunt19.4 
|- B = ( x e. ( 1 ... M ) |-> if ( x = M , M , if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) ) )
metakunt19.5 
|- C = ( x e. ( 1 ... ( I - 1 ) ) |-> ( x + ( M - I ) ) )
metakunt19.6 
|- D = ( x e. ( I ... ( M - 1 ) ) |-> ( x + ( 1 - I ) ) )
Assertion metakunt19 
|- ( ph -> ( ( C Fn ( 1 ... ( I - 1 ) ) /\ D Fn ( I ... ( M - 1 ) ) /\ ( C u. D ) Fn ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) ) /\ { <. M , M >. } Fn { M } ) )

Proof

Step Hyp Ref Expression
1 metakunt19.1 
 |-  ( ph -> M e. NN )
2 metakunt19.2 
 |-  ( ph -> I e. NN )
3 metakunt19.3 
 |-  ( ph -> I <_ M )
4 metakunt19.4 
 |-  B = ( x e. ( 1 ... M ) |-> if ( x = M , M , if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) ) )
5 metakunt19.5 
 |-  C = ( x e. ( 1 ... ( I - 1 ) ) |-> ( x + ( M - I ) ) )
6 metakunt19.6 
 |-  D = ( x e. ( I ... ( M - 1 ) ) |-> ( x + ( 1 - I ) ) )
7 elfzelz 
 |-  ( x e. ( 1 ... ( I - 1 ) ) -> x e. ZZ )
8 7 adantl 
 |-  ( ( ph /\ x e. ( 1 ... ( I - 1 ) ) ) -> x e. ZZ )
9 1 nnzd 
 |-  ( ph -> M e. ZZ )
10 9 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( I - 1 ) ) ) -> M e. ZZ )
11 2 nnzd 
 |-  ( ph -> I e. ZZ )
12 11 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( I - 1 ) ) ) -> I e. ZZ )
13 10 12 zsubcld 
 |-  ( ( ph /\ x e. ( 1 ... ( I - 1 ) ) ) -> ( M - I ) e. ZZ )
14 8 13 zaddcld 
 |-  ( ( ph /\ x e. ( 1 ... ( I - 1 ) ) ) -> ( x + ( M - I ) ) e. ZZ )
15 14 5 fmptd 
 |-  ( ph -> C : ( 1 ... ( I - 1 ) ) --> ZZ )
16 15 ffnd 
 |-  ( ph -> C Fn ( 1 ... ( I - 1 ) ) )
17 elfzelz 
 |-  ( x e. ( I ... ( M - 1 ) ) -> x e. ZZ )
18 17 adantl 
 |-  ( ( ph /\ x e. ( I ... ( M - 1 ) ) ) -> x e. ZZ )
19 1zzd 
 |-  ( ( ph /\ x e. ( I ... ( M - 1 ) ) ) -> 1 e. ZZ )
20 11 adantr 
 |-  ( ( ph /\ x e. ( I ... ( M - 1 ) ) ) -> I e. ZZ )
21 19 20 zsubcld 
 |-  ( ( ph /\ x e. ( I ... ( M - 1 ) ) ) -> ( 1 - I ) e. ZZ )
22 18 21 zaddcld 
 |-  ( ( ph /\ x e. ( I ... ( M - 1 ) ) ) -> ( x + ( 1 - I ) ) e. ZZ )
23 22 6 fmptd 
 |-  ( ph -> D : ( I ... ( M - 1 ) ) --> ZZ )
24 23 ffnd 
 |-  ( ph -> D Fn ( I ... ( M - 1 ) ) )
25 1 2 3 metakunt18 
 |-  ( ph -> ( ( ( ( 1 ... ( I - 1 ) ) i^i ( I ... ( M - 1 ) ) ) = (/) /\ ( ( 1 ... ( I - 1 ) ) i^i { M } ) = (/) /\ ( ( I ... ( M - 1 ) ) i^i { M } ) = (/) ) /\ ( ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) i^i ( 1 ... ( M - I ) ) ) = (/) /\ ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) i^i { M } ) = (/) /\ ( ( 1 ... ( M - I ) ) i^i { M } ) = (/) ) ) )
26 25 simpld 
 |-  ( ph -> ( ( ( 1 ... ( I - 1 ) ) i^i ( I ... ( M - 1 ) ) ) = (/) /\ ( ( 1 ... ( I - 1 ) ) i^i { M } ) = (/) /\ ( ( I ... ( M - 1 ) ) i^i { M } ) = (/) ) )
27 26 simp1d 
 |-  ( ph -> ( ( 1 ... ( I - 1 ) ) i^i ( I ... ( M - 1 ) ) ) = (/) )
28 16 24 27 fnund 
 |-  ( ph -> ( C u. D ) Fn ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) )
29 16 24 28 3jca 
 |-  ( ph -> ( C Fn ( 1 ... ( I - 1 ) ) /\ D Fn ( I ... ( M - 1 ) ) /\ ( C u. D ) Fn ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) ) )
30 fnsng 
 |-  ( ( M e. NN /\ M e. NN ) -> { <. M , M >. } Fn { M } )
31 1 1 30 syl2anc 
 |-  ( ph -> { <. M , M >. } Fn { M } )
32 29 31 jca 
 |-  ( ph -> ( ( C Fn ( 1 ... ( I - 1 ) ) /\ D Fn ( I ... ( M - 1 ) ) /\ ( C u. D ) Fn ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) ) /\ { <. M , M >. } Fn { M } ) )