Metamath Proof Explorer

Theorem psgnfzto1st

Description: The permutation sign for moving one element to the first position. (Contributed by Thierry Arnoux, 21-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 )
psgnfzto1st.s 
|- S = ( pmSgn ` D )
Assertion psgnfzto1st 
|- ( I e. D -> ( S ` P ) = ( -u 1 ^ ( 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 psgnfzto1st.s 
 |-  S = ( pmSgn ` D )
6 elfz1b 
 |-  ( I e. ( 1 ... N ) <-> ( I e. NN /\ N e. NN /\ I <_ N ) )
7 6 biimpi 
 |-  ( I e. ( 1 ... N ) -> ( I e. NN /\ N e. NN /\ I <_ N ) )
8 7 1 eleq2s 
 |-  ( I e. D -> ( I e. NN /\ N e. NN /\ I <_ N ) )
9 3ancoma 
 |-  ( ( N e. NN /\ I e. NN /\ I <_ N ) <-> ( I e. NN /\ N e. NN /\ I <_ N ) )
10 8 9 sylibr 
 |-  ( I e. D -> ( N e. NN /\ I e. NN /\ I <_ N ) )
11 df-3an 
 |-  ( ( N e. NN /\ I e. NN /\ I <_ N ) <-> ( ( N e. NN /\ I e. NN ) /\ I <_ N ) )
12 breq1 
 |-  ( m = 1 -> ( m <_ N <-> 1 <_ N ) )
13 id 
 |-  ( m = 1 -> m = 1 )
14 breq2 
 |-  ( m = 1 -> ( i <_ m <-> i <_ 1 ) )
15 14 ifbid 
 |-  ( m = 1 -> if ( i <_ m , ( i - 1 ) , i ) = if ( i <_ 1 , ( i - 1 ) , i ) )
16 13 15 ifeq12d 
 |-  ( m = 1 -> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) = if ( i = 1 , 1 , if ( i <_ 1 , ( i - 1 ) , i ) ) )
17 16 mpteq2dv 
 |-  ( m = 1 -> ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) = ( i e. D |-> if ( i = 1 , 1 , if ( i <_ 1 , ( i - 1 ) , i ) ) ) )
18 17 fveq2d 
 |-  ( m = 1 -> ( S ` ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) ) = ( S ` ( i e. D |-> if ( i = 1 , 1 , if ( i <_ 1 , ( i - 1 ) , i ) ) ) ) )
19 oveq1 
 |-  ( m = 1 -> ( m + 1 ) = ( 1 + 1 ) )
20 19 oveq2d 
 |-  ( m = 1 -> ( -u 1 ^ ( m + 1 ) ) = ( -u 1 ^ ( 1 + 1 ) ) )
21 18 20 eqeq12d 
 |-  ( m = 1 -> ( ( S ` ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( m + 1 ) ) <-> ( S ` ( i e. D |-> if ( i = 1 , 1 , if ( i <_ 1 , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( 1 + 1 ) ) ) )
22 12 21 imbi12d 
 |-  ( m = 1 -> ( ( m <_ N -> ( S ` ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( m + 1 ) ) ) <-> ( 1 <_ N -> ( S ` ( i e. D |-> if ( i = 1 , 1 , if ( i <_ 1 , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( 1 + 1 ) ) ) ) )
23 breq1 
 |-  ( m = n -> ( m <_ N <-> n <_ N ) )
24 id 
 |-  ( m = n -> m = n )
25 breq2 
 |-  ( m = n -> ( i <_ m <-> i <_ n ) )
26 25 ifbid 
 |-  ( m = n -> if ( i <_ m , ( i - 1 ) , i ) = if ( i <_ n , ( i - 1 ) , i ) )
27 24 26 ifeq12d 
 |-  ( m = n -> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) = if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) )
28 27 mpteq2dv 
 |-  ( m = n -> ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) = ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) )
29 28 fveq2d 
 |-  ( m = n -> ( S ` ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) ) = ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) )
30 oveq1 
 |-  ( m = n -> ( m + 1 ) = ( n + 1 ) )
31 30 oveq2d 
 |-  ( m = n -> ( -u 1 ^ ( m + 1 ) ) = ( -u 1 ^ ( n + 1 ) ) )
32 29 31 eqeq12d 
 |-  ( m = n -> ( ( S ` ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( m + 1 ) ) <-> ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( n + 1 ) ) ) )
33 23 32 imbi12d 
 |-  ( m = n -> ( ( m <_ N -> ( S ` ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( m + 1 ) ) ) <-> ( n <_ N -> ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( n + 1 ) ) ) ) )
34 breq1 
 |-  ( m = ( n + 1 ) -> ( m <_ N <-> ( n + 1 ) <_ N ) )
35 id 
 |-  ( m = ( n + 1 ) -> m = ( n + 1 ) )
36 breq2 
 |-  ( m = ( n + 1 ) -> ( i <_ m <-> i <_ ( n + 1 ) ) )
37 36 ifbid 
 |-  ( m = ( n + 1 ) -> if ( i <_ m , ( i - 1 ) , i ) = if ( i <_ ( n + 1 ) , ( i - 1 ) , i ) )
38 35 37 ifeq12d 
 |-  ( m = ( n + 1 ) -> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) = if ( i = 1 , ( n + 1 ) , if ( i <_ ( n + 1 ) , ( i - 1 ) , i ) ) )
39 38 mpteq2dv 
 |-  ( m = ( n + 1 ) -> ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) = ( i e. D |-> if ( i = 1 , ( n + 1 ) , if ( i <_ ( n + 1 ) , ( i - 1 ) , i ) ) ) )
40 39 fveq2d 
 |-  ( m = ( n + 1 ) -> ( S ` ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) ) = ( S ` ( i e. D |-> if ( i = 1 , ( n + 1 ) , if ( i <_ ( n + 1 ) , ( i - 1 ) , i ) ) ) ) )
41 oveq1 
 |-  ( m = ( n + 1 ) -> ( m + 1 ) = ( ( n + 1 ) + 1 ) )
42 41 oveq2d 
 |-  ( m = ( n + 1 ) -> ( -u 1 ^ ( m + 1 ) ) = ( -u 1 ^ ( ( n + 1 ) + 1 ) ) )
43 40 42 eqeq12d 
 |-  ( m = ( n + 1 ) -> ( ( S ` ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( m + 1 ) ) <-> ( S ` ( i e. D |-> if ( i = 1 , ( n + 1 ) , if ( i <_ ( n + 1 ) , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( ( n + 1 ) + 1 ) ) ) )
44 34 43 imbi12d 
 |-  ( m = ( n + 1 ) -> ( ( m <_ N -> ( S ` ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( m + 1 ) ) ) <-> ( ( n + 1 ) <_ N -> ( S ` ( i e. D |-> if ( i = 1 , ( n + 1 ) , if ( i <_ ( n + 1 ) , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( ( n + 1 ) + 1 ) ) ) ) )
45 breq1 
 |-  ( m = I -> ( m <_ N <-> I <_ N ) )
46 id 
 |-  ( m = I -> m = I )
47 breq2 
 |-  ( m = I -> ( i <_ m <-> i <_ I ) )
48 47 ifbid 
 |-  ( m = I -> if ( i <_ m , ( i - 1 ) , i ) = if ( i <_ I , ( i - 1 ) , i ) )
49 46 48 ifeq12d 
 |-  ( m = I -> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) = if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) )
50 49 mpteq2dv 
 |-  ( m = I -> ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) = ( i e. D |-> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) ) )
51 50 2 eqtr4di 
 |-  ( m = I -> ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) = P )
52 51 fveq2d 
 |-  ( m = I -> ( S ` ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) ) = ( S ` P ) )
53 oveq1 
 |-  ( m = I -> ( m + 1 ) = ( I + 1 ) )
54 53 oveq2d 
 |-  ( m = I -> ( -u 1 ^ ( m + 1 ) ) = ( -u 1 ^ ( I + 1 ) ) )
55 52 54 eqeq12d 
 |-  ( m = I -> ( ( S ` ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( m + 1 ) ) <-> ( S ` P ) = ( -u 1 ^ ( I + 1 ) ) ) )
56 45 55 imbi12d 
 |-  ( m = I -> ( ( m <_ N -> ( S ` ( i e. D |-> if ( i = 1 , m , if ( i <_ m , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( m + 1 ) ) ) <-> ( I <_ N -> ( S ` P ) = ( -u 1 ^ ( I + 1 ) ) ) ) )
57 fzfi 
 |-  ( 1 ... N ) e. Fin
58 1 57 eqeltri 
 |-  D e. Fin
59 5 psgnid 
 |-  ( D e. Fin -> ( S ` ( _I |` D ) ) = 1 )
60 58 59 ax-mp 
 |-  ( S ` ( _I |` D ) ) = 1
61 eqid 
 |-  1 = 1
62 eqid 
 |-  ( i e. D |-> if ( i = 1 , 1 , if ( i <_ 1 , ( i - 1 ) , i ) ) ) = ( i e. D |-> if ( i = 1 , 1 , if ( i <_ 1 , ( i - 1 ) , i ) ) )
63 1 62 fzto1st1 
 |-  ( 1 = 1 -> ( i e. D |-> if ( i = 1 , 1 , if ( i <_ 1 , ( i - 1 ) , i ) ) ) = ( _I |` D ) )
64 61 63 ax-mp 
 |-  ( i e. D |-> if ( i = 1 , 1 , if ( i <_ 1 , ( i - 1 ) , i ) ) ) = ( _I |` D )
65 64 fveq2i 
 |-  ( S ` ( i e. D |-> if ( i = 1 , 1 , if ( i <_ 1 , ( i - 1 ) , i ) ) ) ) = ( S ` ( _I |` D ) )
66 1p1e2 
 |-  ( 1 + 1 ) = 2
67 66 oveq2i 
 |-  ( -u 1 ^ ( 1 + 1 ) ) = ( -u 1 ^ 2 )
68 neg1sqe1 
 |-  ( -u 1 ^ 2 ) = 1
69 67 68 eqtri 
 |-  ( -u 1 ^ ( 1 + 1 ) ) = 1
70 60 65 69 3eqtr4i 
 |-  ( S ` ( i e. D |-> if ( i = 1 , 1 , if ( i <_ 1 , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( 1 + 1 ) )
71 70 2a1i 
 |-  ( N e. NN -> ( 1 <_ N -> ( S ` ( i e. D |-> if ( i = 1 , 1 , if ( i <_ 1 , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( 1 + 1 ) ) ) )
72 simplr 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> n e. NN )
73 72 peano2nnd 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> ( n + 1 ) e. NN )
74 simpll 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> N e. NN )
75 simpr 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> ( n + 1 ) <_ N )
76 73 74 75 3jca 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> ( ( n + 1 ) e. NN /\ N e. NN /\ ( n + 1 ) <_ N ) )
77 elfz1b 
 |-  ( ( n + 1 ) e. ( 1 ... N ) <-> ( ( n + 1 ) e. NN /\ N e. NN /\ ( n + 1 ) <_ N ) )
78 76 77 sylibr 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> ( n + 1 ) e. ( 1 ... N ) )
79 78 1 eleqtrrdi 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> ( n + 1 ) e. D )
80 1 psgnfzto1stlem 
 |-  ( ( n e. NN /\ ( n + 1 ) e. D ) -> ( i e. D |-> if ( i = 1 , ( n + 1 ) , if ( i <_ ( n + 1 ) , ( i - 1 ) , i ) ) ) = ( ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) o. ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) )
81 72 79 80 syl2anc 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> ( i e. D |-> if ( i = 1 , ( n + 1 ) , if ( i <_ ( n + 1 ) , ( i - 1 ) , i ) ) ) = ( ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) o. ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) )
82 81 adantlr 
 |-  ( ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( n + 1 ) ) ) ) /\ ( n + 1 ) <_ N ) -> ( i e. D |-> if ( i = 1 , ( n + 1 ) , if ( i <_ ( n + 1 ) , ( i - 1 ) , i ) ) ) = ( ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) o. ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) )
83 82 fveq2d 
 |-  ( ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( n + 1 ) ) ) ) /\ ( n + 1 ) <_ N ) -> ( S ` ( i e. D |-> if ( i = 1 , ( n + 1 ) , if ( i <_ ( n + 1 ) , ( i - 1 ) , i ) ) ) ) = ( S ` ( ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) o. ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) ) )
84 58 a1i 
 |-  ( ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( n + 1 ) ) ) ) /\ ( n + 1 ) <_ N ) -> D e. Fin )
85 eqid 
 |-  ran ( pmTrsp ` D ) = ran ( pmTrsp ` D )
86 85 3 4 symgtrf 
 |-  ran ( pmTrsp ` D ) C_ B
87 eqid 
 |-  ( pmTrsp ` D ) = ( pmTrsp ` D )
88 1 87 pmtrto1cl 
 |-  ( ( n e. NN /\ ( n + 1 ) e. D ) -> ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) e. ran ( pmTrsp ` D ) )
89 72 79 88 syl2anc 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) e. ran ( pmTrsp ` D ) )
90 89 adantlr 
 |-  ( ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( n + 1 ) ) ) ) /\ ( n + 1 ) <_ N ) -> ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) e. ran ( pmTrsp ` D ) )
91 86 90 sselid 
 |-  ( ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( n + 1 ) ) ) ) /\ ( n + 1 ) <_ N ) -> ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) e. B )
92 72 nnred 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> n e. RR )
93 1red 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> 1 e. RR )
94 92 93 readdcld 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> ( n + 1 ) e. RR )
95 74 nnred 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> N e. RR )
96 92 lep1d 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> n <_ ( n + 1 ) )
97 92 94 95 96 75 letrd 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> n <_ N )
98 72 74 97 3jca 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> ( n e. NN /\ N e. NN /\ n <_ N ) )
99 elfz1b 
 |-  ( n e. ( 1 ... N ) <-> ( n e. NN /\ N e. NN /\ n <_ N ) )
100 98 99 sylibr 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> n e. ( 1 ... N ) )
101 100 1 eleqtrrdi 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> n e. D )
102 101 adantlr 
 |-  ( ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( n + 1 ) ) ) ) /\ ( n + 1 ) <_ N ) -> n e. D )
103 eqid 
 |-  ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) = ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) )
104 1 103 3 4 fzto1st 
 |-  ( n e. D -> ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) e. B )
105 102 104 syl 
 |-  ( ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( n + 1 ) ) ) ) /\ ( n + 1 ) <_ N ) -> ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) e. B )
106 3 5 4 psgnco 
 |-  ( ( D e. Fin /\ ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) e. B /\ ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) e. B ) -> ( S ` ( ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) o. ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) ) = ( ( S ` ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) ) x. ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) ) )
107 84 91 105 106 syl3anc 
 |-  ( ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( n + 1 ) ) ) ) /\ ( n + 1 ) <_ N ) -> ( S ` ( ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) o. ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) ) = ( ( S ` ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) ) x. ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) ) )
108 3 85 5 psgnpmtr 
 |-  ( ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) e. ran ( pmTrsp ` D ) -> ( S ` ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) ) = -u 1 )
109 89 108 syl 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n + 1 ) <_ N ) -> ( S ` ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) ) = -u 1 )
110 109 adantlr 
 |-  ( ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( n + 1 ) ) ) ) /\ ( n + 1 ) <_ N ) -> ( S ` ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) ) = -u 1 )
111 97 adantlr 
 |-  ( ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( n + 1 ) ) ) ) /\ ( n + 1 ) <_ N ) -> n <_ N )
112 simplr 
 |-  ( ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( n + 1 ) ) ) ) /\ ( n + 1 ) <_ N ) -> ( n <_ N -> ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( n + 1 ) ) ) )
113 111 112 mpd 
 |-  ( ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( n + 1 ) ) ) ) /\ ( n + 1 ) <_ N ) -> ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( n + 1 ) ) )
114 110 113 oveq12d 
 |-  ( ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( n + 1 ) ) ) ) /\ ( n + 1 ) <_ N ) -> ( ( S ` ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) ) x. ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) ) = ( -u 1 x. ( -u 1 ^ ( n + 1 ) ) ) )
115 neg1cn 
 |-  -u 1 e. CC
116 peano2nn 
 |-  ( n e. NN -> ( n + 1 ) e. NN )
117 116 nnnn0d 
 |-  ( n e. NN -> ( n + 1 ) e. NN0 )
118 expp1 
 |-  ( ( -u 1 e. CC /\ ( n + 1 ) e. NN0 ) -> ( -u 1 ^ ( ( n + 1 ) + 1 ) ) = ( ( -u 1 ^ ( n + 1 ) ) x. -u 1 ) )
119 115 117 118 sylancr 
 |-  ( n e. NN -> ( -u 1 ^ ( ( n + 1 ) + 1 ) ) = ( ( -u 1 ^ ( n + 1 ) ) x. -u 1 ) )
120 115 a1i 
 |-  ( n e. NN -> -u 1 e. CC )
121 120 117 expcld 
 |-  ( n e. NN -> ( -u 1 ^ ( n + 1 ) ) e. CC )
122 121 120 mulcomd 
 |-  ( n e. NN -> ( ( -u 1 ^ ( n + 1 ) ) x. -u 1 ) = ( -u 1 x. ( -u 1 ^ ( n + 1 ) ) ) )
123 119 122 eqtr2d 
 |-  ( n e. NN -> ( -u 1 x. ( -u 1 ^ ( n + 1 ) ) ) = ( -u 1 ^ ( ( n + 1 ) + 1 ) ) )
124 123 ad3antlr 
 |-  ( ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( n + 1 ) ) ) ) /\ ( n + 1 ) <_ N ) -> ( -u 1 x. ( -u 1 ^ ( n + 1 ) ) ) = ( -u 1 ^ ( ( n + 1 ) + 1 ) ) )
125 114 124 eqtrd 
 |-  ( ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( n + 1 ) ) ) ) /\ ( n + 1 ) <_ N ) -> ( ( S ` ( ( pmTrsp ` D ) ` { n , ( n + 1 ) } ) ) x. ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) ) = ( -u 1 ^ ( ( n + 1 ) + 1 ) ) )
126 83 107 125 3eqtrd 
 |-  ( ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( n + 1 ) ) ) ) /\ ( n + 1 ) <_ N ) -> ( S ` ( i e. D |-> if ( i = 1 , ( n + 1 ) , if ( i <_ ( n + 1 ) , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( ( n + 1 ) + 1 ) ) )
127 126 ex 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ ( n <_ N -> ( S ` ( i e. D |-> if ( i = 1 , n , if ( i <_ n , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( n + 1 ) ) ) ) -> ( ( n + 1 ) <_ N -> ( S ` ( i e. D |-> if ( i = 1 , ( n + 1 ) , if ( i <_ ( n + 1 ) , ( i - 1 ) , i ) ) ) ) = ( -u 1 ^ ( ( n + 1 ) + 1 ) ) ) )
128 22 33 44 56 71 127 nnindd 
 |-  ( ( N e. NN /\ I e. NN ) -> ( I <_ N -> ( S ` P ) = ( -u 1 ^ ( I + 1 ) ) ) )
129 128 imp 
 |-  ( ( ( N e. NN /\ I e. NN ) /\ I <_ N ) -> ( S ` P ) = ( -u 1 ^ ( I + 1 ) ) )
130 11 129 sylbi 
 |-  ( ( N e. NN /\ I e. NN /\ I <_ N ) -> ( S ` P ) = ( -u 1 ^ ( I + 1 ) ) )
131 10 130 syl 
 |-  ( I e. D -> ( S ` P ) = ( -u 1 ^ ( I + 1 ) ) )