Metamath Proof Explorer

Theorem madjusmdetlem2

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

Ref Expression
Hypotheses madjusmdet.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
madjusmdet.a ⊢ 𝐴 = ( ( 1 ... 𝑁 ) Mat 𝑅 )
madjusmdet.d ⊢ 𝐷 = ( ( 1 ... 𝑁 ) maDet 𝑅 )
madjusmdet.k ⊢ 𝐾 = ( ( 1 ... 𝑁 ) maAdju 𝑅 )
madjusmdet.t ⊢ · = ( .r ‘ 𝑅 )
madjusmdet.z ⊢ 𝑍 = ( ℤRHom ‘ 𝑅 )
madjusmdet.e ⊢ 𝐸 = ( ( 1 ... ( 𝑁 − 1 ) ) maDet 𝑅 )
madjusmdet.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
madjusmdet.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
madjusmdet.i ⊢ ( 𝜑 → 𝐼 ∈ ( 1 ... 𝑁 ) )
madjusmdet.j ⊢ ( 𝜑 → 𝐽 ∈ ( 1 ... 𝑁 ) )
madjusmdet.m ⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
madjusmdetlem2.p ⊢ 𝑃 = ( 𝑖 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑖 = 1 , 𝐼 , if ( 𝑖 ≤ 𝐼 , ( 𝑖 − 1 ) , 𝑖 ) ) )
madjusmdetlem2.s ⊢ 𝑆 = ( 𝑖 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑖 = 1 , 𝑁 , if ( 𝑖 ≤ 𝑁 , ( 𝑖 − 1 ) , 𝑖 ) ) )
Assertion madjusmdetlem2 ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) = ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑋 ) )

Proof

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 36 a1i ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑆 = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑥 = 1 , 𝑁 , if ( 𝑥 ≤ 𝑁 , ( 𝑥 − 1 ) , 𝑥 ) ) ) )
38 simpr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → 𝑥 = ( 𝑋 + 1 ) )
39 1red ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → 1 ∈ ℝ )
40 fz1ssnn ⊢ ( 1 ... ( 𝑁 − 1 ) ) ⊆ ℕ
41 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
42 40 41 sselid ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑋 ∈ ℕ )
43 42 nnrpd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑋 ∈ ℝ+ )
44 43 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → 𝑋 ∈ ℝ+ )
45 39 44 ltaddrp2d ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → 1 < ( 𝑋 + 1 ) )
46 39 45 ltned ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → 1 ≠ ( 𝑋 + 1 ) )
47 46 necomd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → ( 𝑋 + 1 ) ≠ 1 )
48 38 47 eqnetrd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → 𝑥 ≠ 1 )
49 48 neneqd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → ¬ 𝑥 = 1 )
50 49 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → if ( 𝑥 = 1 , 𝑁 , if ( 𝑥 ≤ 𝑁 , ( 𝑥 − 1 ) , 𝑥 ) ) = if ( 𝑥 ≤ 𝑁 , ( 𝑥 − 1 ) , 𝑥 ) )
51 8 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℕ )
52 42 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑋 ∈ ℕ0 )
53 51 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℕ0 )
54 elfzle2 ⊢ ( 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑋 ≤ ( 𝑁 − 1 ) )
55 41 54 syl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑋 ≤ ( 𝑁 − 1 ) )
56 nn0ltlem1 ⊢ ( ( 𝑋 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑋 < 𝑁 ↔ 𝑋 ≤ ( 𝑁 − 1 ) ) )
57 56 biimpar ⊢ ( ( ( 𝑋 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑋 ≤ ( 𝑁 − 1 ) ) → 𝑋 < 𝑁 )
58 52 53 55 57 syl21anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑋 < 𝑁 )
59 nnltp1le ⊢ ( ( 𝑋 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑋 < 𝑁 ↔ ( 𝑋 + 1 ) ≤ 𝑁 ) )
60 59 biimpa ⊢ ( ( ( 𝑋 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ 𝑋 < 𝑁 ) → ( 𝑋 + 1 ) ≤ 𝑁 )
61 42 51 58 60 syl21anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑋 + 1 ) ≤ 𝑁 )
62 61 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → ( 𝑋 + 1 ) ≤ 𝑁 )
63 38 62 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → 𝑥 ≤ 𝑁 )
64 63 iftrued ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → if ( 𝑥 ≤ 𝑁 , ( 𝑥 − 1 ) , 𝑥 ) = ( 𝑥 − 1 ) )
65 38 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → ( 𝑥 − 1 ) = ( ( 𝑋 + 1 ) − 1 ) )
66 42 nncnd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑋 ∈ ℂ )
67 1cnd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 1 ∈ ℂ )
68 66 67 pncand ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑋 + 1 ) − 1 ) = 𝑋 )
69 68 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → ( ( 𝑋 + 1 ) − 1 ) = 𝑋 )
70 65 69 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → ( 𝑥 − 1 ) = 𝑋 )
71 50 64 70 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → if ( 𝑥 = 1 , 𝑁 , if ( 𝑥 ≤ 𝑁 , ( 𝑥 − 1 ) , 𝑥 ) ) = 𝑋 )
72 37 71 28 41 fvmptd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑆 ‘ ( 𝑋 + 1 ) ) = 𝑋 )
73 72 idi ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑆 ‘ ( 𝑋 + 1 ) ) = 𝑋 )
74 f1ocnvfv ⊢ ( ( 𝑆 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ ( 𝑋 + 1 ) ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑆 ‘ ( 𝑋 + 1 ) ) = 𝑋 → ( ◡ 𝑆 ‘ 𝑋 ) = ( 𝑋 + 1 ) ) )
75 74 imp ⊢ ( ( ( 𝑆 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ∧ ( 𝑋 + 1 ) ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑆 ‘ ( 𝑋 + 1 ) ) = 𝑋 ) → ( ◡ 𝑆 ‘ 𝑋 ) = ( 𝑋 + 1 ) )
76 26 28 73 75 syl21anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ◡ 𝑆 ‘ 𝑋 ) = ( 𝑋 + 1 ) )
77 76 fveq2d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑃 ‘ ( ◡ 𝑆 ‘ 𝑋 ) ) = ( 𝑃 ‘ ( 𝑋 + 1 ) ) )
78 77 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑋 < 𝐼 ) → ( 𝑃 ‘ ( ◡ 𝑆 ‘ 𝑋 ) ) = ( 𝑃 ‘ ( 𝑋 + 1 ) ) )
79 32 breq1d ⊢ ( 𝑖 = 𝑥 → ( 𝑖 ≤ 𝐼 ↔ 𝑥 ≤ 𝐼 ) )
80 79 31 32 ifbieq12d ⊢ ( 𝑖 = 𝑥 → if ( 𝑖 ≤ 𝐼 , ( 𝑖 − 1 ) , 𝑖 ) = if ( 𝑥 ≤ 𝐼 , ( 𝑥 − 1 ) , 𝑥 ) )
81 29 80 ifbieq2d ⊢ ( 𝑖 = 𝑥 → if ( 𝑖 = 1 , 𝐼 , if ( 𝑖 ≤ 𝐼 , ( 𝑖 − 1 ) , 𝑖 ) ) = if ( 𝑥 = 1 , 𝐼 , if ( 𝑥 ≤ 𝐼 , ( 𝑥 − 1 ) , 𝑥 ) ) )
82 81 cbvmptv ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑖 = 1 , 𝐼 , if ( 𝑖 ≤ 𝐼 , ( 𝑖 − 1 ) , 𝑖 ) ) ) = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑥 = 1 , 𝐼 , if ( 𝑥 ≤ 𝐼 , ( 𝑥 − 1 ) , 𝑥 ) ) )
83 13 82 eqtri ⊢ 𝑃 = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑥 = 1 , 𝐼 , if ( 𝑥 ≤ 𝐼 , ( 𝑥 − 1 ) , 𝑥 ) ) )
84 83 a1i ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑋 < 𝐼 ) → 𝑃 = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑥 = 1 , 𝐼 , if ( 𝑥 ≤ 𝐼 , ( 𝑥 − 1 ) , 𝑥 ) ) ) )
85 45 38 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → 1 < 𝑥 )
86 39 85 ltned ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → 1 ≠ 𝑥 )
87 86 necomd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → 𝑥 ≠ 1 )
88 87 neneqd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → ¬ 𝑥 = 1 )
89 88 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → if ( 𝑥 = 1 , 𝐼 , if ( 𝑥 ≤ 𝐼 , ( 𝑥 − 1 ) , 𝑥 ) ) = if ( 𝑥 ≤ 𝐼 , ( 𝑥 − 1 ) , 𝑥 ) )
90 89 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑋 < 𝐼 ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → if ( 𝑥 = 1 , 𝐼 , if ( 𝑥 ≤ 𝐼 , ( 𝑥 − 1 ) , 𝑥 ) ) = if ( 𝑥 ≤ 𝐼 , ( 𝑥 − 1 ) , 𝑥 ) )
91 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑋 < 𝐼 ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → 𝑥 = ( 𝑋 + 1 ) )
92 42 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑋 < 𝐼 ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → 𝑋 ∈ ℕ )
93 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
94 93 10 sselid ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
95 94 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑋 < 𝐼 ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → 𝐼 ∈ ℕ )
96 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑋 < 𝐼 ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → 𝑋 < 𝐼 )
97 nnltp1le ⊢ ( ( 𝑋 ∈ ℕ ∧ 𝐼 ∈ ℕ ) → ( 𝑋 < 𝐼 ↔ ( 𝑋 + 1 ) ≤ 𝐼 ) )
98 97 biimpa ⊢ ( ( ( 𝑋 ∈ ℕ ∧ 𝐼 ∈ ℕ ) ∧ 𝑋 < 𝐼 ) → ( 𝑋 + 1 ) ≤ 𝐼 )
99 92 95 96 98 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑋 < 𝐼 ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → ( 𝑋 + 1 ) ≤ 𝐼 )
100 91 99 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑋 < 𝐼 ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → 𝑥 ≤ 𝐼 )
101 100 iftrued ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑋 < 𝐼 ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → if ( 𝑥 ≤ 𝐼 , ( 𝑥 − 1 ) , 𝑥 ) = ( 𝑥 − 1 ) )
102 70 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑋 < 𝐼 ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → ( 𝑥 − 1 ) = 𝑋 )
103 90 101 102 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑋 < 𝐼 ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → if ( 𝑥 = 1 , 𝐼 , if ( 𝑥 ≤ 𝐼 , ( 𝑥 − 1 ) , 𝑥 ) ) = 𝑋 )
104 28 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑋 < 𝐼 ) → ( 𝑋 + 1 ) ∈ ( 1 ... 𝑁 ) )
105 simplr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑋 < 𝐼 ) → 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) )
106 84 103 104 105 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑋 < 𝐼 ) → ( 𝑃 ‘ ( 𝑋 + 1 ) ) = 𝑋 )
107 78 106 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑋 < 𝐼 ) → 𝑋 = ( 𝑃 ‘ ( ◡ 𝑆 ‘ 𝑋 ) ) )
108 77 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑋 < 𝐼 ) → ( 𝑃 ‘ ( ◡ 𝑆 ‘ 𝑋 ) ) = ( 𝑃 ‘ ( 𝑋 + 1 ) ) )
109 83 a1i ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑋 < 𝐼 ) → 𝑃 = ( 𝑥 ∈ ( 1 ... 𝑁 ) ↦ if ( 𝑥 = 1 , 𝐼 , if ( 𝑥 ≤ 𝐼 , ( 𝑥 − 1 ) , 𝑥 ) ) ) )
110 89 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑋 < 𝐼 ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → if ( 𝑥 = 1 , 𝐼 , if ( 𝑥 ≤ 𝐼 , ( 𝑥 − 1 ) , 𝑥 ) ) = if ( 𝑥 ≤ 𝐼 , ( 𝑥 − 1 ) , 𝑥 ) )
111 42 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) ∧ 𝑥 ≤ 𝐼 ) → 𝑋 ∈ ℕ )
112 94 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) ∧ 𝑥 ≤ 𝐼 ) → 𝐼 ∈ ℕ )
113 38 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) ∧ 𝑥 ≤ 𝐼 ) → 𝑥 = ( 𝑋 + 1 ) )
114 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) ∧ 𝑥 ≤ 𝐼 ) → 𝑥 ≤ 𝐼 )
115 113 114 eqbrtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) ∧ 𝑥 ≤ 𝐼 ) → ( 𝑋 + 1 ) ≤ 𝐼 )
116 97 biimpar ⊢ ( ( ( 𝑋 ∈ ℕ ∧ 𝐼 ∈ ℕ ) ∧ ( 𝑋 + 1 ) ≤ 𝐼 ) → 𝑋 < 𝐼 )
117 111 112 115 116 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) ∧ 𝑥 ≤ 𝐼 ) → 𝑋 < 𝐼 )
118 117 ex ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → ( 𝑥 ≤ 𝐼 → 𝑋 < 𝐼 ) )
119 118 con3d ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → ( ¬ 𝑋 < 𝐼 → ¬ 𝑥 ≤ 𝐼 ) )
120 119 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ 𝑥 = ( 𝑋 + 1 ) ) ∧ ¬ 𝑋 < 𝐼 ) → ¬ 𝑥 ≤ 𝐼 )
121 120 an32s ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑋 < 𝐼 ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → ¬ 𝑥 ≤ 𝐼 )
122 121 iffalsed ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑋 < 𝐼 ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → if ( 𝑥 ≤ 𝐼 , ( 𝑥 − 1 ) , 𝑥 ) = 𝑥 )
123 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑋 < 𝐼 ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → 𝑥 = ( 𝑋 + 1 ) )
124 122 123 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑋 < 𝐼 ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → if ( 𝑥 ≤ 𝐼 , ( 𝑥 − 1 ) , 𝑥 ) = ( 𝑋 + 1 ) )
125 110 124 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑋 < 𝐼 ) ∧ 𝑥 = ( 𝑋 + 1 ) ) → if ( 𝑥 = 1 , 𝐼 , if ( 𝑥 ≤ 𝐼 , ( 𝑥 − 1 ) , 𝑥 ) ) = ( 𝑋 + 1 ) )
126 28 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑋 < 𝐼 ) → ( 𝑋 + 1 ) ∈ ( 1 ... 𝑁 ) )
127 109 125 126 126 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑋 < 𝐼 ) → ( 𝑃 ‘ ( 𝑋 + 1 ) ) = ( 𝑋 + 1 ) )
128 108 127 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) ∧ ¬ 𝑋 < 𝐼 ) → ( 𝑋 + 1 ) = ( 𝑃 ‘ ( ◡ 𝑆 ‘ 𝑋 ) ) )
129 107 128 ifeqda ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) = ( 𝑃 ‘ ( ◡ 𝑆 ‘ 𝑋 ) ) )
130 f1ocnv ⊢ ( 𝑆 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → ◡ 𝑆 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
131 23 24 130 3syl ⊢ ( 𝜑 → ◡ 𝑆 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
132 f1ofun ⊢ ( ◡ 𝑆 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → Fun ◡ 𝑆 )
133 131 132 syl ⊢ ( 𝜑 → Fun ◡ 𝑆 )
134 133 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → Fun ◡ 𝑆 )
135 fzdif2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) = ( 1 ... ( 𝑁 − 1 ) ) )
136 16 135 syl ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) = ( 1 ... ( 𝑁 − 1 ) ) )
137 difss ⊢ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ⊆ ( 1 ... 𝑁 )
138 136 137 eqsstrrdi ⊢ ( 𝜑 → ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) )
139 f1odm ⊢ ( ◡ 𝑆 : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) → dom ◡ 𝑆 = ( 1 ... 𝑁 ) )
140 131 139 syl ⊢ ( 𝜑 → dom ◡ 𝑆 = ( 1 ... 𝑁 ) )
141 138 140 sseqtrrd ⊢ ( 𝜑 → ( 1 ... ( 𝑁 − 1 ) ) ⊆ dom ◡ 𝑆 )
142 141 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 1 ... ( 𝑁 − 1 ) ) ⊆ dom ◡ 𝑆 )
143 142 41 sseldd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑋 ∈ dom ◡ 𝑆 )
144 fvco ⊢ ( ( Fun ◡ 𝑆 ∧ 𝑋 ∈ dom ◡ 𝑆 ) → ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑋 ) = ( 𝑃 ‘ ( ◡ 𝑆 ‘ 𝑋 ) ) )
145 134 143 144 syl2anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑋 ) = ( 𝑃 ‘ ( ◡ 𝑆 ‘ 𝑋 ) ) )
146 129 145 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) = ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑋 ) )