Theorem fzto1stinvn

Description: Value of the inverse of our permutation P at I . (Contributed by Thierry Arnoux, 23-Aug-2020)

	Ref	Expression
Hypotheses	psgnfzto1st.d	$$⊢D=\left(1\dots N\right)$$
	psgnfzto1st.p	$$⊢P=\left(i\in D⟼if\left(i=1,I,if\left(i\le I,i-1,i\right)\right)\right)$$
	psgnfzto1st.g	$$⊢G=\mathrm{SymGrp}\left(D\right)$$
	psgnfzto1st.b	$$⊢B={\mathrm{Base}}_G$$
Assertion	fzto1stinvn	$$⊢I\in D\to P^{-1}\left(I\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		psgnfzto1st.d	$$⊢D=\left(1\dots N\right)$$
2		psgnfzto1st.p	$$⊢P=\left(i\in D⟼if\left(i=1,I,if\left(i\le I,i-1,i\right)\right)\right)$$
3		psgnfzto1st.g	$$⊢G=\mathrm{SymGrp}\left(D\right)$$
4		psgnfzto1st.b	$$⊢B={\mathrm{Base}}_G$$
5	1 2	fzto1stfv1	$$⊢I\in D\to P\left(1\right)=I$$
6	5	fveq2d	$$⊢I\in D\to P^{-1}\left(P\left(1\right)\right)=P^{-1}\left(I\right)$$
7	1 2 3 4	fzto1st	$$⊢I\in D\to P\in B$$
8	3 4	symgbasf1o	$$⊢P\in B\to P:D\underset{1-1\; onto}{⟶}D$$
9	7 8	syl	$$⊢I\in D\to P:D\underset{1-1\; onto}{⟶}D$$
10		elfzuz2	$$⊢I\in \left(1\dots N\right)\to N\in {\mathbb{Z}}_{\ge 1}$$
11	10 1	eleq2s	$$⊢I\in D\to N\in {\mathbb{Z}}_{\ge 1}$$
12		eluzfz1	$$⊢N\in {\mathbb{Z}}_{\ge 1}\to 1\in \left(1\dots N\right)$$
13	12 1	eleqtrrdi	$$⊢N\in {\mathbb{Z}}_{\ge 1}\to 1\in D$$
14	11 13	syl	$$⊢I\in D\to 1\in D$$
15		f1ocnvfv1	$$⊢\left(P:D\underset{1-1\; onto}{⟶}D\wedge 1\in D\right)\to P^{-1}\left(P\left(1\right)\right)=1$$
16	9 14 15	syl2anc	$$⊢I\in D\to P^{-1}\left(P\left(1\right)\right)=1$$
17	6 16	eqtr3d	$$⊢I\in D\to P^{-1}\left(I\right)=1$$