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 = ( 1 ... N )
	psgnfzto1st.p	|- P = ( i e. D |-> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) )
	psgnfzto1st.g	|- G = ( SymGrp ` D )
	psgnfzto1st.b	|- B = ( Base ` G )
Assertion	fzto1stinvn	|- ( I e. D -> ( `' P ` I ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		psgnfzto1st.d	|- D = ( 1 ... N )
2		psgnfzto1st.p	|- P = ( i e. D |-> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) )
3		psgnfzto1st.g	|- G = ( SymGrp ` D )
4		psgnfzto1st.b	|- B = ( Base ` G )
5	1 2	fzto1stfv1	|- ( I e. D -> ( P ` 1 ) = I )
6	5	fveq2d	|- ( I e. D -> ( `' P ` ( P ` 1 ) ) = ( `' P ` I ) )
7	1 2 3 4	fzto1st	|- ( I e. D -> P e. B )
8	3 4	symgbasf1o	|- ( P e. B -> P : D -1-1-onto-> D )
9	7 8	syl	|- ( I e. D -> P : D -1-1-onto-> D )
10		elfzuz2	|- ( I e. ( 1 ... N ) -> N e. ( ZZ>= ` 1 ) )
11	10 1	eleq2s	|- ( I e. D -> N e. ( ZZ>= ` 1 ) )
12		eluzfz1	|- ( N e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... N ) )
13	12 1	eleqtrrdi	|- ( N e. ( ZZ>= ` 1 ) -> 1 e. D )
14	11 13	syl	|- ( I e. D -> 1 e. D )
15		f1ocnvfv1	|- ( ( P : D -1-1-onto-> D /\ 1 e. D ) -> ( `' P ` ( P ` 1 ) ) = 1 )
16	9 14 15	syl2anc	|- ( I e. D -> ( `' P ` ( P ` 1 ) ) = 1 )
17	6 16	eqtr3d	|- ( I e. D -> ( `' P ` I ) = 1 )