Metamath Proof Explorer

Theorem madjusmdetlem2

Description: Lemma for madjusmdet . (Contributed by Thierry Arnoux, 26-Aug-2020)

Ref Expression
Hypotheses madjusmdet.b 
|- B = ( Base ` A )
madjusmdet.a 
|- A = ( ( 1 ... N ) Mat R )
madjusmdet.d 
|- D = ( ( 1 ... N ) maDet R )
madjusmdet.k 
|- K = ( ( 1 ... N ) maAdju R )
madjusmdet.t 
|- .x. = ( .r ` R )
madjusmdet.z 
|- Z = ( ZRHom ` R )
madjusmdet.e 
|- E = ( ( 1 ... ( N - 1 ) ) maDet R )
madjusmdet.n 
|- ( ph -> N e. NN )
madjusmdet.r 
|- ( ph -> R e. CRing )
madjusmdet.i 
|- ( ph -> I e. ( 1 ... N ) )
madjusmdet.j 
|- ( ph -> J e. ( 1 ... N ) )
madjusmdet.m 
|- ( ph -> M e. B )
madjusmdetlem2.p 
|- P = ( i e. ( 1 ... N ) |-> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) )
madjusmdetlem2.s 
|- S = ( i e. ( 1 ... N ) |-> if ( i = 1 , N , if ( i <_ N , ( i - 1 ) , i ) ) )
Assertion madjusmdetlem2 
|- ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> if ( X < I , X , ( X + 1 ) ) = ( ( P o. `' S ) ` X ) )

Proof

Step Hyp Ref Expression
1 madjusmdet.b 
 |-  B = ( Base ` A )
2 madjusmdet.a 
 |-  A = ( ( 1 ... N ) Mat R )
3 madjusmdet.d 
 |-  D = ( ( 1 ... N ) maDet R )
4 madjusmdet.k 
 |-  K = ( ( 1 ... N ) maAdju R )
5 madjusmdet.t 
 |-  .x. = ( .r ` R )
6 madjusmdet.z 
 |-  Z = ( ZRHom ` R )
7 madjusmdet.e 
 |-  E = ( ( 1 ... ( N - 1 ) ) maDet R )
8 madjusmdet.n 
 |-  ( ph -> N e. NN )
9 madjusmdet.r 
 |-  ( ph -> R e. CRing )
10 madjusmdet.i 
 |-  ( ph -> I e. ( 1 ... N ) )
11 madjusmdet.j 
 |-  ( ph -> J e. ( 1 ... N ) )
12 madjusmdet.m 
 |-  ( ph -> M e. B )
13 madjusmdetlem2.p 
 |-  P = ( i e. ( 1 ... N ) |-> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) )
14 madjusmdetlem2.s 
 |-  S = ( i e. ( 1 ... N ) |-> if ( i = 1 , N , if ( i <_ N , ( i - 1 ) , i ) ) )
15 nnuz 
 |-  NN = ( ZZ>= ` 1 )
16 8 15 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 1 ) )
17 eluzfz2 
 |-  ( N e. ( ZZ>= ` 1 ) -> N e. ( 1 ... N ) )
18 16 17 syl 
 |-  ( ph -> N e. ( 1 ... N ) )
19 eqid 
 |-  ( 1 ... N ) = ( 1 ... N )
20 eqid 
 |-  ( SymGrp ` ( 1 ... N ) ) = ( SymGrp ` ( 1 ... N ) )
21 eqid 
 |-  ( Base ` ( SymGrp ` ( 1 ... N ) ) ) = ( Base ` ( SymGrp ` ( 1 ... N ) ) )
22 19 14 20 21 fzto1st 
 |-  ( N e. ( 1 ... N ) -> S e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
23 18 22 syl 
 |-  ( ph -> S e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) )
24 20 21 symgbasf1o 
 |-  ( S e. ( Base ` ( SymGrp ` ( 1 ... N ) ) ) -> S : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
25 23 24 syl 
 |-  ( ph -> S : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
26 25 adantr 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> S : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
27 fznatpl1 
 |-  ( ( N e. NN /\ X e. ( 1 ... ( N - 1 ) ) ) -> ( X + 1 ) e. ( 1 ... N ) )
28 8 27 sylan 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> ( X + 1 ) e. ( 1 ... N ) )
29 eqeq1 
 |-  ( i = x -> ( i = 1 <-> x = 1 ) )
30 breq1 
 |-  ( i = x -> ( i <_ N <-> x <_ N ) )
31 oveq1 
 |-  ( i = x -> ( i - 1 ) = ( x - 1 ) )
32 id 
 |-  ( i = x -> i = x )
33 30 31 32 ifbieq12d 
 |-  ( i = x -> if ( i <_ N , ( i - 1 ) , i ) = if ( x <_ N , ( x - 1 ) , x ) )
34 29 33 ifbieq2d 
 |-  ( i = x -> if ( i = 1 , N , if ( i <_ N , ( i - 1 ) , i ) ) = if ( x = 1 , N , if ( x <_ N , ( x - 1 ) , x ) ) )
35 34 cbvmptv 
 |-  ( i e. ( 1 ... N ) |-> if ( i = 1 , N , if ( i <_ N , ( i - 1 ) , i ) ) ) = ( x e. ( 1 ... N ) |-> if ( x = 1 , N , if ( x <_ N , ( x - 1 ) , x ) ) )
36 14 35 eqtri 
 |-  S = ( x e. ( 1 ... N ) |-> if ( x = 1 , N , if ( x <_ N , ( x - 1 ) , x ) ) )
37 simpr 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> x = ( X + 1 ) )
38 1red 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> 1 e. RR )
39 fz1ssnn 
 |-  ( 1 ... ( N - 1 ) ) C_ NN
40 simpr 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> X e. ( 1 ... ( N - 1 ) ) )
41 39 40 sselid 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> X e. NN )
42 41 nnrpd 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> X e. RR+ )
43 42 adantr 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> X e. RR+ )
44 38 43 ltaddrp2d 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> 1 < ( X + 1 ) )
45 38 44 gtned 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> ( X + 1 ) =/= 1 )
46 37 45 eqnetrd 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> x =/= 1 )
47 46 neneqd 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> -. x = 1 )
48 47 iffalsed 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> if ( x = 1 , N , if ( x <_ N , ( x - 1 ) , x ) ) = if ( x <_ N , ( x - 1 ) , x ) )
49 8 adantr 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> N e. NN )
50 41 nnnn0d 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> X e. NN0 )
51 49 nnnn0d 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> N e. NN0 )
52 elfzle2 
 |-  ( X e. ( 1 ... ( N - 1 ) ) -> X <_ ( N - 1 ) )
53 40 52 syl 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> X <_ ( N - 1 ) )
54 nn0ltlem1 
 |-  ( ( X e. NN0 /\ N e. NN0 ) -> ( X < N <-> X <_ ( N - 1 ) ) )
55 54 biimpar 
 |-  ( ( ( X e. NN0 /\ N e. NN0 ) /\ X <_ ( N - 1 ) ) -> X < N )
56 50 51 53 55 syl21anc 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> X < N )
57 nnltp1le 
 |-  ( ( X e. NN /\ N e. NN ) -> ( X < N <-> ( X + 1 ) <_ N ) )
58 57 biimpa 
 |-  ( ( ( X e. NN /\ N e. NN ) /\ X < N ) -> ( X + 1 ) <_ N )
59 41 49 56 58 syl21anc 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> ( X + 1 ) <_ N )
60 59 adantr 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> ( X + 1 ) <_ N )
61 37 60 eqbrtrd 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> x <_ N )
62 61 iftrued 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> if ( x <_ N , ( x - 1 ) , x ) = ( x - 1 ) )
63 37 oveq1d 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> ( x - 1 ) = ( ( X + 1 ) - 1 ) )
64 41 nncnd 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> X e. CC )
65 1cnd 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> 1 e. CC )
66 64 65 pncand 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> ( ( X + 1 ) - 1 ) = X )
67 66 adantr 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> ( ( X + 1 ) - 1 ) = X )
68 63 67 eqtrd 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> ( x - 1 ) = X )
69 48 62 68 3eqtrd 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> if ( x = 1 , N , if ( x <_ N , ( x - 1 ) , x ) ) = X )
70 36 69 28 40 fvmptd2 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> ( S ` ( X + 1 ) ) = X )
71 f1ocnvfv 
 |-  ( ( S : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ ( X + 1 ) e. ( 1 ... N ) ) -> ( ( S ` ( X + 1 ) ) = X -> ( `' S ` X ) = ( X + 1 ) ) )
72 71 imp 
 |-  ( ( ( S : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ ( X + 1 ) e. ( 1 ... N ) ) /\ ( S ` ( X + 1 ) ) = X ) -> ( `' S ` X ) = ( X + 1 ) )
73 26 28 70 72 syl21anc 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> ( `' S ` X ) = ( X + 1 ) )
74 73 fveq2d 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> ( P ` ( `' S ` X ) ) = ( P ` ( X + 1 ) ) )
75 74 adantr 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) -> ( P ` ( `' S ` X ) ) = ( P ` ( X + 1 ) ) )
76 breq1 
 |-  ( i = x -> ( i <_ I <-> x <_ I ) )
77 76 31 32 ifbieq12d 
 |-  ( i = x -> if ( i <_ I , ( i - 1 ) , i ) = if ( x <_ I , ( x - 1 ) , x ) )
78 29 77 ifbieq2d 
 |-  ( i = x -> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) = if ( x = 1 , I , if ( x <_ I , ( x - 1 ) , x ) ) )
79 78 cbvmptv 
 |-  ( i e. ( 1 ... N ) |-> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) ) = ( x e. ( 1 ... N ) |-> if ( x = 1 , I , if ( x <_ I , ( x - 1 ) , x ) ) )
80 13 79 eqtri 
 |-  P = ( x e. ( 1 ... N ) |-> if ( x = 1 , I , if ( x <_ I , ( x - 1 ) , x ) ) )
81 44 37 breqtrrd 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> 1 < x )
82 38 81 gtned 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> x =/= 1 )
83 82 neneqd 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> -. x = 1 )
84 83 iffalsed 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> if ( x = 1 , I , if ( x <_ I , ( x - 1 ) , x ) ) = if ( x <_ I , ( x - 1 ) , x ) )
85 84 adantlr 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) /\ x = ( X + 1 ) ) -> if ( x = 1 , I , if ( x <_ I , ( x - 1 ) , x ) ) = if ( x <_ I , ( x - 1 ) , x ) )
86 simpr 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) /\ x = ( X + 1 ) ) -> x = ( X + 1 ) )
87 41 ad2antrr 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) /\ x = ( X + 1 ) ) -> X e. NN )
88 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
89 88 10 sselid 
 |-  ( ph -> I e. NN )
90 89 ad3antrrr 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) /\ x = ( X + 1 ) ) -> I e. NN )
91 simplr 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) /\ x = ( X + 1 ) ) -> X < I )
92 nnltp1le 
 |-  ( ( X e. NN /\ I e. NN ) -> ( X < I <-> ( X + 1 ) <_ I ) )
93 92 biimpa 
 |-  ( ( ( X e. NN /\ I e. NN ) /\ X < I ) -> ( X + 1 ) <_ I )
94 87 90 91 93 syl21anc 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) /\ x = ( X + 1 ) ) -> ( X + 1 ) <_ I )
95 86 94 eqbrtrd 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) /\ x = ( X + 1 ) ) -> x <_ I )
96 95 iftrued 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) /\ x = ( X + 1 ) ) -> if ( x <_ I , ( x - 1 ) , x ) = ( x - 1 ) )
97 68 adantlr 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) /\ x = ( X + 1 ) ) -> ( x - 1 ) = X )
98 85 96 97 3eqtrd 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) /\ x = ( X + 1 ) ) -> if ( x = 1 , I , if ( x <_ I , ( x - 1 ) , x ) ) = X )
99 28 adantr 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) -> ( X + 1 ) e. ( 1 ... N ) )
100 simplr 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) -> X e. ( 1 ... ( N - 1 ) ) )
101 80 98 99 100 fvmptd2 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) -> ( P ` ( X + 1 ) ) = X )
102 75 101 eqtr2d 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) -> X = ( P ` ( `' S ` X ) ) )
103 74 adantr 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ -. X < I ) -> ( P ` ( `' S ` X ) ) = ( P ` ( X + 1 ) ) )
104 84 adantlr 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ -. X < I ) /\ x = ( X + 1 ) ) -> if ( x = 1 , I , if ( x <_ I , ( x - 1 ) , x ) ) = if ( x <_ I , ( x - 1 ) , x ) )
105 41 ad2antrr 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) /\ x <_ I ) -> X e. NN )
106 89 ad3antrrr 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) /\ x <_ I ) -> I e. NN )
107 simplr 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) /\ x <_ I ) -> x = ( X + 1 ) )
108 simpr 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) /\ x <_ I ) -> x <_ I )
109 107 108 eqbrtrrd 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) /\ x <_ I ) -> ( X + 1 ) <_ I )
110 92 biimpar 
 |-  ( ( ( X e. NN /\ I e. NN ) /\ ( X + 1 ) <_ I ) -> X < I )
111 105 106 109 110 syl21anc 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) /\ x <_ I ) -> X < I )
112 111 stoic1a 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) /\ -. X < I ) -> -. x <_ I )
113 112 an32s 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ -. X < I ) /\ x = ( X + 1 ) ) -> -. x <_ I )
114 113 iffalsed 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ -. X < I ) /\ x = ( X + 1 ) ) -> if ( x <_ I , ( x - 1 ) , x ) = x )
115 simpr 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ -. X < I ) /\ x = ( X + 1 ) ) -> x = ( X + 1 ) )
116 104 114 115 3eqtrd 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ -. X < I ) /\ x = ( X + 1 ) ) -> if ( x = 1 , I , if ( x <_ I , ( x - 1 ) , x ) ) = ( X + 1 ) )
117 28 adantr 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ -. X < I ) -> ( X + 1 ) e. ( 1 ... N ) )
118 80 116 117 117 fvmptd2 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ -. X < I ) -> ( P ` ( X + 1 ) ) = ( X + 1 ) )
119 103 118 eqtr2d 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ -. X < I ) -> ( X + 1 ) = ( P ` ( `' S ` X ) ) )
120 102 119 ifeqda 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> if ( X < I , X , ( X + 1 ) ) = ( P ` ( `' S ` X ) ) )
121 f1ocnv 
 |-  ( S : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> `' S : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
122 23 24 121 3syl 
 |-  ( ph -> `' S : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
123 f1ofun 
 |-  ( `' S : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> Fun `' S )
124 122 123 syl 
 |-  ( ph -> Fun `' S )
125 fzdif2 
 |-  ( N e. ( ZZ>= ` 1 ) -> ( ( 1 ... N ) \ { N } ) = ( 1 ... ( N - 1 ) ) )
126 16 125 syl 
 |-  ( ph -> ( ( 1 ... N ) \ { N } ) = ( 1 ... ( N - 1 ) ) )
127 difss 
 |-  ( ( 1 ... N ) \ { N } ) C_ ( 1 ... N )
128 126 127 eqsstrrdi 
 |-  ( ph -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
129 f1odm 
 |-  ( `' S : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> dom `' S = ( 1 ... N ) )
130 122 129 syl 
 |-  ( ph -> dom `' S = ( 1 ... N ) )
131 128 130 sseqtrrd 
 |-  ( ph -> ( 1 ... ( N - 1 ) ) C_ dom `' S )
132 131 sselda 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> X e. dom `' S )
133 fvco 
 |-  ( ( Fun `' S /\ X e. dom `' S ) -> ( ( P o. `' S ) ` X ) = ( P ` ( `' S ` X ) ) )
134 124 132 133 syl2an2r 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> ( ( P o. `' S ) ` X ) = ( P ` ( `' S ` X ) ) )
135 120 134 eqtr4d 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> if ( X < I , X , ( X + 1 ) ) = ( ( P o. `' S ) ` X ) )