P. 227 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22601-22700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mvmumamul1 22601*	The multiplication of an MxN matrix with an N-dimensional vector corresponds to the matrix multiplication of an MxN matrix with an Nx1 matrix. (Contributed by AV, 14-Mar-2019.)
⊢ × = (𝑅 maMul ⟨𝑀, 𝑁, {∅}⟩)    &   ⊢ · = (𝑅 maVecMul ⟨𝑀, 𝑁⟩)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m 𝑁))    &   ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m (𝑁 × {∅})))    ⇒   ⊢ (𝜑 → (∀𝑗 ∈ 𝑁 (𝑌‘𝑗) = (𝑗𝑍∅) → ∀𝑖 ∈ 𝑀 ((𝐴 · 𝑌)‘𝑖) = (𝑖(𝐴 × 𝑍)∅)))
Theorem	mavmumamul1 22602*	The multiplication of an NxN matrix with an N-dimensional vector corresponds to the matrix multiplication of an NxN matrix with an Nx1 matrix. (Contributed by AV, 14-Mar-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ × = (𝑅 maMul ⟨𝑁, 𝑁, {∅}⟩)    &   ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐴))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m 𝑁))    &   ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m (𝑁 × {∅})))    ⇒   ⊢ (𝜑 → (∀𝑗 ∈ 𝑁 (𝑌‘𝑗) = (𝑗𝑍∅) → ∀𝑖 ∈ 𝑁 ((𝑋 · 𝑌)‘𝑖) = (𝑖(𝑋 × 𝑍)∅)))
11.4.7  Replacement functions for a square matrix
Syntax	cmarrep 22603	Syntax for the row replacing function for a square matrix.
class matRRep
Syntax	cmatrepV 22604	Syntax for the function replacing a column of a matrix by a vector.
class matRepV
Definition	df-marrep 22605*	Define the matrices whose k-th row is replaced by 0's and an arbitrary element of the underlying ring at the l-th column. (Contributed by AV, 12-Feb-2019.)
⊢ matRRep = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)), 𝑠 ∈ (Base‘𝑟) ↦ (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, (0g‘𝑟)), (𝑖𝑚𝑗))))))
Definition	df-marepv 22606*	Function replacing a column of a matrix by a vector. (Contributed by AV, 9-Feb-2019.) (Revised by AV, 26-Feb-2019.)
⊢ matRepV = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)), 𝑣 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑘 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑗 = 𝑘, (𝑣‘𝑖), (𝑖𝑚𝑗))))))
Theorem	marrepfval 22607*	First substitution for the definition of the matrix row replacement function. (Contributed by AV, 12-Feb-2019.) (Proof shortened by AV, 2-Mar-2024.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑄 = (𝑁 matRRep 𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ 𝑄 = (𝑚 ∈ 𝐵, 𝑠 ∈ (Base‘𝑅) ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, 0 ), (𝑖𝑚𝑗)))))
Theorem	marrepval0 22608*	Second substitution for the definition of the matrix row replacement function. (Contributed by AV, 12-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑄 = (𝑁 matRRep 𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑀 ∈ 𝐵 ∧ 𝑆 ∈ (Base‘𝑅)) → (𝑀𝑄𝑆) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑆, 0 ), (𝑖𝑀𝑗)))))
Theorem	marrepval 22609*	Third substitution for the definition of the matrix row replacement function. (Contributed by AV, 12-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑄 = (𝑁 matRRep 𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (((𝑀 ∈ 𝐵 ∧ 𝑆 ∈ (Base‘𝑅)) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁)) → (𝐾(𝑀𝑄𝑆)𝐿) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 𝑆, 0 ), (𝑖𝑀𝑗))))
Theorem	marrepeval 22610	An entry of a matrix with a replaced row. (Contributed by AV, 12-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑄 = (𝑁 matRRep 𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (((𝑀 ∈ 𝐵 ∧ 𝑆 ∈ (Base‘𝑅)) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝐾(𝑀𝑄𝑆)𝐿)𝐽) = if(𝐼 = 𝐾, if(𝐽 = 𝐿, 𝑆, 0 ), (𝐼𝑀𝐽)))
Theorem	marrepcl 22611	Closure of the row replacement function for square matrices. (Contributed by AV, 13-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ (Base‘𝑅)) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁)) → (𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐿) ∈ 𝐵)
Theorem	marepvfval 22612*	First substitution for the definition of the function replacing a column of a matrix by a vector. (Contributed by AV, 14-Feb-2019.) (Revised by AV, 26-Feb-2019.) (Proof shortened by AV, 2-Mar-2024.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑄 = (𝑁 matRepV 𝑅)    &   ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁)    ⇒   ⊢ 𝑄 = (𝑚 ∈ 𝐵, 𝑣 ∈ 𝑉 ↦ (𝑘 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑗 = 𝑘, (𝑣‘𝑖), (𝑖𝑚𝑗)))))
Theorem	marepvval0 22613*	Second substitution for the definition of the function replacing a column of a matrix by a vector. (Contributed by AV, 14-Feb-2019.) (Revised by AV, 26-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑄 = (𝑁 matRepV 𝑅)    &   ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁)    ⇒   ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉) → (𝑀𝑄𝐶) = (𝑘 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑗 = 𝑘, (𝐶‘𝑖), (𝑖𝑀𝑗)))))
Theorem	marepvval 22614*	Third substitution for the definition of the function replacing a column of a matrix by a vector. (Contributed by AV, 14-Feb-2019.) (Revised by AV, 26-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑄 = (𝑁 matRepV 𝑅)    &   ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁)    ⇒   ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁) → ((𝑀𝑄𝐶)‘𝐾) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑗 = 𝐾, (𝐶‘𝑖), (𝑖𝑀𝑗))))
Theorem	marepveval 22615	An entry of a matrix with a replaced column. (Contributed by AV, 14-Feb-2019.) (Revised by AV, 26-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑄 = (𝑁 matRepV 𝑅)    &   ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁)    ⇒   ⊢ (((𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼((𝑀𝑄𝐶)‘𝐾)𝐽) = if(𝐽 = 𝐾, (𝐶‘𝐼), (𝐼𝑀𝐽)))
Theorem	marepvcl 22616	Closure of the column replacement function for square matrices. (Contributed by AV, 14-Feb-2019.) (Revised by AV, 26-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁)) → ((𝑀(𝑁 matRepV 𝑅)𝐶)‘𝐾) ∈ 𝐵)
Theorem	ma1repvcl 22617	Closure of the column replacement function for identity matrices. (Contributed by AV, 15-Feb-2019.) (Revised by AV, 26-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁)    &   ⊢ 1 = (1r‘𝐴)    ⇒   ⊢ (((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) ∧ (𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁)) → (( 1 (𝑁 matRepV 𝑅)𝐶)‘𝐾) ∈ 𝐵)
Theorem	ma1repveval 22618	An entry of an identity matrix with a replaced column. (Contributed by AV, 16-Feb-2019.) (Revised by AV, 26-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐸 = (( 1 (𝑁 matRepV 𝑅)𝐶)‘𝐾)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼𝐸𝐽) = if(𝐽 = 𝐾, (𝐶‘𝐼), if(𝐽 = 𝐼, (1r‘𝑅), 0 )))
Theorem	mulmarep1el 22619	Element by element multiplication of a matrix with an identity matrix with a column replaced by a vector. (Contributed by AV, 16-Feb-2019.) (Revised by AV, 26-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐸 = (( 1 (𝑁 matRepV 𝑅)𝐶)‘𝐾)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁)) → ((𝐼𝑋𝐿)(.r‘𝑅)(𝐿𝐸𝐽)) = if(𝐽 = 𝐾, ((𝐼𝑋𝐿)(.r‘𝑅)(𝐶‘𝐿)), if(𝐽 = 𝐿, (𝐼𝑋𝐿), 0 )))
Theorem	mulmarep1gsum1 22620*	The sum of element by element multiplications of a matrix with an identity matrix with a column replaced by a vector. (Contributed by AV, 16-Feb-2019.) (Revised by AV, 26-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐸 = (( 1 (𝑁 matRepV 𝑅)𝐶)‘𝐾)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾)) → (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝐼𝑋𝑙)(.r‘𝑅)(𝑙𝐸𝐽)))) = (𝐼𝑋𝐽))
Theorem	mulmarep1gsum2 22621*	The sum of element by element multiplications of a matrix with an identity matrix with a column replaced by a vector. (Contributed by AV, 18-Feb-2019.) (Revised by AV, 26-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐸 = (( 1 (𝑁 matRepV 𝑅)𝐶)‘𝐾)    &   ⊢ × = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ (𝑋 × 𝐶) = 𝑍)) → (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝐼𝑋𝑙)(.r‘𝑅)(𝑙𝐸𝐽)))) = if(𝐽 = 𝐾, (𝑍‘𝐼), (𝐼𝑋𝐽)))
Theorem	1marepvmarrepid 22622	Replacing the ith row by 0's and the ith component of a (column) vector at the diagonal position for the identity matrix with the ith column replaced by the vector results in the matrix itself. (Contributed by AV, 14-Feb-2019.) (Revised by AV, 27-Feb-2019.)
⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁)    &   ⊢ 1 = (1r‘(𝑁 Mat 𝑅))    &   ⊢ 𝑋 = (( 1 (𝑁 matRepV 𝑅)𝑍)‘𝐼)    ⇒   ⊢ (((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) ∧ (𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉)) → (𝐼(𝑋(𝑁 matRRep 𝑅)(𝑍‘𝐼))𝐼) = 𝑋)
11.4.8  Submatrices
Syntax	csubma 22623	Syntax for submatrices of a square matrix.
class subMat
Definition	df-subma 22624*	Define the submatrices of a square matrix. A submatrix is obtained by deleting a row and a column of the original matrix. Since the indices of a matrix need not to be sequential integers, it does not matter that there may be gaps in the numbering of the indices for the submatrix. The determinants of such submatrices are called the "minors" of the original matrix. (Contributed by AV, 27-Dec-2018.)
⊢ subMat = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ (𝑛 ∖ {𝑘}), 𝑗 ∈ (𝑛 ∖ {𝑙}) ↦ (𝑖𝑚𝑗)))))
Theorem	submabas 22625*	Any subset of the index set of a square matrix defines a submatrix of the matrix. (Contributed by AV, 1-Jan-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐷 ⊆ 𝑁) → (𝑖 ∈ 𝐷, 𝑗 ∈ 𝐷 ↦ (𝑖𝑀𝑗)) ∈ (Base‘(𝐷 Mat 𝑅)))
Theorem	submafval 22626*	First substitution for a submatrix. (Contributed by AV, 28-Dec-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (𝑁 subMat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ 𝑄 = (𝑚 ∈ 𝐵 ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ (𝑁 ∖ {𝑘}), 𝑗 ∈ (𝑁 ∖ {𝑙}) ↦ (𝑖𝑚𝑗))))
Theorem	submaval0 22627*	Second substitution for a submatrix. (Contributed by AV, 28-Dec-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (𝑁 subMat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ (𝑀 ∈ 𝐵 → (𝑄‘𝑀) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ (𝑁 ∖ {𝑘}), 𝑗 ∈ (𝑁 ∖ {𝑙}) ↦ (𝑖𝑀𝑗))))
Theorem	submaval 22628*	Third substitution for a submatrix. (Contributed by AV, 28-Dec-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (𝑁 subMat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → (𝐾(𝑄‘𝑀)𝐿) = (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝑀𝑗)))
Theorem	submaeval 22629	An entry of a submatrix of a square matrix. (Contributed by AV, 28-Dec-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑄 = (𝑁 subMat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ ((𝑀 ∈ 𝐵 ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) ∧ (𝐼 ∈ (𝑁 ∖ {𝐾}) ∧ 𝐽 ∈ (𝑁 ∖ {𝐿}))) → (𝐼(𝐾(𝑄‘𝑀)𝐿)𝐽) = (𝐼𝑀𝐽))
Theorem	1marepvsma1 22630	The submatrix of the identity matrix with the ith column replaced by the vector obtained by removing the ith row and the ith column is an identity matrix. (Contributed by AV, 14-Feb-2019.) (Revised by AV, 27-Feb-2019.)
⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁)    &   ⊢ 1 = (1r‘(𝑁 Mat 𝑅))    &   ⊢ 𝑋 = (( 1 (𝑁 matRepV 𝑅)𝑍)‘𝐼)    ⇒   ⊢ (((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) ∧ (𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉)) → (𝐼((𝑁 subMat 𝑅)‘𝑋)𝐼) = (1r‘((𝑁 ∖ {𝐼}) Mat 𝑅)))
11.5  The determinant
11.5.1  Definition and basic properties
Syntax	cmdat 22631	Syntax for the matrix determinant function.
class maDet
Definition	df-mdet 22632*	Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib 22634). The properties of the axiomatic definition of a determinant according to [Weierstrass] p. 272 are derived from this definition as theorems: "The determinant function is the unique multilinear, alternating and normalized function from the algebra of square matrices of the same dimension over a commutative ring to this ring". Functionality is shown by mdetf 22642. Multilineary means "linear for each row" - the additivity is shown by mdetrlin 22649, the homogeneity by mdetrsca 22650. Furthermore, it is shown that the determinant function is alternating (see mdetralt 22655) and normalized (see mdet1 22648). Finally, uniqueness is shown by mdetuni 22669. As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib 22634. (Contributed by Stefan O'Rear, 9-Sep-2015.) (Revised by SO, 10-Jul-2018.)
⊢ maDet = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥))))))))
Theorem	mdetfval 22633*	First substitution for the determinant definition. (Contributed by Stefan O'Rear, 9-Sep-2015.) (Revised by SO, 9-Jul-2018.)
⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑌 = (ℤRHom‘𝑅)    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑈 = (mulGrp‘𝑅)    ⇒   ⊢ 𝐷 = (𝑚 ∈ 𝐵 ↦ (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))
Theorem	mdetleib 22634*	Full substitution of our determinant definition (also known as Leibniz' Formula, expanding by columns). Proposition 4.6 in [Lang] p. 514. (Contributed by Stefan O'Rear, 3-Oct-2015.) (Revised by SO, 9-Jul-2018.)
⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑌 = (ℤRHom‘𝑅)    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑈 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑀 ∈ 𝐵 → (𝐷‘𝑀) = (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥)))))))
Theorem	mdetleib2 22635*	Leibniz' formula can also be expanded by rows. (Contributed by Stefan O'Rear, 9-Jul-2018.) (Proof shortened by AV, 23-Jul-2019.)
⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑌 = (ℤRHom‘𝑅)    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑈 = (mulGrp‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ (𝑥𝑀(𝑝‘𝑥))))))))
Theorem	nfimdetndef 22636	The determinant is not defined for an infinite matrix. (Contributed by AV, 27-Dec-2018.)
⊢ 𝐷 = (𝑁 maDet 𝑅)    ⇒   ⊢ (𝑁 ∉ Fin → 𝐷 = ∅)
Theorem	mdetfval1 22637*	First substitution of an alternative determinant definition. (Contributed by Stefan O'Rear, 9-Sep-2015.) (Revised by AV, 27-Dec-2018.)
⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑌 = (ℤRHom‘𝑅)    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑈 = (mulGrp‘𝑅)    ⇒   ⊢ 𝐷 = (𝑚 ∈ 𝐵 ↦ (𝑅 Σg (𝑝 ∈ 𝑃 ↦ ((𝑌‘(𝑆‘𝑝)) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))
Theorem	mdetleib1 22638*	Full substitution of an alternative determinant definition (also known as Leibniz' Formula). (Contributed by Stefan O'Rear, 3-Oct-2015.) (Revised by AV, 26-Dec-2018.)
⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑌 = (ℤRHom‘𝑅)    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝑈 = (mulGrp‘𝑅)    ⇒   ⊢ (𝑀 ∈ 𝐵 → (𝐷‘𝑀) = (𝑅 Σg (𝑝 ∈ 𝑃 ↦ ((𝑌‘(𝑆‘𝑝)) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥)))))))
Theorem	mdet0pr 22639	The determinant function for 0-dimensional matrices on a given ring is the function mapping the empty set to the unity element of that ring. (Contributed by AV, 28-Feb-2019.)
⊢ (𝑅 ∈ Ring → (∅ maDet 𝑅) = {⟨∅, (1r‘𝑅)⟩})
Theorem	mdet0f1o 22640	The determinant function for 0-dimensional matrices on a given ring is a bijection from the singleton containing the empty set (empty matrix) onto the singleton containing the unity element of that ring. (Contributed by AV, 28-Feb-2019.)
⊢ (𝑅 ∈ Ring → (∅ maDet 𝑅):{∅}–1-1-onto→{(1r‘𝑅)})
Theorem	mdet0fv0 22641	The determinant of the empty matrix on a given ring is the unity element of that ring. (Contributed by AV, 28-Feb-2019.)
⊢ (𝑅 ∈ Ring → ((∅ maDet 𝑅)‘∅) = (1r‘𝑅))
Theorem	mdetf 22642	Functionality of the determinant, see also definition in [Lang] p. 513. (Contributed by Stefan O'Rear, 9-Jul-2018.) (Proof shortened by AV, 23-Jul-2019.)
⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝐷:𝐵⟶𝐾)
Theorem	mdetcl 22643	The determinant evaluates to an element of the base ring. (Contributed by Stefan O'Rear, 9-Sep-2015.) (Revised by AV, 7-Feb-2019.)
⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) ∈ 𝐾)
Theorem	m1detdiag 22644	The determinant of a 1-dimensional matrix equals its (single) entry. (Contributed by AV, 6-Aug-2019.)
⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (𝐼𝑀𝐼))
Theorem	mdetdiaglem 22645*	Lemma for mdetdiag 22646. Previously part of proof for mdet1 22648. (Contributed by SO, 10-Jul-2018.) (Revised by AV, 17-Aug-2019.)
⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐻 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑍 = (ℤRHom‘𝑅)    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → (((𝑍 ∘ 𝑆)‘𝑃) · (𝐺 Σg (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘)))) = 0 )
Theorem	mdetdiag 22646*	The determinant of a diagonal matrix is the product of the entries in the diagonal. (Contributed by AV, 17-Aug-2019.)
⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) → (𝐷‘𝑀) = (𝐺 Σg (𝑘 ∈ 𝑁 ↦ (𝑘𝑀𝑘)))))
Theorem	mdetdiagid 22647*	The determinant of a diagonal matrix with identical entries is the power of the entry in the diagonal. (Contributed by AV, 17-Aug-2019.)
⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑅)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶)) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑀𝑗) = if(𝑖 = 𝑗, 𝑋, 0 ) → (𝐷‘𝑀) = ((♯‘𝑁) · 𝑋)))
Theorem	mdet1 22648	The determinant of the identity matrix is 1, i.e. the determinant function is normalized, see also definition in [Lang] p. 513. (Contributed by SO, 10-Jul-2018.) (Proof shortened by AV, 25-Nov-2019.)
⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐼 = (1r‘𝐴)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → (𝐷‘𝐼) = 1 )
Theorem	mdetrlin 22649	The determinant function is additive for each row: The matrices X, Y, Z are identical except for the I's row, and the I's row of the matrix X is the componentwise sum of the I's row of the matrices Y and Z. In this case the determinant of X is the sum of the determinants of Y and Z. (Contributed by SO, 9-Jul-2018.) (Proof shortened by AV, 23-Jul-2019.)
⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ + = (+g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑁)    &   ⊢ (𝜑 → (𝑋 ↾ ({𝐼} × 𝑁)) = ((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁))))    &   ⊢ (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑌 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)))    &   ⊢ (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)))    ⇒   ⊢ (𝜑 → (𝐷‘𝑋) = ((𝐷‘𝑌) + (𝐷‘𝑍)))
Theorem	mdetrsca 22650	The determinant function is homogeneous for each row: If the matrices 𝑋 and 𝑍 are identical except for the 𝐼-th row, and the 𝐼-th row of the matrix 𝑋 is the componentwise product of the 𝐼-th row of the matrix 𝑍 and the scalar 𝑌, then the determinant of 𝑋 is the determinant of 𝑍 multiplied by 𝑌. (Contributed by SO, 9-Jul-2018.) (Proof shortened by AV, 23-Jul-2019.)
⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑁)    &   ⊢ (𝜑 → (𝑋 ↾ ({𝐼} × 𝑁)) = ((({𝐼} × 𝑁) × {𝑌}) ∘f · (𝑍 ↾ ({𝐼} × 𝑁))))    &   ⊢ (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)))    ⇒   ⊢ (𝜑 → (𝐷‘𝑋) = (𝑌 · (𝐷‘𝑍)))
Theorem	mdetrsca2 22651*	The determinant function is homogeneous for each row (matrices are given explicitly by their entries). (Contributed by SO, 16-Jul-2018.)
⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑋 ∈ 𝐾)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑌 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑁)    ⇒   ⊢ (𝜑 → (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝐹 · 𝑋), 𝑌))) = (𝐹 · (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, 𝑌)))))
Theorem	mdetr0 22652*	The determinant of a matrix with a row containing only 0's is 0. (Contributed by SO, 16-Jul-2018.)
⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑁)    ⇒   ⊢ (𝜑 → (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 0 , 𝑋))) = 0 )
Theorem	mdet0 22653	The determinant of the zero matrix (of dimension greater 0!) is 0. (Contributed by AV, 17-Aug-2019.) (Revised by AV, 3-Jul-2022.)
⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑍 = (0g‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅) → (𝐷‘𝑍) = 0 )
Theorem	mdetrlin2 22654*	The determinant function is additive for each row (matrices are given explicitly by their entries). (Contributed by SO, 16-Jul-2018.)
⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑋 ∈ 𝐾)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑌 ∈ 𝐾)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑍 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑁)    ⇒   ⊢ (𝜑 → (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍))) = ((𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, 𝑍))) + (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑌, 𝑍)))))
Theorem	mdetralt 22655*	The determinant function is alternating regarding rows: if a matrix has two identical rows, its determinant is 0. Corollary 4.9 in [Lang] p. 515. (Contributed by SO, 10-Jul-2018.) (Proof shortened by AV, 23-Jul-2018.)
⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑁)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑁)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → ∀𝑎 ∈ 𝑁 (𝐼𝑋𝑎) = (𝐽𝑋𝑎))    ⇒   ⊢ (𝜑 → (𝐷‘𝑋) = 0 )
Theorem	mdetralt2 22656*	The determinant function is alternating regarding rows (matrix is given explicitly by its entries). (Contributed by SO, 16-Jul-2018.)
⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑁) → 𝑋 ∈ 𝐾)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑌 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑁)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑁)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    ⇒   ⊢ (𝜑 → (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, if(𝑖 = 𝐽, 𝑋, 𝑌)))) = 0 )
Theorem	mdetero 22657*	The determinant function is multilinear (additive and homogeneous for each row (matrices are given explicitly by their entries). Corollary 4.9 in [Lang] p. 515. (Contributed by SO, 16-Jul-2018.)
⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑁) → 𝑋 ∈ 𝐾)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑁) → 𝑌 ∈ 𝐾)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑍 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑁)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑁)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    ⇒   ⊢ (𝜑 → (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑋 + (𝑊 · 𝑌)), if(𝑖 = 𝐽, 𝑌, 𝑍)))) = (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, if(𝑖 = 𝐽, 𝑌, 𝑍)))))
Theorem	mdettpos 22658	Determinant is invariant under transposition. Proposition 4.8 in [Lang] p. 514. (Contributed by Stefan O'Rear, 9-Jul-2018.)
⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐷‘tpos 𝑀) = (𝐷‘𝑀))
Theorem	mdetunilem1 22659*	Lemma for mdetuni 22669. (Contributed by SO, 14-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐷:𝐵⟶𝐾)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 ))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧))))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧))))    ⇒   ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝐺𝐸𝑤)) ∧ (𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺)) → (𝐷‘𝐸) = 0 )
Theorem	mdetunilem2 22660*	Lemma for mdetuni 22669. (Contributed by SO, 15-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐷:𝐵⟶𝐾)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 ))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧))))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧))))    &   ⊢ (𝜓 → 𝜑)    &   ⊢ (𝜓 → (𝐸 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐸 ≠ 𝐺))    &   ⊢ ((𝜓 ∧ 𝑏 ∈ 𝑁) → 𝐹 ∈ 𝐾)    &   ⊢ ((𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝐻 ∈ 𝐾)    ⇒   ⊢ (𝜓 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)))) = 0 )
Theorem	mdetunilem3 22661*	Lemma for mdetuni 22669. (Contributed by SO, 15-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐷:𝐵⟶𝐾)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 ))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧))))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧))))    ⇒   ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵) ∧ (𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘f + (𝐺 ↾ ({𝐻} × 𝑁)))) ∧ ((𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐷‘𝐸) = ((𝐷‘𝐹) + (𝐷‘𝐺)))
Theorem	mdetunilem4 22662*	Lemma for mdetuni 22669. (Contributed by SO, 15-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐷:𝐵⟶𝐾)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 ))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧))))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧))))    ⇒   ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ (𝐻 ∈ 𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘f · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝐺)))
Theorem	mdetunilem5 22663*	Lemma for mdetuni 22669. (Contributed by SO, 15-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐷:𝐵⟶𝐾)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 ))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧))))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧))))    &   ⊢ (𝜓 → 𝜑)    &   ⊢ (𝜓 → 𝐸 ∈ 𝑁)    &   ⊢ ((𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐾 ∧ 𝐻 ∈ 𝐾))    ⇒   ⊢ (𝜓 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, (𝐹 + 𝐺), 𝐻))) = ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, 𝐹, 𝐻))) + (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, 𝐺, 𝐻)))))
Theorem	mdetunilem6 22664*	Lemma for mdetuni 22669. (Contributed by SO, 15-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐷:𝐵⟶𝐾)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 ))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧))))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧))))    &   ⊢ (𝜓 → 𝜑)    &   ⊢ (𝜓 → (𝐸 ∈ 𝑁 ∧ 𝐹 ∈ 𝑁 ∧ 𝐸 ≠ 𝐹))    &   ⊢ ((𝜓 ∧ 𝑏 ∈ 𝑁) → (𝐺 ∈ 𝐾 ∧ 𝐻 ∈ 𝐾))    &   ⊢ ((𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝐼 ∈ 𝐾)    ⇒   ⊢ (𝜓 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, 𝐺, if(𝑎 = 𝐹, 𝐻, 𝐼)))) = ((invg‘𝑅)‘(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, 𝐻, if(𝑎 = 𝐹, 𝐺, 𝐼))))))
Theorem	mdetunilem7 22665*	Lemma for mdetuni 22669. (Contributed by SO, 15-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐷:𝐵⟶𝐾)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 ))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧))))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧))))    ⇒   ⊢ ((𝜑 ∧ 𝐸:𝑁–1-1-onto→𝑁 ∧ 𝐹 ∈ 𝐵) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝐸‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸) · (𝐷‘𝐹)))
Theorem	mdetunilem8 22666*	Lemma for mdetuni 22669. (Contributed by SO, 15-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐷:𝐵⟶𝐾)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 ))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧))))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧))))    &   ⊢ (𝜑 → (𝐷‘(1r‘𝐴)) = 0 )    ⇒   ⊢ ((𝜑 ∧ 𝐸:𝑁⟶𝑁) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if((𝐸‘𝑎) = 𝑏, 1 , 0 ))) = 0 )
Theorem	mdetunilem9 22667*	Lemma for mdetuni 22669. (Contributed by SO, 15-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐷:𝐵⟶𝐾)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 ))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧))))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧))))    &   ⊢ (𝜑 → (𝐷‘(1r‘𝐴)) = 0 )    &   ⊢ 𝑌 = {𝑥 ∣ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ (𝑁 ↑m 𝑁)(∀𝑤 ∈ 𝑥 (𝑦‘𝑤) = if(𝑤 ∈ 𝑧, 1 , 0 ) → (𝐷‘𝑦) = 0 )}    ⇒   ⊢ (𝜑 → 𝐷 = (𝐵 × { 0 }))
Theorem	mdetuni0 22668*	Lemma for mdetuni 22669. (Contributed by SO, 15-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐷:𝐵⟶𝐾)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 ))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧))))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧))))    &   ⊢ 𝐸 = (𝑁 maDet 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐷‘𝐹) = ((𝐷‘(1r‘𝐴)) · (𝐸‘𝐹)))
Theorem	mdetuni 22669*	According to the definition in [Weierstrass] p. 272, the determinant function is the unique multilinear, alternating and normalized function from the algebra of square matrices of the same dimension over a commutative ring to this ring. So for any multilinear (mdetuni.li and mdetuni.sc), alternating (mdetuni.al) and normalized (mdetuni.no) function D (mdetuni.ff) from the algebra of square matrices (mdetuni.a) to their underlying commutative ring (mdetuni.cr), the function value of this function D for a matrix F (mdetuni.f) is the determinant of this matrix. (Contributed by Stefan O'Rear, 15-Jul-2018.) (Revised by Alexander van der Vekens, 8-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐷:𝐵⟶𝐾)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 ))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧))))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧))))    &   ⊢ 𝐸 = (𝑁 maDet 𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐷‘(1r‘𝐴)) = 1 )    ⇒   ⊢ (𝜑 → (𝐷‘𝐹) = (𝐸‘𝐹))
Theorem	mdetmul 22670	Multiplicativity of the determinant function: the determinant of a matrix product of square matrices equals the product of their determinants. Proposition 4.15 in [Lang] p. 517. (Contributed by Stefan O'Rear, 16-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∙ = (.r‘𝐴)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐷‘(𝐹 ∙ 𝐺)) = ((𝐷‘𝐹) · (𝐷‘𝐺)))
11.5.2  Determinants of 2 x 2 -matrices
Theorem	m2detleiblem1 22671	Lemma 1 for m2detleib 22678. (Contributed by AV, 12-Dec-2018.)
⊢ 𝑁 = {1, 2}    &   ⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑌 = (ℤRHom‘𝑅)    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃) → (𝑌‘(𝑆‘𝑄)) = (((pmSgn‘𝑁)‘𝑄)(.g‘𝑅) 1 ))
Theorem	m2detleiblem5 22672	Lemma 5 for m2detleib 22678. (Contributed by AV, 20-Dec-2018.)
⊢ 𝑁 = {1, 2}    &   ⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑌 = (ℤRHom‘𝑅)    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {⟨1, 1⟩, ⟨2, 2⟩}) → (𝑌‘(𝑆‘𝑄)) = 1 )
Theorem	m2detleiblem6 22673	Lemma 6 for m2detleib 22678. (Contributed by AV, 20-Dec-2018.)
⊢ 𝑁 = {1, 2}    &   ⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑌 = (ℤRHom‘𝑅)    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invg‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {⟨1, 2⟩, ⟨2, 1⟩}) → (𝑌‘(𝑆‘𝑄)) = (𝐼‘ 1 ))
Theorem	m2detleiblem7 22674	Lemma 7 for m2detleib 22678. (Contributed by AV, 20-Dec-2018.)
⊢ 𝑁 = {1, 2}    &   ⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑌 = (ℤRHom‘𝑅)    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invg‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ − = (-g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (Base‘𝑅) ∧ 𝑍 ∈ (Base‘𝑅)) → (𝑋(+g‘𝑅)((𝐼‘ 1 ) · 𝑍)) = (𝑋 − 𝑍))
Theorem	m2detleiblem2 22675*	Lemma 2 for m2detleib 22678. (Contributed by AV, 16-Dec-2018.) (Proof shortened by AV, 1-Jan-2019.)
⊢ 𝑁 = {1, 2}    &   ⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵) → (𝐺 Σg (𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅))
Theorem	m2detleiblem3 22676*	Lemma 3 for m2detleib 22678. (Contributed by AV, 16-Dec-2018.) (Proof shortened by AV, 2-Jan-2019.)
⊢ 𝑁 = {1, 2}    &   ⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ · = (+g‘𝐺)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {⟨1, 1⟩, ⟨2, 2⟩} ∧ 𝑀 ∈ 𝐵) → (𝐺 Σg (𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))) = ((1𝑀1) · (2𝑀2)))
Theorem	m2detleiblem4 22677*	Lemma 4 for m2detleib 22678. (Contributed by AV, 20-Dec-2018.) (Proof shortened by AV, 2-Jan-2019.)
⊢ 𝑁 = {1, 2}    &   ⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    &   ⊢ · = (+g‘𝐺)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {⟨1, 2⟩, ⟨2, 1⟩} ∧ 𝑀 ∈ 𝐵) → (𝐺 Σg (𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))) = ((2𝑀1) · (1𝑀2)))
Theorem	m2detleib 22678	Leibniz' Formula for 2x2-matrices. (Contributed by AV, 21-Dec-2018.) (Revised by AV, 26-Dec-2018.) (Proof shortened by AV, 23-Jul-2019.)
⊢ 𝑁 = {1, 2}    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ − = (-g‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (((1𝑀1) · (2𝑀2)) − ((2𝑀1) · (1𝑀2))))
11.5.3  The matrix adjugate/adjunct
Syntax	cmadu 22679	Syntax for the matrix adjugate/adjunct function.
class maAdju
Syntax	cminmar1 22680	Syntax for the minor matrices of a square matrix.
class minMatR1
Definition	df-madu 22681*	Define the adjugate or adjunct (matrix of cofactors) of a square matrix. This definition gives the standard cofactors, however the internal minors are not the standard minors, see definition in [Lang] p. 518. (Contributed by Stefan O'Rear, 7-Sep-2015.) (Revised by SO, 10-Jul-2018.)
⊢ maAdju = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r‘𝑟), (0g‘𝑟)), (𝑘𝑚𝑙)))))))
Definition	df-minmar1 22682*	Define the matrices whose determinants are the minors of a square matrix. In contrast to the standard definition of minors, a row is replaced by 0's and one 1 instead of deleting the column and row (e.g., definition in [Lang] p. 515). By this, the determinant of such a matrix is equal to the minor determined in the standard way (as determinant of a submatrix, see df-subma 22624- note that the matrix is transposed compared with the submatrix defined in df-subma 22624, but this does not matter because the determinants are the same, see mdettpos 22658). Such matrices are used in the definition of an adjunct of a square matrix, see df-madu 22681. (Contributed by AV, 27-Dec-2018.)
⊢ minMatR1 = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, (1r‘𝑟), (0g‘𝑟)), (𝑖𝑚𝑗))))))
Theorem	mndifsplit 22683	Lemma for maducoeval2 22687. (Contributed by SO, 16-Jul-2018.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 0 = (0g‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ ((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 )))
Theorem	madufval 22684*	First substitution for the adjunct (cofactor) matrix. (Contributed by SO, 11-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐽 = (𝑁 maAdju 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ 𝐽 = (𝑚 ∈ 𝐵 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝐷‘(𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, 1 , 0 ), (𝑘𝑚𝑙))))))
Theorem	maduval 22685*	Second substitution for the adjunct (cofactor) matrix. (Contributed by SO, 11-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐽 = (𝑁 maAdju 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑀 ∈ 𝐵 → (𝐽‘𝑀) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝐷‘(𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, 1 , 0 ), (𝑘𝑀𝑙))))))
Theorem	maducoeval 22686*	An entry of the adjunct (cofactor) matrix. (Contributed by SO, 11-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐽 = (𝑁 maAdju 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁 ∧ 𝐻 ∈ 𝑁) → (𝐼(𝐽‘𝑀)𝐻) = (𝐷‘(𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ if(𝑘 = 𝐻, if(𝑙 = 𝐼, 1 , 0 ), (𝑘𝑀𝑙)))))
Theorem	maducoeval2 22687*	An entry of the adjunct (cofactor) matrix. (Contributed by SO, 17-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐽 = (𝑁 maAdju 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐻 ∈ 𝑁) → (𝐼(𝐽‘𝑀)𝐻) = (𝐷‘(𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ if((𝑘 = 𝐻 ∨ 𝑙 = 𝐼), if((𝑙 = 𝐼 ∧ 𝑘 = 𝐻), 1 , 0 ), (𝑘𝑀𝑙)))))
Theorem	maduf 22688	Creating the adjunct of matrices is a function from the set of matrices into the set of matrices. (Contributed by Stefan O'Rear, 11-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐽 = (𝑁 maAdju 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ (𝑅 ∈ CRing → 𝐽:𝐵⟶𝐵)
Theorem	madutpos 22689	The adjuct of a transposed matrix is the transposition of the adjunct of the matrix. (Contributed by Stefan O'Rear, 17-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐽 = (𝑁 maAdju 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐽‘tpos 𝑀) = tpos (𝐽‘𝑀))
Theorem	madugsum 22690*	The determinant of a matrix with a row 𝐿 consisting of the same element 𝑋 is the sum of the elements of the 𝐿-th column of the adjunct of the matrix multiplied with 𝑋. (Contributed by Stefan O'Rear, 16-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐽 = (𝑁 maAdju 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝐿 ∈ 𝑁)    ⇒   ⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ 𝑁 ↦ (𝑋 · (𝑖(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑗 ∈ 𝑁, 𝑖 ∈ 𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖)))))
Theorem	madurid 22691	Multiplying a matrix with its adjunct results in the identity matrix multiplied with the determinant of the matrix. See Proposition 4.16 in [Lang] p. 518. (Contributed by Stefan O'Rear, 16-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐽 = (𝑁 maAdju 𝑅)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ · = (.r‘𝐴)    &   ⊢ ∙ = ( ·𝑠 ‘𝐴)    ⇒   ⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → (𝑀 · (𝐽‘𝑀)) = ((𝐷‘𝑀) ∙ 1 ))
Theorem	madulid 22692	Multiplying the adjunct of a matrix with the matrix results in the identity matrix multiplied with the determinant of the matrix. See Proposition 4.16 in [Lang] p. 518. (Contributed by Stefan O'Rear, 17-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐽 = (𝑁 maAdju 𝑅)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ · = (.r‘𝐴)    &   ⊢ ∙ = ( ·𝑠 ‘𝐴)    ⇒   ⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → ((𝐽‘𝑀) · 𝑀) = ((𝐷‘𝑀) ∙ 1 ))
Theorem	minmar1fval 22693*	First substitution for the definition of a matrix for a minor. (Contributed by AV, 31-Dec-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑄 = (𝑁 minMatR1 𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ 𝑄 = (𝑚 ∈ 𝐵 ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 1 , 0 ), (𝑖𝑚𝑗)))))
Theorem	minmar1val0 22694*	Second substitution for the definition of a matrix for a minor. (Contributed by AV, 31-Dec-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑄 = (𝑁 minMatR1 𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑀 ∈ 𝐵 → (𝑄‘𝑀) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 1 , 0 ), (𝑖𝑀𝑗)))))
Theorem	minmar1val 22695*	Third substitution for the definition of a matrix for a minor. (Contributed by AV, 31-Dec-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑄 = (𝑁 minMatR1 𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → (𝐾(𝑄‘𝑀)𝐿) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 1 , 0 ), (𝑖𝑀𝑗))))
Theorem	minmar1eval 22696	An entry of a matrix for a minor. (Contributed by AV, 31-Dec-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑄 = (𝑁 minMatR1 𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑀 ∈ 𝐵 ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝐾(𝑄‘𝑀)𝐿)𝐽) = if(𝐼 = 𝐾, if(𝐽 = 𝐿, 1 , 0 ), (𝐼𝑀𝐽)))
Theorem	minmar1marrep 22697	The minor matrix is a special case of a matrix with a replaced row. (Contributed by AV, 12-Feb-2019.) (Revised by AV, 4-Jul-2022.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((𝑁 minMatR1 𝑅)‘𝑀) = (𝑀(𝑁 matRRep 𝑅) 1 ))
Theorem	minmar1cl 22698	Closure of the row replacement function for square matrices: The matrix for a minor is a matrix. (Contributed by AV, 13-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁)) → (𝐾((𝑁 minMatR1 𝑅)‘𝑀)𝐿) ∈ 𝐵)
Theorem	maducoevalmin1 22699	The coefficients of an adjunct (matrix of cofactors) expressed as determinants of the minor matrices (alternative definition) of the original matrix. (Contributed by AV, 31-Dec-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐽 = (𝑁 maAdju 𝑅)    ⇒   ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁 ∧ 𝐻 ∈ 𝑁) → (𝐼(𝐽‘𝑀)𝐻) = (𝐷‘(𝐻((𝑁 minMatR1 𝑅)‘𝑀)𝐼)))
11.5.4  Laplace expansion of determinants (special case) According to Wikipedia ("Laplace expansion", 08-Mar-2019, https://en.wikipedia.org/wiki/Laplace_expansion) "In linear algebra, the Laplace expansion, named after Pierre-Simon Laplace, also called cofactor expansion, is an expression for the determinant det(B) of an n x n -matrix B that is a weighted sum of the determinants of n sub-matrices of B, each of size (n-1) x (n-1)". The expansion is usually performed for a row of matrix B (alternately for a column of matrix B). The mentioned "sub-matrices" are the matrices resultung from deleting the i-th row and the j-th column of matrix B. The mentioned "weights" (factors/coefficients) are the elements at position i and j in matrix B. If the expansion is performed for a row, the coefficients are the elements of the selected row. In the following, only the case where the row for the expansion contains only the zero element of the underlying ring except at the diagonal position. By this, the sum for the Laplace expansion is reduced to one summand, consisting of the element at the diagonal position multiplied with the determinant of the corresponding submatrix, see smadiadetg 22720 or smadiadetr 22722.
Theorem	symgmatr01lem 22700*	Lemma for symgmatr01 22701. (Contributed by AV, 3-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    ⇒   ⊢ ((𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → (𝑄 ∈ (𝑃 ∖ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐿}) → ∃𝑘 ∈ 𝑁 if(𝑘 = 𝐾, if((𝑄‘𝑘) = 𝐿, 𝐴, 𝐵), (𝑘𝑀(𝑄‘𝑘))) = 𝐵))