![]() |
Metamath
Proof Explorer Theorem List (p. 224 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | submabas 22301* | 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 22302* | First substitution for a submatrix. (Contributed by AV, 28-Dec-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ = (๐ subMat ๐ ) & โข ๐ต = (Baseโ๐ด) โ โข ๐ = (๐ โ ๐ต โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ โ (๐ โ {๐}), ๐ โ (๐ โ {๐}) โฆ (๐๐๐)))) | ||
Theorem | submaval0 22303* | Second substitution for a submatrix. (Contributed by AV, 28-Dec-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ = (๐ subMat ๐ ) & โข ๐ต = (Baseโ๐ด) โ โข (๐ โ ๐ต โ (๐โ๐) = (๐ โ ๐, ๐ โ ๐ โฆ (๐ โ (๐ โ {๐}), ๐ โ (๐ โ {๐}) โฆ (๐๐๐)))) | ||
Theorem | submaval 22304* | Third substitution for a submatrix. (Contributed by AV, 28-Dec-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ = (๐ subMat ๐ ) & โข ๐ต = (Baseโ๐ด) โ โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ฟ โ ๐) โ (๐พ(๐โ๐)๐ฟ) = (๐ โ (๐ โ {๐พ}), ๐ โ (๐ โ {๐ฟ}) โฆ (๐๐๐))) | ||
Theorem | submaeval 22305 | An entry of a submatrix of a square matrix. (Contributed by AV, 28-Dec-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ = (๐ subMat ๐ ) & โข ๐ต = (Baseโ๐ด) โ โข ((๐ โ ๐ต โง (๐พ โ ๐ โง ๐ฟ โ ๐) โง (๐ผ โ (๐ โ {๐พ}) โง ๐ฝ โ (๐ โ {๐ฟ}))) โ (๐ผ(๐พ(๐โ๐)๐ฟ)๐ฝ) = (๐ผ๐๐ฝ)) | ||
Theorem | 1marepvsma1 22306 | 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 ๐ ))) | ||
Syntax | cmdat 22307 | Syntax for the matrix determinant function. |
class maDet | ||
Definition | df-mdet 22308* | Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib 22310). 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 22318. Multilineary means "linear for each row" - the additivity is shown by mdetrlin 22325, the homogeneity by mdetrsca 22326. Furthermore, it is shown that the determinant function is alternating (see mdetralt 22331) and normalized (see mdet1 22324). Finally, uniqueness is shown by mdetuni 22345. As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib 22310. (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 22309* | 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 22310* | 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 22311* | 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 22312 | The determinant is not defined for an infinite matrix. (Contributed by AV, 27-Dec-2018.) |
โข ๐ท = (๐ maDet ๐ ) โ โข (๐ โ Fin โ ๐ท = โ ) | ||
Theorem | mdetfval1 22313* | 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 22314* | 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 22315 | 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 22316 | 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 22317 | 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 22318 | 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 22319 | 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 22320 | The determinant of a 1-dimensional matrix equals its (single) entry. (Contributed by AV, 6-Aug-2019.) |
โข ๐ท = (๐ maDet ๐ ) & โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) โ โข ((๐ โ CRing โง (๐ = {๐ผ} โง ๐ผ โ ๐) โง ๐ โ ๐ต) โ (๐ทโ๐) = (๐ผ๐๐ผ)) | ||
Theorem | mdetdiaglem 22321* | Lemma for mdetdiag 22322. Previously part of proof for mdet1 22324. (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 22322* | 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 22323* | 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 22324 | 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 22325 | 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 22326 | 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 22327* | 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 22328* | 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 22329 | 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 22330* | 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 22331* | 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 22332* | 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 22333* | 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 22334 | 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 22335* | Lemma for mdetuni 22345. (Contributed by SO, 14-Jul-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐พ = (Baseโ๐ ) & โข 0 = (0gโ๐ ) & โข 1 = (1rโ๐ ) & โข + = (+gโ๐ ) & โข ยท = (.rโ๐ ) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ท:๐ตโถ๐พ) & โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฆ โ ๐ง โง โ๐ค โ ๐ (๐ฆ๐ฅ๐ค) = (๐ง๐ฅ๐ค)) โ (๐ทโ๐ฅ) = 0 )) & โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ฅ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = ((๐ทโ๐ฆ) + (๐ทโ๐ง)))) & โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐พ โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ฅ โพ ({๐ค} ร ๐)) = ((({๐ค} ร ๐) ร {๐ฆ}) โf ยท (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = (๐ฆ ยท (๐ทโ๐ง)))) โ โข (((๐ โง ๐ธ โ ๐ต โง โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐บ๐ธ๐ค)) โง (๐น โ ๐ โง ๐บ โ ๐ โง ๐น โ ๐บ)) โ (๐ทโ๐ธ) = 0 ) | ||
Theorem | mdetunilem2 22336* | Lemma for mdetuni 22345. (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 22337* | Lemma for mdetuni 22345. (Contributed by SO, 15-Jul-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐พ = (Baseโ๐ ) & โข 0 = (0gโ๐ ) & โข 1 = (1rโ๐ ) & โข + = (+gโ๐ ) & โข ยท = (.rโ๐ ) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ท:๐ตโถ๐พ) & โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฆ โ ๐ง โง โ๐ค โ ๐ (๐ฆ๐ฅ๐ค) = (๐ง๐ฅ๐ค)) โ (๐ทโ๐ฅ) = 0 )) & โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ฅ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = ((๐ทโ๐ฆ) + (๐ทโ๐ง)))) & โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐พ โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ฅ โพ ({๐ค} ร ๐)) = ((({๐ค} ร ๐) ร {๐ฆ}) โf ยท (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = (๐ฆ ยท (๐ทโ๐ง)))) โ โข (((๐ โง ๐ธ โ ๐ต โง ๐น โ ๐ต) โง (๐บ โ ๐ต โง ๐ป โ ๐ โง (๐ธ โพ ({๐ป} ร ๐)) = ((๐น โพ ({๐ป} ร ๐)) โf + (๐บ โพ ({๐ป} ร ๐)))) โง ((๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐น โพ ((๐ โ {๐ป}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐บ โพ ((๐ โ {๐ป}) ร ๐)))) โ (๐ทโ๐ธ) = ((๐ทโ๐น) + (๐ทโ๐บ))) | ||
Theorem | mdetunilem4 22338* | Lemma for mdetuni 22345. (Contributed by SO, 15-Jul-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐พ = (Baseโ๐ ) & โข 0 = (0gโ๐ ) & โข 1 = (1rโ๐ ) & โข + = (+gโ๐ ) & โข ยท = (.rโ๐ ) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ท:๐ตโถ๐พ) & โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฆ โ ๐ง โง โ๐ค โ ๐ (๐ฆ๐ฅ๐ค) = (๐ง๐ฅ๐ค)) โ (๐ทโ๐ฅ) = 0 )) & โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ฅ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = ((๐ทโ๐ฆ) + (๐ทโ๐ง)))) & โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐พ โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ฅ โพ ({๐ค} ร ๐)) = ((({๐ค} ร ๐) ร {๐ฆ}) โf ยท (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = (๐ฆ ยท (๐ทโ๐ง)))) โ โข ((๐ โง (๐ธ โ ๐ต โง ๐น โ ๐พ โง ๐บ โ ๐ต) โง (๐ป โ ๐ โง (๐ธ โพ ({๐ป} ร ๐)) = ((({๐ป} ร ๐) ร {๐น}) โf ยท (๐บ โพ ({๐ป} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐บ โพ ((๐ โ {๐ป}) ร ๐)))) โ (๐ทโ๐ธ) = (๐น ยท (๐ทโ๐บ))) | ||
Theorem | mdetunilem5 22339* | Lemma for mdetuni 22345. (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 22340* | Lemma for mdetuni 22345. (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 22341* | Lemma for mdetuni 22345. (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 22342* | Lemma for mdetuni 22345. (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 22343* | Lemma for mdetuni 22345. (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 22344* | Lemma for mdetuni 22345. (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 22345* | 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 22346 | 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 โง ๐น โ ๐ต โง ๐บ โ ๐ต) โ (๐ทโ(๐น โ ๐บ)) = ((๐ทโ๐น) ยท (๐ทโ๐บ))) | ||
Theorem | m2detleiblem1 22347 | Lemma 1 for m2detleib 22354. (Contributed by AV, 12-Dec-2018.) |
โข ๐ = {1, 2} & โข ๐ = (Baseโ(SymGrpโ๐)) & โข ๐ = (โคRHomโ๐ ) & โข ๐ = (pmSgnโ๐) & โข 1 = (1rโ๐ ) โ โข ((๐ โ Ring โง ๐ โ ๐) โ (๐โ(๐โ๐)) = (((pmSgnโ๐)โ๐)(.gโ๐ ) 1 )) | ||
Theorem | m2detleiblem5 22348 | Lemma 5 for m2detleib 22354. (Contributed by AV, 20-Dec-2018.) |
โข ๐ = {1, 2} & โข ๐ = (Baseโ(SymGrpโ๐)) & โข ๐ = (โคRHomโ๐ ) & โข ๐ = (pmSgnโ๐) & โข 1 = (1rโ๐ ) โ โข ((๐ โ Ring โง ๐ = {โจ1, 1โฉ, โจ2, 2โฉ}) โ (๐โ(๐โ๐)) = 1 ) | ||
Theorem | m2detleiblem6 22349 | Lemma 6 for m2detleib 22354. (Contributed by AV, 20-Dec-2018.) |
โข ๐ = {1, 2} & โข ๐ = (Baseโ(SymGrpโ๐)) & โข ๐ = (โคRHomโ๐ ) & โข ๐ = (pmSgnโ๐) & โข 1 = (1rโ๐ ) & โข ๐ผ = (invgโ๐ ) โ โข ((๐ โ Ring โง ๐ = {โจ1, 2โฉ, โจ2, 1โฉ}) โ (๐โ(๐โ๐)) = (๐ผโ 1 )) | ||
Theorem | m2detleiblem7 22350 | Lemma 7 for m2detleib 22354. (Contributed by AV, 20-Dec-2018.) |
โข ๐ = {1, 2} & โข ๐ = (Baseโ(SymGrpโ๐)) & โข ๐ = (โคRHomโ๐ ) & โข ๐ = (pmSgnโ๐) & โข 1 = (1rโ๐ ) & โข ๐ผ = (invgโ๐ ) & โข ยท = (.rโ๐ ) & โข โ = (-gโ๐ ) โ โข ((๐ โ Ring โง ๐ โ (Baseโ๐ ) โง ๐ โ (Baseโ๐ )) โ (๐(+gโ๐ )((๐ผโ 1 ) ยท ๐)) = (๐ โ ๐)) | ||
Theorem | m2detleiblem2 22351* | Lemma 2 for m2detleib 22354. (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 22352* | Lemma 3 for m2detleib 22354. (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 22353* | Lemma 4 for m2detleib 22354. (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 22354 | 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)))) | ||
Syntax | cmadu 22355 | Syntax for the matrix adjugate/adjunct function. |
class maAdju | ||
Syntax | cminmar1 22356 | Syntax for the minor matrices of a square matrix. |
class minMatR1 | ||
Definition | df-madu 22357* | 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 22358* | 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 22300- note that the matrix is transposed compared with the submatrix defined in df-subma 22300, but this does not matter because the determinants are the same, see mdettpos 22334). Such matrices are used in the definition of an adjunct of a square matrix, see df-madu 22357. (Contributed by AV, 27-Dec-2018.) |
โข minMatR1 = (๐ โ V, ๐ โ V โฆ (๐ โ (Baseโ(๐ Mat ๐)) โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, if(๐ = ๐, (1rโ๐), (0gโ๐)), (๐๐๐)))))) | ||
Theorem | mndifsplit 22359 | Lemma for maducoeval2 22363. (Contributed by SO, 16-Jul-2018.) |
โข ๐ต = (Baseโ๐) & โข 0 = (0gโ๐) & โข + = (+gโ๐) โ โข ((๐ โ Mnd โง ๐ด โ ๐ต โง ยฌ (๐ โง ๐)) โ if((๐ โจ ๐), ๐ด, 0 ) = (if(๐, ๐ด, 0 ) + if(๐, ๐ด, 0 ))) | ||
Theorem | madufval 22360* | 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 22361* | 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 22362* | 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 22363* | 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 22364 | 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 22365 | 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 22366* | 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 22367 | 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 22368 | 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 22369* | 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 22370* | 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 22371* | 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 22372 | 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 22373 | 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 22374 | 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 22375 | 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 ๐ )โ๐)๐ผ))) | ||
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 22396 or smadiadetr 22398. | ||
Theorem | symgmatr01lem 22376* | Lemma for symgmatr01 22377. (Contributed by AV, 3-Jan-2019.) |
โข ๐ = (Baseโ(SymGrpโ๐)) โ โข ((๐พ โ ๐ โง ๐ฟ โ ๐) โ (๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ}) โ โ๐ โ ๐ if(๐ = ๐พ, if((๐โ๐) = ๐ฟ, ๐ด, ๐ต), (๐๐(๐โ๐))) = ๐ต)) | ||
Theorem | symgmatr01 22377* | Applying a permutation that does not fix a certain element of a set to a second element to an index of a matrix a row with 0's and a 1. (Contributed by AV, 3-Jan-2019.) |
โข ๐ = (Baseโ(SymGrpโ๐)) & โข 0 = (0gโ๐ ) & โข 1 = (1rโ๐ ) โ โข ((๐พ โ ๐ โง ๐ฟ โ ๐) โ (๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ}) โ โ๐ โ ๐ (๐(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐ฟ, 1 , 0 ), (๐๐๐)))(๐โ๐)) = 0 )) | ||
Theorem | gsummatr01lem1 22378* | Lemma A for gsummatr01 22382. (Contributed by AV, 8-Jan-2019.) |
โข ๐ = (Baseโ(SymGrpโ๐)) & โข ๐ = {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ} โ โข ((๐ โ ๐ โง ๐ โ ๐) โ (๐โ๐) โ ๐) | ||
Theorem | gsummatr01lem2 22379* | Lemma B for gsummatr01 22382. (Contributed by AV, 8-Jan-2019.) |
โข ๐ = (Baseโ(SymGrpโ๐)) & โข ๐ = {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ} โ โข ((๐ โ ๐ โง ๐ โ ๐) โ (โ๐ โ ๐ โ๐ โ ๐ (๐๐ด๐) โ (Baseโ๐บ) โ (๐๐ด(๐โ๐)) โ (Baseโ๐บ))) | ||
Theorem | gsummatr01lem3 22380* | Lemma 1 for gsummatr01 22382. (Contributed by AV, 8-Jan-2019.) |
โข ๐ = (Baseโ(SymGrpโ๐)) & โข ๐ = {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ} & โข 0 = (0gโ๐บ) & โข ๐ = (Baseโ๐บ) โ โข (((๐บ โ CMnd โง ๐ โ Fin) โง (โ๐ โ ๐ โ๐ โ ๐ (๐๐ด๐) โ ๐ โง ๐ต โ ๐) โง (๐พ โ ๐ โง ๐ฟ โ ๐ โง ๐ โ ๐ )) โ (๐บ ฮฃg (๐ โ ((๐ โ {๐พ}) โช {๐พ}) โฆ (๐(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐ฟ, 0 , ๐ต), (๐๐ด๐)))(๐โ๐)))) = ((๐บ ฮฃg (๐ โ (๐ โ {๐พ}) โฆ (๐(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐ฟ, 0 , ๐ต), (๐๐ด๐)))(๐โ๐))))(+gโ๐บ)(๐พ(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐ฟ, 0 , ๐ต), (๐๐ด๐)))(๐โ๐พ)))) | ||
Theorem | gsummatr01lem4 22381* | Lemma 2 for gsummatr01 22382. (Contributed by AV, 8-Jan-2019.) |
โข ๐ = (Baseโ(SymGrpโ๐)) & โข ๐ = {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ} & โข 0 = (0gโ๐บ) & โข ๐ = (Baseโ๐บ) โ โข ((((๐บ โ CMnd โง ๐ โ Fin) โง (โ๐ โ ๐ โ๐ โ ๐ (๐๐ด๐) โ ๐ โง ๐ต โ ๐) โง (๐พ โ ๐ โง ๐ฟ โ ๐ โง ๐ โ ๐ )) โง ๐ โ (๐ โ {๐พ})) โ (๐(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐ฟ, 0 , ๐ต), (๐๐ด๐)))(๐โ๐)) = (๐(๐ โ (๐ โ {๐พ}), ๐ โ (๐ โ {๐ฟ}) โฆ (๐๐ด๐))(๐โ๐))) | ||
Theorem | gsummatr01 22382* | Lemma 1 for smadiadetlem4 22392. (Contributed by AV, 8-Jan-2019.) |
โข ๐ = (Baseโ(SymGrpโ๐)) & โข ๐ = {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ} & โข 0 = (0gโ๐บ) & โข ๐ = (Baseโ๐บ) โ โข (((๐บ โ CMnd โง ๐ โ Fin) โง (โ๐ โ ๐ โ๐ โ ๐ (๐๐ด๐) โ ๐ โง ๐ต โ ๐) โง (๐พ โ ๐ โง ๐ฟ โ ๐ โง ๐ โ ๐ )) โ (๐บ ฮฃg (๐ โ ๐ โฆ (๐(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐ฟ, 0 , ๐ต), (๐๐ด๐)))(๐โ๐)))) = (๐บ ฮฃg (๐ โ (๐ โ {๐พ}) โฆ (๐(๐ โ (๐ โ {๐พ}), ๐ โ (๐ โ {๐ฟ}) โฆ (๐๐ด๐))(๐โ๐))))) | ||
Theorem | marep01ma 22383* | Replacing a row of a square matrix by a row with 0's and a 1 results in a square matrix of the same dimension. (Contributed by AV, 30-Dec-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ โ CRing & โข 0 = (0gโ๐ ) & โข 1 = (1rโ๐ ) โ โข (๐ โ ๐ต โ (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐ป, if(๐ = ๐ผ, 1 , 0 ), (๐๐๐))) โ ๐ต) | ||
Theorem | smadiadetlem0 22384* | Lemma 0 for smadiadet 22393: The products of the Leibniz' formula vanish for all permutations fixing the index of the row containing the 0's and the 1 to the column with the 1. (Contributed by AV, 3-Jan-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ โ CRing & โข 0 = (0gโ๐ ) & โข 1 = (1rโ๐ ) & โข ๐ = (Baseโ(SymGrpโ๐)) & โข ๐บ = (mulGrpโ๐ ) โ โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ฟ โ ๐) โ (๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ}) โ (๐บ ฮฃg (๐ โ ๐ โฆ (๐(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐ฟ, 1 , 0 ), (๐๐๐)))(๐โ๐)))) = 0 )) | ||
Theorem | smadiadetlem1 22385* | Lemma 1 for smadiadet 22393: A summand of the determinant of a matrix belongs to the underlying ring. (Contributed by AV, 1-Jan-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ โ CRing & โข 0 = (0gโ๐ ) & โข 1 = (1rโ๐ ) & โข ๐ = (Baseโ(SymGrpโ๐)) & โข ๐บ = (mulGrpโ๐ ) & โข ๐ = (โคRHomโ๐ ) & โข ๐ = (pmSgnโ๐) & โข ยท = (.rโ๐ ) โ โข (((๐ โ ๐ต โง ๐พ โ ๐) โง ๐ โ ๐) โ (((๐ โ ๐)โ๐)(.rโ๐ )(๐บ ฮฃg (๐ โ ๐ โฆ (๐(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐พ, 1 , 0 ), (๐๐๐)))(๐โ๐))))) โ (Baseโ๐ )) | ||
Theorem | smadiadetlem1a 22386* | Lemma 1a for smadiadet 22393: The summands of the Leibniz' formula vanish for all permutations fixing the index of the row containing the 0's and the 1 to the column with the 1. (Contributed by AV, 3-Jan-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ โ CRing & โข 0 = (0gโ๐ ) & โข 1 = (1rโ๐ ) & โข ๐ = (Baseโ(SymGrpโ๐)) & โข ๐บ = (mulGrpโ๐ ) & โข ๐ = (โคRHomโ๐ ) & โข ๐ = (pmSgnโ๐) & โข ยท = (.rโ๐ ) โ โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ฟ โ ๐) โ (๐ ฮฃg (๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐ฟ}) โฆ (((๐ โ ๐)โ๐) ยท (๐บ ฮฃg (๐ โ ๐ โฆ (๐(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐ฟ, 1 , 0 ), (๐๐๐)))(๐โ๐))))))) = 0 ) | ||
Theorem | smadiadetlem2 22387* | Lemma 2 for smadiadet 22393: The summands of the Leibniz' formula vanish for all permutations fixing the index of the row containing the 0's and the 1 to itself. (Contributed by AV, 31-Dec-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ โ CRing & โข 0 = (0gโ๐ ) & โข 1 = (1rโ๐ ) & โข ๐ = (Baseโ(SymGrpโ๐)) & โข ๐บ = (mulGrpโ๐ ) & โข ๐ = (โคRHomโ๐ ) & โข ๐ = (pmSgnโ๐) & โข ยท = (.rโ๐ ) โ โข ((๐ โ ๐ต โง ๐พ โ ๐) โ (๐ ฮฃg (๐ โ (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐พ}) โฆ (((๐ โ ๐)โ๐) ยท (๐บ ฮฃg (๐ โ ๐ โฆ (๐(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐พ, 1 , 0 ), (๐๐๐)))(๐โ๐))))))) = 0 ) | ||
Theorem | smadiadetlem3lem0 22388* | Lemma 0 for smadiadetlem3 22391. (Contributed by AV, 12-Jan-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ โ CRing & โข 0 = (0gโ๐ ) & โข 1 = (1rโ๐ ) & โข ๐ = (Baseโ(SymGrpโ๐)) & โข ๐บ = (mulGrpโ๐ ) & โข ๐ = (โคRHomโ๐ ) & โข ๐ = (pmSgnโ๐) & โข ยท = (.rโ๐ ) & โข ๐ = (Baseโ(SymGrpโ(๐ โ {๐พ}))) & โข ๐ = (pmSgnโ(๐ โ {๐พ})) โ โข (((๐ โ ๐ต โง ๐พ โ ๐) โง ๐ โ ๐) โ (((๐ โ ๐)โ๐)(.rโ๐ )(๐บ ฮฃg (๐ โ (๐ โ {๐พ}) โฆ (๐(๐ โ (๐ โ {๐พ}), ๐ โ (๐ โ {๐พ}) โฆ (๐๐๐))(๐โ๐))))) โ (Baseโ๐ )) | ||
Theorem | smadiadetlem3lem1 22389* | Lemma 1 for smadiadetlem3 22391. (Contributed by AV, 12-Jan-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ โ CRing & โข 0 = (0gโ๐ ) & โข 1 = (1rโ๐ ) & โข ๐ = (Baseโ(SymGrpโ๐)) & โข ๐บ = (mulGrpโ๐ ) & โข ๐ = (โคRHomโ๐ ) & โข ๐ = (pmSgnโ๐) & โข ยท = (.rโ๐ ) & โข ๐ = (Baseโ(SymGrpโ(๐ โ {๐พ}))) & โข ๐ = (pmSgnโ(๐ โ {๐พ})) โ โข ((๐ โ ๐ต โง ๐พ โ ๐) โ (๐ โ ๐ โฆ (((๐ โ ๐)โ๐)(.rโ๐ )(๐บ ฮฃg (๐ โ (๐ โ {๐พ}) โฆ (๐(๐ โ (๐ โ {๐พ}), ๐ โ (๐ โ {๐พ}) โฆ (๐๐๐))(๐โ๐)))))):๐โถ(Baseโ๐ )) | ||
Theorem | smadiadetlem3lem2 22390* | Lemma 2 for smadiadetlem3 22391. (Contributed by AV, 12-Jan-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ โ CRing & โข 0 = (0gโ๐ ) & โข 1 = (1rโ๐ ) & โข ๐ = (Baseโ(SymGrpโ๐)) & โข ๐บ = (mulGrpโ๐ ) & โข ๐ = (โคRHomโ๐ ) & โข ๐ = (pmSgnโ๐) & โข ยท = (.rโ๐ ) & โข ๐ = (Baseโ(SymGrpโ(๐ โ {๐พ}))) & โข ๐ = (pmSgnโ(๐ โ {๐พ})) โ โข ((๐ โ ๐ต โง ๐พ โ ๐) โ ran (๐ โ ๐ โฆ (((๐ โ ๐)โ๐)(.rโ๐ )(๐บ ฮฃg (๐ โ (๐ โ {๐พ}) โฆ (๐(๐ โ (๐ โ {๐พ}), ๐ โ (๐ โ {๐พ}) โฆ (๐๐๐))(๐โ๐)))))) โ ((Cntzโ๐ )โran (๐ โ ๐ โฆ (((๐ โ ๐)โ๐)(.rโ๐ )(๐บ ฮฃg (๐ โ (๐ โ {๐พ}) โฆ (๐(๐ โ (๐ โ {๐พ}), ๐ โ (๐ โ {๐พ}) โฆ (๐๐๐))(๐โ๐)))))))) | ||
Theorem | smadiadetlem3 22391* | Lemma 3 for smadiadet 22393. (Contributed by AV, 31-Jan-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ โ CRing & โข 0 = (0gโ๐ ) & โข 1 = (1rโ๐ ) & โข ๐ = (Baseโ(SymGrpโ๐)) & โข ๐บ = (mulGrpโ๐ ) & โข ๐ = (โคRHomโ๐ ) & โข ๐ = (pmSgnโ๐) & โข ยท = (.rโ๐ ) & โข ๐ = (Baseโ(SymGrpโ(๐ โ {๐พ}))) & โข ๐ = (pmSgnโ(๐ โ {๐พ})) โ โข ((๐ โ ๐ต โง ๐พ โ ๐) โ (๐ ฮฃg (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐พ} โฆ (((๐ โ ๐)โ๐)(.rโ๐ )(๐บ ฮฃg (๐ โ (๐ โ {๐พ}) โฆ (๐(๐ โ (๐ โ {๐พ}), ๐ โ (๐ โ {๐พ}) โฆ (๐๐๐))(๐โ๐))))))) = (๐ ฮฃg (๐ โ ๐ โฆ (((๐ โ ๐)โ๐)(.rโ๐ )(๐บ ฮฃg (๐ โ (๐ โ {๐พ}) โฆ (๐(๐ โ (๐ โ {๐พ}), ๐ โ (๐ โ {๐พ}) โฆ (๐๐๐))(๐โ๐)))))))) | ||
Theorem | smadiadetlem4 22392* | Lemma 4 for smadiadet 22393. (Contributed by AV, 31-Jan-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ โ CRing & โข 0 = (0gโ๐ ) & โข 1 = (1rโ๐ ) & โข ๐ = (Baseโ(SymGrpโ๐)) & โข ๐บ = (mulGrpโ๐ ) & โข ๐ = (โคRHomโ๐ ) & โข ๐ = (pmSgnโ๐) & โข ยท = (.rโ๐ ) & โข ๐ = (Baseโ(SymGrpโ(๐ โ {๐พ}))) & โข ๐ = (pmSgnโ(๐ โ {๐พ})) โ โข ((๐ โ ๐ต โง ๐พ โ ๐) โ (๐ ฮฃg (๐ โ {๐ โ ๐ โฃ (๐โ๐พ) = ๐พ} โฆ (((๐ โ ๐)โ๐)(.rโ๐ )(๐บ ฮฃg (๐ โ ๐ โฆ (๐(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐พ, if(๐ = ๐พ, 1 , 0 ), (๐๐๐)))(๐โ๐))))))) = (๐ ฮฃg (๐ โ ๐ โฆ (((๐ โ ๐)โ๐)(.rโ๐ )(๐บ ฮฃg (๐ โ (๐ โ {๐พ}) โฆ (๐(๐ โ (๐ โ {๐พ}), ๐ โ (๐ โ {๐พ}) โฆ (๐๐๐))(๐โ๐)))))))) | ||
Theorem | smadiadet 22393 | The determinant of a submatrix of a square matrix obtained by removing a row and a column at the same index equals the determinant of the original matrix with the row replaced with 0's and a 1 at the diagonal position. (Contributed by AV, 31-Jan-2019.) (Proof shortened by AV, 24-Jul-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ โ CRing & โข ๐ท = (๐ maDet ๐ ) & โข ๐ธ = ((๐ โ {๐พ}) maDet ๐ ) โ โข ((๐ โ ๐ต โง ๐พ โ ๐) โ (๐ธโ(๐พ((๐ subMat ๐ )โ๐)๐พ)) = (๐ทโ(๐พ((๐ minMatR1 ๐ )โ๐)๐พ))) | ||
Theorem | smadiadetglem1 22394 | Lemma 1 for smadiadetg 22396. (Contributed by AV, 13-Feb-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ โ CRing & โข ๐ท = (๐ maDet ๐ ) & โข ๐ธ = ((๐ โ {๐พ}) maDet ๐ ) โ โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐ )) โ ((๐พ(๐(๐ matRRep ๐ )๐)๐พ) โพ ((๐ โ {๐พ}) ร ๐)) = ((๐พ((๐ minMatR1 ๐ )โ๐)๐พ) โพ ((๐ โ {๐พ}) ร ๐))) | ||
Theorem | smadiadetglem2 22395 | Lemma 2 for smadiadetg 22396. (Contributed by AV, 14-Feb-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ โ CRing & โข ๐ท = (๐ maDet ๐ ) & โข ๐ธ = ((๐ โ {๐พ}) maDet ๐ ) & โข ยท = (.rโ๐ ) โ โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐ )) โ ((๐พ(๐(๐ matRRep ๐ )๐)๐พ) โพ ({๐พ} ร ๐)) = ((({๐พ} ร ๐) ร {๐}) โf ยท ((๐พ((๐ minMatR1 ๐ )โ๐)๐พ) โพ ({๐พ} ร ๐)))) | ||
Theorem | smadiadetg 22396 | 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.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ โ CRing & โข ๐ท = (๐ maDet ๐ ) & โข ๐ธ = ((๐ โ {๐พ}) maDet ๐ ) & โข ยท = (.rโ๐ ) โ โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ โ (Baseโ๐ )) โ (๐ทโ(๐พ(๐(๐ matRRep ๐ )๐)๐พ)) = (๐ ยท (๐ธโ(๐พ((๐ subMat ๐ )โ๐)๐พ)))) | ||
Theorem | smadiadetg0 22397 | Lemma for smadiadetr 22398: version of smadiadetg 22396 with all hypotheses defining class variables removed, i.e. all class variables defined in the hypotheses replaced in the theorem by their definition. (Contributed by AV, 15-Feb-2019.) |
โข ๐ โ CRing โ โข ((๐ โ (Baseโ(๐ Mat ๐ )) โง ๐พ โ ๐ โง ๐ โ (Baseโ๐ )) โ ((๐ maDet ๐ )โ(๐พ(๐(๐ matRRep ๐ )๐)๐พ)) = (๐(.rโ๐ )(((๐ โ {๐พ}) maDet ๐ )โ(๐พ((๐ subMat ๐ )โ๐)๐พ)))) | ||
Theorem | smadiadetr 22398 | 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. Closed form of smadiadetg 22396. Special case of the "Laplace expansion", see definition in [Lang] p. 515. (Contributed by AV, 15-Feb-2019.) |
โข (((๐ โ CRing โง ๐ โ (Baseโ(๐ Mat ๐ ))) โง (๐พ โ ๐ โง ๐ โ (Baseโ๐ ))) โ ((๐ maDet ๐ )โ(๐พ(๐(๐ matRRep ๐ )๐)๐พ)) = (๐(.rโ๐ )(((๐ โ {๐พ}) maDet ๐ )โ(๐พ((๐ subMat ๐ )โ๐)๐พ)))) | ||
Theorem | invrvald 22399 | If a matrix multiplied with a given matrix (from the left as well as from the right) results in the identity matrix, this matrix is the inverse (matrix) of the given matrix. (Contributed by Stefan O'Rear, 17-Jul-2018.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข 1 = (1rโ๐ ) & โข ๐ = (Unitโ๐ ) & โข ๐ผ = (invrโ๐ ) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ (๐ ยท ๐) = 1 ) & โข (๐ โ (๐ ยท ๐) = 1 ) โ โข (๐ โ (๐ โ ๐ โง (๐ผโ๐) = ๐)) | ||
Theorem | matinv 22400 | The inverse of a matrix is the adjunct of the matrix multiplied with the inverse of the determinant of the matrix if the determinant is a unit in the underlying ring. Proposition 4.16 in [Lang] p. 518. (Contributed by Stefan O'Rear, 17-Jul-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ฝ = (๐ maAdju ๐ ) & โข ๐ท = (๐ maDet ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐ = (Unitโ๐ด) & โข ๐ = (Unitโ๐ ) & โข ๐ป = (invrโ๐ ) & โข ๐ผ = (invrโ๐ด) & โข โ = ( ยท๐ โ๐ด) โ โข ((๐ โ CRing โง ๐ โ ๐ต โง (๐ทโ๐) โ ๐) โ (๐ โ ๐ โง (๐ผโ๐) = ((๐ปโ(๐ทโ๐)) โ (๐ฝโ๐)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |