Home | Metamath
Proof Explorer Theorem List (p. 219 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | scmatfo 21801* | There is a function from a ring onto any ring of scalar matrices over this ring. (Contributed by AV, 26-Dec-2019.) |
โข ๐พ = (Baseโ๐ ) & โข ๐ด = (๐ Mat ๐ ) & โข 1 = (1rโ๐ด) & โข โ = ( ยท๐ โ๐ด) & โข ๐น = (๐ฅ โ ๐พ โฆ (๐ฅ โ 1 )) & โข ๐ถ = (๐ ScMat ๐ ) โ โข ((๐ โ Fin โง ๐ โ Ring) โ ๐น:๐พโontoโ๐ถ) | ||
Theorem | scmatf1 21802* | There is a 1-1 function from a ring to any ring of scalar matrices with positive dimension over this ring. (Contributed by AV, 25-Dec-2019.) |
โข ๐พ = (Baseโ๐ ) & โข ๐ด = (๐ Mat ๐ ) & โข 1 = (1rโ๐ด) & โข โ = ( ยท๐ โ๐ด) & โข ๐น = (๐ฅ โ ๐พ โฆ (๐ฅ โ 1 )) & โข ๐ถ = (๐ ScMat ๐ ) โ โข ((๐ โ Fin โง ๐ โ โ โง ๐ โ Ring) โ ๐น:๐พโ1-1โ๐ถ) | ||
Theorem | scmatf1o 21803* | There is a bijection between a ring and any ring of scalar matrices with positive dimension over this ring. (Contributed by AV, 26-Dec-2019.) |
โข ๐พ = (Baseโ๐ ) & โข ๐ด = (๐ Mat ๐ ) & โข 1 = (1rโ๐ด) & โข โ = ( ยท๐ โ๐ด) & โข ๐น = (๐ฅ โ ๐พ โฆ (๐ฅ โ 1 )) & โข ๐ถ = (๐ ScMat ๐ ) โ โข ((๐ โ Fin โง ๐ โ โ โง ๐ โ Ring) โ ๐น:๐พโ1-1-ontoโ๐ถ) | ||
Theorem | scmatghm 21804* | There is a group homomorphism from the additive group of a ring to the additive group of the ring of scalar matrices over this ring. (Contributed by AV, 22-Dec-2019.) |
โข ๐พ = (Baseโ๐ ) & โข ๐ด = (๐ Mat ๐ ) & โข 1 = (1rโ๐ด) & โข โ = ( ยท๐ โ๐ด) & โข ๐น = (๐ฅ โ ๐พ โฆ (๐ฅ โ 1 )) & โข ๐ถ = (๐ ScMat ๐ ) & โข ๐ = (๐ด โพs ๐ถ) โ โข ((๐ โ Fin โง ๐ โ Ring) โ ๐น โ (๐ GrpHom ๐)) | ||
Theorem | scmatmhm 21805* | There is a monoid homomorphism from the multiplicative group of a ring to the multiplicative group of the ring of scalar matrices over this ring. (Contributed by AV, 29-Dec-2019.) |
โข ๐พ = (Baseโ๐ ) & โข ๐ด = (๐ Mat ๐ ) & โข 1 = (1rโ๐ด) & โข โ = ( ยท๐ โ๐ด) & โข ๐น = (๐ฅ โ ๐พ โฆ (๐ฅ โ 1 )) & โข ๐ถ = (๐ ScMat ๐ ) & โข ๐ = (๐ด โพs ๐ถ) & โข ๐ = (mulGrpโ๐ ) & โข ๐ = (mulGrpโ๐) โ โข ((๐ โ Fin โง ๐ โ Ring) โ ๐น โ (๐ MndHom ๐)) | ||
Theorem | scmatrhm 21806* | There is a ring homomorphism from a ring to the ring of scalar matrices over this ring. (Contributed by AV, 29-Dec-2019.) |
โข ๐พ = (Baseโ๐ ) & โข ๐ด = (๐ Mat ๐ ) & โข 1 = (1rโ๐ด) & โข โ = ( ยท๐ โ๐ด) & โข ๐น = (๐ฅ โ ๐พ โฆ (๐ฅ โ 1 )) & โข ๐ถ = (๐ ScMat ๐ ) & โข ๐ = (๐ด โพs ๐ถ) โ โข ((๐ โ Fin โง ๐ โ Ring) โ ๐น โ (๐ RingHom ๐)) | ||
Theorem | scmatrngiso 21807* | There is a ring isomorphism from a ring to the ring of scalar matrices over this ring with positive dimension. (Contributed by AV, 29-Dec-2019.) |
โข ๐พ = (Baseโ๐ ) & โข ๐ด = (๐ Mat ๐ ) & โข 1 = (1rโ๐ด) & โข โ = ( ยท๐ โ๐ด) & โข ๐น = (๐ฅ โ ๐พ โฆ (๐ฅ โ 1 )) & โข ๐ถ = (๐ ScMat ๐ ) & โข ๐ = (๐ด โพs ๐ถ) โ โข ((๐ โ Fin โง ๐ โ โ โง ๐ โ Ring) โ ๐น โ (๐ RingIso ๐)) | ||
Theorem | scmatric 21808 | A ring is isomorphic to every ring of scalar matrices over this ring with positive dimension. (Contributed by AV, 29-Dec-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ถ = (๐ ScMat ๐ ) & โข ๐ = (๐ด โพs ๐ถ) โ โข ((๐ โ Fin โง ๐ โ โ โง ๐ โ Ring) โ ๐ โ๐ ๐) | ||
Theorem | mat0scmat 21809 | The empty matrix over a ring is a scalar matrix (and therefore, by scmatdmat 21786, also a diagonal matrix). (Contributed by AV, 21-Dec-2019.) |
โข (๐ โ Ring โ โ โ (โ ScMat ๐ )) | ||
Theorem | mat1scmat 21810 | A 1-dimensional matrix over a ring is always a scalar matrix (and therefore, by scmatdmat 21786, also a diagonal matrix). (Contributed by AV, 21-Dec-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) โ โข ((๐ โ ๐ โง (โฏโ๐) = 1 โง ๐ โ Ring) โ (๐ โ ๐ต โ ๐ โ (๐ ScMat ๐ ))) | ||
The module of ๐-dimensional "column vectors" over a ring ๐ is the ๐-dimensional free module over a ring ๐, which is the product of ๐ -many copies of the ring with componentwise addition and multiplication. Although a "column vector" could also be defined as n x 1 -matrix (according to Wikipedia "Row and column vectors", 22-Feb-2019, https://en.wikipedia.org/wiki/Row_and_column_vectors: "In linear algebra, a column vector [... ] is an m x 1 matrix, that is, a matrix consisting of a single column of m elements"), which would allow for using the matrix multiplication df-mamu 21655 for multiplying a matrix with a column vector, it seems more natural to use the definition of a free (left) module, avoiding to provide a singleton as 1-dimensional index set for the column, and to introduce a new operator df-mvmul 21812 for the multiplication of a matrix with a column vector. In most cases, it is sufficient to regard members of ((Baseโ๐ ) โm ๐) as "column vectors", because ((Baseโ๐ ) โm ๐) is the base set of (๐ freeLMod ๐), see frlmbasmap 21088. See also the statements in [Lang] p. 508. | ||
Syntax | cmvmul 21811 | Syntax for the operator for the multiplication of a vector with a matrix. |
class maVecMul | ||
Definition | df-mvmul 21812* | The operator which multiplies an M x N -matrix with an N-dimensional vector. (Contributed by AV, 23-Feb-2019.) |
โข maVecMul = (๐ โ V, ๐ โ V โฆ โฆ(1st โ๐) / ๐โฆโฆ(2nd โ๐) / ๐โฆ(๐ฅ โ ((Baseโ๐) โm (๐ ร ๐)), ๐ฆ โ ((Baseโ๐) โm ๐) โฆ (๐ โ ๐ โฆ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐ฆโ๐))))))) | ||
Theorem | mvmulfval 21813* | Functional value of the matrix vector multiplication operator. (Contributed by AV, 23-Feb-2019.) |
โข ร = (๐ maVecMul โจ๐, ๐โฉ) & โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ Fin) โ โข (๐ โ ร = (๐ฅ โ (๐ต โm (๐ ร ๐)), ๐ฆ โ (๐ต โm ๐) โฆ (๐ โ ๐ โฆ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐) ยท (๐ฆโ๐))))))) | ||
Theorem | mvmulval 21814* | Multiplication of a vector with a matrix. (Contributed by AV, 23-Feb-2019.) |
โข ร = (๐ maVecMul โจ๐, ๐โฉ) & โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ (๐ต โm (๐ ร ๐))) & โข (๐ โ ๐ โ (๐ต โm ๐)) โ โข (๐ โ (๐ ร ๐) = (๐ โ ๐ โฆ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐๐) ยท (๐โ๐)))))) | ||
Theorem | mvmulfv 21815* | A cell/element in the vector resulting from a multiplication of a vector with a matrix. (Contributed by AV, 23-Feb-2019.) |
โข ร = (๐ maVecMul โจ๐, ๐โฉ) & โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ (๐ต โm (๐ ร ๐))) & โข (๐ โ ๐ โ (๐ต โm ๐)) & โข (๐ โ ๐ผ โ ๐) โ โข (๐ โ ((๐ ร ๐)โ๐ผ) = (๐ ฮฃg (๐ โ ๐ โฆ ((๐ผ๐๐) ยท (๐โ๐))))) | ||
Theorem | mavmulval 21816* | Multiplication of a vector with a square matrix. (Contributed by AV, 23-Feb-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ร = (๐ maVecMul โจ๐, ๐โฉ) & โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ (Baseโ๐ด)) & โข (๐ โ ๐ โ (๐ต โm ๐)) โ โข (๐ โ (๐ ร ๐) = (๐ โ ๐ โฆ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐๐) ยท (๐โ๐)))))) | ||
Theorem | mavmulfv 21817* | A cell/element in the vector resulting from a multiplication of a vector with a square matrix. (Contributed by AV, 6-Dec-2018.) (Revised by AV, 18-Feb-2019.) (Revised by AV, 23-Feb-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ร = (๐ maVecMul โจ๐, ๐โฉ) & โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ (Baseโ๐ด)) & โข (๐ โ ๐ โ (๐ต โm ๐)) & โข (๐ โ ๐ผ โ ๐) โ โข (๐ โ ((๐ ร ๐)โ๐ผ) = (๐ ฮฃg (๐ โ ๐ โฆ ((๐ผ๐๐) ยท (๐โ๐))))) | ||
Theorem | mavmulcl 21818 | Multiplication of an NxN matrix with an N-dimensional vector results in an N-dimensional vector. (Contributed by AV, 6-Dec-2018.) (Revised by AV, 23-Feb-2019.) (Proof shortened by AV, 23-Jul-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ร = (๐ maVecMul โจ๐, ๐โฉ) & โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ (Baseโ๐ด)) & โข (๐ โ ๐ โ (๐ต โm ๐)) โ โข (๐ โ (๐ ร ๐) โ (๐ต โm ๐)) | ||
Theorem | 1mavmul 21819 | Multiplication of the identity NxN matrix with an N-dimensional vector results in the vector itself. (Contributed by AV, 9-Feb-2019.) (Revised by AV, 23-Feb-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ ) & โข ยท = (๐ maVecMul โจ๐, ๐โฉ) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ (๐ต โm ๐)) โ โข (๐ โ ((1rโ๐ด) ยท ๐) = ๐) | ||
Theorem | mavmulass 21820 | Associativity of the multiplication of two NxN matrices with an N-dimensional vector. (Contributed by AV, 9-Feb-2019.) (Revised by AV, 25-Feb-2019.) (Proof shortened by AV, 22-Jul-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ ) & โข ยท = (๐ maVecMul โจ๐, ๐โฉ) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ (๐ต โm ๐)) & โข ร = (๐ maMul โจ๐, ๐, ๐โฉ) & โข (๐ โ ๐ โ (Baseโ๐ด)) & โข (๐ โ ๐ โ (Baseโ๐ด)) โ โข (๐ โ ((๐ ร ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) | ||
Theorem | mavmuldm 21821 | The domain of the matrix vector multiplication function. (Contributed by AV, 27-Feb-2019.) |
โข ๐ต = (Baseโ๐ ) & โข ๐ถ = (๐ต โm (๐ ร ๐)) & โข ๐ท = (๐ต โm ๐) & โข ยท = (๐ maVecMul โจ๐, ๐โฉ) โ โข ((๐ โ ๐ โง ๐ โ Fin โง ๐ โ Fin) โ dom ยท = (๐ถ ร ๐ท)) | ||
Theorem | mavmulsolcl 21822 | Every solution of the equation ๐ดโ๐ = ๐ for a matrix ๐ด and a vector ๐ต is a vector. (Contributed by AV, 27-Feb-2019.) |
โข ๐ต = (Baseโ๐ ) & โข ๐ถ = (๐ต โm (๐ ร ๐)) & โข ๐ท = (๐ต โm ๐) & โข ยท = (๐ maVecMul โจ๐, ๐โฉ) & โข ๐ธ = (๐ต โm ๐) โ โข (((๐ โ Fin โง ๐ โ Fin โง ๐ โ โ ) โง (๐ โ ๐ โง ๐ โ ๐ธ)) โ ((๐ด ยท ๐) = ๐ โ ๐ โ ๐ท)) | ||
Theorem | mavmul0 21823 | Multiplication of a 0-dimensional matrix with a 0-dimensional vector. (Contributed by AV, 28-Feb-2019.) |
โข ยท = (๐ maVecMul โจ๐, ๐โฉ) โ โข ((๐ = โ โง ๐ โ ๐) โ (โ ยท โ ) = โ ) | ||
Theorem | mavmul0g 21824 | The result of the 0-dimensional multiplication of a matrix with a vector is always the empty set. (Contributed by AV, 1-Mar-2019.) |
โข ยท = (๐ maVecMul โจ๐, ๐โฉ) โ โข ((๐ = โ โง ๐ โ ๐) โ (๐ ยท ๐) = โ ) | ||
Theorem | mvmumamul1 21825* | 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 21826* | 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 (๐ ร {โ }))) โ โข (๐ โ (โ๐ โ ๐ (๐โ๐) = (๐๐โ ) โ โ๐ โ ๐ ((๐ ยท ๐)โ๐) = (๐(๐ ร ๐)โ ))) | ||
Syntax | cmarrep 21827 | Syntax for the row replacing function for a square matrix. |
class matRRep | ||
Syntax | cmatrepV 21828 | Syntax for the function replacing a column of a matrix by a vector. |
class matRepV | ||
Definition | df-marrep 21829* | 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 21830* | 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 21831* | 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 21832* | 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 21833* | 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 21834 | 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 21835 | Closure of the row replacement function for square matrices. (Contributed by AV, 13-Feb-2019.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) โ โข (((๐ โ Ring โง ๐ โ ๐ต โง ๐ โ (Baseโ๐ )) โง (๐พ โ ๐ โง ๐ฟ โ ๐)) โ (๐พ(๐(๐ matRRep ๐ )๐)๐ฟ) โ ๐ต) | ||
Theorem | marepvfval 21836* | 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 21837* | 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 21838* | 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 21839 | 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 21840 | 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 21841 | 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 21842 | 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 21843 | 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 21844* | 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 21845* | 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 21846 | 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 ๐ )(๐โ๐ผ))๐ผ) = ๐) | ||
Syntax | csubma 21847 | Syntax for submatrices of a square matrix. |
class subMat | ||
Definition | df-subma 21848* | 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 21849* | 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 21850* | First substitution for a submatrix. (Contributed by AV, 28-Dec-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ = (๐ subMat ๐ ) & โข ๐ต = (Baseโ๐ด) โ โข ๐ = (๐ โ ๐ต โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ โ (๐ โ {๐}), ๐ โ (๐ โ {๐}) โฆ (๐๐๐)))) | ||
Theorem | submaval0 21851* | Second substitution for a submatrix. (Contributed by AV, 28-Dec-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ = (๐ subMat ๐ ) & โข ๐ต = (Baseโ๐ด) โ โข (๐ โ ๐ต โ (๐โ๐) = (๐ โ ๐, ๐ โ ๐ โฆ (๐ โ (๐ โ {๐}), ๐ โ (๐ โ {๐}) โฆ (๐๐๐)))) | ||
Theorem | submaval 21852* | Third substitution for a submatrix. (Contributed by AV, 28-Dec-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ = (๐ subMat ๐ ) & โข ๐ต = (Baseโ๐ด) โ โข ((๐ โ ๐ต โง ๐พ โ ๐ โง ๐ฟ โ ๐) โ (๐พ(๐โ๐)๐ฟ) = (๐ โ (๐ โ {๐พ}), ๐ โ (๐ โ {๐ฟ}) โฆ (๐๐๐))) | ||
Theorem | submaeval 21853 | An entry of a submatrix of a square matrix. (Contributed by AV, 28-Dec-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ = (๐ subMat ๐ ) & โข ๐ต = (Baseโ๐ด) โ โข ((๐ โ ๐ต โง (๐พ โ ๐ โง ๐ฟ โ ๐) โง (๐ผ โ (๐ โ {๐พ}) โง ๐ฝ โ (๐ โ {๐ฟ}))) โ (๐ผ(๐พ(๐โ๐)๐ฟ)๐ฝ) = (๐ผ๐๐ฝ)) | ||
Theorem | 1marepvsma1 21854 | 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 21855 | Syntax for the matrix determinant function. |
class maDet | ||
Definition | df-mdet 21856* | Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib 21858). 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 21866. Multilineary means "linear for each row" - the additivity is shown by mdetrlin 21873, the homogeneity by mdetrsca 21874. Furthermore, it is shown that the determinant function is alternating (see mdetralt 21879) and normalized (see mdet1 21872). Finally, uniqueness is shown by mdetuni 21893. As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib 21858. (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 21857* | 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 21858* | 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 21859* | 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 21860 | The determinant is not defined for an infinite matrix. (Contributed by AV, 27-Dec-2018.) |
โข ๐ท = (๐ maDet ๐ ) โ โข (๐ โ Fin โ ๐ท = โ ) | ||
Theorem | mdetfval1 21861* | 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 21862* | 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 21863 | 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 21864 | 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 21865 | 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 21866 | 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 21867 | 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 21868 | The determinant of a 1-dimensional matrix equals its (single) entry. (Contributed by AV, 6-Aug-2019.) |
โข ๐ท = (๐ maDet ๐ ) & โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) โ โข ((๐ โ CRing โง (๐ = {๐ผ} โง ๐ผ โ ๐) โง ๐ โ ๐ต) โ (๐ทโ๐) = (๐ผ๐๐ผ)) | ||
Theorem | mdetdiaglem 21869* | Lemma for mdetdiag 21870. Previously part of proof for mdet1 21872. (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 21870* | 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 21871* | 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 21872 | 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 21873 | 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 21874 | 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 21875* | 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 21876* | 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 21877 | 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 21878* | 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 21879* | 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 21880* | 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 21881* | 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 21882 | 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 21883* | Lemma for mdetuni 21893. (Contributed by SO, 14-Jul-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐พ = (Baseโ๐ ) & โข 0 = (0gโ๐ ) & โข 1 = (1rโ๐ ) & โข + = (+gโ๐ ) & โข ยท = (.rโ๐ ) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ท:๐ตโถ๐พ) & โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฆ โ ๐ง โง โ๐ค โ ๐ (๐ฆ๐ฅ๐ค) = (๐ง๐ฅ๐ค)) โ (๐ทโ๐ฅ) = 0 )) & โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ฅ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = ((๐ทโ๐ฆ) + (๐ทโ๐ง)))) & โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐พ โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ฅ โพ ({๐ค} ร ๐)) = ((({๐ค} ร ๐) ร {๐ฆ}) โf ยท (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = (๐ฆ ยท (๐ทโ๐ง)))) โ โข (((๐ โง ๐ธ โ ๐ต โง โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐บ๐ธ๐ค)) โง (๐น โ ๐ โง ๐บ โ ๐ โง ๐น โ ๐บ)) โ (๐ทโ๐ธ) = 0 ) | ||
Theorem | mdetunilem2 21884* | Lemma for mdetuni 21893. (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 21885* | Lemma for mdetuni 21893. (Contributed by SO, 15-Jul-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐พ = (Baseโ๐ ) & โข 0 = (0gโ๐ ) & โข 1 = (1rโ๐ ) & โข + = (+gโ๐ ) & โข ยท = (.rโ๐ ) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ท:๐ตโถ๐พ) & โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฆ โ ๐ง โง โ๐ค โ ๐ (๐ฆ๐ฅ๐ค) = (๐ง๐ฅ๐ค)) โ (๐ทโ๐ฅ) = 0 )) & โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ฅ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = ((๐ทโ๐ฆ) + (๐ทโ๐ง)))) & โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐พ โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ฅ โพ ({๐ค} ร ๐)) = ((({๐ค} ร ๐) ร {๐ฆ}) โf ยท (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = (๐ฆ ยท (๐ทโ๐ง)))) โ โข (((๐ โง ๐ธ โ ๐ต โง ๐น โ ๐ต) โง (๐บ โ ๐ต โง ๐ป โ ๐ โง (๐ธ โพ ({๐ป} ร ๐)) = ((๐น โพ ({๐ป} ร ๐)) โf + (๐บ โพ ({๐ป} ร ๐)))) โง ((๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐น โพ ((๐ โ {๐ป}) ร ๐)) โง (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐บ โพ ((๐ โ {๐ป}) ร ๐)))) โ (๐ทโ๐ธ) = ((๐ทโ๐น) + (๐ทโ๐บ))) | ||
Theorem | mdetunilem4 21886* | Lemma for mdetuni 21893. (Contributed by SO, 15-Jul-2018.) |
โข ๐ด = (๐ Mat ๐ ) & โข ๐ต = (Baseโ๐ด) & โข ๐พ = (Baseโ๐ ) & โข 0 = (0gโ๐ ) & โข 1 = (1rโ๐ ) & โข + = (+gโ๐ ) & โข ยท = (.rโ๐ ) & โข (๐ โ ๐ โ Fin) & โข (๐ โ ๐ โ Ring) & โข (๐ โ ๐ท:๐ตโถ๐พ) & โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฆ โ ๐ง โง โ๐ค โ ๐ (๐ฆ๐ฅ๐ค) = (๐ง๐ฅ๐ค)) โ (๐ทโ๐ฅ) = 0 )) & โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ฅ โพ ({๐ค} ร ๐)) = ((๐ฆ โพ ({๐ค} ร ๐)) โf + (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ฆ โพ ((๐ โ {๐ค}) ร ๐)) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = ((๐ทโ๐ฆ) + (๐ทโ๐ง)))) & โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐พ โ๐ง โ ๐ต โ๐ค โ ๐ (((๐ฅ โพ ({๐ค} ร ๐)) = ((({๐ค} ร ๐) ร {๐ฆ}) โf ยท (๐ง โพ ({๐ค} ร ๐))) โง (๐ฅ โพ ((๐ โ {๐ค}) ร ๐)) = (๐ง โพ ((๐ โ {๐ค}) ร ๐))) โ (๐ทโ๐ฅ) = (๐ฆ ยท (๐ทโ๐ง)))) โ โข ((๐ โง (๐ธ โ ๐ต โง ๐น โ ๐พ โง ๐บ โ ๐ต) โง (๐ป โ ๐ โง (๐ธ โพ ({๐ป} ร ๐)) = ((({๐ป} ร ๐) ร {๐น}) โf ยท (๐บ โพ ({๐ป} ร ๐))) โง (๐ธ โพ ((๐ โ {๐ป}) ร ๐)) = (๐บ โพ ((๐ โ {๐ป}) ร ๐)))) โ (๐ทโ๐ธ) = (๐น ยท (๐ทโ๐บ))) | ||
Theorem | mdetunilem5 21887* | Lemma for mdetuni 21893. (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 21888* | Lemma for mdetuni 21893. (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 21889* | Lemma for mdetuni 21893. (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 21890* | Lemma for mdetuni 21893. (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 21891* | Lemma for mdetuni 21893. (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 21892* | Lemma for mdetuni 21893. (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 21893* | 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 21894 | 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 21895 | Lemma 1 for m2detleib 21902. (Contributed by AV, 12-Dec-2018.) |
โข ๐ = {1, 2} & โข ๐ = (Baseโ(SymGrpโ๐)) & โข ๐ = (โคRHomโ๐ ) & โข ๐ = (pmSgnโ๐) & โข 1 = (1rโ๐ ) โ โข ((๐ โ Ring โง ๐ โ ๐) โ (๐โ(๐โ๐)) = (((pmSgnโ๐)โ๐)(.gโ๐ ) 1 )) | ||
Theorem | m2detleiblem5 21896 | Lemma 5 for m2detleib 21902. (Contributed by AV, 20-Dec-2018.) |
โข ๐ = {1, 2} & โข ๐ = (Baseโ(SymGrpโ๐)) & โข ๐ = (โคRHomโ๐ ) & โข ๐ = (pmSgnโ๐) & โข 1 = (1rโ๐ ) โ โข ((๐ โ Ring โง ๐ = {โจ1, 1โฉ, โจ2, 2โฉ}) โ (๐โ(๐โ๐)) = 1 ) | ||
Theorem | m2detleiblem6 21897 | Lemma 6 for m2detleib 21902. (Contributed by AV, 20-Dec-2018.) |
โข ๐ = {1, 2} & โข ๐ = (Baseโ(SymGrpโ๐)) & โข ๐ = (โคRHomโ๐ ) & โข ๐ = (pmSgnโ๐) & โข 1 = (1rโ๐ ) & โข ๐ผ = (invgโ๐ ) โ โข ((๐ โ Ring โง ๐ = {โจ1, 2โฉ, โจ2, 1โฉ}) โ (๐โ(๐โ๐)) = (๐ผโ 1 )) | ||
Theorem | m2detleiblem7 21898 | Lemma 7 for m2detleib 21902. (Contributed by AV, 20-Dec-2018.) |
โข ๐ = {1, 2} & โข ๐ = (Baseโ(SymGrpโ๐)) & โข ๐ = (โคRHomโ๐ ) & โข ๐ = (pmSgnโ๐) & โข 1 = (1rโ๐ ) & โข ๐ผ = (invgโ๐ ) & โข ยท = (.rโ๐ ) & โข โ = (-gโ๐ ) โ โข ((๐ โ Ring โง ๐ โ (Baseโ๐ ) โง ๐ โ (Baseโ๐ )) โ (๐(+gโ๐ )((๐ผโ 1 ) ยท ๐)) = (๐ โ ๐)) | ||
Theorem | m2detleiblem2 21899* | Lemma 2 for m2detleib 21902. (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 21900* | Lemma 3 for m2detleib 21902. (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))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |