Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  smadiadetg Structured version   Visualization version   GIF version

 Description: The determinant of a square matrix with one row replaced with 0's and an arbitrary element of the underlying ring at the diagonal position equals the ring element multiplied with the determinant of a submatrix of the square matrix obtained by removing the row and the column at the same index. (Contributed by AV, 14-Feb-2019.)
Hypotheses
Ref Expression
Assertion
Ref Expression
smadiadetg ((𝑀𝐵𝐾𝑁𝑆 ∈ (Base‘𝑅)) → (𝐷‘(𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐾)) = (𝑆 · (𝐸‘(𝐾((𝑁 subMat 𝑅)‘𝑀)𝐾))))

StepHypRef Expression
4 eqid 2610 . . 3 (Base‘𝑅) = (Base‘𝑅)
76a1i 11 . . 3 ((𝑀𝐵𝐾𝑁𝑆 ∈ (Base‘𝑅)) → 𝑅 ∈ CRing)
8 crngring 18381 . . . . 5 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
96, 8mp1i 13 . . . 4 ((𝑀𝐵𝐾𝑁𝑆 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring)
10 simp1 1054 . . . 4 ((𝑀𝐵𝐾𝑁𝑆 ∈ (Base‘𝑅)) → 𝑀𝐵)
11 simp3 1056 . . . 4 ((𝑀𝐵𝐾𝑁𝑆 ∈ (Base‘𝑅)) → 𝑆 ∈ (Base‘𝑅))
12 simp2 1055 . . . 4 ((𝑀𝐵𝐾𝑁𝑆 ∈ (Base‘𝑅)) → 𝐾𝑁)
132, 3marrepcl 20189 . . . 4 (((𝑅 ∈ Ring ∧ 𝑀𝐵𝑆 ∈ (Base‘𝑅)) ∧ (𝐾𝑁𝐾𝑁)) → (𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐾) ∈ 𝐵)
149, 10, 11, 12, 12, 13syl32anc 1326 . . 3 ((𝑀𝐵𝐾𝑁𝑆 ∈ (Base‘𝑅)) → (𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐾) ∈ 𝐵)
152, 3minmar1cl 20276 . . . 4 (((𝑅 ∈ Ring ∧ 𝑀𝐵) ∧ (𝐾𝑁𝐾𝑁)) → (𝐾((𝑁 minMatR1 𝑅)‘𝑀)𝐾) ∈ 𝐵)
169, 10, 12, 12, 15syl22anc 1319 . . 3 ((𝑀𝐵𝐾𝑁𝑆 ∈ (Base‘𝑅)) → (𝐾((𝑁 minMatR1 𝑅)‘𝑀)𝐾) ∈ 𝐵)