Metamath Proof Explorer

Theorem metakunt20

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

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

Proof

Step Hyp Ref Expression
1 metakunt20.1 
 |-  ( ph -> M e. NN )
2 metakunt20.2 
 |-  ( ph -> I e. NN )
3 metakunt20.3 
 |-  ( ph -> I <_ M )
4 metakunt20.4 
 |-  B = ( x e. ( 1 ... M ) |-> if ( x = M , M , if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) ) )
5 metakunt20.5 
 |-  C = ( x e. ( 1 ... ( I - 1 ) ) |-> ( x + ( M - I ) ) )
6 metakunt20.6 
 |-  D = ( x e. ( I ... ( M - 1 ) ) |-> ( x + ( 1 - I ) ) )
7 metakunt20.7 
 |-  ( ph -> X e. ( 1 ... M ) )
8 metakunt20.8 
 |-  ( ph -> X = M )
9 4 a1i 
 |-  ( ph -> B = ( x e. ( 1 ... M ) |-> if ( x = M , M , if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) ) ) )
10 eqeq1 
 |-  ( x = X -> ( x = M <-> X = M ) )
11 breq1 
 |-  ( x = X -> ( x < I <-> X < I ) )
12 oveq1 
 |-  ( x = X -> ( x + ( M - I ) ) = ( X + ( M - I ) ) )
13 oveq1 
 |-  ( x = X -> ( x + ( 1 - I ) ) = ( X + ( 1 - I ) ) )
14 11 12 13 ifbieq12d 
 |-  ( x = X -> if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) = if ( X < I , ( X + ( M - I ) ) , ( X + ( 1 - I ) ) ) )
15 10 14 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 ) ) ) ) )
16 15 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 ) ) ) ) )
17 iftrue 
 |-  ( X = M -> if ( X = M , M , if ( X < I , ( X + ( M - I ) ) , ( X + ( 1 - I ) ) ) ) = M )
18 8 17 syl 
 |-  ( ph -> if ( X = M , M , if ( X < I , ( X + ( M - I ) ) , ( X + ( 1 - I ) ) ) ) = M )
19 18 adantr 
 |-  ( ( ph /\ x = X ) -> if ( X = M , M , if ( X < I , ( X + ( M - I ) ) , ( X + ( 1 - I ) ) ) ) = M )
20 8 eqcomd 
 |-  ( ph -> M = X )
21 20 adantr 
 |-  ( ( ph /\ x = X ) -> M = X )
22 19 21 eqtrd 
 |-  ( ( ph /\ x = X ) -> if ( X = M , M , if ( X < I , ( X + ( M - I ) ) , ( X + ( 1 - I ) ) ) ) = X )
23 16 22 eqtrd 
 |-  ( ( ph /\ x = X ) -> if ( x = M , M , if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) ) = X )
24 9 23 7 7 fvmptd 
 |-  ( ph -> ( B ` X ) = X )
25 8 fveq2d 
 |-  ( ph -> ( { <. M , M >. } ` X ) = ( { <. M , M >. } ` M ) )
26 fvsng 
 |-  ( ( M e. NN /\ M e. NN ) -> ( { <. M , M >. } ` M ) = M )
27 1 1 26 syl2anc 
 |-  ( ph -> ( { <. M , M >. } ` M ) = M )
28 25 27 eqtrd 
 |-  ( ph -> ( { <. M , M >. } ` X ) = M )
29 28 eqcomd 
 |-  ( ph -> M = ( { <. M , M >. } ` X ) )
30 24 8 29 3eqtrd 
 |-  ( ph -> ( B ` X ) = ( { <. M , M >. } ` X ) )
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 1 nnzd 
 |-  ( ph -> M e. ZZ )
36 fzsn 
 |-  ( M e. ZZ -> ( M ... M ) = { M } )
37 35 36 syl 
 |-  ( ph -> ( M ... M ) = { M } )
38 37 ineq2d 
 |-  ( ph -> ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) i^i ( M ... M ) ) = ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) i^i { M } ) )
39 38 eqcomd 
 |-  ( ph -> ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) i^i { M } ) = ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) i^i ( M ... M ) ) )
40 2 nncnd 
 |-  ( ph -> I e. CC )
41 1 nncnd 
 |-  ( ph -> M e. CC )
42 40 41 pncan3d 
 |-  ( ph -> ( I + ( M - I ) ) = M )
43 42 oveq2d 
 |-  ( ph -> ( 1 ..^ ( I + ( M - I ) ) ) = ( 1 ..^ M ) )
44 fzoval 
 |-  ( M e. ZZ -> ( 1 ..^ M ) = ( 1 ... ( M - 1 ) ) )
45 35 44 syl 
 |-  ( ph -> ( 1 ..^ M ) = ( 1 ... ( M - 1 ) ) )
46 43 45 eqtrd 
 |-  ( ph -> ( 1 ..^ ( I + ( M - I ) ) ) = ( 1 ... ( M - 1 ) ) )
47 46 eqcomd 
 |-  ( ph -> ( 1 ... ( M - 1 ) ) = ( 1 ..^ ( I + ( M - I ) ) ) )
48 nnuz 
 |-  NN = ( ZZ>= ` 1 )
49 2 48 eleqtrdi 
 |-  ( ph -> I e. ( ZZ>= ` 1 ) )
50 2 nnzd 
 |-  ( ph -> I e. ZZ )
51 50 35 jca 
 |-  ( ph -> ( I e. ZZ /\ M e. ZZ ) )
52 znn0sub 
 |-  ( ( I e. ZZ /\ M e. ZZ ) -> ( I <_ M <-> ( M - I ) e. NN0 ) )
53 51 52 syl 
 |-  ( ph -> ( I <_ M <-> ( M - I ) e. NN0 ) )
54 3 53 mpbid 
 |-  ( ph -> ( M - I ) e. NN0 )
55 fzoun 
 |-  ( ( I e. ( ZZ>= ` 1 ) /\ ( M - I ) e. NN0 ) -> ( 1 ..^ ( I + ( M - I ) ) ) = ( ( 1 ..^ I ) u. ( I ..^ ( I + ( M - I ) ) ) ) )
56 49 54 55 syl2anc 
 |-  ( ph -> ( 1 ..^ ( I + ( M - I ) ) ) = ( ( 1 ..^ I ) u. ( I ..^ ( I + ( M - I ) ) ) ) )
57 47 56 eqtrd 
 |-  ( ph -> ( 1 ... ( M - 1 ) ) = ( ( 1 ..^ I ) u. ( I ..^ ( I + ( M - I ) ) ) ) )
58 fzoval 
 |-  ( I e. ZZ -> ( 1 ..^ I ) = ( 1 ... ( I - 1 ) ) )
59 50 58 syl 
 |-  ( ph -> ( 1 ..^ I ) = ( 1 ... ( I - 1 ) ) )
60 42 oveq2d 
 |-  ( ph -> ( I ..^ ( I + ( M - I ) ) ) = ( I ..^ M ) )
61 fzoval 
 |-  ( M e. ZZ -> ( I ..^ M ) = ( I ... ( M - 1 ) ) )
62 35 61 syl 
 |-  ( ph -> ( I ..^ M ) = ( I ... ( M - 1 ) ) )
63 60 62 eqtrd 
 |-  ( ph -> ( I ..^ ( I + ( M - I ) ) ) = ( I ... ( M - 1 ) ) )
64 59 63 uneq12d 
 |-  ( ph -> ( ( 1 ..^ I ) u. ( I ..^ ( I + ( M - I ) ) ) ) = ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) )
65 57 64 eqtrd 
 |-  ( ph -> ( 1 ... ( M - 1 ) ) = ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) )
66 65 ineq1d 
 |-  ( ph -> ( ( 1 ... ( M - 1 ) ) i^i ( M ... M ) ) = ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) i^i ( M ... M ) ) )
67 66 eqcomd 
 |-  ( ph -> ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) i^i ( M ... M ) ) = ( ( 1 ... ( M - 1 ) ) i^i ( M ... M ) ) )
68 1 nnred 
 |-  ( ph -> M e. RR )
69 68 ltm1d 
 |-  ( ph -> ( M - 1 ) < M )
70 fzdisj 
 |-  ( ( M - 1 ) < M -> ( ( 1 ... ( M - 1 ) ) i^i ( M ... M ) ) = (/) )
71 69 70 syl 
 |-  ( ph -> ( ( 1 ... ( M - 1 ) ) i^i ( M ... M ) ) = (/) )
72 67 71 eqtrd 
 |-  ( ph -> ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) i^i ( M ... M ) ) = (/) )
73 39 72 eqtrd 
 |-  ( ph -> ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) i^i { M } ) = (/) )
74 elsng 
 |-  ( X e. ( 1 ... M ) -> ( X e. { M } <-> X = M ) )
75 7 74 syl 
 |-  ( ph -> ( X e. { M } <-> X = M ) )
76 8 75 mpbird 
 |-  ( ph -> X e. { M } )
77 33 34 73 76 fvun2d 
 |-  ( ph -> ( ( ( C u. D ) u. { <. M , M >. } ) ` X ) = ( { <. M , M >. } ` X ) )
78 77 eqcomd 
 |-  ( ph -> ( { <. M , M >. } ` X ) = ( ( ( C u. D ) u. { <. M , M >. } ) ` X ) )
79 30 78 eqtrd 
 |-  ( ph -> ( B ` X ) = ( ( ( C u. D ) u. { <. M , M >. } ) ` X ) )