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 36 a1i 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> S = ( x e. ( 1 ... N ) |-> if ( x = 1 , N , if ( x <_ N , ( x - 1 ) , x ) ) ) )
38 simpr 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> x = ( X + 1 ) )
39 1red 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> 1 e. RR )
40 fz1ssnn 
 |-  ( 1 ... ( N - 1 ) ) C_ NN
41 simpr 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> X e. ( 1 ... ( N - 1 ) ) )
42 40 41 sselid 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> X e. NN )
43 42 nnrpd 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> X e. RR+ )
44 43 adantr 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> X e. RR+ )
45 39 44 ltaddrp2d 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> 1 < ( X + 1 ) )
46 39 45 ltned 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> 1 =/= ( X + 1 ) )
47 46 necomd 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> ( X + 1 ) =/= 1 )
48 38 47 eqnetrd 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> x =/= 1 )
49 48 neneqd 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> -. x = 1 )
50 49 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 ) )
51 8 adantr 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> N e. NN )
52 42 nnnn0d 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> X e. NN0 )
53 51 nnnn0d 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> N e. NN0 )
54 elfzle2 
 |-  ( X e. ( 1 ... ( N - 1 ) ) -> X <_ ( N - 1 ) )
55 41 54 syl 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> X <_ ( N - 1 ) )
56 nn0ltlem1 
 |-  ( ( X e. NN0 /\ N e. NN0 ) -> ( X < N <-> X <_ ( N - 1 ) ) )
57 56 biimpar 
 |-  ( ( ( X e. NN0 /\ N e. NN0 ) /\ X <_ ( N - 1 ) ) -> X < N )
58 52 53 55 57 syl21anc 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> X < N )
59 nnltp1le 
 |-  ( ( X e. NN /\ N e. NN ) -> ( X < N <-> ( X + 1 ) <_ N ) )
60 59 biimpa 
 |-  ( ( ( X e. NN /\ N e. NN ) /\ X < N ) -> ( X + 1 ) <_ N )
61 42 51 58 60 syl21anc 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> ( X + 1 ) <_ N )
62 61 adantr 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> ( X + 1 ) <_ N )
63 38 62 eqbrtrd 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> x <_ N )
64 63 iftrued 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> if ( x <_ N , ( x - 1 ) , x ) = ( x - 1 ) )
65 38 oveq1d 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> ( x - 1 ) = ( ( X + 1 ) - 1 ) )
66 42 nncnd 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> X e. CC )
67 1cnd 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> 1 e. CC )
68 66 67 pncand 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> ( ( X + 1 ) - 1 ) = X )
69 68 adantr 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> ( ( X + 1 ) - 1 ) = X )
70 65 69 eqtrd 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> ( x - 1 ) = X )
71 50 64 70 3eqtrd 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> if ( x = 1 , N , if ( x <_ N , ( x - 1 ) , x ) ) = X )
72 37 71 28 41 fvmptd 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> ( S ` ( X + 1 ) ) = X )
73 72 idi 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> ( S ` ( X + 1 ) ) = X )
74 f1ocnvfv 
 |-  ( ( S : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ ( X + 1 ) e. ( 1 ... N ) ) -> ( ( S ` ( X + 1 ) ) = X -> ( `' S ` X ) = ( X + 1 ) ) )
75 74 imp 
 |-  ( ( ( S : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ ( X + 1 ) e. ( 1 ... N ) ) /\ ( S ` ( X + 1 ) ) = X ) -> ( `' S ` X ) = ( X + 1 ) )
76 26 28 73 75 syl21anc 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> ( `' S ` X ) = ( X + 1 ) )
77 76 fveq2d 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> ( P ` ( `' S ` X ) ) = ( P ` ( X + 1 ) ) )
78 77 adantr 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) -> ( P ` ( `' S ` X ) ) = ( P ` ( X + 1 ) ) )
79 32 breq1d 
 |-  ( i = x -> ( i <_ I <-> x <_ I ) )
80 79 31 32 ifbieq12d 
 |-  ( i = x -> if ( i <_ I , ( i - 1 ) , i ) = if ( x <_ I , ( x - 1 ) , x ) )
81 29 80 ifbieq2d 
 |-  ( i = x -> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) = if ( x = 1 , I , if ( x <_ I , ( x - 1 ) , x ) ) )
82 81 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 ) ) )
83 13 82 eqtri 
 |-  P = ( x e. ( 1 ... N ) |-> if ( x = 1 , I , if ( x <_ I , ( x - 1 ) , x ) ) )
84 83 a1i 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) -> P = ( x e. ( 1 ... N ) |-> if ( x = 1 , I , if ( x <_ I , ( x - 1 ) , x ) ) ) )
85 45 38 breqtrrd 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> 1 < x )
86 39 85 ltned 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> 1 =/= x )
87 86 necomd 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> x =/= 1 )
88 87 neneqd 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> -. x = 1 )
89 88 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 ) )
90 89 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 ) )
91 simpr 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) /\ x = ( X + 1 ) ) -> x = ( X + 1 ) )
92 42 ad2antrr 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) /\ x = ( X + 1 ) ) -> X e. NN )
93 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
94 93 10 sselid 
 |-  ( ph -> I e. NN )
95 94 ad3antrrr 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) /\ x = ( X + 1 ) ) -> I e. NN )
96 simplr 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) /\ x = ( X + 1 ) ) -> X < I )
97 nnltp1le 
 |-  ( ( X e. NN /\ I e. NN ) -> ( X < I <-> ( X + 1 ) <_ I ) )
98 97 biimpa 
 |-  ( ( ( X e. NN /\ I e. NN ) /\ X < I ) -> ( X + 1 ) <_ I )
99 92 95 96 98 syl21anc 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) /\ x = ( X + 1 ) ) -> ( X + 1 ) <_ I )
100 91 99 eqbrtrd 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) /\ x = ( X + 1 ) ) -> x <_ I )
101 100 iftrued 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) /\ x = ( X + 1 ) ) -> if ( x <_ I , ( x - 1 ) , x ) = ( x - 1 ) )
102 70 adantlr 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) /\ x = ( X + 1 ) ) -> ( x - 1 ) = X )
103 90 101 102 3eqtrd 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) /\ x = ( X + 1 ) ) -> if ( x = 1 , I , if ( x <_ I , ( x - 1 ) , x ) ) = X )
104 28 adantr 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) -> ( X + 1 ) e. ( 1 ... N ) )
105 simplr 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) -> X e. ( 1 ... ( N - 1 ) ) )
106 84 103 104 105 fvmptd 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) -> ( P ` ( X + 1 ) ) = X )
107 78 106 eqtr2d 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ X < I ) -> X = ( P ` ( `' S ` X ) ) )
108 77 adantr 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ -. X < I ) -> ( P ` ( `' S ` X ) ) = ( P ` ( X + 1 ) ) )
109 83 a1i 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ -. X < I ) -> P = ( x e. ( 1 ... N ) |-> if ( x = 1 , I , if ( x <_ I , ( x - 1 ) , x ) ) ) )
110 89 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 ) )
111 42 ad2antrr 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) /\ x <_ I ) -> X e. NN )
112 94 ad3antrrr 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) /\ x <_ I ) -> I e. NN )
113 38 adantr 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) /\ x <_ I ) -> x = ( X + 1 ) )
114 simpr 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) /\ x <_ I ) -> x <_ I )
115 113 114 eqbrtrrd 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) /\ x <_ I ) -> ( X + 1 ) <_ I )
116 97 biimpar 
 |-  ( ( ( X e. NN /\ I e. NN ) /\ ( X + 1 ) <_ I ) -> X < I )
117 111 112 115 116 syl21anc 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) /\ x <_ I ) -> X < I )
118 117 ex 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> ( x <_ I -> X < I ) )
119 118 con3d 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) -> ( -. X < I -> -. x <_ I ) )
120 119 imp 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ x = ( X + 1 ) ) /\ -. X < I ) -> -. x <_ I )
121 120 an32s 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ -. X < I ) /\ x = ( X + 1 ) ) -> -. x <_ I )
122 121 iffalsed 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ -. X < I ) /\ x = ( X + 1 ) ) -> if ( x <_ I , ( x - 1 ) , x ) = x )
123 simpr 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ -. X < I ) /\ x = ( X + 1 ) ) -> x = ( X + 1 ) )
124 122 123 eqtrd 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ -. X < I ) /\ x = ( X + 1 ) ) -> if ( x <_ I , ( x - 1 ) , x ) = ( X + 1 ) )
125 110 124 eqtrd 
 |-  ( ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ -. X < I ) /\ x = ( X + 1 ) ) -> if ( x = 1 , I , if ( x <_ I , ( x - 1 ) , x ) ) = ( X + 1 ) )
126 28 adantr 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ -. X < I ) -> ( X + 1 ) e. ( 1 ... N ) )
127 109 125 126 126 fvmptd 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ -. X < I ) -> ( P ` ( X + 1 ) ) = ( X + 1 ) )
128 108 127 eqtr2d 
 |-  ( ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) /\ -. X < I ) -> ( X + 1 ) = ( P ` ( `' S ` X ) ) )
129 107 128 ifeqda 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> if ( X < I , X , ( X + 1 ) ) = ( P ` ( `' S ` X ) ) )
130 f1ocnv 
 |-  ( S : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> `' S : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
131 23 24 130 3syl 
 |-  ( ph -> `' S : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
132 f1ofun 
 |-  ( `' S : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> Fun `' S )
133 131 132 syl 
 |-  ( ph -> Fun `' S )
134 133 adantr 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> Fun `' S )
135 fzdif2 
 |-  ( N e. ( ZZ>= ` 1 ) -> ( ( 1 ... N ) \ { N } ) = ( 1 ... ( N - 1 ) ) )
136 16 135 syl 
 |-  ( ph -> ( ( 1 ... N ) \ { N } ) = ( 1 ... ( N - 1 ) ) )
137 difss 
 |-  ( ( 1 ... N ) \ { N } ) C_ ( 1 ... N )
138 136 137 eqsstrrdi 
 |-  ( ph -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
139 f1odm 
 |-  ( `' S : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> dom `' S = ( 1 ... N ) )
140 131 139 syl 
 |-  ( ph -> dom `' S = ( 1 ... N ) )
141 138 140 sseqtrrd 
 |-  ( ph -> ( 1 ... ( N - 1 ) ) C_ dom `' S )
142 141 adantr 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> ( 1 ... ( N - 1 ) ) C_ dom `' S )
143 142 41 sseldd 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> X e. dom `' S )
144 fvco 
 |-  ( ( Fun `' S /\ X e. dom `' S ) -> ( ( P o. `' S ) ` X ) = ( P ` ( `' S ` X ) ) )
145 134 143 144 syl2anc 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> ( ( P o. `' S ) ` X ) = ( P ` ( `' S ` X ) ) )
146 129 145 eqtr4d 
 |-  ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> if ( X < I , X , ( X + 1 ) ) = ( ( P o. `' S ) ` X ) )