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

 Description: Express the cofactor of the matrix, i.e. the entries of its adjunct matrix, using determinant of submatrices. (Contributed by Thierry Arnoux, 23-Aug-2020.)
Hypotheses
Ref Expression
madjusmdet.a 𝐴 = ((1...𝑁) Mat 𝑅)
Assertion
Ref Expression
madjusmdet (𝜑 → (𝐽(𝐾𝑀)𝐼) = ((𝑍‘(-1↑(𝐼 + 𝐽))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))

Dummy variables 𝑖 𝑗 𝑘 𝑙 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 madjusmdet.b . 2 𝐵 = (Base‘𝐴)
2 madjusmdet.a . 2 𝐴 = ((1...𝑁) Mat 𝑅)
5 madjusmdet.t . 2 · = (.r𝑅)
6 madjusmdet.z . 2 𝑍 = (ℤRHom‘𝑅)
8 madjusmdet.n . 2 (𝜑𝑁 ∈ ℕ)
9 madjusmdet.r . 2 (𝜑𝑅 ∈ CRing)
10 madjusmdet.i . 2 (𝜑𝐼 ∈ (1...𝑁))
11 madjusmdet.j . 2 (𝜑𝐽 ∈ (1...𝑁))
13 eqeq1 2802 . . . 4 (𝑘 = 𝑖 → (𝑘 = 1 ↔ 𝑖 = 1))
14 breq1 5033 . . . . 5 (𝑘 = 𝑖 → (𝑘𝐼𝑖𝐼))
15 oveq1 7142 . . . . 5 (𝑘 = 𝑖 → (𝑘 − 1) = (𝑖 − 1))
16 id 22 . . . . 5 (𝑘 = 𝑖𝑘 = 𝑖)
1714, 15, 16ifbieq12d 4452 . . . 4 (𝑘 = 𝑖 → if(𝑘𝐼, (𝑘 − 1), 𝑘) = if(𝑖𝐼, (𝑖 − 1), 𝑖))
1813, 17ifbieq2d 4450 . . 3 (𝑘 = 𝑖 → if(𝑘 = 1, 𝐼, if(𝑘𝐼, (𝑘 − 1), 𝑘)) = if(𝑖 = 1, 𝐼, if(𝑖𝐼, (𝑖 − 1), 𝑖)))
1918cbvmptv 5133 . 2 (𝑘 ∈ (1...𝑁) ↦ if(𝑘 = 1, 𝐼, if(𝑘𝐼, (𝑘 − 1), 𝑘))) = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝐼, if(𝑖𝐼, (𝑖 − 1), 𝑖)))
20 breq1 5033 . . . . 5 (𝑘 = 𝑖 → (𝑘𝑁𝑖𝑁))
2120, 15, 16ifbieq12d 4452 . . . 4 (𝑘 = 𝑖 → if(𝑘𝑁, (𝑘 − 1), 𝑘) = if(𝑖𝑁, (𝑖 − 1), 𝑖))
2213, 21ifbieq2d 4450 . . 3 (𝑘 = 𝑖 → if(𝑘 = 1, 𝑁, if(𝑘𝑁, (𝑘 − 1), 𝑘)) = if(𝑖 = 1, 𝑁, if(𝑖𝑁, (𝑖 − 1), 𝑖)))
2322cbvmptv 5133 . 2 (𝑘 ∈ (1...𝑁) ↦ if(𝑘 = 1, 𝑁, if(𝑘𝑁, (𝑘 − 1), 𝑘))) = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝑁, if(𝑖𝑁, (𝑖 − 1), 𝑖)))
24 eqeq1 2802 . . . 4 (𝑙 = 𝑗 → (𝑙 = 1 ↔ 𝑗 = 1))
25 breq1 5033 . . . . 5 (𝑙 = 𝑗 → (𝑙𝐽𝑗𝐽))
26 oveq1 7142 . . . . 5 (𝑙 = 𝑗 → (𝑙 − 1) = (𝑗 − 1))
27 id 22 . . . . 5 (𝑙 = 𝑗𝑙 = 𝑗)
2825, 26, 27ifbieq12d 4452 . . . 4 (𝑙 = 𝑗 → if(𝑙𝐽, (𝑙 − 1), 𝑙) = if(𝑗𝐽, (𝑗 − 1), 𝑗))
2924, 28ifbieq2d 4450 . . 3 (𝑙 = 𝑗 → if(𝑙 = 1, 𝐽, if(𝑙𝐽, (𝑙 − 1), 𝑙)) = if(𝑗 = 1, 𝐽, if(𝑗𝐽, (𝑗 − 1), 𝑗)))
3029cbvmptv 5133 . 2 (𝑙 ∈ (1...𝑁) ↦ if(𝑙 = 1, 𝐽, if(𝑙𝐽, (𝑙 − 1), 𝑙))) = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝐽, if(𝑗𝐽, (𝑗 − 1), 𝑗)))
31 breq1 5033 . . . . 5 (𝑙 = 𝑗 → (𝑙𝑁𝑗𝑁))
3231, 26, 27ifbieq12d 4452 . . . 4 (𝑙 = 𝑗 → if(𝑙𝑁, (𝑙 − 1), 𝑙) = if(𝑗𝑁, (𝑗 − 1), 𝑗))
3324, 32ifbieq2d 4450 . . 3 (𝑙 = 𝑗 → if(𝑙 = 1, 𝑁, if(𝑙𝑁, (𝑙 − 1), 𝑙)) = if(𝑗 = 1, 𝑁, if(𝑗𝑁, (𝑗 − 1), 𝑗)))
3433cbvmptv 5133 . 2 (𝑙 ∈ (1...𝑁) ↦ if(𝑙 = 1, 𝑁, if(𝑙𝑁, (𝑙 − 1), 𝑙))) = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝑁, if(𝑗𝑁, (𝑗 − 1), 𝑗)))
351, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 19, 23, 30, 34madjusmdetlem4 31195 1 (𝜑 → (𝐽(𝐾𝑀)𝐼) = ((𝑍‘(-1↑(𝐼 + 𝐽))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽))))