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 ∈ D ⟼ if i = 1 I if i ≤ I i − 1 i
psgnfzto1st.g ⊢ G = SymGrp ⁡ D
psgnfzto1st.b ⊢ B = Base G
Assertion fzto1st ⊢ I ∈ D → P ∈ B

Proof

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