Metamath Proof Explorer


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 D if i = 1 I if i I i 1 i
psgnfzto1st.g G = SymGrp D
psgnfzto1st.b B = Base G
Assertion fzto1stinvn I D P -1 I = 1

Proof

Step Hyp Ref Expression
1 psgnfzto1st.d D = 1 N
2 psgnfzto1st.p P = i 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 D P 1 = I
6 5 fveq2d I D P -1 P 1 = P -1 I
7 1 2 3 4 fzto1st I D P B
8 3 4 symgbasf1o P B P : D 1-1 onto D
9 7 8 syl I D P : D 1-1 onto D
10 elfzuz2 I 1 N N 1
11 10 1 eleq2s I D N 1
12 eluzfz1 N 1 1 1 N
13 12 1 eleqtrrdi N 1 1 D
14 11 13 syl I D 1 D
15 f1ocnvfv1 P : D 1-1 onto D 1 D P -1 P 1 = 1
16 9 14 15 syl2anc I D P -1 P 1 = 1
17 6 16 eqtr3d I D P -1 I = 1