Metamath Proof Explorer

Theorem fzto1st

Description: The function moving one element to the first position (and shifting all elements before it) is a permutation. (Contributed by Thierry Arnoux, 21-Aug-2020)

Ref Expression
Hypotheses psgnfzto1st.d 
|- D = ( 1 ... N )
psgnfzto1st.p 
|- P = ( i e. D |-> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) )
psgnfzto1st.g 
|- G = ( SymGrp ` D )
psgnfzto1st.b 
|- B = ( Base ` G )
Assertion fzto1st 
|- ( I e. D -> P e. B )

Proof

Step Hyp Ref Expression
1 psgnfzto1st.d 
 |-  D = ( 1 ... N )
2 psgnfzto1st.p 
 |-  P = ( i e. D |-> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) )
3 psgnfzto1st.g 
 |-  G = ( SymGrp ` D )
4 psgnfzto1st.b 
 |-  B = ( Base ` G )
5 elfz1b 
 |-  ( I e. ( 1 ... N ) <-> ( I e. NN /\ N e. NN /\ I <_ N ) )
6 5 biimpi 
 |-  ( I e. ( 1 ... N ) -> ( I e. NN /\ N e. NN /\ I <_ N ) )
7 6 1 eleq2s 
 |-  ( I e. D -> ( I e. NN /\ N e. NN /\ I <_ N ) )
8 3ancoma 
 |-  ( ( N e. NN /\ I e. NN /\ I <_ N ) <-> ( I e. NN /\ N e. NN /\ I <_ N ) )
9 7 8 sylibr 
 |-  ( I e. D -> ( N e. NN /\ I e. NN /\ I <_ N ) )
10 df-3an 
 |-  ( ( N e. NN /\ I e. NN /\ I <_ N ) <-> ( ( N e. NN /\ I e. NN ) /\ I <_ N ) )
11 breq1 
 |-  ( m = 1 -> ( m <_ N <-> 1 <_ N ) )
12 simpl 
 |-  ( ( m = 1 /\ i e. D ) -> m = 1 )
13 12 breq2d 
 |-  ( ( m = 1 /\ i e. D ) -> ( i <_ m <-> i <_ 1 ) )
14 13 ifbid 
 |-  ( ( m = 1 /\ i e. D ) -> if ( i <_ m , ( i - 1 ) , i ) = if ( i <_ 1 , ( i - 1 ) , i ) )
15 12 14 ifeq12d 
 |-  ( ( m = 1 /\ i e. D ) -> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) = if ( i = 1 , 1 , if ( i <_ 1 , ( i - 1 ) , i ) ) )
16 15 mpteq2dva 
 |-  ( m = 1 -> ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) = ( i e. D |-> if ( i = 1 , 1 , if ( i <_ 1 , ( i - 1 ) , i ) ) ) )
17 eqid 
 |-  1 = 1
18 eqid 
 |-  ( i e. D |-> if ( i = 1 , 1 , if ( i <_ 1 , ( i - 1 ) , i ) ) ) = ( i e. D |-> if ( i = 1 , 1 , if ( i <_ 1 , ( i - 1 ) , i ) ) )
19 1 18 fzto1st1 
 |-  ( 1 = 1 -> ( i e. D |-> if ( i = 1 , 1 , if ( i <_ 1 , ( i - 1 ) , i ) ) ) = ( _I |` D ) )
20 17 19 ax-mp 
 |-  ( i e. D |-> if ( i = 1 , 1 , if ( i <_ 1 , ( i - 1 ) , i ) ) ) = ( _I |` D )
21 16 20 eqtrdi 
 |-  ( m = 1 -> ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) = ( _I |` D ) )
22 21 eleq1d 
 |-  ( m = 1 -> ( ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) e. B <-> ( _I |` D ) e. B ) )
23 11 22 imbi12d 
 |-  ( m = 1 -> ( ( m <_ N -> ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) e. B ) <-> ( 1 <_ N -> ( _I |` D ) e. B ) ) )
24 breq1 
 |-  ( m = n -> ( m <_ N <-> n <_ N ) )
25 simpl 
 |-  ( ( m = n /\ i e. D ) -> m = n )
26 25 breq2d 
 |-  ( ( m = n /\ i e. D ) -> ( i <_ m <-> i <_ n ) )
27 26 ifbid 
 |-  ( ( m = n /\ i e. D ) -> if ( i <_ m , ( i - 1 ) , i ) = if ( i <_ n , ( i - 1 ) , i ) )
28 25 27 ifeq12d 
 |-  ( ( m = n /\ i e. D ) -> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) = if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) )
29 28 mpteq2dva 
 |-  ( m = n -> ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) = ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) )
30 29 eleq1d 
 |-  ( m = n -> ( ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) e. B <-> ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) e. B ) )
31 24 30 imbi12d 
 |-  ( m = n -> ( ( m <_ N -> ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) e. B ) <-> ( n <_ N -> ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) e. B ) ) )
32 breq1 
 |-  ( m = ( n + 1 ) -> ( m <_ N <-> ( n + 1 ) <_ N ) )
33 simpl 
 |-  ( ( m = ( n + 1 ) /\ i e. D ) -> m = ( n + 1 ) )
34 33 breq2d 
 |-  ( ( m = ( n + 1 ) /\ i e. D ) -> ( i <_ m <-> i <_ ( n + 1 ) ) )
35 34 ifbid 
 |-  ( ( m = ( n + 1 ) /\ i e. D ) -> if ( i <_ m , ( i - 1 ) , i ) = if ( i <_ ( n + 1 ) , ( i - 1 ) , i ) )
36 33 35 ifeq12d 
 |-  ( ( m = ( n + 1 ) /\ i e. D ) -> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) = if ( i = 1 , ( n + 1 ) , if ( i <_ ( n + 1 ) , ( i - 1 ) , i ) ) )
37 36 mpteq2dva 
 |-  ( m = ( n + 1 ) -> ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) = ( i e. D |-> if ( i = 1 , ( n + 1 ) , if ( i <_ ( n + 1 ) , ( i - 1 ) , i ) ) ) )
38 37 eleq1d 
 |-  ( m = ( n + 1 ) -> ( ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) e. B <-> ( i e. D |-> if ( i = 1 , ( n + 1 ) , if ( i <_ ( n + 1 ) , ( i - 1 ) , i ) ) ) e. B ) )
39 32 38 imbi12d 
 |-  ( m = ( n + 1 ) -> ( ( m <_ N -> ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) e. B ) <-> ( ( n + 1 ) <_ N -> ( i e. D |-> if ( i = 1 , ( n + 1 ) , if ( i <_ ( n + 1 ) , ( i - 1 ) , i ) ) ) e. B ) ) )
40 breq1 
 |-  ( m = I -> ( m <_ N <-> I <_ N ) )
41 simpl 
 |-  ( ( m = I /\ i e. D ) -> m = I )
42 41 breq2d 
 |-  ( ( m = I /\ i e. D ) -> ( i <_ m <-> i <_ I ) )
43 42 ifbid 
 |-  ( ( m = I /\ i e. D ) -> if ( i <_ m , ( i - 1 ) , i ) = if ( i <_ I , ( i - 1 ) , i ) )
44 41 43 ifeq12d 
 |-  ( ( m = I /\ i e. D ) -> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) = if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) )
45 44 mpteq2dva 
 |-  ( m = I -> ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) = ( i e. D |-> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) ) )
46 45 2 eqtr4di 
 |-  ( m = I -> ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) = P )
47 46 eleq1d 
 |-  ( m = I -> ( ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) e. B <-> P e. B ) )
48 40 47 imbi12d 
 |-  ( m = I -> ( ( m <_ N -> ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) e. B ) <-> ( I <_ N -> P e. B ) ) )
49 fzfi 
 |-  ( 1 ... N ) e. Fin
50 1 49 eqeltri 
 |-  D e. Fin
51 3 idresperm 
 |-  ( D e. Fin -> ( _I |` D ) e. ( Base ` G ) )
52 50 51 ax-mp 
 |-  ( _I |` D ) e. ( Base ` G )
53 52 4 eleqtrri 
 |-  ( _I |` D ) e. B
54 53 2a1i 
 |-  ( N e. NN -> ( 1 <_ N -> ( _I |` D ) e. B ) )
55 simplr 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> n e. NN )
56 55 peano2nnd 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> ( n + 1 ) e. NN )
57 simpll 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> N e. NN )
58 simpr 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> ( n + 1 ) <_ N )
59 56 57 58 3jca 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> ( ( n + 1 ) e. NN /\ N e. NN /\ ( n + 1 ) <_ N ) )
60 elfz1b 
 |-  ( ( n + 1 ) e. ( 1 ... N ) <-> ( ( n + 1 ) e. NN /\ N e. NN /\ ( n + 1 ) <_ N ) )
61 59 60 sylibr 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> ( n + 1 ) e. ( 1 ... N ) )
62 61 1 eleqtrrdi 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> ( n + 1 ) e. D )
63 1 psgnfzto1stlem 
 |-  ( ( n e. NN /\ ( n + 1 ) e. D ) -> ( i e. D |-> if ( i = 1 , ( n + 1 ) , if ( i <_ ( n + 1 ) , ( i - 1 ) , i ) ) ) = ( ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) o. ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) )
64 55 62 63 syl2anc 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> ( i e. D |-> if ( i = 1 , ( n + 1 ) , if ( i <_ ( n + 1 ) , ( i - 1 ) , i ) ) ) = ( ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) o. ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) )
65 64 adantlr 
 |-  ( ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) e. B ) ) /\ ( n + 1 ) <_ N ) -> ( i e. D |-> if ( i = 1 , ( n + 1 ) , if ( i <_ ( n + 1 ) , ( i - 1 ) , i ) ) ) = ( ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) o. ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) )
66 eqid 
 |-  ran ( pmTrsp ` D ) = ran ( pmTrsp ` D )
67 66 3 4 symgtrf 
 |-  ran ( pmTrsp ` D ) C_ B
68 eqid 
 |-  ( pmTrsp ` D ) = ( pmTrsp ` D )
69 1 68 pmtrto1cl 
 |-  ( ( n e. NN /\ ( n + 1 ) e. D ) -> ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) e. ran ( pmTrsp ` D ) )
70 55 62 69 syl2anc 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) e. ran ( pmTrsp ` D ) )
71 70 adantlr 
 |-  ( ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) e. B ) ) /\ ( n + 1 ) <_ N ) -> ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) e. ran ( pmTrsp ` D ) )
72 67 71 sseldi 
 |-  ( ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) e. B ) ) /\ ( n + 1 ) <_ N ) -> ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) e. B )
73 55 nnred 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> n e. RR )
74 1red 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> 1 e. RR )
75 73 74 readdcld 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> ( n + 1 ) e. RR )
76 57 nnred 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> N e. RR )
77 73 lep1d 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> n <_ ( n + 1 ) )
78 73 75 76 77 58 letrd 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> n <_ N )
79 78 adantlr 
 |-  ( ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) e. B ) ) /\ ( n + 1 ) <_ N ) -> n <_ N )
80 simplr 
 |-  ( ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) e. B ) ) /\ ( n + 1 ) <_ N ) -> ( n <_ N -> ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) e. B ) )
81 79 80 mpd 
 |-  ( ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) e. B ) ) /\ ( n + 1 ) <_ N ) -> ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) e. B )
82 eqid 
 |-  ( +g ` G ) = ( +g ` G )
83 3 4 82 symgov 
 |-  ( ( ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) e. B /\ ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) e. B ) -> ( ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) ( +g ` G ) ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) = ( ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) o. ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) )
84 3 4 82 symgcl 
 |-  ( ( ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) e. B /\ ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) e. B ) -> ( ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) ( +g ` G ) ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) e. B )
85 83 84 eqeltrrd 
 |-  ( ( ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) e. B /\ ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) e. B ) -> ( ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) o. ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) e. B )
86 72 81 85 syl2anc 
 |-  ( ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) e. B ) ) /\ ( n + 1 ) <_ N ) -> ( ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) o. ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) e. B )
87 65 86 eqeltrd 
 |-  ( ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) e. B ) ) /\ ( n + 1 ) <_ N ) -> ( i e. D |-> if ( i = 1 , ( n + 1 ) , if ( i <_ ( n + 1 ) , ( i - 1 ) , i ) ) ) e. B )
88 87 ex 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) e. B ) ) -> ( ( n + 1 ) <_ N -> ( i e. D |-> if ( i = 1 , ( n + 1 ) , if ( i <_ ( n + 1 ) , ( i - 1 ) , i ) ) ) e. B ) )
89 23 31 39 48 54 88 nnindd 
 |-  ( ( N e. NN /\ I e. NN ) -> ( I <_ N -> P e. B ) )
90 89 imp 
 |-  ( ( ( N e. NN /\ I e. NN ) /\ I <_ N ) -> P e. B )
91 10 90 sylbi 
 |-  ( ( N e. NN /\ I e. NN /\ I <_ N ) -> P e. B )
92 9 91 syl 
 |-  ( I e. D -> P e. B )