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 𝐷 = ( 1 ... 𝑁 )
psgnfzto1st.p 𝑃 = ( 𝑖𝐷 ↦ if ( 𝑖 = 1 , 𝐼 , if ( 𝑖𝐼 , ( 𝑖 − 1 ) , 𝑖 ) ) )
psgnfzto1st.g 𝐺 = ( SymGrp ‘ 𝐷 )
psgnfzto1st.b 𝐵 = ( Base ‘ 𝐺 )
Assertion fzto1st ( 𝐼𝐷𝑃𝐵 )

Proof

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