Theorem fzto1st 33543

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.)

Hypotheses

Ref	Expression
psgnfzto1st.d	⊢ 𝐷 = (1...𝑁)
psgnfzto1st.p	⊢ 𝑃 = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖)))
psgnfzto1st.g	⊢ 𝐺 = (SymGrp‘𝐷)
psgnfzto1st.b	⊢ 𝐵 = (Base‘𝐺)

Assertion

Ref	Expression
fzto1st	⊢ (𝐼 ∈ 𝐷 → 𝑃 ∈ 𝐵)

Distinct variable groups:   𝐷,𝑖   𝑖,𝐼   𝑖,𝑁   𝐵,𝑖

Allowed substitution hints:   𝑃(𝑖)   𝐺(𝑖)

Proof of Theorem fzto1st

Dummy variables 𝑚 𝑛 are mutually distinct and distinct from all other variables.

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ifcif 4482  {cpr 4586   class class class wbr 5103   ↦ cmpt 5186   I cid 5549  ran crn 5656   ↾ cres 5657   ∘ ccom 5659  ‘cfv 6533  (class class class)co 7413  Fincfn 8952  1c1 11125   + caddc 11127   ≤ cle 11268   − cmin 11465  ℕcn 12257  ...cfz 13561  Basecbs 17301  +_gcplusg 17342  SymGrpcsymg 19496  pmTrspcpmtr 19568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-cnex 11180  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7863  df-1st 7986  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-1o 8455  df-2o 8456  df-er 8696  df-map 8828  df-en 8953  df-dom 8954  df-sdom 8955  df-fin 8956  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11467  df-neg 11468  df-nn 12258  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334  df-n0 12529  df-z 12616  df-uz 12888  df-fz 13562  df-struct 17239  df-sets 17256  df-slot 17274  df-ndx 17286  df-base 17302  df-ress 17323  df-plusg 17355  df-tset 17361  df-efmnd 18978  df-symg 19497  df-pmtr 19569

This theorem is used by:  fzto1stinvn  33544  psgnfzto1st  33545  madjusmdetlem2  34338  madjusmdetlem3  34339  madjusmdetlem4  34340