Metamath Proof Explorer

Theorem metakunt22

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

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

Proof

Step Hyp Ref Expression
1 metakunt22.1 
 |-  ( ph -> M e. NN )
2 metakunt22.2 
 |-  ( ph -> I e. NN )
3 metakunt22.3 
 |-  ( ph -> I <_ M )
4 metakunt22.4 
 |-  B = ( x e. ( 1 ... M ) |-> if ( x = M , M , if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) ) )
5 metakunt22.5 
 |-  C = ( x e. ( 1 ... ( I - 1 ) ) |-> ( x + ( M - I ) ) )
6 metakunt22.6 
 |-  D = ( x e. ( I ... ( M - 1 ) ) |-> ( x + ( 1 - I ) ) )
7 metakunt22.7 
 |-  ( ph -> X e. ( 1 ... M ) )
8 metakunt22.8 
 |-  ( ph -> -. X = M )
9 metakunt22.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 iffalse 
 |-  ( -. X = M -> if ( X = M , M , if ( X < I , ( X + ( M - I ) ) , ( X + ( 1 - I ) ) ) ) = if ( X < I , ( X + ( M - I ) ) , ( X + ( 1 - I ) ) ) )
19 8 18 syl 
 |-  ( ph -> if ( X = M , M , if ( X < I , ( X + ( M - I ) ) , ( X + ( 1 - I ) ) ) ) = if ( X < I , ( X + ( M - I ) ) , ( X + ( 1 - I ) ) ) )
20 iffalse 
 |-  ( -. X < I -> if ( X < I , ( X + ( M - I ) ) , ( X + ( 1 - I ) ) ) = ( X + ( 1 - I ) ) )
21 9 20 syl 
 |-  ( ph -> if ( X < I , ( X + ( M - I ) ) , ( X + ( 1 - I ) ) ) = ( X + ( 1 - I ) ) )
22 19 21 eqtrd 
 |-  ( ph -> if ( X = M , M , if ( X < I , ( X + ( M - I ) ) , ( X + ( 1 - I ) ) ) ) = ( X + ( 1 - I ) ) )
23 22 adantr 
 |-  ( ( ph /\ x = X ) -> if ( X = M , M , if ( X < I , ( X + ( M - I ) ) , ( X + ( 1 - I ) ) ) ) = ( X + ( 1 - I ) ) )
24 17 23 eqtrd 
 |-  ( ( ph /\ x = X ) -> if ( x = M , M , if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) ) = ( X + ( 1 - I ) ) )
25 7 elfzelzd 
 |-  ( ph -> X e. ZZ )
26 1zzd 
 |-  ( ph -> 1 e. ZZ )
27 2 nnzd 
 |-  ( ph -> I e. ZZ )
28 26 27 zsubcld 
 |-  ( ph -> ( 1 - I ) e. ZZ )
29 25 28 zaddcld 
 |-  ( ph -> ( X + ( 1 - I ) ) e. ZZ )
30 10 24 7 29 fvmptd 
 |-  ( ph -> ( B ` X ) = ( X + ( 1 - I ) ) )
31 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 } ) )
32 31 simpld 
 |-  ( ph -> ( C Fn ( 1 ... ( I - 1 ) ) /\ D Fn ( I ... ( M - 1 ) ) /\ ( C u. D ) Fn ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) ) )
33 32 simp3d 
 |-  ( ph -> ( C u. D ) Fn ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) )
34 31 simprd 
 |-  ( ph -> { <. M , M >. } Fn { M } )
35 indir 
 |-  ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) i^i { M } ) = ( ( ( 1 ... ( I - 1 ) ) i^i { M } ) u. ( ( I ... ( M - 1 ) ) i^i { M } ) )
36 35 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 } ) ) )
37 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 } ) = (/) ) ) )
38 37 simpld 
 |-  ( ph -> ( ( ( 1 ... ( I - 1 ) ) i^i ( I ... ( M - 1 ) ) ) = (/) /\ ( ( 1 ... ( I - 1 ) ) i^i { M } ) = (/) /\ ( ( I ... ( M - 1 ) ) i^i { M } ) = (/) ) )
39 38 simp2d 
 |-  ( ph -> ( ( 1 ... ( I - 1 ) ) i^i { M } ) = (/) )
40 38 simp3d 
 |-  ( ph -> ( ( I ... ( M - 1 ) ) i^i { M } ) = (/) )
41 39 40 uneq12d 
 |-  ( ph -> ( ( ( 1 ... ( I - 1 ) ) i^i { M } ) u. ( ( I ... ( M - 1 ) ) i^i { M } ) ) = ( (/) u. (/) ) )
42 unidm 
 |-  ( (/) u. (/) ) = (/)
43 42 a1i 
 |-  ( ph -> ( (/) u. (/) ) = (/) )
44 41 43 eqtrd 
 |-  ( ph -> ( ( ( 1 ... ( I - 1 ) ) i^i { M } ) u. ( ( I ... ( M - 1 ) ) i^i { M } ) ) = (/) )
45 36 44 eqtrd 
 |-  ( ph -> ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) i^i { M } ) = (/) )
46 1 nnzd 
 |-  ( ph -> M e. ZZ )
47 46 26 zsubcld 
 |-  ( ph -> ( M - 1 ) e. ZZ )
48 2 nnred 
 |-  ( ph -> I e. RR )
49 elfznn 
 |-  ( X e. ( 1 ... M ) -> X e. NN )
50 7 49 syl 
 |-  ( ph -> X e. NN )
51 50 nnred 
 |-  ( ph -> X e. RR )
52 48 51 lenltd 
 |-  ( ph -> ( I <_ X <-> -. X < I ) )
53 9 52 mpbird 
 |-  ( ph -> I <_ X )
54 elfzle2 
 |-  ( X e. ( 1 ... M ) -> X <_ M )
55 7 54 syl 
 |-  ( ph -> X <_ M )
56 df-ne 
 |-  ( X =/= M <-> -. X = M )
57 8 56 sylibr 
 |-  ( ph -> X =/= M )
58 57 necomd 
 |-  ( ph -> M =/= X )
59 55 58 jca 
 |-  ( ph -> ( X <_ M /\ M =/= X ) )
60 1 nnred 
 |-  ( ph -> M e. RR )
61 51 60 ltlend 
 |-  ( ph -> ( X < M <-> ( X <_ M /\ M =/= X ) ) )
62 59 61 mpbird 
 |-  ( ph -> X < M )
63 zltlem1 
 |-  ( ( X e. ZZ /\ M e. ZZ ) -> ( X < M <-> X <_ ( M - 1 ) ) )
64 25 46 63 syl2anc 
 |-  ( ph -> ( X < M <-> X <_ ( M - 1 ) ) )
65 62 64 mpbid 
 |-  ( ph -> X <_ ( M - 1 ) )
66 27 47 25 53 65 elfzd 
 |-  ( ph -> X e. ( I ... ( M - 1 ) ) )
67 elun2 
 |-  ( X e. ( I ... ( M - 1 ) ) -> X e. ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) )
68 66 67 syl 
 |-  ( ph -> X e. ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) )
69 33 34 45 68 fvun1d 
 |-  ( ph -> ( ( ( C u. D ) u. { <. M , M >. } ) ` X ) = ( ( C u. D ) ` X ) )
70 32 simp1d 
 |-  ( ph -> C Fn ( 1 ... ( I - 1 ) ) )
71 32 simp2d 
 |-  ( ph -> D Fn ( I ... ( M - 1 ) ) )
72 38 simp1d 
 |-  ( ph -> ( ( 1 ... ( I - 1 ) ) i^i ( I ... ( M - 1 ) ) ) = (/) )
73 70 71 72 66 fvun2d 
 |-  ( ph -> ( ( C u. D ) ` X ) = ( D ` X ) )
74 6 a1i 
 |-  ( ph -> D = ( x e. ( I ... ( M - 1 ) ) |-> ( x + ( 1 - I ) ) ) )
75 simpr 
 |-  ( ( ph /\ x = X ) -> x = X )
76 75 oveq1d 
 |-  ( ( ph /\ x = X ) -> ( x + ( 1 - I ) ) = ( X + ( 1 - I ) ) )
77 25 zred 
 |-  ( ph -> X e. RR )
78 lenlt 
 |-  ( ( I e. RR /\ X e. RR ) -> ( I <_ X <-> -. X < I ) )
79 48 77 78 syl2anc 
 |-  ( ph -> ( I <_ X <-> -. X < I ) )
80 9 79 mpbird 
 |-  ( ph -> I <_ X )
81 77 60 ltlend 
 |-  ( ph -> ( X < M <-> ( X <_ M /\ M =/= X ) ) )
82 59 81 mpbird 
 |-  ( ph -> X < M )
83 82 64 mpbid 
 |-  ( ph -> X <_ ( M - 1 ) )
84 27 47 25 80 83 elfzd 
 |-  ( ph -> X e. ( I ... ( M - 1 ) ) )
85 74 76 84 29 fvmptd 
 |-  ( ph -> ( D ` X ) = ( X + ( 1 - I ) ) )
86 73 85 eqtrd 
 |-  ( ph -> ( ( C u. D ) ` X ) = ( X + ( 1 - I ) ) )
87 69 86 eqtrd 
 |-  ( ph -> ( ( ( C u. D ) u. { <. M , M >. } ) ` X ) = ( X + ( 1 - I ) ) )
88 87 eqcomd 
 |-  ( ph -> ( X + ( 1 - I ) ) = ( ( ( C u. D ) u. { <. M , M >. } ) ` X ) )
89 30 88 eqtrd 
 |-  ( ph -> ( B ` X ) = ( ( ( C u. D ) u. { <. M , M >. } ) ` X ) )