Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  madjusmdetlem2 Structured version   Visualization version   GIF version

Theorem madjusmdetlem2 33788
Description: Lemma for madjusmdet 33791. (Contributed by Thierry Arnoux, 26-Aug-2020.)
Hypotheses
Ref Expression
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
Ref Expression
madjusmdetlem2 ((𝜑𝑋 ∈ (1...(𝑁 − 1))) → if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)) = ((𝑃𝑆)‘𝑋))
Distinct variable groups:   𝐵,𝑖   𝑖,𝐼   𝑖,𝐽   𝑖,𝑀   𝑖,𝑁   𝑃,𝑖   𝑅,𝑖   𝜑,𝑖   𝑆,𝑖
Allowed substitution hints:   𝐴(𝑖)   𝐷(𝑖)   · (𝑖)   𝐸(𝑖)   𝐾(𝑖)   𝑋(𝑖)   𝑍(𝑖)

Proof of Theorem madjusmdetlem2
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 madjusmdet.n . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ)
2 nnuz 12918 . . . . . . . . . . . 12 ℕ = (ℤ‘1)
31, 2eleqtrdi 2848 . . . . . . . . . . 11 (𝜑𝑁 ∈ (ℤ‘1))
4 eluzfz2 13568 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘1) → 𝑁 ∈ (1...𝑁))
53, 4syl 17 . . . . . . . . . 10 (𝜑𝑁 ∈ (1...𝑁))
6 eqid 2734 . . . . . . . . . . 11 (1...𝑁) = (1...𝑁)
7 madjusmdetlem2.s . . . . . . . . . . 11 𝑆 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝑁, if(𝑖𝑁, (𝑖 − 1), 𝑖)))
8 eqid 2734 . . . . . . . . . . 11 (SymGrp‘(1...𝑁)) = (SymGrp‘(1...𝑁))
9 eqid 2734 . . . . . . . . . . 11 (Base‘(SymGrp‘(1...𝑁))) = (Base‘(SymGrp‘(1...𝑁)))
106, 7, 8, 9fzto1st 33105 . . . . . . . . . 10 (𝑁 ∈ (1...𝑁) → 𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))))
115, 10syl 17 . . . . . . . . 9 (𝜑𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))))
128, 9symgbasf1o 19406 . . . . . . . . 9 (𝑆 ∈ (Base‘(SymGrp‘(1...𝑁))) → 𝑆:(1...𝑁)–1-1-onto→(1...𝑁))
1311, 12syl 17 . . . . . . . 8 (𝜑𝑆:(1...𝑁)–1-1-onto→(1...𝑁))
1413adantr 480 . . . . . . 7 ((𝜑𝑋 ∈ (1...(𝑁 − 1))) → 𝑆:(1...𝑁)–1-1-onto→(1...𝑁))
15 fznatpl1 13614 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑋 ∈ (1...(𝑁 − 1))) → (𝑋 + 1) ∈ (1...𝑁))
161, 15sylan 580 . . . . . . 7 ((𝜑𝑋 ∈ (1...(𝑁 − 1))) → (𝑋 + 1) ∈ (1...𝑁))
17 eqeq1 2738 . . . . . . . . . . 11 (𝑖 = 𝑥 → (𝑖 = 1 ↔ 𝑥 = 1))
18 breq1 5150 . . . . . . . . . . . 12 (𝑖 = 𝑥 → (𝑖𝑁𝑥𝑁))
19 oveq1 7437 . . . . . . . . . . . 12 (𝑖 = 𝑥 → (𝑖 − 1) = (𝑥 − 1))
20 id 22 . . . . . . . . . . . 12 (𝑖 = 𝑥𝑖 = 𝑥)
2118, 19, 20ifbieq12d 4558 . . . . . . . . . . 11 (𝑖 = 𝑥 → if(𝑖𝑁, (𝑖 − 1), 𝑖) = if(𝑥𝑁, (𝑥 − 1), 𝑥))
2217, 21ifbieq2d 4556 . . . . . . . . . 10 (𝑖 = 𝑥 → if(𝑖 = 1, 𝑁, if(𝑖𝑁, (𝑖 − 1), 𝑖)) = if(𝑥 = 1, 𝑁, if(𝑥𝑁, (𝑥 − 1), 𝑥)))
2322cbvmptv 5260 . . . . . . . . 9 (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝑁, if(𝑖𝑁, (𝑖 − 1), 𝑖))) = (𝑥 ∈ (1...𝑁) ↦ if(𝑥 = 1, 𝑁, if(𝑥𝑁, (𝑥 − 1), 𝑥)))
247, 23eqtri 2762 . . . . . . . 8 𝑆 = (𝑥 ∈ (1...𝑁) ↦ if(𝑥 = 1, 𝑁, if(𝑥𝑁, (𝑥 − 1), 𝑥)))
25 simpr 484 . . . . . . . . . . . 12 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → 𝑥 = (𝑋 + 1))
26 1red 11259 . . . . . . . . . . . . 13 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → 1 ∈ ℝ)
27 fz1ssnn 13591 . . . . . . . . . . . . . . . . 17 (1...(𝑁 − 1)) ⊆ ℕ
28 simpr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑋 ∈ (1...(𝑁 − 1))) → 𝑋 ∈ (1...(𝑁 − 1)))
2927, 28sselid 3992 . . . . . . . . . . . . . . . 16 ((𝜑𝑋 ∈ (1...(𝑁 − 1))) → 𝑋 ∈ ℕ)
3029nnrpd 13072 . . . . . . . . . . . . . . 15 ((𝜑𝑋 ∈ (1...(𝑁 − 1))) → 𝑋 ∈ ℝ+)
3130adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → 𝑋 ∈ ℝ+)
3226, 31ltaddrp2d 13108 . . . . . . . . . . . . 13 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → 1 < (𝑋 + 1))
3326, 32gtned 11393 . . . . . . . . . . . 12 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → (𝑋 + 1) ≠ 1)
3425, 33eqnetrd 3005 . . . . . . . . . . 11 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → 𝑥 ≠ 1)
3534neneqd 2942 . . . . . . . . . 10 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → ¬ 𝑥 = 1)
3635iffalsed 4541 . . . . . . . . 9 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥 = 1, 𝑁, if(𝑥𝑁, (𝑥 − 1), 𝑥)) = if(𝑥𝑁, (𝑥 − 1), 𝑥))
371adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑋 ∈ (1...(𝑁 − 1))) → 𝑁 ∈ ℕ)
3829nnnn0d 12584 . . . . . . . . . . . . . 14 ((𝜑𝑋 ∈ (1...(𝑁 − 1))) → 𝑋 ∈ ℕ0)
3937nnnn0d 12584 . . . . . . . . . . . . . 14 ((𝜑𝑋 ∈ (1...(𝑁 − 1))) → 𝑁 ∈ ℕ0)
40 elfzle2 13564 . . . . . . . . . . . . . . 15 (𝑋 ∈ (1...(𝑁 − 1)) → 𝑋 ≤ (𝑁 − 1))
4128, 40syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑋 ∈ (1...(𝑁 − 1))) → 𝑋 ≤ (𝑁 − 1))
42 nn0ltlem1 12675 . . . . . . . . . . . . . . 15 ((𝑋 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑋 < 𝑁𝑋 ≤ (𝑁 − 1)))
4342biimpar 477 . . . . . . . . . . . . . 14 (((𝑋 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝑋 ≤ (𝑁 − 1)) → 𝑋 < 𝑁)
4438, 39, 41, 43syl21anc 838 . . . . . . . . . . . . 13 ((𝜑𝑋 ∈ (1...(𝑁 − 1))) → 𝑋 < 𝑁)
45 nnltp1le 12671 . . . . . . . . . . . . . 14 ((𝑋 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑋 < 𝑁 ↔ (𝑋 + 1) ≤ 𝑁))
4645biimpa 476 . . . . . . . . . . . . 13 (((𝑋 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝑋 < 𝑁) → (𝑋 + 1) ≤ 𝑁)
4729, 37, 44, 46syl21anc 838 . . . . . . . . . . . 12 ((𝜑𝑋 ∈ (1...(𝑁 − 1))) → (𝑋 + 1) ≤ 𝑁)
4847adantr 480 . . . . . . . . . . 11 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → (𝑋 + 1) ≤ 𝑁)
4925, 48eqbrtrd 5169 . . . . . . . . . 10 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → 𝑥𝑁)
5049iftrued 4538 . . . . . . . . 9 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥𝑁, (𝑥 − 1), 𝑥) = (𝑥 − 1))
5125oveq1d 7445 . . . . . . . . . 10 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → (𝑥 − 1) = ((𝑋 + 1) − 1))
5229nncnd 12279 . . . . . . . . . . . 12 ((𝜑𝑋 ∈ (1...(𝑁 − 1))) → 𝑋 ∈ ℂ)
53 1cnd 11253 . . . . . . . . . . . 12 ((𝜑𝑋 ∈ (1...(𝑁 − 1))) → 1 ∈ ℂ)
5452, 53pncand 11618 . . . . . . . . . . 11 ((𝜑𝑋 ∈ (1...(𝑁 − 1))) → ((𝑋 + 1) − 1) = 𝑋)
5554adantr 480 . . . . . . . . . 10 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → ((𝑋 + 1) − 1) = 𝑋)
5651, 55eqtrd 2774 . . . . . . . . 9 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → (𝑥 − 1) = 𝑋)
5736, 50, 563eqtrd 2778 . . . . . . . 8 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥 = 1, 𝑁, if(𝑥𝑁, (𝑥 − 1), 𝑥)) = 𝑋)
5824, 57, 16, 28fvmptd2 7023 . . . . . . 7 ((𝜑𝑋 ∈ (1...(𝑁 − 1))) → (𝑆‘(𝑋 + 1)) = 𝑋)
59 f1ocnvfv 7297 . . . . . . . 8 ((𝑆:(1...𝑁)–1-1-onto→(1...𝑁) ∧ (𝑋 + 1) ∈ (1...𝑁)) → ((𝑆‘(𝑋 + 1)) = 𝑋 → (𝑆𝑋) = (𝑋 + 1)))
6059imp 406 . . . . . . 7 (((𝑆:(1...𝑁)–1-1-onto→(1...𝑁) ∧ (𝑋 + 1) ∈ (1...𝑁)) ∧ (𝑆‘(𝑋 + 1)) = 𝑋) → (𝑆𝑋) = (𝑋 + 1))
6114, 16, 58, 60syl21anc 838 . . . . . 6 ((𝜑𝑋 ∈ (1...(𝑁 − 1))) → (𝑆𝑋) = (𝑋 + 1))
6261fveq2d 6910 . . . . 5 ((𝜑𝑋 ∈ (1...(𝑁 − 1))) → (𝑃‘(𝑆𝑋)) = (𝑃‘(𝑋 + 1)))
6362adantr 480 . . . 4 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) → (𝑃‘(𝑆𝑋)) = (𝑃‘(𝑋 + 1)))
64 madjusmdetlem2.p . . . . . 6 𝑃 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝐼, if(𝑖𝐼, (𝑖 − 1), 𝑖)))
65 breq1 5150 . . . . . . . . 9 (𝑖 = 𝑥 → (𝑖𝐼𝑥𝐼))
6665, 19, 20ifbieq12d 4558 . . . . . . . 8 (𝑖 = 𝑥 → if(𝑖𝐼, (𝑖 − 1), 𝑖) = if(𝑥𝐼, (𝑥 − 1), 𝑥))
6717, 66ifbieq2d 4556 . . . . . . 7 (𝑖 = 𝑥 → if(𝑖 = 1, 𝐼, if(𝑖𝐼, (𝑖 − 1), 𝑖)) = if(𝑥 = 1, 𝐼, if(𝑥𝐼, (𝑥 − 1), 𝑥)))
6867cbvmptv 5260 . . . . . 6 (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝐼, if(𝑖𝐼, (𝑖 − 1), 𝑖))) = (𝑥 ∈ (1...𝑁) ↦ if(𝑥 = 1, 𝐼, if(𝑥𝐼, (𝑥 − 1), 𝑥)))
6964, 68eqtri 2762 . . . . 5 𝑃 = (𝑥 ∈ (1...𝑁) ↦ if(𝑥 = 1, 𝐼, if(𝑥𝐼, (𝑥 − 1), 𝑥)))
7032, 25breqtrrd 5175 . . . . . . . . . 10 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → 1 < 𝑥)
7126, 70gtned 11393 . . . . . . . . 9 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → 𝑥 ≠ 1)
7271neneqd 2942 . . . . . . . 8 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → ¬ 𝑥 = 1)
7372iffalsed 4541 . . . . . . 7 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥 = 1, 𝐼, if(𝑥𝐼, (𝑥 − 1), 𝑥)) = if(𝑥𝐼, (𝑥 − 1), 𝑥))
7473adantlr 715 . . . . . 6 ((((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥 = 1, 𝐼, if(𝑥𝐼, (𝑥 − 1), 𝑥)) = if(𝑥𝐼, (𝑥 − 1), 𝑥))
75 simpr 484 . . . . . . . 8 ((((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → 𝑥 = (𝑋 + 1))
7629ad2antrr 726 . . . . . . . . 9 ((((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → 𝑋 ∈ ℕ)
77 fz1ssnn 13591 . . . . . . . . . . 11 (1...𝑁) ⊆ ℕ
78 madjusmdet.i . . . . . . . . . . 11 (𝜑𝐼 ∈ (1...𝑁))
7977, 78sselid 3992 . . . . . . . . . 10 (𝜑𝐼 ∈ ℕ)
8079ad3antrrr 730 . . . . . . . . 9 ((((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → 𝐼 ∈ ℕ)
81 simplr 769 . . . . . . . . 9 ((((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → 𝑋 < 𝐼)
82 nnltp1le 12671 . . . . . . . . . 10 ((𝑋 ∈ ℕ ∧ 𝐼 ∈ ℕ) → (𝑋 < 𝐼 ↔ (𝑋 + 1) ≤ 𝐼))
8382biimpa 476 . . . . . . . . 9 (((𝑋 ∈ ℕ ∧ 𝐼 ∈ ℕ) ∧ 𝑋 < 𝐼) → (𝑋 + 1) ≤ 𝐼)
8476, 80, 81, 83syl21anc 838 . . . . . . . 8 ((((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → (𝑋 + 1) ≤ 𝐼)
8575, 84eqbrtrd 5169 . . . . . . 7 ((((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → 𝑥𝐼)
8685iftrued 4538 . . . . . 6 ((((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥𝐼, (𝑥 − 1), 𝑥) = (𝑥 − 1))
8756adantlr 715 . . . . . 6 ((((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → (𝑥 − 1) = 𝑋)
8874, 86, 873eqtrd 2778 . . . . 5 ((((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥 = 1, 𝐼, if(𝑥𝐼, (𝑥 − 1), 𝑥)) = 𝑋)
8916adantr 480 . . . . 5 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) → (𝑋 + 1) ∈ (1...𝑁))
90 simplr 769 . . . . 5 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) → 𝑋 ∈ (1...(𝑁 − 1)))
9169, 88, 89, 90fvmptd2 7023 . . . 4 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) → (𝑃‘(𝑋 + 1)) = 𝑋)
9263, 91eqtr2d 2775 . . 3 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑋 < 𝐼) → 𝑋 = (𝑃‘(𝑆𝑋)))
9362adantr 480 . . . 4 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) → (𝑃‘(𝑆𝑋)) = (𝑃‘(𝑋 + 1)))
9473adantlr 715 . . . . . 6 ((((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥 = 1, 𝐼, if(𝑥𝐼, (𝑥 − 1), 𝑥)) = if(𝑥𝐼, (𝑥 − 1), 𝑥))
9529ad2antrr 726 . . . . . . . . . 10 ((((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) ∧ 𝑥𝐼) → 𝑋 ∈ ℕ)
9679ad3antrrr 730 . . . . . . . . . 10 ((((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) ∧ 𝑥𝐼) → 𝐼 ∈ ℕ)
97 simplr 769 . . . . . . . . . . 11 ((((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) ∧ 𝑥𝐼) → 𝑥 = (𝑋 + 1))
98 simpr 484 . . . . . . . . . . 11 ((((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) ∧ 𝑥𝐼) → 𝑥𝐼)
9997, 98eqbrtrrd 5171 . . . . . . . . . 10 ((((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) ∧ 𝑥𝐼) → (𝑋 + 1) ≤ 𝐼)
10082biimpar 477 . . . . . . . . . 10 (((𝑋 ∈ ℕ ∧ 𝐼 ∈ ℕ) ∧ (𝑋 + 1) ≤ 𝐼) → 𝑋 < 𝐼)
10195, 96, 99, 100syl21anc 838 . . . . . . . . 9 ((((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) ∧ 𝑥𝐼) → 𝑋 < 𝐼)
102101stoic1a 1768 . . . . . . . 8 ((((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ 𝑥 = (𝑋 + 1)) ∧ ¬ 𝑋 < 𝐼) → ¬ 𝑥𝐼)
103102an32s 652 . . . . . . 7 ((((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → ¬ 𝑥𝐼)
104103iffalsed 4541 . . . . . 6 ((((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥𝐼, (𝑥 − 1), 𝑥) = 𝑥)
105 simpr 484 . . . . . 6 ((((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → 𝑥 = (𝑋 + 1))
10694, 104, 1053eqtrd 2778 . . . . 5 ((((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) ∧ 𝑥 = (𝑋 + 1)) → if(𝑥 = 1, 𝐼, if(𝑥𝐼, (𝑥 − 1), 𝑥)) = (𝑋 + 1))
10716adantr 480 . . . . 5 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) → (𝑋 + 1) ∈ (1...𝑁))
10869, 106, 107, 107fvmptd2 7023 . . . 4 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) → (𝑃‘(𝑋 + 1)) = (𝑋 + 1))
10993, 108eqtr2d 2775 . . 3 (((𝜑𝑋 ∈ (1...(𝑁 − 1))) ∧ ¬ 𝑋 < 𝐼) → (𝑋 + 1) = (𝑃‘(𝑆𝑋)))
11092, 109ifeqda 4566 . 2 ((𝜑𝑋 ∈ (1...(𝑁 − 1))) → if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)) = (𝑃‘(𝑆𝑋)))
111 f1ocnv 6860 . . . . 5 (𝑆:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑆:(1...𝑁)–1-1-onto→(1...𝑁))
11211, 12, 1113syl 18 . . . 4 (𝜑𝑆:(1...𝑁)–1-1-onto→(1...𝑁))
113 f1ofun 6850 . . . 4 (𝑆:(1...𝑁)–1-1-onto→(1...𝑁) → Fun 𝑆)
114112, 113syl 17 . . 3 (𝜑 → Fun 𝑆)
115 fzdif2 32798 . . . . . . 7 (𝑁 ∈ (ℤ‘1) → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1)))
1163, 115syl 17 . . . . . 6 (𝜑 → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1)))
117 difss 4145 . . . . . 6 ((1...𝑁) ∖ {𝑁}) ⊆ (1...𝑁)
118116, 117eqsstrrdi 4050 . . . . 5 (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
119 f1odm 6852 . . . . . 6 (𝑆:(1...𝑁)–1-1-onto→(1...𝑁) → dom 𝑆 = (1...𝑁))
120112, 119syl 17 . . . . 5 (𝜑 → dom 𝑆 = (1...𝑁))
121118, 120sseqtrrd 4036 . . . 4 (𝜑 → (1...(𝑁 − 1)) ⊆ dom 𝑆)
122121sselda 3994 . . 3 ((𝜑𝑋 ∈ (1...(𝑁 − 1))) → 𝑋 ∈ dom 𝑆)
123 fvco 7006 . . 3 ((Fun 𝑆𝑋 ∈ dom 𝑆) → ((𝑃𝑆)‘𝑋) = (𝑃‘(𝑆𝑋)))
124114, 122, 123syl2an2r 685 . 2 ((𝜑𝑋 ∈ (1...(𝑁 − 1))) → ((𝑃𝑆)‘𝑋) = (𝑃‘(𝑆𝑋)))
125110, 124eqtr4d 2777 1 ((𝜑𝑋 ∈ (1...(𝑁 − 1))) → if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)) = ((𝑃𝑆)‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395   = wceq 1536  wcel 2105  cdif 3959  ifcif 4530  {csn 4630   class class class wbr 5147  cmpt 5230  ccnv 5687  dom cdm 5688  ccom 5692  Fun wfun 6556  1-1-ontowf1o 6561  cfv 6562  (class class class)co 7430  1c1 11153   + caddc 11155   < clt 11292  cle 11293  cmin 11489  cn 12263  0cn0 12523  cuz 12875  +crp 13031  ...cfz 13543  Basecbs 17244  .rcmulr 17298  SymGrpcsymg 19400  CRingccrg 20251  ℤRHomczrh 21527   Mat cmat 22426   maDet cmdat 22605   maAdju cmadu 22653
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-er 8743  df-map 8866  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-9 12333  df-n0 12524  df-z 12611  df-uz 12876  df-rp 13032  df-fz 13544  df-struct 17180  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-tset 17316  df-efmnd 18894  df-symg 19401  df-pmtr 19474
This theorem is referenced by:  madjusmdetlem3  33789
  Copyright terms: Public domain W3C validator