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 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 ) ) = ( ( 𝑃 ∘ ◡ 𝑆 ) ‘ 𝑋 ) )