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 elfznn 
 |-  ( X e. ( 1 ... M ) -> X e. NN )
49 7 48 syl 
 |-  ( ph -> X e. NN )
50 49 nnzd 
 |-  ( ph -> X e. ZZ )
51 2 nnred 
 |-  ( ph -> I e. RR )
52 49 nnred 
 |-  ( ph -> X e. RR )
53 51 52 lenltd 
 |-  ( ph -> ( I <_ X <-> -. X < I ) )
54 9 53 mpbird 
 |-  ( ph -> I <_ X )
55 elfzle2 
 |-  ( X e. ( 1 ... M ) -> X <_ M )
56 7 55 syl 
 |-  ( ph -> X <_ M )
57 df-ne 
 |-  ( X =/= M <-> -. X = M )
58 8 57 sylibr 
 |-  ( ph -> X =/= M )
59 58 necomd 
 |-  ( ph -> M =/= X )
60 56 59 jca 
 |-  ( ph -> ( X <_ M /\ M =/= X ) )
61 1 nnred 
 |-  ( ph -> M e. RR )
62 52 61 ltlend 
 |-  ( ph -> ( X < M <-> ( X <_ M /\ M =/= X ) ) )
63 60 62 mpbird 
 |-  ( ph -> X < M )
64 zltlem1 
 |-  ( ( X e. ZZ /\ M e. ZZ ) -> ( X < M <-> X <_ ( M - 1 ) ) )
65 50 46 64 syl2anc 
 |-  ( ph -> ( X < M <-> X <_ ( M - 1 ) ) )
66 63 65 mpbid 
 |-  ( ph -> X <_ ( M - 1 ) )
67 27 47 50 54 66 elfzd 
 |-  ( ph -> X e. ( I ... ( M - 1 ) ) )
68 elun2 
 |-  ( X e. ( I ... ( M - 1 ) ) -> X e. ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) )
69 67 68 syl 
 |-  ( ph -> X e. ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) )
70 33 34 45 69 fvun1d 
 |-  ( ph -> ( ( ( C u. D ) u. { <. M , M >. } ) ` X ) = ( ( C u. D ) ` X ) )
71 32 simp1d 
 |-  ( ph -> C Fn ( 1 ... ( I - 1 ) ) )
72 32 simp2d 
 |-  ( ph -> D Fn ( I ... ( M - 1 ) ) )
73 38 simp1d 
 |-  ( ph -> ( ( 1 ... ( I - 1 ) ) i^i ( I ... ( M - 1 ) ) ) = (/) )
74 71 72 73 67 fvun2d 
 |-  ( ph -> ( ( C u. D ) ` X ) = ( D ` X ) )
75 6 a1i 
 |-  ( ph -> D = ( x e. ( I ... ( M - 1 ) ) |-> ( x + ( 1 - I ) ) ) )
76 simpr 
 |-  ( ( ph /\ x = X ) -> x = X )
77 76 oveq1d 
 |-  ( ( ph /\ x = X ) -> ( x + ( 1 - I ) ) = ( X + ( 1 - I ) ) )
78 25 zred 
 |-  ( ph -> X e. RR )
79 lenlt 
 |-  ( ( I e. RR /\ X e. RR ) -> ( I <_ X <-> -. X < I ) )
80 51 78 79 syl2anc 
 |-  ( ph -> ( I <_ X <-> -. X < I ) )
81 9 80 mpbird 
 |-  ( ph -> I <_ X )
82 78 61 ltlend 
 |-  ( ph -> ( X < M <-> ( X <_ M /\ M =/= X ) ) )
83 60 82 mpbird 
 |-  ( ph -> X < M )
84 25 46 64 syl2anc 
 |-  ( ph -> ( X < M <-> X <_ ( M - 1 ) ) )
85 83 84 mpbid 
 |-  ( ph -> X <_ ( M - 1 ) )
86 27 47 25 81 85 elfzd 
 |-  ( ph -> X e. ( I ... ( M - 1 ) ) )
87 75 77 86 29 fvmptd 
 |-  ( ph -> ( D ` X ) = ( X + ( 1 - I ) ) )
88 74 87 eqtrd 
 |-  ( ph -> ( ( C u. D ) ` X ) = ( X + ( 1 - I ) ) )
89 70 88 eqtrd 
 |-  ( ph -> ( ( ( C u. D ) u. { <. M , M >. } ) ` X ) = ( X + ( 1 - I ) ) )
90 89 eqcomd 
 |-  ( ph -> ( X + ( 1 - I ) ) = ( ( ( C u. D ) u. { <. M , M >. } ) ` X ) )
91 30 90 eqtrd 
 |-  ( ph -> ( B ` X ) = ( ( ( C u. D ) u. { <. M , M >. } ) ` X ) )