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 ⊢ ( 𝐼 ∈ 𝐷 → 𝑃 ∈ 𝐵 )