![]() |
Metamath
Proof Explorer Theorem List (p. 225 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | scmateALT 22401* | Alternate proof of scmate 22399: An entry of an π x π scalar matrix over the ring π . This prove makes use of scmatmats 22400 but is longer and requires more distinct variables. (Contributed by AV, 19-Dec-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ π = (π ScMat π ) & β’ πΎ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ (((π β Fin β§ π β Ring β§ π β π) β§ (πΌ β π β§ π½ β π)) β βπ β πΎ (πΌππ½) = if(πΌ = π½, π, 0 )) | ||
Theorem | scmatscm 22402* | The multiplication of a matrix with a scalar matrix corresponds to a scalar multiplication. (Contributed by AV, 28-Dec-2019.) |
β’ πΎ = (Baseβπ ) & β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ β = ( Β·π βπ΄) & β’ Γ = (.rβπ΄) & β’ π = (π ScMat π ) β β’ (((π β Fin β§ π β Ring) β§ πΆ β π) β βπ β πΎ βπ β π΅ (πΆ Γ π) = (π β π)) | ||
Theorem | scmatid 22403 | The identity matrix is a scalar matrix. (Contributed by AV, 20-Aug-2019.) (Revised by AV, 18-Dec-2019.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ πΈ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (π ScMat π ) β β’ ((π β Fin β§ π β Ring) β (1rβπ΄) β π) | ||
Theorem | scmatdmat 22404 | A scalar matrix is a diagonal matrix. (Contributed by AV, 20-Aug-2019.) (Revised by AV, 19-Dec-2019.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ πΈ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (π ScMat π ) & β’ π· = (π DMat π ) β β’ ((π β Fin β§ π β Ring) β (π β π β π β π·)) | ||
Theorem | scmataddcl 22405 | The sum of two scalar matrices is a scalar matrix. (Contributed by AV, 25-Dec-2019.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ πΈ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (π ScMat π ) β β’ (((π β Fin β§ π β Ring) β§ (π β π β§ π β π)) β (π(+gβπ΄)π) β π) | ||
Theorem | scmatsubcl 22406 | The difference of two scalar matrices is a scalar matrix. (Contributed by AV, 20-Aug-2019.) (Revised by AV, 19-Dec-2019.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ πΈ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (π ScMat π ) β β’ (((π β Fin β§ π β Ring) β§ (π β π β§ π β π)) β (π(-gβπ΄)π) β π) | ||
Theorem | scmatmulcl 22407 | The product of two scalar matrices is a scalar matrix. (Contributed by AV, 21-Aug-2019.) (Revised by AV, 19-Dec-2019.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ πΈ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (π ScMat π ) β β’ (((π β Fin β§ π β Ring) β§ (π β π β§ π β π)) β (π(.rβπ΄)π) β π) | ||
Theorem | scmatsgrp 22408 | The set of scalar matrices is a subgroup of the matrix group/algebra. (Contributed by AV, 20-Aug-2019.) (Revised by AV, 19-Dec-2019.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ πΈ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (π ScMat π ) β β’ ((π β Fin β§ π β Ring) β π β (SubGrpβπ΄)) | ||
Theorem | scmatsrng 22409 | The set of scalar matrices is a subring of the matrix ring/algebra. (Contributed by AV, 21-Aug-2019.) (Revised by AV, 19-Dec-2019.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ πΈ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (π ScMat π ) β β’ ((π β Fin β§ π β Ring) β π β (SubRingβπ΄)) | ||
Theorem | scmatcrng 22410 | The subring of scalar matrices (over a commutative ring) is a commutative ring. (Contributed by AV, 21-Aug-2019.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ πΈ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (π ScMat π ) & β’ πΆ = (π΄ βΎs π) β β’ ((π β Fin β§ π β CRing) β πΆ β CRing) | ||
Theorem | scmatsgrp1 22411 | The set of scalar matrices is a subgroup of the group/ring of diagonal matrices. (Contributed by AV, 21-Aug-2019.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ πΈ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (π ScMat π ) & β’ π· = (π DMat π ) & β’ πΆ = (π΄ βΎs π·) β β’ ((π β Fin β§ π β Ring) β π β (SubGrpβπΆ)) | ||
Theorem | scmatsrng1 22412 | The set of scalar matrices is a subring of the ring of diagonal matrices. (Contributed by AV, 21-Aug-2019.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) & β’ πΈ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (π ScMat π ) & β’ π· = (π DMat π ) & β’ πΆ = (π΄ βΎs π·) β β’ ((π β Fin β§ π β Ring) β π β (SubRingβπΆ)) | ||
Theorem | smatvscl 22413 | Closure of the scalar multiplication in the ring of scalar matrices. (matvscl 22320 analog.) (Contributed by AV, 24-Dec-2019.) |
β’ πΎ = (Baseβπ ) & β’ π΄ = (π Mat π ) & β’ π = (π ScMat π ) & β’ β = ( Β·π βπ΄) β β’ (((π β Fin β§ π β Ring) β§ (πΆ β πΎ β§ π β π)) β (πΆ β π) β π) | ||
Theorem | scmatlss 22414 | The set of scalar matrices is a linear subspace of the matrix algebra. (Contributed by AV, 25-Dec-2019.) |
β’ π΄ = (π Mat π ) & β’ π = (π ScMat π ) β β’ ((π β Fin β§ π β Ring) β π β (LSubSpβπ΄)) | ||
Theorem | scmatstrbas 22415 | The set of scalar matrices is the base set of the ring of corresponding scalar matrices. (Contributed by AV, 26-Dec-2019.) |
β’ π΄ = (π Mat π ) & β’ πΆ = (π ScMat π ) & β’ π = (π΄ βΎs πΆ) β β’ ((π β Fin β§ π β Ring) β (Baseβπ) = πΆ) | ||
Theorem | scmatrhmval 22416* | The value of the ring homomorphism πΉ. (Contributed by AV, 22-Dec-2019.) |
β’ πΎ = (Baseβπ ) & β’ π΄ = (π Mat π ) & β’ 1 = (1rβπ΄) & β’ β = ( Β·π βπ΄) & β’ πΉ = (π₯ β πΎ β¦ (π₯ β 1 )) β β’ ((π β π β§ π β πΎ) β (πΉβπ) = (π β 1 )) | ||
Theorem | scmatrhmcl 22417* | The value of the ring homomorphism πΉ is a scalar matrix. (Contributed by AV, 22-Dec-2019.) |
β’ πΎ = (Baseβπ ) & β’ π΄ = (π Mat π ) & β’ 1 = (1rβπ΄) & β’ β = ( Β·π βπ΄) & β’ πΉ = (π₯ β πΎ β¦ (π₯ β 1 )) & β’ πΆ = (π ScMat π ) β β’ ((π β Fin β§ π β Ring β§ π β πΎ) β (πΉβπ) β πΆ) | ||
Theorem | scmatf 22418* | There is a function from a ring to any ring of scalar matrices over this ring. (Contributed by AV, 25-Dec-2019.) |
β’ πΎ = (Baseβπ ) & β’ π΄ = (π Mat π ) & β’ 1 = (1rβπ΄) & β’ β = ( Β·π βπ΄) & β’ πΉ = (π₯ β πΎ β¦ (π₯ β 1 )) & β’ πΆ = (π ScMat π ) β β’ ((π β Fin β§ π β Ring) β πΉ:πΎβΆπΆ) | ||
Theorem | scmatfo 22419* | 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 22420* | 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 22421* | 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 22422* | 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 22423* | 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 22424* | 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 22425* | 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 22426 | 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 22427 | The empty matrix over a ring is a scalar matrix (and therefore, by scmatdmat 22404, also a diagonal matrix). (Contributed by AV, 21-Dec-2019.) |
β’ (π β Ring β β β (β ScMat π )) | ||
Theorem | mat1scmat 22428 | A 1-dimensional matrix over a ring is always a scalar matrix (and therefore, by scmatdmat 22404, 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 22273 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 22430 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 21680. See also the statements in [Lang] p. 508. | ||
Syntax | cmvmul 22429 | Syntax for the operator for the multiplication of a vector with a matrix. |
class maVecMul | ||
Definition | df-mvmul 22430* | 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 22431* | Functional value of the matrix vector multiplication operator. (Contributed by AV, 23-Feb-2019.) |
β’ Γ = (π maVecMul β¨π, πβ©) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β π) & β’ (π β π β Fin) & β’ (π β π β Fin) β β’ (π β Γ = (π₯ β (π΅ βm (π Γ π)), π¦ β (π΅ βm π) β¦ (π β π β¦ (π Ξ£g (π β π β¦ ((ππ₯π) Β· (π¦βπ))))))) | ||
Theorem | mvmulval 22432* | Multiplication of a vector with a matrix. (Contributed by AV, 23-Feb-2019.) |
β’ Γ = (π maVecMul β¨π, πβ©) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β π) & β’ (π β π β Fin) & β’ (π β π β Fin) & β’ (π β π β (π΅ βm (π Γ π))) & β’ (π β π β (π΅ βm π)) β β’ (π β (π Γ π) = (π β π β¦ (π Ξ£g (π β π β¦ ((πππ) Β· (πβπ)))))) | ||
Theorem | mvmulfv 22433* | 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 22434* | Multiplication of a vector with a square matrix. (Contributed by AV, 23-Feb-2019.) |
β’ π΄ = (π Mat π ) & β’ Γ = (π maVecMul β¨π, πβ©) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β π) & β’ (π β π β Fin) & β’ (π β π β (Baseβπ΄)) & β’ (π β π β (π΅ βm π)) β β’ (π β (π Γ π) = (π β π β¦ (π Ξ£g (π β π β¦ ((πππ) Β· (πβπ)))))) | ||
Theorem | mavmulfv 22435* | 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 22436 | 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 22437 | 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 22438 | 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 22439 | The domain of the matrix vector multiplication function. (Contributed by AV, 27-Feb-2019.) |
β’ π΅ = (Baseβπ ) & β’ πΆ = (π΅ βm (π Γ π)) & β’ π· = (π΅ βm π) & β’ Β· = (π maVecMul β¨π, πβ©) β β’ ((π β π β§ π β Fin β§ π β Fin) β dom Β· = (πΆ Γ π·)) | ||
Theorem | mavmulsolcl 22440 | 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 22441 | Multiplication of a 0-dimensional matrix with a 0-dimensional vector. (Contributed by AV, 28-Feb-2019.) |
β’ Β· = (π maVecMul β¨π, πβ©) β β’ ((π = β β§ π β π) β (β Β· β ) = β ) | ||
Theorem | mavmul0g 22442 | 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 22443* | 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 22444* | 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 22445 | Syntax for the row replacing function for a square matrix. |
class matRRep | ||
Syntax | cmatrepV 22446 | Syntax for the function replacing a column of a matrix by a vector. |
class matRepV | ||
Definition | df-marrep 22447* | 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 22448* | 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 22449* | 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 22450* | 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 22451* | 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 22452 | 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 22453 | Closure of the row replacement function for square matrices. (Contributed by AV, 13-Feb-2019.) |
β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) β β’ (((π β Ring β§ π β π΅ β§ π β (Baseβπ )) β§ (πΎ β π β§ πΏ β π)) β (πΎ(π(π matRRep π )π)πΏ) β π΅) | ||
Theorem | marepvfval 22454* | 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 22455* | 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 22456* | 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 22457 | 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 22458 | 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 22459 | 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 22460 | 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 22461 | 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 22462* | 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 22463* | 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 22464 | 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 22465 | Syntax for submatrices of a square matrix. |
class subMat | ||
Definition | df-subma 22466* | 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 22467* | 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 22468* | First substitution for a submatrix. (Contributed by AV, 28-Dec-2018.) |
β’ π΄ = (π Mat π ) & β’ π = (π subMat π ) & β’ π΅ = (Baseβπ΄) β β’ π = (π β π΅ β¦ (π β π, π β π β¦ (π β (π β {π}), π β (π β {π}) β¦ (πππ)))) | ||
Theorem | submaval0 22469* | Second substitution for a submatrix. (Contributed by AV, 28-Dec-2018.) |
β’ π΄ = (π Mat π ) & β’ π = (π subMat π ) & β’ π΅ = (Baseβπ΄) β β’ (π β π΅ β (πβπ) = (π β π, π β π β¦ (π β (π β {π}), π β (π β {π}) β¦ (πππ)))) | ||
Theorem | submaval 22470* | Third substitution for a submatrix. (Contributed by AV, 28-Dec-2018.) |
β’ π΄ = (π Mat π ) & β’ π = (π subMat π ) & β’ π΅ = (Baseβπ΄) β β’ ((π β π΅ β§ πΎ β π β§ πΏ β π) β (πΎ(πβπ)πΏ) = (π β (π β {πΎ}), π β (π β {πΏ}) β¦ (πππ))) | ||
Theorem | submaeval 22471 | An entry of a submatrix of a square matrix. (Contributed by AV, 28-Dec-2018.) |
β’ π΄ = (π Mat π ) & β’ π = (π subMat π ) & β’ π΅ = (Baseβπ΄) β β’ ((π β π΅ β§ (πΎ β π β§ πΏ β π) β§ (πΌ β (π β {πΎ}) β§ π½ β (π β {πΏ}))) β (πΌ(πΎ(πβπ)πΏ)π½) = (πΌππ½)) | ||
Theorem | 1marepvsma1 22472 | 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 22473 | Syntax for the matrix determinant function. |
class maDet | ||
Definition | df-mdet 22474* | Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib 22476). 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 22484. Multilineary means "linear for each row" - the additivity is shown by mdetrlin 22491, the homogeneity by mdetrsca 22492. Furthermore, it is shown that the determinant function is alternating (see mdetralt 22497) and normalized (see mdet1 22490). Finally, uniqueness is shown by mdetuni 22511. As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib 22476. (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 22475* | 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 22476* | 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 22477* | 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 22478 | The determinant is not defined for an infinite matrix. (Contributed by AV, 27-Dec-2018.) |
β’ π· = (π maDet π ) β β’ (π β Fin β π· = β ) | ||
Theorem | mdetfval1 22479* | 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 22480* | 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 22481 | 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 22482 | 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 22483 | 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 22484 | 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 22485 | 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 22486 | The determinant of a 1-dimensional matrix equals its (single) entry. (Contributed by AV, 6-Aug-2019.) |
β’ π· = (π maDet π ) & β’ π΄ = (π Mat π ) & β’ π΅ = (Baseβπ΄) β β’ ((π β CRing β§ (π = {πΌ} β§ πΌ β π) β§ π β π΅) β (π·βπ) = (πΌππΌ)) | ||
Theorem | mdetdiaglem 22487* | Lemma for mdetdiag 22488. Previously part of proof for mdet1 22490. (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 22488* | 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 22489* | 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 22490 | 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 22491 | 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 22492 | 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 22493* | 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 22494* | 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 22495 | 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 22496* | 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 22497* | 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 22498* | 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 22499* | 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 22500 | 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 π) = (π·βπ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |