Metamath Proof Explorer

Theorem metakunt21

Description: Show that B coincides on the union of bijections of functions. (Contributed by metakunt, 28-May-2024)

Ref Expression
Hypotheses metakunt21.1 
|- ( ph -> M e. NN )
metakunt21.2 
|- ( ph -> I e. NN )
metakunt21.3 
|- ( ph -> I <_ M )
metakunt21.4 
|- B = ( x e. ( 1 ... M ) |-> if ( x = M , M , if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) ) )
metakunt21.5 
|- C = ( x e. ( 1 ... ( I - 1 ) ) |-> ( x + ( M - I ) ) )
metakunt21.6 
|- D = ( x e. ( I ... ( M - 1 ) ) |-> ( x + ( 1 - I ) ) )
metakunt21.7 
|- ( ph -> X e. ( 1 ... M ) )
metakunt21.8 
|- ( ph -> -. X = M )
metakunt21.9 
|- ( ph -> X < I )
Assertion metakunt21 
|- ( ph -> ( B ` X ) = ( ( ( C u. D ) u. { <. M , M >. } ) ` X ) )

Proof

Step Hyp Ref Expression
1 metakunt21.1 
 |-  ( ph -> M e. NN )
2 metakunt21.2 
 |-  ( ph -> I e. NN )
3 metakunt21.3 
 |-  ( ph -> I <_ M )
4 metakunt21.4 
 |-  B = ( x e. ( 1 ... M ) |-> if ( x = M , M , if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) ) )
5 metakunt21.5 
 |-  C = ( x e. ( 1 ... ( I - 1 ) ) |-> ( x + ( M - I ) ) )
6 metakunt21.6 
 |-  D = ( x e. ( I ... ( M - 1 ) ) |-> ( x + ( 1 - I ) ) )
7 metakunt21.7 
 |-  ( ph -> X e. ( 1 ... M ) )
8 metakunt21.8 
 |-  ( ph -> -. X = M )
9 metakunt21.9 
 |-  ( ph -> X < I )
10 4 a1i 
 |-  ( ph -> B = ( x e. ( 1 ... M ) |-> if ( x = M , M , if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) ) ) )
11 eqeq1 
 |-  ( x = X -> ( x = M <-> X = M ) )
12 breq1 
 |-  ( x = X -> ( x < I <-> X < I ) )
13 oveq1 
 |-  ( x = X -> ( x + ( M - I ) ) = ( X + ( M - I ) ) )
14 oveq1 
 |-  ( x = X -> ( x + ( 1 - I ) ) = ( X + ( 1 - I ) ) )
15 12 13 14 ifbieq12d 
 |-  ( x = X -> if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) = if ( X < I , ( X + ( M - I ) ) , ( X + ( 1 - I ) ) ) )
16 11 15 ifbieq2d 
 |-  ( x = X -> if ( x = M , M , if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) ) = if ( X = M , M , if ( X < I , ( X + ( M - I ) ) , ( X + ( 1 - I ) ) ) ) )
17 16 adantl 
 |-  ( ( ph /\ x = X ) -> if ( x = M , M , if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) ) = if ( X = M , M , if ( X < I , ( X + ( M - I ) ) , ( X + ( 1 - I ) ) ) ) )
18 8 iffalsed 
 |-  ( ph -> if ( X = M , M , if ( X < I , ( X + ( M - I ) ) , ( X + ( 1 - I ) ) ) ) = if ( X < I , ( X + ( M - I ) ) , ( X + ( 1 - I ) ) ) )
19 9 iftrued 
 |-  ( ph -> if ( X < I , ( X + ( M - I ) ) , ( X + ( 1 - I ) ) ) = ( X + ( M - I ) ) )
20 18 19 eqtrd 
 |-  ( ph -> if ( X = M , M , if ( X < I , ( X + ( M - I ) ) , ( X + ( 1 - I ) ) ) ) = ( X + ( M - I ) ) )
21 20 adantr 
 |-  ( ( ph /\ x = X ) -> if ( X = M , M , if ( X < I , ( X + ( M - I ) ) , ( X + ( 1 - I ) ) ) ) = ( X + ( M - I ) ) )
22 17 21 eqtrd 
 |-  ( ( ph /\ x = X ) -> if ( x = M , M , if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) ) = ( X + ( M - I ) ) )
23 7 elfzelzd 
 |-  ( ph -> X e. ZZ )
24 1 nnzd 
 |-  ( ph -> M e. ZZ )
25 2 nnzd 
 |-  ( ph -> I e. ZZ )
26 24 25 zsubcld 
 |-  ( ph -> ( M - I ) e. ZZ )
27 23 26 zaddcld 
 |-  ( ph -> ( X + ( M - I ) ) e. ZZ )
28 10 22 7 27 fvmptd 
 |-  ( ph -> ( B ` X ) = ( X + ( M - I ) ) )
29 1 2 3 4 5 6 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 } ) )
30 29 simpld 
 |-  ( ph -> ( C Fn ( 1 ... ( I - 1 ) ) /\ D Fn ( I ... ( M - 1 ) ) /\ ( C u. D ) Fn ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) ) )
31 30 simp3d 
 |-  ( ph -> ( C u. D ) Fn ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) )
32 29 simprd 
 |-  ( ph -> { <. M , M >. } Fn { M } )
33 indir 
 |-  ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) i^i { M } ) = ( ( ( 1 ... ( I - 1 ) ) i^i { M } ) u. ( ( I ... ( M - 1 ) ) i^i { M } ) )
34 33 a1i 
 |-  ( ph -> ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) i^i { M } ) = ( ( ( 1 ... ( I - 1 ) ) i^i { M } ) u. ( ( I ... ( M - 1 ) ) i^i { M } ) ) )
35 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 } ) = (/) ) ) )
36 35 simpld 
 |-  ( ph -> ( ( ( 1 ... ( I - 1 ) ) i^i ( I ... ( M - 1 ) ) ) = (/) /\ ( ( 1 ... ( I - 1 ) ) i^i { M } ) = (/) /\ ( ( I ... ( M - 1 ) ) i^i { M } ) = (/) ) )
37 36 simp2d 
 |-  ( ph -> ( ( 1 ... ( I - 1 ) ) i^i { M } ) = (/) )
38 36 simp3d 
 |-  ( ph -> ( ( I ... ( M - 1 ) ) i^i { M } ) = (/) )
39 37 38 uneq12d 
 |-  ( ph -> ( ( ( 1 ... ( I - 1 ) ) i^i { M } ) u. ( ( I ... ( M - 1 ) ) i^i { M } ) ) = ( (/) u. (/) ) )
40 unidm 
 |-  ( (/) u. (/) ) = (/)
41 40 a1i 
 |-  ( ph -> ( (/) u. (/) ) = (/) )
42 39 41 eqtrd 
 |-  ( ph -> ( ( ( 1 ... ( I - 1 ) ) i^i { M } ) u. ( ( I ... ( M - 1 ) ) i^i { M } ) ) = (/) )
43 34 42 eqtrd 
 |-  ( ph -> ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) i^i { M } ) = (/) )
44 1zzd 
 |-  ( ph -> 1 e. ZZ )
45 25 44 zsubcld 
 |-  ( ph -> ( I - 1 ) e. ZZ )
46 elfznn 
 |-  ( X e. ( 1 ... M ) -> X e. NN )
47 7 46 syl 
 |-  ( ph -> X e. NN )
48 47 nnge1d 
 |-  ( ph -> 1 <_ X )
49 zltlem1 
 |-  ( ( X e. ZZ /\ I e. ZZ ) -> ( X < I <-> X <_ ( I - 1 ) ) )
50 23 25 49 syl2anc 
 |-  ( ph -> ( X < I <-> X <_ ( I - 1 ) ) )
51 9 50 mpbid 
 |-  ( ph -> X <_ ( I - 1 ) )
52 44 45 23 48 51 elfzd 
 |-  ( ph -> X e. ( 1 ... ( I - 1 ) ) )
53 elun1 
 |-  ( X e. ( 1 ... ( I - 1 ) ) -> X e. ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) )
54 52 53 syl 
 |-  ( ph -> X e. ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) )
55 31 32 43 54 fvun1d 
 |-  ( ph -> ( ( ( C u. D ) u. { <. M , M >. } ) ` X ) = ( ( C u. D ) ` X ) )
56 30 simp1d 
 |-  ( ph -> C Fn ( 1 ... ( I - 1 ) ) )
57 30 simp2d 
 |-  ( ph -> D Fn ( I ... ( M - 1 ) ) )
58 36 simp1d 
 |-  ( ph -> ( ( 1 ... ( I - 1 ) ) i^i ( I ... ( M - 1 ) ) ) = (/) )
59 56 57 58 52 fvun1d 
 |-  ( ph -> ( ( C u. D ) ` X ) = ( C ` X ) )
60 5 a1i 
 |-  ( ph -> C = ( x e. ( 1 ... ( I - 1 ) ) |-> ( x + ( M - I ) ) ) )
61 13 adantl 
 |-  ( ( ph /\ x = X ) -> ( x + ( M - I ) ) = ( X + ( M - I ) ) )
62 60 61 52 27 fvmptd 
 |-  ( ph -> ( C ` X ) = ( X + ( M - I ) ) )
63 59 62 eqtrd 
 |-  ( ph -> ( ( C u. D ) ` X ) = ( X + ( M - I ) ) )
64 55 63 eqtrd 
 |-  ( ph -> ( ( ( C u. D ) u. { <. M , M >. } ) ` X ) = ( X + ( M - I ) ) )
65 64 eqcomd 
 |-  ( ph -> ( X + ( M - I ) ) = ( ( ( C u. D ) u. { <. M , M >. } ) ` X ) )
66 28 65 eqtrd 
 |-  ( ph -> ( B ` X ) = ( ( ( C u. D ) u. { <. M , M >. } ) ` X ) )