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