| 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 ) ) |