| Step | Hyp | Ref | Expression | 
						
							| 1 |  | madjusmdet.b | ⊢ 𝐵  =  ( Base ‘ 𝐴 ) | 
						
							| 2 |  | madjusmdet.a | ⊢ 𝐴  =  ( ( 1 ... 𝑁 )  Mat  𝑅 ) | 
						
							| 3 |  | madjusmdet.d | ⊢ 𝐷  =  ( ( 1 ... 𝑁 )  maDet  𝑅 ) | 
						
							| 4 |  | madjusmdet.k | ⊢ 𝐾  =  ( ( 1 ... 𝑁 )  maAdju  𝑅 ) | 
						
							| 5 |  | madjusmdet.t | ⊢  ·   =  ( .r ‘ 𝑅 ) | 
						
							| 6 |  | madjusmdet.z | ⊢ 𝑍  =  ( ℤRHom ‘ 𝑅 ) | 
						
							| 7 |  | madjusmdet.e | ⊢ 𝐸  =  ( ( 1 ... ( 𝑁  −  1 ) )  maDet  𝑅 ) | 
						
							| 8 |  | madjusmdet.n | ⊢ ( 𝜑  →  𝑁  ∈  ℕ ) | 
						
							| 9 |  | madjusmdet.r | ⊢ ( 𝜑  →  𝑅  ∈  CRing ) | 
						
							| 10 |  | madjusmdet.i | ⊢ ( 𝜑  →  𝐼  ∈  ( 1 ... 𝑁 ) ) | 
						
							| 11 |  | madjusmdet.j | ⊢ ( 𝜑  →  𝐽  ∈  ( 1 ... 𝑁 ) ) | 
						
							| 12 |  | madjusmdet.m | ⊢ ( 𝜑  →  𝑀  ∈  𝐵 ) | 
						
							| 13 |  | madjusmdetlem2.p | ⊢ 𝑃  =  ( 𝑖  ∈  ( 1 ... 𝑁 )  ↦  if ( 𝑖  =  1 ,  𝐼 ,  if ( 𝑖  ≤  𝐼 ,  ( 𝑖  −  1 ) ,  𝑖 ) ) ) | 
						
							| 14 |  | madjusmdetlem2.s | ⊢ 𝑆  =  ( 𝑖  ∈  ( 1 ... 𝑁 )  ↦  if ( 𝑖  =  1 ,  𝑁 ,  if ( 𝑖  ≤  𝑁 ,  ( 𝑖  −  1 ) ,  𝑖 ) ) ) | 
						
							| 15 |  | nnuz | ⊢ ℕ  =  ( ℤ≥ ‘ 1 ) | 
						
							| 16 | 8 15 | eleqtrdi | ⊢ ( 𝜑  →  𝑁  ∈  ( ℤ≥ ‘ 1 ) ) | 
						
							| 17 |  | eluzfz2 | ⊢ ( 𝑁  ∈  ( ℤ≥ ‘ 1 )  →  𝑁  ∈  ( 1 ... 𝑁 ) ) | 
						
							| 18 | 16 17 | syl | ⊢ ( 𝜑  →  𝑁  ∈  ( 1 ... 𝑁 ) ) | 
						
							| 19 |  | eqid | ⊢ ( 1 ... 𝑁 )  =  ( 1 ... 𝑁 ) | 
						
							| 20 |  | eqid | ⊢ ( SymGrp ‘ ( 1 ... 𝑁 ) )  =  ( SymGrp ‘ ( 1 ... 𝑁 ) ) | 
						
							| 21 |  | eqid | ⊢ ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) )  =  ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) | 
						
							| 22 | 19 14 20 21 | fzto1st | ⊢ ( 𝑁  ∈  ( 1 ... 𝑁 )  →  𝑆  ∈  ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ) | 
						
							| 23 | 18 22 | syl | ⊢ ( 𝜑  →  𝑆  ∈  ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) ) ) | 
						
							| 24 | 20 21 | symgbasf1o | ⊢ ( 𝑆  ∈  ( Base ‘ ( SymGrp ‘ ( 1 ... 𝑁 ) ) )  →  𝑆 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) | 
						
							| 25 | 23 24 | syl | ⊢ ( 𝜑  →  𝑆 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) | 
						
							| 26 | 25 | adantr | ⊢ ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  →  𝑆 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) | 
						
							| 27 |  | fznatpl1 | ⊢ ( ( 𝑁  ∈  ℕ  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  →  ( 𝑋  +  1 )  ∈  ( 1 ... 𝑁 ) ) | 
						
							| 28 | 8 27 | sylan | ⊢ ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  →  ( 𝑋  +  1 )  ∈  ( 1 ... 𝑁 ) ) | 
						
							| 29 |  | eqeq1 | ⊢ ( 𝑖  =  𝑥  →  ( 𝑖  =  1  ↔  𝑥  =  1 ) ) | 
						
							| 30 |  | breq1 | ⊢ ( 𝑖  =  𝑥  →  ( 𝑖  ≤  𝑁  ↔  𝑥  ≤  𝑁 ) ) | 
						
							| 31 |  | oveq1 | ⊢ ( 𝑖  =  𝑥  →  ( 𝑖  −  1 )  =  ( 𝑥  −  1 ) ) | 
						
							| 32 |  | id | ⊢ ( 𝑖  =  𝑥  →  𝑖  =  𝑥 ) | 
						
							| 33 | 30 31 32 | ifbieq12d | ⊢ ( 𝑖  =  𝑥  →  if ( 𝑖  ≤  𝑁 ,  ( 𝑖  −  1 ) ,  𝑖 )  =  if ( 𝑥  ≤  𝑁 ,  ( 𝑥  −  1 ) ,  𝑥 ) ) | 
						
							| 34 | 29 33 | ifbieq2d | ⊢ ( 𝑖  =  𝑥  →  if ( 𝑖  =  1 ,  𝑁 ,  if ( 𝑖  ≤  𝑁 ,  ( 𝑖  −  1 ) ,  𝑖 ) )  =  if ( 𝑥  =  1 ,  𝑁 ,  if ( 𝑥  ≤  𝑁 ,  ( 𝑥  −  1 ) ,  𝑥 ) ) ) | 
						
							| 35 | 34 | cbvmptv | ⊢ ( 𝑖  ∈  ( 1 ... 𝑁 )  ↦  if ( 𝑖  =  1 ,  𝑁 ,  if ( 𝑖  ≤  𝑁 ,  ( 𝑖  −  1 ) ,  𝑖 ) ) )  =  ( 𝑥  ∈  ( 1 ... 𝑁 )  ↦  if ( 𝑥  =  1 ,  𝑁 ,  if ( 𝑥  ≤  𝑁 ,  ( 𝑥  −  1 ) ,  𝑥 ) ) ) | 
						
							| 36 | 14 35 | eqtri | ⊢ 𝑆  =  ( 𝑥  ∈  ( 1 ... 𝑁 )  ↦  if ( 𝑥  =  1 ,  𝑁 ,  if ( 𝑥  ≤  𝑁 ,  ( 𝑥  −  1 ) ,  𝑥 ) ) ) | 
						
							| 37 |  | simpr | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  𝑥  =  ( 𝑋  +  1 ) ) | 
						
							| 38 |  | 1red | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  1  ∈  ℝ ) | 
						
							| 39 |  | fz1ssnn | ⊢ ( 1 ... ( 𝑁  −  1 ) )  ⊆  ℕ | 
						
							| 40 |  | simpr | ⊢ ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  →  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) ) | 
						
							| 41 | 39 40 | sselid | ⊢ ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  →  𝑋  ∈  ℕ ) | 
						
							| 42 | 41 | nnrpd | ⊢ ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  →  𝑋  ∈  ℝ+ ) | 
						
							| 43 | 42 | adantr | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  𝑋  ∈  ℝ+ ) | 
						
							| 44 | 38 43 | ltaddrp2d | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  1  <  ( 𝑋  +  1 ) ) | 
						
							| 45 | 38 44 | gtned | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  ( 𝑋  +  1 )  ≠  1 ) | 
						
							| 46 | 37 45 | eqnetrd | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  𝑥  ≠  1 ) | 
						
							| 47 | 46 | neneqd | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  ¬  𝑥  =  1 ) | 
						
							| 48 | 47 | iffalsed | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  if ( 𝑥  =  1 ,  𝑁 ,  if ( 𝑥  ≤  𝑁 ,  ( 𝑥  −  1 ) ,  𝑥 ) )  =  if ( 𝑥  ≤  𝑁 ,  ( 𝑥  −  1 ) ,  𝑥 ) ) | 
						
							| 49 | 8 | adantr | ⊢ ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  →  𝑁  ∈  ℕ ) | 
						
							| 50 | 41 | nnnn0d | ⊢ ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  →  𝑋  ∈  ℕ0 ) | 
						
							| 51 | 49 | nnnn0d | ⊢ ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  →  𝑁  ∈  ℕ0 ) | 
						
							| 52 |  | elfzle2 | ⊢ ( 𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) )  →  𝑋  ≤  ( 𝑁  −  1 ) ) | 
						
							| 53 | 40 52 | syl | ⊢ ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  →  𝑋  ≤  ( 𝑁  −  1 ) ) | 
						
							| 54 |  | nn0ltlem1 | ⊢ ( ( 𝑋  ∈  ℕ0  ∧  𝑁  ∈  ℕ0 )  →  ( 𝑋  <  𝑁  ↔  𝑋  ≤  ( 𝑁  −  1 ) ) ) | 
						
							| 55 | 54 | biimpar | ⊢ ( ( ( 𝑋  ∈  ℕ0  ∧  𝑁  ∈  ℕ0 )  ∧  𝑋  ≤  ( 𝑁  −  1 ) )  →  𝑋  <  𝑁 ) | 
						
							| 56 | 50 51 53 55 | syl21anc | ⊢ ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  →  𝑋  <  𝑁 ) | 
						
							| 57 |  | nnltp1le | ⊢ ( ( 𝑋  ∈  ℕ  ∧  𝑁  ∈  ℕ )  →  ( 𝑋  <  𝑁  ↔  ( 𝑋  +  1 )  ≤  𝑁 ) ) | 
						
							| 58 | 57 | biimpa | ⊢ ( ( ( 𝑋  ∈  ℕ  ∧  𝑁  ∈  ℕ )  ∧  𝑋  <  𝑁 )  →  ( 𝑋  +  1 )  ≤  𝑁 ) | 
						
							| 59 | 41 49 56 58 | syl21anc | ⊢ ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  →  ( 𝑋  +  1 )  ≤  𝑁 ) | 
						
							| 60 | 59 | adantr | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  ( 𝑋  +  1 )  ≤  𝑁 ) | 
						
							| 61 | 37 60 | eqbrtrd | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  𝑥  ≤  𝑁 ) | 
						
							| 62 | 61 | iftrued | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  if ( 𝑥  ≤  𝑁 ,  ( 𝑥  −  1 ) ,  𝑥 )  =  ( 𝑥  −  1 ) ) | 
						
							| 63 | 37 | oveq1d | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  ( 𝑥  −  1 )  =  ( ( 𝑋  +  1 )  −  1 ) ) | 
						
							| 64 | 41 | nncnd | ⊢ ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  →  𝑋  ∈  ℂ ) | 
						
							| 65 |  | 1cnd | ⊢ ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  →  1  ∈  ℂ ) | 
						
							| 66 | 64 65 | pncand | ⊢ ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  →  ( ( 𝑋  +  1 )  −  1 )  =  𝑋 ) | 
						
							| 67 | 66 | adantr | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  ( ( 𝑋  +  1 )  −  1 )  =  𝑋 ) | 
						
							| 68 | 63 67 | eqtrd | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  ( 𝑥  −  1 )  =  𝑋 ) | 
						
							| 69 | 48 62 68 | 3eqtrd | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  if ( 𝑥  =  1 ,  𝑁 ,  if ( 𝑥  ≤  𝑁 ,  ( 𝑥  −  1 ) ,  𝑥 ) )  =  𝑋 ) | 
						
							| 70 | 36 69 28 40 | fvmptd2 | ⊢ ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  →  ( 𝑆 ‘ ( 𝑋  +  1 ) )  =  𝑋 ) | 
						
							| 71 |  | f1ocnvfv | ⊢ ( ( 𝑆 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 )  ∧  ( 𝑋  +  1 )  ∈  ( 1 ... 𝑁 ) )  →  ( ( 𝑆 ‘ ( 𝑋  +  1 ) )  =  𝑋  →  ( ◡ 𝑆 ‘ 𝑋 )  =  ( 𝑋  +  1 ) ) ) | 
						
							| 72 | 71 | imp | ⊢ ( ( ( 𝑆 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 )  ∧  ( 𝑋  +  1 )  ∈  ( 1 ... 𝑁 ) )  ∧  ( 𝑆 ‘ ( 𝑋  +  1 ) )  =  𝑋 )  →  ( ◡ 𝑆 ‘ 𝑋 )  =  ( 𝑋  +  1 ) ) | 
						
							| 73 | 26 28 70 72 | syl21anc | ⊢ ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  →  ( ◡ 𝑆 ‘ 𝑋 )  =  ( 𝑋  +  1 ) ) | 
						
							| 74 | 73 | fveq2d | ⊢ ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  →  ( 𝑃 ‘ ( ◡ 𝑆 ‘ 𝑋 ) )  =  ( 𝑃 ‘ ( 𝑋  +  1 ) ) ) | 
						
							| 75 | 74 | adantr | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑋  <  𝐼 )  →  ( 𝑃 ‘ ( ◡ 𝑆 ‘ 𝑋 ) )  =  ( 𝑃 ‘ ( 𝑋  +  1 ) ) ) | 
						
							| 76 |  | breq1 | ⊢ ( 𝑖  =  𝑥  →  ( 𝑖  ≤  𝐼  ↔  𝑥  ≤  𝐼 ) ) | 
						
							| 77 | 76 31 32 | ifbieq12d | ⊢ ( 𝑖  =  𝑥  →  if ( 𝑖  ≤  𝐼 ,  ( 𝑖  −  1 ) ,  𝑖 )  =  if ( 𝑥  ≤  𝐼 ,  ( 𝑥  −  1 ) ,  𝑥 ) ) | 
						
							| 78 | 29 77 | ifbieq2d | ⊢ ( 𝑖  =  𝑥  →  if ( 𝑖  =  1 ,  𝐼 ,  if ( 𝑖  ≤  𝐼 ,  ( 𝑖  −  1 ) ,  𝑖 ) )  =  if ( 𝑥  =  1 ,  𝐼 ,  if ( 𝑥  ≤  𝐼 ,  ( 𝑥  −  1 ) ,  𝑥 ) ) ) | 
						
							| 79 | 78 | cbvmptv | ⊢ ( 𝑖  ∈  ( 1 ... 𝑁 )  ↦  if ( 𝑖  =  1 ,  𝐼 ,  if ( 𝑖  ≤  𝐼 ,  ( 𝑖  −  1 ) ,  𝑖 ) ) )  =  ( 𝑥  ∈  ( 1 ... 𝑁 )  ↦  if ( 𝑥  =  1 ,  𝐼 ,  if ( 𝑥  ≤  𝐼 ,  ( 𝑥  −  1 ) ,  𝑥 ) ) ) | 
						
							| 80 | 13 79 | eqtri | ⊢ 𝑃  =  ( 𝑥  ∈  ( 1 ... 𝑁 )  ↦  if ( 𝑥  =  1 ,  𝐼 ,  if ( 𝑥  ≤  𝐼 ,  ( 𝑥  −  1 ) ,  𝑥 ) ) ) | 
						
							| 81 | 44 37 | breqtrrd | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  1  <  𝑥 ) | 
						
							| 82 | 38 81 | gtned | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  𝑥  ≠  1 ) | 
						
							| 83 | 82 | neneqd | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  ¬  𝑥  =  1 ) | 
						
							| 84 | 83 | iffalsed | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  if ( 𝑥  =  1 ,  𝐼 ,  if ( 𝑥  ≤  𝐼 ,  ( 𝑥  −  1 ) ,  𝑥 ) )  =  if ( 𝑥  ≤  𝐼 ,  ( 𝑥  −  1 ) ,  𝑥 ) ) | 
						
							| 85 | 84 | adantlr | ⊢ ( ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑋  <  𝐼 )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  if ( 𝑥  =  1 ,  𝐼 ,  if ( 𝑥  ≤  𝐼 ,  ( 𝑥  −  1 ) ,  𝑥 ) )  =  if ( 𝑥  ≤  𝐼 ,  ( 𝑥  −  1 ) ,  𝑥 ) ) | 
						
							| 86 |  | simpr | ⊢ ( ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑋  <  𝐼 )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  𝑥  =  ( 𝑋  +  1 ) ) | 
						
							| 87 | 41 | ad2antrr | ⊢ ( ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑋  <  𝐼 )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  𝑋  ∈  ℕ ) | 
						
							| 88 |  | fz1ssnn | ⊢ ( 1 ... 𝑁 )  ⊆  ℕ | 
						
							| 89 | 88 10 | sselid | ⊢ ( 𝜑  →  𝐼  ∈  ℕ ) | 
						
							| 90 | 89 | ad3antrrr | ⊢ ( ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑋  <  𝐼 )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  𝐼  ∈  ℕ ) | 
						
							| 91 |  | simplr | ⊢ ( ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑋  <  𝐼 )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  𝑋  <  𝐼 ) | 
						
							| 92 |  | nnltp1le | ⊢ ( ( 𝑋  ∈  ℕ  ∧  𝐼  ∈  ℕ )  →  ( 𝑋  <  𝐼  ↔  ( 𝑋  +  1 )  ≤  𝐼 ) ) | 
						
							| 93 | 92 | biimpa | ⊢ ( ( ( 𝑋  ∈  ℕ  ∧  𝐼  ∈  ℕ )  ∧  𝑋  <  𝐼 )  →  ( 𝑋  +  1 )  ≤  𝐼 ) | 
						
							| 94 | 87 90 91 93 | syl21anc | ⊢ ( ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑋  <  𝐼 )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  ( 𝑋  +  1 )  ≤  𝐼 ) | 
						
							| 95 | 86 94 | eqbrtrd | ⊢ ( ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑋  <  𝐼 )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  𝑥  ≤  𝐼 ) | 
						
							| 96 | 95 | iftrued | ⊢ ( ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑋  <  𝐼 )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  if ( 𝑥  ≤  𝐼 ,  ( 𝑥  −  1 ) ,  𝑥 )  =  ( 𝑥  −  1 ) ) | 
						
							| 97 | 68 | adantlr | ⊢ ( ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑋  <  𝐼 )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  ( 𝑥  −  1 )  =  𝑋 ) | 
						
							| 98 | 85 96 97 | 3eqtrd | ⊢ ( ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑋  <  𝐼 )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  if ( 𝑥  =  1 ,  𝐼 ,  if ( 𝑥  ≤  𝐼 ,  ( 𝑥  −  1 ) ,  𝑥 ) )  =  𝑋 ) | 
						
							| 99 | 28 | adantr | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑋  <  𝐼 )  →  ( 𝑋  +  1 )  ∈  ( 1 ... 𝑁 ) ) | 
						
							| 100 |  | simplr | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑋  <  𝐼 )  →  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) ) | 
						
							| 101 | 80 98 99 100 | fvmptd2 | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑋  <  𝐼 )  →  ( 𝑃 ‘ ( 𝑋  +  1 ) )  =  𝑋 ) | 
						
							| 102 | 75 101 | eqtr2d | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑋  <  𝐼 )  →  𝑋  =  ( 𝑃 ‘ ( ◡ 𝑆 ‘ 𝑋 ) ) ) | 
						
							| 103 | 74 | adantr | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  ¬  𝑋  <  𝐼 )  →  ( 𝑃 ‘ ( ◡ 𝑆 ‘ 𝑋 ) )  =  ( 𝑃 ‘ ( 𝑋  +  1 ) ) ) | 
						
							| 104 | 84 | adantlr | ⊢ ( ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  ¬  𝑋  <  𝐼 )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  if ( 𝑥  =  1 ,  𝐼 ,  if ( 𝑥  ≤  𝐼 ,  ( 𝑥  −  1 ) ,  𝑥 ) )  =  if ( 𝑥  ≤  𝐼 ,  ( 𝑥  −  1 ) ,  𝑥 ) ) | 
						
							| 105 | 41 | ad2antrr | ⊢ ( ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  ∧  𝑥  ≤  𝐼 )  →  𝑋  ∈  ℕ ) | 
						
							| 106 | 89 | ad3antrrr | ⊢ ( ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  ∧  𝑥  ≤  𝐼 )  →  𝐼  ∈  ℕ ) | 
						
							| 107 |  | simplr | ⊢ ( ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  ∧  𝑥  ≤  𝐼 )  →  𝑥  =  ( 𝑋  +  1 ) ) | 
						
							| 108 |  | simpr | ⊢ ( ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  ∧  𝑥  ≤  𝐼 )  →  𝑥  ≤  𝐼 ) | 
						
							| 109 | 107 108 | eqbrtrrd | ⊢ ( ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  ∧  𝑥  ≤  𝐼 )  →  ( 𝑋  +  1 )  ≤  𝐼 ) | 
						
							| 110 | 92 | biimpar | ⊢ ( ( ( 𝑋  ∈  ℕ  ∧  𝐼  ∈  ℕ )  ∧  ( 𝑋  +  1 )  ≤  𝐼 )  →  𝑋  <  𝐼 ) | 
						
							| 111 | 105 106 109 110 | syl21anc | ⊢ ( ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  ∧  𝑥  ≤  𝐼 )  →  𝑋  <  𝐼 ) | 
						
							| 112 | 111 | stoic1a | ⊢ ( ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  𝑥  =  ( 𝑋  +  1 ) )  ∧  ¬  𝑋  <  𝐼 )  →  ¬  𝑥  ≤  𝐼 ) | 
						
							| 113 | 112 | an32s | ⊢ ( ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  ¬  𝑋  <  𝐼 )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  ¬  𝑥  ≤  𝐼 ) | 
						
							| 114 | 113 | iffalsed | ⊢ ( ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  ¬  𝑋  <  𝐼 )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  if ( 𝑥  ≤  𝐼 ,  ( 𝑥  −  1 ) ,  𝑥 )  =  𝑥 ) | 
						
							| 115 |  | simpr | ⊢ ( ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  ¬  𝑋  <  𝐼 )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  𝑥  =  ( 𝑋  +  1 ) ) | 
						
							| 116 | 104 114 115 | 3eqtrd | ⊢ ( ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  ¬  𝑋  <  𝐼 )  ∧  𝑥  =  ( 𝑋  +  1 ) )  →  if ( 𝑥  =  1 ,  𝐼 ,  if ( 𝑥  ≤  𝐼 ,  ( 𝑥  −  1 ) ,  𝑥 ) )  =  ( 𝑋  +  1 ) ) | 
						
							| 117 | 28 | adantr | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  ¬  𝑋  <  𝐼 )  →  ( 𝑋  +  1 )  ∈  ( 1 ... 𝑁 ) ) | 
						
							| 118 | 80 116 117 117 | fvmptd2 | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  ¬  𝑋  <  𝐼 )  →  ( 𝑃 ‘ ( 𝑋  +  1 ) )  =  ( 𝑋  +  1 ) ) | 
						
							| 119 | 103 118 | eqtr2d | ⊢ ( ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  ∧  ¬  𝑋  <  𝐼 )  →  ( 𝑋  +  1 )  =  ( 𝑃 ‘ ( ◡ 𝑆 ‘ 𝑋 ) ) ) | 
						
							| 120 | 102 119 | ifeqda | ⊢ ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  →  if ( 𝑋  <  𝐼 ,  𝑋 ,  ( 𝑋  +  1 ) )  =  ( 𝑃 ‘ ( ◡ 𝑆 ‘ 𝑋 ) ) ) | 
						
							| 121 |  | f1ocnv | ⊢ ( 𝑆 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 )  →  ◡ 𝑆 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) | 
						
							| 122 | 23 24 121 | 3syl | ⊢ ( 𝜑  →  ◡ 𝑆 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) | 
						
							| 123 |  | f1ofun | ⊢ ( ◡ 𝑆 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 )  →  Fun  ◡ 𝑆 ) | 
						
							| 124 | 122 123 | syl | ⊢ ( 𝜑  →  Fun  ◡ 𝑆 ) | 
						
							| 125 |  | fzdif2 | ⊢ ( 𝑁  ∈  ( ℤ≥ ‘ 1 )  →  ( ( 1 ... 𝑁 )  ∖  { 𝑁 } )  =  ( 1 ... ( 𝑁  −  1 ) ) ) | 
						
							| 126 | 16 125 | syl | ⊢ ( 𝜑  →  ( ( 1 ... 𝑁 )  ∖  { 𝑁 } )  =  ( 1 ... ( 𝑁  −  1 ) ) ) | 
						
							| 127 |  | difss | ⊢ ( ( 1 ... 𝑁 )  ∖  { 𝑁 } )  ⊆  ( 1 ... 𝑁 ) | 
						
							| 128 | 126 127 | eqsstrrdi | ⊢ ( 𝜑  →  ( 1 ... ( 𝑁  −  1 ) )  ⊆  ( 1 ... 𝑁 ) ) | 
						
							| 129 |  | f1odm | ⊢ ( ◡ 𝑆 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 )  →  dom  ◡ 𝑆  =  ( 1 ... 𝑁 ) ) | 
						
							| 130 | 122 129 | syl | ⊢ ( 𝜑  →  dom  ◡ 𝑆  =  ( 1 ... 𝑁 ) ) | 
						
							| 131 | 128 130 | sseqtrrd | ⊢ ( 𝜑  →  ( 1 ... ( 𝑁  −  1 ) )  ⊆  dom  ◡ 𝑆 ) | 
						
							| 132 | 131 | sselda | ⊢ ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  →  𝑋  ∈  dom  ◡ 𝑆 ) | 
						
							| 133 |  | fvco | ⊢ ( ( Fun  ◡ 𝑆  ∧  𝑋  ∈  dom  ◡ 𝑆 )  →  ( ( 𝑃  ∘  ◡ 𝑆 ) ‘ 𝑋 )  =  ( 𝑃 ‘ ( ◡ 𝑆 ‘ 𝑋 ) ) ) | 
						
							| 134 | 124 132 133 | syl2an2r | ⊢ ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  →  ( ( 𝑃  ∘  ◡ 𝑆 ) ‘ 𝑋 )  =  ( 𝑃 ‘ ( ◡ 𝑆 ‘ 𝑋 ) ) ) | 
						
							| 135 | 120 134 | eqtr4d | ⊢ ( ( 𝜑  ∧  𝑋  ∈  ( 1 ... ( 𝑁  −  1 ) ) )  →  if ( 𝑋  <  𝐼 ,  𝑋 ,  ( 𝑋  +  1 ) )  =  ( ( 𝑃  ∘  ◡ 𝑆 ) ‘ 𝑋 ) ) |