P. 205 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20401-20500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mdetf 20401	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.)
|- D = ( N maDet R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- K = ( Base ` R )   =>    |- ( R e. CRing -> D : B --> K )
Theorem	mdetcl 20402	The determinant evaluates to an element of the base ring. (Contributed by Stefan O'Rear, 9-Sep-2015.) (Revised by AV, 7-Feb-2019.)
|- D = ( N maDet R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- K = ( Base ` R )   =>    |- ( ( R e. CRing /\ M e. B ) -> ( D ` M ) e. K )
Theorem	m1detdiag 20403	The determinant of a 1-dimensional matrix equals its (single) entry. (Contributed by AV, 6-Aug-2019.)
|- D = ( N maDet R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   =>    |- ( ( R e. CRing /\ ( N = { I } /\ I e. V ) /\ M e. B ) -> ( D ` M ) = ( I M I ) )
Theorem	mdetdiaglem 20404*	Lemma for mdetdiag 20405. Previously part of proof for mdet1 20407. (Contributed by SO, 10-Jul-2018.) (Revised by AV, 17-Aug-2019.)
|- D = ( N maDet R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- G = (mulGrp ` R )   &    |- .0. = ( 0g ` R )   &    |- H = ( Base ` ( SymGrp ` N ) )   &    |- Z = ( ZRHom ` R )   &    |- S = (pmSgn ` N )   &    |- .x. = ( .r ` R )   =>    |- ( ( ( R e. CRing /\ N e. Fin /\ M e. B ) /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) /\ ( P e. H /\ P =/= ( _I |` N ) ) ) -> ( ( ( Z o. S ) ` P ) .x. ( G gsumg ( k e. N |-> ( ( P ` k ) M k ) ) ) ) = .0. )
Theorem	mdetdiag 20405*	The determinant of a diagonal matrix is the product of the entries in the diagonal. (Contributed by AV, 17-Aug-2019.)
|- D = ( N maDet R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- G = (mulGrp ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. CRing /\ N e. Fin /\ M e. B ) -> ( A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) -> ( D ` M ) = ( G gsumg ( k e. N |-> ( k M k ) ) ) ) )
Theorem	mdetdiagid 20406*	The determinant of a diagonal matrix with identical entries is the power of the entry in the diagonal. (Contributed by AV, 17-Aug-2019.)
|- D = ( N maDet R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- G = (mulGrp ` R )   &    |- .0. = ( 0g ` R )   &    |- C = ( Base ` R )   &    |- .x. = (.g ` G )   =>    |- ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ X e. C ) ) -> ( A. i e. N A. j e. N ( i M j ) = if ( i = j , X , .0. ) -> ( D ` M ) = ( ( # ` N ) .x. X ) ) )
Theorem	mdet1 20407	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.)
|- D = ( N maDet R )   &    |- A = ( N Mat R )   &    |- I = ( 1r ` A )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. CRing /\ N e. Fin ) -> ( D ` I ) = .1. )
Theorem	mdetrlin 20408	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.)
|- D = ( N maDet R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- .+ = ( +g ` R )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- ( ph -> I e. N )   &    |- ( ph -> ( X |` ( { I } X. N ) ) = ( ( Y |` ( { I } X. N ) ) oF .+ ( Z |` ( { I } X. N ) ) ) )   &    |- ( ph -> ( X |` ( ( N \ { I } ) X. N ) ) = ( Y |` ( ( N \ { I } ) X. N ) ) )   &    |- ( ph -> ( X |` ( ( N \ { I } ) X. N ) ) = ( Z |` ( ( N \ { I } ) X. N ) ) )   =>    |- ( ph -> ( D ` X ) = ( ( D ` Y ) .+ ( D ` Z ) ) )
Theorem	mdetrsca 20409	The determinant function is homogeneous for each row: The matrices X and Z are identical except for the I's row, and the I's row of the matrix X is the componentwise product of the I's row of the matrix Z and the scalar Y. In this case the determinant of X is the determinant of Z multiplied by Y. (Contributed by SO, 9-Jul-2018.) (Proof shortened by AV, 23-Jul-2019.)
|- D = ( N maDet R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- K = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. K )   &    |- ( ph -> Z e. B )   &    |- ( ph -> I e. N )   &    |- ( ph -> ( X |` ( { I } X. N ) ) = ( ( ( { I } X. N ) X. { Y } ) oF .x. ( Z |` ( { I } X. N ) ) ) )   &    |- ( ph -> ( X |` ( ( N \ { I } ) X. N ) ) = ( Z |` ( ( N \ { I } ) X. N ) ) )   =>    |- ( ph -> ( D ` X ) = ( Y .x. ( D ` Z ) ) )
Theorem	mdetrsca2 20410*	The determinant function is homogeneous for each row (matrices are given explicitly by their entries). (Contributed by SO, 16-Jul-2018.)
|- D = ( N maDet R )   &    |- K = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> N e. Fin )   &    |- ( ( ph /\ i e. N /\ j e. N ) -> X e. K )   &    |- ( ( ph /\ i e. N /\ j e. N ) -> Y e. K )   &    |- ( ph -> F e. K )   &    |- ( ph -> I e. N )   =>    |- ( ph -> ( D ` ( i e. N , j e. N |-> if ( i = I , ( F .x. X ) , Y ) ) ) = ( F .x. ( D ` ( i e. N , j e. N |-> if ( i = I , X , Y ) ) ) ) )
Theorem	mdetr0 20411*	The determinant of a matrix with a row containing only 0's is 0. (Contributed by SO, 16-Jul-2018.)
|- D = ( N maDet R )   &    |- K = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> N e. Fin )   &    |- ( ( ph /\ i e. N /\ j e. N ) -> X e. K )   &    |- ( ph -> I e. N )   =>    |- ( ph -> ( D ` ( i e. N , j e. N |-> if ( i = I , .0. , X ) ) ) = .0. )
Theorem	mdet0 20412	The determinant of the zero matrix (of dimension greater 0!) is 0. (Contributed by AV, 17-Aug-2019.)
|- D = ( N maDet R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- Z = ( 0g ` A )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. CRing /\ N e. Fin /\ N =/= (/) ) -> ( D ` Z ) = .0. )
Theorem	mdetrlin2 20413*	The determinant function is additive for each row (matrices are given explicitly by their entries). (Contributed by SO, 16-Jul-2018.)
|- D = ( N maDet R )   &    |- K = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> N e. Fin )   &    |- ( ( ph /\ i e. N /\ j e. N ) -> X e. K )   &    |- ( ( ph /\ i e. N /\ j e. N ) -> Y e. K )   &    |- ( ( ph /\ i e. N /\ j e. N ) -> Z e. K )   &    |- ( ph -> I e. N )   =>    |- ( ph -> ( D ` ( i e. N , j e. N |-> if ( i = I , ( X .+ Y ) , Z ) ) ) = ( ( D ` ( i e. N , j e. N |-> if ( i = I , X , Z ) ) ) .+ ( D ` ( i e. N , j e. N |-> if ( i = I , Y , Z ) ) ) ) )
Theorem	mdetralt 20414*	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.)
|- D = ( N maDet R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- .0. = ( 0g ` R )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> X e. B )   &    |- ( ph -> I e. N )   &    |- ( ph -> J e. N )   &    |- ( ph -> I =/= J )   &    |- ( ph -> A. a e. N ( I X a ) = ( J X a ) )   =>    |- ( ph -> ( D ` X ) = .0. )
Theorem	mdetralt2 20415*	The determinant function is alternating regarding rows (matrix is given explicitly by its entries). (Contributed by SO, 16-Jul-2018.)
|- D = ( N maDet R )   &    |- K = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> N e. Fin )   &    |- ( ( ph /\ j e. N ) -> X e. K )   &    |- ( ( ph /\ i e. N /\ j e. N ) -> Y e. K )   &    |- ( ph -> I e. N )   &    |- ( ph -> J e. N )   &    |- ( ph -> I =/= J )   =>    |- ( ph -> ( D ` ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , X , Y ) ) ) ) = .0. )
Theorem	mdetero 20416*	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.)
|- D = ( N maDet R )   &    |- K = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> N e. Fin )   &    |- ( ( ph /\ j e. N ) -> X e. K )   &    |- ( ( ph /\ j e. N ) -> Y e. K )   &    |- ( ( ph /\ i e. N /\ j e. N ) -> Z e. K )   &    |- ( ph -> W e. K )   &    |- ( ph -> I e. N )   &    |- ( ph -> J e. N )   &    |- ( ph -> I =/= J )   =>    |- ( ph -> ( D ` ( i e. N , j e. N |-> if ( i = I , ( X .+ ( W .x. Y ) ) , if ( i = J , Y , Z ) ) ) ) = ( D ` ( i e. N , j e. N |-> if ( i = I , X , if ( i = J , Y , Z ) ) ) ) )
Theorem	mdettpos 20417	Determinant is invariant under transposition. Proposition 4.8 in [Lang] p. 514. (Contributed by Stefan O'Rear, 9-Jul-2018.)
|- D = ( N maDet R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   =>    |- ( ( R e. CRing /\ M e. B ) -> ( D ` tpos M ) = ( D ` M ) )
Theorem	mdetunilem1 20418*	Lemma for mdetuni 20428. (Contributed by SO, 14-Jul-2018.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- K = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> D : B --> K )   &    |- ( ph -> A. x e. B A. y e. N A. z e. N ( ( y =/= z /\ A. w e. N ( y x w ) = ( z x w ) ) -> ( D ` x ) = .0. ) )   &    |- ( ph -> A. x e. B A. y e. B A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) ) )   &    |- ( ph -> A. x e. B A. y e. K A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( y .x. ( D ` z ) ) ) )   =>    |- ( ( ( ph /\ E e. B /\ A. w e. N ( F E w ) = ( G E w ) ) /\ ( F e. N /\ G e. N /\ F =/= G ) ) -> ( D ` E ) = .0. )
Theorem	mdetunilem2 20419*	Lemma for mdetuni 20428. (Contributed by SO, 15-Jul-2018.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- K = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> D : B --> K )   &    |- ( ph -> A. x e. B A. y e. N A. z e. N ( ( y =/= z /\ A. w e. N ( y x w ) = ( z x w ) ) -> ( D ` x ) = .0. ) )   &    |- ( ph -> A. x e. B A. y e. B A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) ) )   &    |- ( ph -> A. x e. B A. y e. K A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( y .x. ( D ` z ) ) ) )   &    |- ( ps -> ph )   &    |- ( ps -> ( E e. N /\ G e. N /\ E =/= G ) )   &    |- ( ( ps /\ b e. N ) -> F e. K )   &    |- ( ( ps /\ a e. N /\ b e. N ) -> H e. K )   =>    |- ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = E , F , if ( a = G , F , H ) ) ) ) = .0. )
Theorem	mdetunilem3 20420*	Lemma for mdetuni 20428. (Contributed by SO, 15-Jul-2018.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- K = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> D : B --> K )   &    |- ( ph -> A. x e. B A. y e. N A. z e. N ( ( y =/= z /\ A. w e. N ( y x w ) = ( z x w ) ) -> ( D ` x ) = .0. ) )   &    |- ( ph -> A. x e. B A. y e. B A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) ) )   &    |- ( ph -> A. x e. B A. y e. K A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( y .x. ( D ` z ) ) ) )   =>    |- ( ( ( ph /\ E e. B /\ F e. B ) /\ ( G e. B /\ H e. N /\ ( E |` ( { H } X. N ) ) = ( ( F |` ( { H } X. N ) ) oF .+ ( G |` ( { H } X. N ) ) ) ) /\ ( ( E |` ( ( N \ { H } ) X. N ) ) = ( F |` ( ( N \ { H } ) X. N ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) ) -> ( D ` E ) = ( ( D ` F ) .+ ( D ` G ) ) )
Theorem	mdetunilem4 20421*	Lemma for mdetuni 20428. (Contributed by SO, 15-Jul-2018.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- K = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> D : B --> K )   &    |- ( ph -> A. x e. B A. y e. N A. z e. N ( ( y =/= z /\ A. w e. N ( y x w ) = ( z x w ) ) -> ( D ` x ) = .0. ) )   &    |- ( ph -> A. x e. B A. y e. B A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) ) )   &    |- ( ph -> A. x e. B A. y e. K A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( y .x. ( D ` z ) ) ) )   =>    |- ( ( ph /\ ( E e. B /\ F e. K /\ G e. B ) /\ ( H e. N /\ ( E |` ( { H } X. N ) ) = ( ( ( { H } X. N ) X. { F } ) oF .x. ( G |` ( { H } X. N ) ) ) /\ ( E |` ( ( N \ { H } ) X. N ) ) = ( G |` ( ( N \ { H } ) X. N ) ) ) ) -> ( D ` E ) = ( F .x. ( D ` G ) ) )
Theorem	mdetunilem5 20422*	Lemma for mdetuni 20428. (Contributed by SO, 15-Jul-2018.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- K = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> D : B --> K )   &    |- ( ph -> A. x e. B A. y e. N A. z e. N ( ( y =/= z /\ A. w e. N ( y x w ) = ( z x w ) ) -> ( D ` x ) = .0. ) )   &    |- ( ph -> A. x e. B A. y e. B A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) ) )   &    |- ( ph -> A. x e. B A. y e. K A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( y .x. ( D ` z ) ) ) )   &    |- ( ps -> ph )   &    |- ( ps -> E e. N )   &    |- ( ( ps /\ a e. N /\ b e. N ) -> ( F e. K /\ G e. K /\ H e. K ) )   =>    |- ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = E , ( F .+ G ) , H ) ) ) = ( ( D ` ( a e. N , b e. N |-> if ( a = E , F , H ) ) ) .+ ( D ` ( a e. N , b e. N |-> if ( a = E , G , H ) ) ) ) )
Theorem	mdetunilem6 20423*	Lemma for mdetuni 20428. (Contributed by SO, 15-Jul-2018.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- K = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> D : B --> K )   &    |- ( ph -> A. x e. B A. y e. N A. z e. N ( ( y =/= z /\ A. w e. N ( y x w ) = ( z x w ) ) -> ( D ` x ) = .0. ) )   &    |- ( ph -> A. x e. B A. y e. B A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) ) )   &    |- ( ph -> A. x e. B A. y e. K A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( y .x. ( D ` z ) ) ) )   &    |- ( ps -> ph )   &    |- ( ps -> ( E e. N /\ F e. N /\ E =/= F ) )   &    |- ( ( ps /\ b e. N ) -> ( G e. K /\ H e. K ) )   &    |- ( ( ps /\ a e. N /\ b e. N ) -> I e. K )   =>    |- ( ps -> ( D ` ( a e. N , b e. N |-> if ( a = E , G , if ( a = F , H , I ) ) ) ) = ( ( invg ` R ) ` ( D ` ( a e. N , b e. N |-> if ( a = E , H , if ( a = F , G , I ) ) ) ) ) )
Theorem	mdetunilem7 20424*	Lemma for mdetuni 20428. (Contributed by SO, 15-Jul-2018.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- K = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> D : B --> K )   &    |- ( ph -> A. x e. B A. y e. N A. z e. N ( ( y =/= z /\ A. w e. N ( y x w ) = ( z x w ) ) -> ( D ` x ) = .0. ) )   &    |- ( ph -> A. x e. B A. y e. B A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) ) )   &    |- ( ph -> A. x e. B A. y e. K A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( y .x. ( D ` z ) ) ) )   =>    |- ( ( ph /\ E : N -1-1-onto-> N /\ F e. B ) -> ( D ` ( a e. N , b e. N |-> ( ( E ` a ) F b ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` N ) ) ` E ) .x. ( D ` F ) ) )
Theorem	mdetunilem8 20425*	Lemma for mdetuni 20428. (Contributed by SO, 15-Jul-2018.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- K = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> D : B --> K )   &    |- ( ph -> A. x e. B A. y e. N A. z e. N ( ( y =/= z /\ A. w e. N ( y x w ) = ( z x w ) ) -> ( D ` x ) = .0. ) )   &    |- ( ph -> A. x e. B A. y e. B A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) ) )   &    |- ( ph -> A. x e. B A. y e. K A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( y .x. ( D ` z ) ) ) )   &    |- ( ph -> ( D ` ( 1r ` A ) ) = .0. )   =>    |- ( ( ph /\ E : N --> N ) -> ( D ` ( a e. N , b e. N |-> if ( ( E ` a ) = b , .1. , .0. ) ) ) = .0. )
Theorem	mdetunilem9 20426*	Lemma for mdetuni 20428. (Contributed by SO, 15-Jul-2018.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- K = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> D : B --> K )   &    |- ( ph -> A. x e. B A. y e. N A. z e. N ( ( y =/= z /\ A. w e. N ( y x w ) = ( z x w ) ) -> ( D ` x ) = .0. ) )   &    |- ( ph -> A. x e. B A. y e. B A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) ) )   &    |- ( ph -> A. x e. B A. y e. K A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( y .x. ( D ` z ) ) ) )   &    |- ( ph -> ( D ` ( 1r ` A ) ) = .0. )   &    |- Y = { x | A. y e. B A. z e. ( N ^m N ) ( A. w e. x ( y ` w ) = if ( w e. z , .1. , .0. ) -> ( D ` y ) = .0. ) }   =>    |- ( ph -> D = ( B X. { .0. } ) )
Theorem	mdetuni0 20427*	Lemma for mdetuni 20428. (Contributed by SO, 15-Jul-2018.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- K = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> D : B --> K )   &    |- ( ph -> A. x e. B A. y e. N A. z e. N ( ( y =/= z /\ A. w e. N ( y x w ) = ( z x w ) ) -> ( D ` x ) = .0. ) )   &    |- ( ph -> A. x e. B A. y e. B A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) ) )   &    |- ( ph -> A. x e. B A. y e. K A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( y .x. ( D ` z ) ) ) )   &    |- E = ( N maDet R )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> F e. B )   =>    |- ( ph -> ( D ` F ) = ( ( D ` ( 1r ` A ) ) .x. ( E ` F ) ) )
Theorem	mdetuni 20428*	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.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- K = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> D : B --> K )   &    |- ( ph -> A. x e. B A. y e. N A. z e. N ( ( y =/= z /\ A. w e. N ( y x w ) = ( z x w ) ) -> ( D ` x ) = .0. ) )   &    |- ( ph -> A. x e. B A. y e. B A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( y |` ( { w } X. N ) ) oF .+ ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( y |` ( ( N \ { w } ) X. N ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( ( D ` y ) .+ ( D ` z ) ) ) )   &    |- ( ph -> A. x e. B A. y e. K A. z e. B A. w e. N ( ( ( x |` ( { w } X. N ) ) = ( ( ( { w } X. N ) X. { y } ) oF .x. ( z |` ( { w } X. N ) ) ) /\ ( x |` ( ( N \ { w } ) X. N ) ) = ( z |` ( ( N \ { w } ) X. N ) ) ) -> ( D ` x ) = ( y .x. ( D ` z ) ) ) )   &    |- E = ( N maDet R )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> F e. B )   &    |- ( ph -> ( D ` ( 1r ` A ) ) = .1. )   =>    |- ( ph -> ( D ` F ) = ( E ` F ) )
Theorem	mdetmul 20429	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.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- D = ( N maDet R )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` A )   =>    |- ( ( R e. CRing /\ F e. B /\ G e. B ) -> ( D ` ( F .xb G ) ) = ( ( D ` F ) .x. ( D ` G ) ) )
11.3.2  Determinants of 2 x 2 -matrices
Theorem	m2detleiblem1 20430	Lemma 1 for m2detleib 20437. (Contributed by AV, 12-Dec-2018.)
|- N = { 1 , 2 }   &    |- P = ( Base ` ( SymGrp ` N ) )   &    |- Y = ( ZRHom ` R )   &    |- S = (pmSgn ` N )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ Q e. P ) -> ( Y ` ( S ` Q ) ) = ( ( (pmSgn ` N ) ` Q ) (.g ` R ) .1. ) )
Theorem	m2detleiblem5 20431	Lemma 5 for m2detleib 20437. (Contributed by AV, 20-Dec-2018.)
|- N = { 1 , 2 }   &    |- P = ( Base ` ( SymGrp ` N ) )   &    |- Y = ( ZRHom ` R )   &    |- S = (pmSgn ` N )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } ) -> ( Y ` ( S ` Q ) ) = .1. )
Theorem	m2detleiblem6 20432	Lemma 6 for m2detleib 20437. (Contributed by AV, 20-Dec-2018.)
|- N = { 1 , 2 }   &    |- P = ( Base ` ( SymGrp ` N ) )   &    |- Y = ( ZRHom ` R )   &    |- S = (pmSgn ` N )   &    |- .1. = ( 1r ` R )   &    |- I = ( invg ` R )   =>    |- ( ( R e. Ring /\ Q = { <. 1 , 2 >. , <. 2 , 1 >. } ) -> ( Y ` ( S ` Q ) ) = ( I ` .1. ) )
Theorem	m2detleiblem7 20433	Lemma 7 for m2detleib 20437. (Contributed by AV, 20-Dec-2018.)
|- N = { 1 , 2 }   &    |- P = ( Base ` ( SymGrp ` N ) )   &    |- Y = ( ZRHom ` R )   &    |- S = (pmSgn ` N )   &    |- .1. = ( 1r ` R )   &    |- I = ( invg ` R )   &    |- .x. = ( .r ` R )   &    |- .- = ( -g ` R )   =>    |- ( ( R e. Ring /\ X e. ( Base ` R ) /\ Z e. ( Base ` R ) ) -> ( X ( +g ` R ) ( ( I ` .1. ) .x. Z ) ) = ( X .- Z ) )
Theorem	m2detleiblem2 20434*	Lemma 2 for m2detleib 20437. (Contributed by AV, 16-Dec-2018.) (Proof shortened by AV, 1-Jan-2019.)
|- N = { 1 , 2 }   &    |- P = ( Base ` ( SymGrp ` N ) )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- G = (mulGrp ` R )   =>    |- ( ( R e. Ring /\ Q e. P /\ M e. B ) -> ( G gsumg ( n e. N |-> ( ( Q ` n ) M n ) ) ) e. ( Base ` R ) )
Theorem	m2detleiblem3 20435*	Lemma 3 for m2detleib 20437. (Contributed by AV, 16-Dec-2018.) (Proof shortened by AV, 2-Jan-2019.)
|- N = { 1 , 2 }   &    |- P = ( Base ` ( SymGrp ` N ) )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- G = (mulGrp ` R )   &    |- .x. = ( +g ` G )   =>    |- ( ( R e. Ring /\ Q = { <. 1 , 1 >. , <. 2 , 2 >. } /\ M e. B ) -> ( G gsumg ( n e. N |-> ( ( Q ` n ) M n ) ) ) = ( ( 1 M 1 ) .x. ( 2 M 2 ) ) )
Theorem	m2detleiblem4 20436*	Lemma 4 for m2detleib 20437. (Contributed by AV, 20-Dec-2018.) (Proof shortened by AV, 2-Jan-2019.)
|- N = { 1 , 2 }   &    |- P = ( Base ` ( SymGrp ` N ) )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- G = (mulGrp ` R )   &    |- .x. = ( +g ` G )   =>    |- ( ( R e. Ring /\ Q = { <. 1 , 2 >. , <. 2 , 1 >. } /\ M e. B ) -> ( G gsumg ( n e. N |-> ( ( Q ` n ) M n ) ) ) = ( ( 2 M 1 ) .x. ( 1 M 2 ) ) )
Theorem	m2detleib 20437	Leibniz' Formula for 2x2-matrices. (Contributed by AV, 21-Dec-2018.) (Revised by AV, 26-Dec-2018.) (Proof shortened by AV, 23-Jul-2019.)
|- N = { 1 , 2 }   &    |- D = ( N maDet R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- .- = ( -g ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ M e. B ) -> ( D ` M ) = ( ( ( 1 M 1 ) .x. ( 2 M 2 ) ) .- ( ( 2 M 1 ) .x. ( 1 M 2 ) ) ) )
11.3.3  The matrix adjugate/adjunct
Syntax	cmadu 20438	Syntax for the matrix adjugate/adjunct function.
class maAdju
Syntax	cminmar1 20439	Syntax for the minor matrices of a square matrix.
class minMatR1
Definition	df-madu 20440*	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 = ( n e. _V , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) |-> ( i e. n , j e. n |-> ( ( n maDet r ) ` ( k e. n , l e. n |-> if ( k = j , if ( l = i , ( 1r ` r ) , ( 0g ` r ) ) , ( k m l ) ) ) ) ) ) )
Definition	df-minmar1 20441*	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 20383- note that the matrix is transposed compared with the submatrix defined in df-subma 20383, but this does not matter because the determinants are the same, see mdettpos 20417). Such matrices are used in the definition of an adjunct of a square matrix, see df-madu 20440. (Contributed by AV, 27-Dec-2018.)
|- minMatR1 = ( n e. _V , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) |-> ( k e. n , l e. n |-> ( i e. n , j e. n |-> if ( i = k , if ( j = l , ( 1r ` r ) , ( 0g ` r ) ) , ( i m j ) ) ) ) ) )
Theorem	mndifsplit 20442	Lemma for maducoeval2 20446. (Contributed by SO, 16-Jul-2018.)
|- B = ( Base ` M )   &    |- .0. = ( 0g ` M )   &    |- .+ = ( +g ` M )   =>    |- ( ( M e. Mnd /\ A e. B /\ -. ( ph /\ ps ) ) -> if ( ( ph \/ ps ) , A , .0. ) = ( if ( ph , A , .0. ) .+ if ( ps , A , .0. ) ) )
Theorem	madufval 20443*	First substitution for the adjunct (cofactor) matrix. (Contributed by SO, 11-Jul-2018.)
|- A = ( N Mat R )   &    |- D = ( N maDet R )   &    |- J = ( N maAdju R )   &    |- B = ( Base ` A )   &    |- .1. = ( 1r ` R )   &    |- .0. = ( 0g ` R )   =>    |- J = ( m e. B |-> ( i e. N , j e. N |-> ( D ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , .1. , .0. ) , ( k m l ) ) ) ) ) )
Theorem	maduval 20444*	Second substitution for the adjunct (cofactor) matrix. (Contributed by SO, 11-Jul-2018.)
|- A = ( N Mat R )   &    |- D = ( N maDet R )   &    |- J = ( N maAdju R )   &    |- B = ( Base ` A )   &    |- .1. = ( 1r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( M e. B -> ( J ` M ) = ( i e. N , j e. N |-> ( D ` ( k e. N , l e. N |-> if ( k = j , if ( l = i , .1. , .0. ) , ( k M l ) ) ) ) ) )
Theorem	maducoeval 20445*	An entry of the adjunct (cofactor) matrix. (Contributed by SO, 11-Jul-2018.)
|- A = ( N Mat R )   &    |- D = ( N maDet R )   &    |- J = ( N maAdju R )   &    |- B = ( Base ` A )   &    |- .1. = ( 1r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( M e. B /\ I e. N /\ H e. N ) -> ( I ( J ` M ) H ) = ( D ` ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) ) ) )
Theorem	maducoeval2 20446*	An entry of the adjunct (cofactor) matrix. (Contributed by SO, 17-Jul-2018.)
|- A = ( N Mat R )   &    |- D = ( N maDet R )   &    |- J = ( N maAdju R )   &    |- B = ( Base ` A )   &    |- .1. = ( 1r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( ( R e. CRing /\ M e. B ) /\ I e. N /\ H e. N ) -> ( I ( J ` M ) H ) = ( D ` ( k e. N , l e. N |-> if ( ( k = H \/ l = I ) , if ( ( l = I /\ k = H ) , .1. , .0. ) , ( k M l ) ) ) ) )
Theorem	maduf 20447	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.)
|- A = ( N Mat R )   &    |- J = ( N maAdju R )   &    |- B = ( Base ` A )   =>    |- ( R e. CRing -> J : B --> B )
Theorem	madutpos 20448	The adjuct of a transposed matrix is the transposition of the adjunct of the matrix. (Contributed by Stefan O'Rear, 17-Jul-2018.)
|- A = ( N Mat R )   &    |- J = ( N maAdju R )   &    |- B = ( Base ` A )   =>    |- ( ( R e. CRing /\ M e. B ) -> ( J ` tpos M ) = tpos ( J ` M ) )
Theorem	madugsum 20449*	The determinant of a matrix with a row L consisting of the same element X is the sum of the elements of the L-th column of the adjunct of the matrix multiplied with X. (Contributed by Stefan O'Rear, 16-Jul-2018.)
|- A = ( N Mat R )   &    |- J = ( N maAdju R )   &    |- B = ( Base ` A )   &    |- D = ( N maDet R )   &    |- .x. = ( .r ` R )   &    |- K = ( Base ` R )   &    |- ( ph -> M e. B )   &    |- ( ph -> R e. CRing )   &    |- ( ( ph /\ i e. N ) -> X e. K )   &    |- ( ph -> L e. N )   =>    |- ( ph -> ( R gsumg ( i e. N |-> ( X .x. ( i ( J ` M ) L ) ) ) ) = ( D ` ( j e. N , i e. N |-> if ( j = L , X , ( j M i ) ) ) ) )
Theorem	madurid 20450	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.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- J = ( N maAdju R )   &    |- D = ( N maDet R )   &    |- .1. = ( 1r ` A )   &    |- .x. = ( .r ` A )   &    |- .xb = ( .s ` A )   =>    |- ( ( M e. B /\ R e. CRing ) -> ( M .x. ( J ` M ) ) = ( ( D ` M ) .xb .1. ) )
Theorem	madulid 20451	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.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- J = ( N maAdju R )   &    |- D = ( N maDet R )   &    |- .1. = ( 1r ` A )   &    |- .x. = ( .r ` A )   &    |- .xb = ( .s ` A )   =>    |- ( ( M e. B /\ R e. CRing ) -> ( ( J ` M ) .x. M ) = ( ( D ` M ) .xb .1. ) )
Theorem	minmar1fval 20452*	First substitution for the definition of a matrix for a minor. (Contributed by AV, 31-Dec-2018.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- Q = ( N minMatR1 R )   &    |- .1. = ( 1r ` R )   &    |- .0. = ( 0g ` R )   =>    |- Q = ( m e. B |-> ( k e. N , l e. N |-> ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , .0. ) , ( i m j ) ) ) ) )
Theorem	minmar1val0 20453*	Second substitution for the definition of a matrix for a minor. (Contributed by AV, 31-Dec-2018.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- Q = ( N minMatR1 R )   &    |- .1. = ( 1r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( M e. B -> ( Q ` M ) = ( k e. N , l e. N |-> ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , .0. ) , ( i M j ) ) ) ) )
Theorem	minmar1val 20454*	Third substitution for the definition of a matrix for a minor. (Contributed by AV, 31-Dec-2018.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- Q = ( N minMatR1 R )   &    |- .1. = ( 1r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( M e. B /\ K e. N /\ L e. N ) -> ( K ( Q ` M ) L ) = ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) )
Theorem	minmar1eval 20455	An entry of a matrix for a minor. (Contributed by AV, 31-Dec-2018.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- Q = ( N minMatR1 R )   &    |- .1. = ( 1r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( M e. B /\ ( K e. N /\ L e. N ) /\ ( I e. N /\ J e. N ) ) -> ( I ( K ( Q ` M ) L ) J ) = if ( I = K , if ( J = L , .1. , .0. ) , ( I M J ) ) )
Theorem	minmar1marrep 20456	The minor matrix is a special case of a matrix with a replaced row. (Contributed by AV, 12-Feb-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- Q = ( N matRRep R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ M e. B ) -> ( ( N minMatR1 R ) ` M ) = ( M ( N matRRep R ) .1. ) )
Theorem	minmar1cl 20457	Closure of the row replacement function for square matrices: The matrix for a minor is a matrix. (Contributed by AV, 13-Feb-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   =>    |- ( ( ( R e. Ring /\ M e. B ) /\ ( K e. N /\ L e. N ) ) -> ( K ( ( N minMatR1 R ) ` M ) L ) e. B )
Theorem	maducoevalmin1 20458	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.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- D = ( N maDet R )   &    |- J = ( N maAdju R )   =>    |- ( ( M e. B /\ I e. N /\ H e. N ) -> ( I ( J ` M ) H ) = ( D ` ( H ( ( N minMatR1 R ) ` M ) I ) ) )
11.3.4  Laplace expansion of determinants (special case) According to Wikipedia ("Laplace expansion", 08-Mar-2019, https://en.wikipedia.org/wiki/Laplace_expansion) "In linear algebra, the Laplace expansion, named after Pierre-Simon Laplace, also called cofactor expansion, is an expression for the determinant det(B) of an n x n -matrix B that is a weighted sum of the determinants of n sub-matrices of B, each of size (n-1) x (n-1)". The expansion is usually performed for a row of matrix B (alternately for a column of matrix B). The mentioned "sub-matrices" are the matrices resultung from deleting the i-th row and the j-th column of matrix B. The mentioned "weights" (factors/coefficients) are the elements at position i and j in matrix B. If the expansion is performed for a row, the coefficients are the elements of the selected row. In the following, only the case where the row for the expansion contains only the zero element of the underlying ring except at the diagonal position. By this, the sum for the Laplace expansion is reduced to one summand, consisting of the element at the diagonal position multiplied with the determinant of the corresponding submatrix, see smadiadetg 20479 or smadiadetr 20481.
Theorem	symgmatr01lem 20459*	Lemma for symgmatr01 20460. (Contributed by AV, 3-Jan-2019.)
|- P = ( Base ` ( SymGrp ` N ) )   =>    |- ( ( K e. N /\ L e. N ) -> ( Q e. ( P \ { q e. P | ( q ` K ) = L } ) -> E. k e. N if ( k = K , if ( ( Q ` k ) = L , A , B ) , ( k M ( Q ` k ) ) ) = B ) )
Theorem	symgmatr01 20460*	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.)
|- P = ( Base ` ( SymGrp ` N ) )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( K e. N /\ L e. N ) -> ( Q e. ( P \ { q e. P | ( q ` K ) = L } ) -> E. k e. N ( k ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` k ) ) = .0. ) )
Theorem	gsummatr01lem1 20461*	Lemma A for gsummatr01 20465. (Contributed by AV, 8-Jan-2019.)
|- P = ( Base ` ( SymGrp ` N ) )   &    |- R = { r e. P | ( r ` K ) = L }   =>    |- ( ( Q e. R /\ X e. N ) -> ( Q ` X ) e. N )
Theorem	gsummatr01lem2 20462*	Lemma B for gsummatr01 20465. (Contributed by AV, 8-Jan-2019.)
|- P = ( Base ` ( SymGrp ` N ) )   &    |- R = { r e. P | ( r ` K ) = L }   =>    |- ( ( Q e. R /\ X e. N ) -> ( A. i e. N A. j e. N ( i A j ) e. ( Base ` G ) -> ( X A ( Q ` X ) ) e. ( Base ` G ) ) )
Theorem	gsummatr01lem3 20463*	Lemma 1 for gsummatr01 20465. (Contributed by AV, 8-Jan-2019.)
|- P = ( Base ` ( SymGrp ` N ) )   &    |- R = { r e. P | ( r ` K ) = L }   &    |- .0. = ( 0g ` G )   &    |- S = ( Base ` G )   =>    |- ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> ( G gsumg ( n e. ( ( N \ { K } ) u. { K } ) |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) ) ) = ( ( G gsumg ( n e. ( N \ { K } ) |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) ) ) ( +g ` G ) ( K ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` K ) ) ) )
Theorem	gsummatr01lem4 20464*	Lemma 2 for gsummatr01 20465. (Contributed by AV, 8-Jan-2019.)
|- P = ( Base ` ( SymGrp ` N ) )   &    |- R = { r e. P | ( r ` K ) = L }   &    |- .0. = ( 0g ` G )   &    |- S = ( Base ` G )   =>    |- ( ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) /\ n e. ( N \ { K } ) ) -> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) = ( n ( i e. ( N \ { K } ) , j e. ( N \ { L } ) |-> ( i A j ) ) ( Q ` n ) ) )
Theorem	gsummatr01 20465*	Lemma 1 for smadiadetlem4 20475. (Contributed by AV, 8-Jan-2019.)
|- P = ( Base ` ( SymGrp ` N ) )   &    |- R = { r e. P | ( r ` K ) = L }   &    |- .0. = ( 0g ` G )   &    |- S = ( Base ` G )   =>    |- ( ( ( G e. CMnd /\ N e. Fin ) /\ ( A. i e. N A. j e. N ( i A j ) e. S /\ B e. S ) /\ ( K e. N /\ L e. N /\ Q e. R ) ) -> ( G gsumg ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .0. , B ) , ( i A j ) ) ) ( Q ` n ) ) ) ) = ( G gsumg ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { L } ) |-> ( i A j ) ) ( Q ` n ) ) ) ) )
Theorem	marep01ma 20466*	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.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- R e. CRing   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( M e. B -> ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) ) e. B )
Theorem	smadiadetlem0 20467*	Lemma 0 for smadiadet 20476: 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.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- R e. CRing   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- P = ( Base ` ( SymGrp ` N ) )   &    |- G = (mulGrp ` R )   =>    |- ( ( M e. B /\ K e. N /\ L e. N ) -> ( Q e. ( P \ { q e. P | ( q ` K ) = L } ) -> ( G gsumg ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( Q ` n ) ) ) ) = .0. ) )
Theorem	smadiadetlem1 20468*	Lemma 1 for smadiadet 20476: A summand of the determinant of a matrix belongs to the underlying ring. (Contributed by AV, 1-Jan-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- R e. CRing   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- P = ( Base ` ( SymGrp ` N ) )   &    |- G = (mulGrp ` R )   &    |- Y = ( ZRHom ` R )   &    |- S = (pmSgn ` N )   &    |- .x. = ( .r ` R )   =>    |- ( ( ( M e. B /\ K e. N ) /\ p e. P ) -> ( ( ( Y o. S ) ` p ) ( .r ` R ) ( G gsumg ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = K , .1. , .0. ) , ( i M j ) ) ) ( p ` n ) ) ) ) ) e. ( Base ` R ) )
Theorem	smadiadetlem1a 20469*	Lemma 1a for smadiadet 20476: 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.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- R e. CRing   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- P = ( Base ` ( SymGrp ` N ) )   &    |- G = (mulGrp ` R )   &    |- Y = ( ZRHom ` R )   &    |- S = (pmSgn ` N )   &    |- .x. = ( .r ` R )   =>    |- ( ( M e. B /\ K e. N /\ L e. N ) -> ( R gsumg ( p e. ( P \ { q e. P | ( q ` K ) = L } ) |-> ( ( ( Y o. S ) ` p ) .x. ( G gsumg ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) ( p ` n ) ) ) ) ) ) ) = .0. )
Theorem	smadiadetlem2 20470*	Lemma 2 for smadiadet 20476: 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.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- R e. CRing   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- P = ( Base ` ( SymGrp ` N ) )   &    |- G = (mulGrp ` R )   &    |- Y = ( ZRHom ` R )   &    |- S = (pmSgn ` N )   &    |- .x. = ( .r ` R )   =>    |- ( ( M e. B /\ K e. N ) -> ( R gsumg ( p e. ( P \ { q e. P | ( q ` K ) = K } ) |-> ( ( ( Y o. S ) ` p ) .x. ( G gsumg ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = K , .1. , .0. ) , ( i M j ) ) ) ( p ` n ) ) ) ) ) ) ) = .0. )
Theorem	smadiadetlem3lem0 20471*	Lemma 0 for smadiadetlem3 20474. (Contributed by AV, 12-Jan-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- R e. CRing   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- P = ( Base ` ( SymGrp ` N ) )   &    |- G = (mulGrp ` R )   &    |- Y = ( ZRHom ` R )   &    |- S = (pmSgn ` N )   &    |- .x. = ( .r ` R )   &    |- W = ( Base ` ( SymGrp ` ( N \ { K } ) ) )   &    |- Z = (pmSgn ` ( N \ { K } ) )   =>    |- ( ( ( M e. B /\ K e. N ) /\ Q e. W ) -> ( ( ( Y o. Z ) ` Q ) ( .r ` R ) ( G gsumg ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( Q ` n ) ) ) ) ) e. ( Base ` R ) )
Theorem	smadiadetlem3lem1 20472*	Lemma 1 for smadiadetlem3 20474. (Contributed by AV, 12-Jan-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- R e. CRing   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- P = ( Base ` ( SymGrp ` N ) )   &    |- G = (mulGrp ` R )   &    |- Y = ( ZRHom ` R )   &    |- S = (pmSgn ` N )   &    |- .x. = ( .r ` R )   &    |- W = ( Base ` ( SymGrp ` ( N \ { K } ) ) )   &    |- Z = (pmSgn ` ( N \ { K } ) )   =>    |- ( ( M e. B /\ K e. N ) -> ( p e. W |-> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsumg ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) : W --> ( Base ` R ) )
Theorem	smadiadetlem3lem2 20473*	Lemma 2 for smadiadetlem3 20474. (Contributed by AV, 12-Jan-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- R e. CRing   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- P = ( Base ` ( SymGrp ` N ) )   &    |- G = (mulGrp ` R )   &    |- Y = ( ZRHom ` R )   &    |- S = (pmSgn ` N )   &    |- .x. = ( .r ` R )   &    |- W = ( Base ` ( SymGrp ` ( N \ { K } ) ) )   &    |- Z = (pmSgn ` ( N \ { K } ) )   =>    |- ( ( M e. B /\ K e. N ) -> ran ( p e. W |-> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsumg ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) C_ ( (Cntz ` R ) ` ran ( p e. W |-> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsumg ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) ) )
Theorem	smadiadetlem3 20474*	Lemma 3 for smadiadet 20476. (Contributed by AV, 31-Jan-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- R e. CRing   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- P = ( Base ` ( SymGrp ` N ) )   &    |- G = (mulGrp ` R )   &    |- Y = ( ZRHom ` R )   &    |- S = (pmSgn ` N )   &    |- .x. = ( .r ` R )   &    |- W = ( Base ` ( SymGrp ` ( N \ { K } ) ) )   &    |- Z = (pmSgn ` ( N \ { K } ) )   =>    |- ( ( M e. B /\ K e. N ) -> ( R gsumg ( p e. { q e. P | ( q ` K ) = K } |-> ( ( ( Y o. S ) ` p ) ( .r ` R ) ( G gsumg ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) ) = ( R gsumg ( p e. W |-> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsumg ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) ) )
Theorem	smadiadetlem4 20475*	Lemma 4 for smadiadet 20476. (Contributed by AV, 31-Jan-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- R e. CRing   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- P = ( Base ` ( SymGrp ` N ) )   &    |- G = (mulGrp ` R )   &    |- Y = ( ZRHom ` R )   &    |- S = (pmSgn ` N )   &    |- .x. = ( .r ` R )   &    |- W = ( Base ` ( SymGrp ` ( N \ { K } ) ) )   &    |- Z = (pmSgn ` ( N \ { K } ) )   =>    |- ( ( M e. B /\ K e. N ) -> ( R gsumg ( p e. { q e. P | ( q ` K ) = K } |-> ( ( ( Y o. S ) ` p ) ( .r ` R ) ( G gsumg ( n e. N |-> ( n ( i e. N , j e. N |-> if ( i = K , if ( j = K , .1. , .0. ) , ( i M j ) ) ) ( p ` n ) ) ) ) ) ) ) = ( R gsumg ( p e. W |-> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsumg ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) ) )
Theorem	smadiadet 20476	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.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- R e. CRing   &    |- D = ( N maDet R )   &    |- E = ( ( N \ { K } ) maDet R )   =>    |- ( ( M e. B /\ K e. N ) -> ( E ` ( K ( ( N subMat R ) ` M ) K ) ) = ( D ` ( K ( ( N minMatR1 R ) ` M ) K ) ) )
Theorem	smadiadetglem1 20477	Lemma 1 for smadiadetg 20479. (Contributed by AV, 13-Feb-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- R e. CRing   &    |- D = ( N maDet R )   &    |- E = ( ( N \ { K } ) maDet R )   =>    |- ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( K ( M ( N matRRep R ) S ) K ) |` ( ( N \ { K } ) X. N ) ) = ( ( K ( ( N minMatR1 R ) ` M ) K ) |` ( ( N \ { K } ) X. N ) ) )
Theorem	smadiadetglem2 20478	Lemma 2 for smadiadetg 20479. (Contributed by AV, 14-Feb-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- R e. CRing   &    |- D = ( N maDet R )   &    |- E = ( ( N \ { K } ) maDet R )   &    |- .x. = ( .r ` R )   =>    |- ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( K ( M ( N matRRep R ) S ) K ) |` ( { K } X. N ) ) = ( ( ( { K } X. N ) X. { S } ) oF .x. ( ( K ( ( N minMatR1 R ) ` M ) K ) |` ( { K } X. N ) ) ) )
Theorem	smadiadetg 20479	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.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- R e. CRing   &    |- D = ( N maDet R )   &    |- E = ( ( N \ { K } ) maDet R )   &    |- .x. = ( .r ` R )   =>    |- ( ( M e. B /\ K e. N /\ S e. ( Base ` R ) ) -> ( D ` ( K ( M ( N matRRep R ) S ) K ) ) = ( S .x. ( E ` ( K ( ( N subMat R ) ` M ) K ) ) ) )
Theorem	smadiadetg0 20480	Lemma for smadiadetr 20481: version of smadiadetg 20479 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.)
|- R e. CRing   =>    |- ( ( M e. ( Base ` ( N Mat R ) ) /\ K e. N /\ S e. ( Base ` R ) ) -> ( ( N maDet R ) ` ( K ( M ( N matRRep R ) S ) K ) ) = ( S ( .r ` R ) ( ( ( N \ { K } ) maDet R ) ` ( K ( ( N subMat R ) ` M ) K ) ) ) )
Theorem	smadiadetr 20481	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 20479. Special case of the "Laplace expansion", see definition in [Lang] p. 515. (Contributed by AV, 15-Feb-2019.)
|- ( ( ( R e. CRing /\ M e. ( Base ` ( N Mat R ) ) ) /\ ( K e. N /\ S e. ( Base ` R ) ) ) -> ( ( N maDet R ) ` ( K ( M ( N matRRep R ) S ) K ) ) = ( S ( .r ` R ) ( ( ( N \ { K } ) maDet R ) ` ( K ( ( N subMat R ) ` M ) K ) ) ) )
11.3.5  Inverse matrix
Theorem	invrvald 20482	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.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   &    |- U = (Unit ` R )   &    |- I = ( invr ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> ( X .x. Y ) = .1. )   &    |- ( ph -> ( Y .x. X ) = .1. )   =>    |- ( ph -> ( X e. U /\ ( I ` X ) = Y ) )
Theorem	matinv 20483	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.)
|- A = ( N Mat R )   &    |- J = ( N maAdju R )   &    |- D = ( N maDet R )   &    |- B = ( Base ` A )   &    |- U = (Unit ` A )   &    |- V = (Unit ` R )   &    |- H = ( invr ` R )   &    |- I = ( invr ` A )   &    |- .xb = ( .s ` A )   =>    |- ( ( R e. CRing /\ M e. B /\ ( D ` M ) e. V ) -> ( M e. U /\ ( I ` M ) = ( ( H ` ( D ` M ) ) .xb ( J ` M ) ) ) )
Theorem	matunit 20484	A matrix is a unit in the ring of matrices iff its determinant is a unit in the underlying ring. (Contributed by Stefan O'Rear, 17-Jul-2018.)
|- A = ( N Mat R )   &    |- D = ( N maDet R )   &    |- B = ( Base ` A )   &    |- U = (Unit ` A )   &    |- V = (Unit ` R )   =>    |- ( ( R e. CRing /\ M e. B ) -> ( M e. U <-> ( D ` M ) e. V ) )
11.3.6  Cramer's rule In the following, Cramer's rule cramer 20497 is proven. According to Wikipedia "Cramer's rule", 21-Feb-2019, https://en.wikipedia.org/wiki/Cramer%27s_rule: "[Cramer's rule] ... expresses the [unique] solution [of a system of linear equations] in terms of the determinants of the (square) coefficient matrix and of matrices obtained from it by replacing one column by the column vector of right-hand sides of the equations." The outline of the proof for systems of linear equations with coefficients from a commutative ring, according to the proof in Wikipedia (https://en.wikipedia.org/wiki/Cramer's_rule#A_short_proof), is as follows: The system of linear equations A .X. X = B to be solved shall be given by the N x N coefficient matrix A and the N-dimensional vector B. Let ( A ` i ) be the matrix obtained by replacing the i-th column of the coefficient matrix A by the right-hand side vector B. Additionally, let ( X ` i ) be the the matrix obtained by replacing the i-th column of the identity matrix by the solution vector X, with X = ( x ` i ). Finally, it is assumed that det A is a unit in the underlying ring. With these definitions, it follows that A .X. ( X ` i ) = ( A ` i ) (cramerimplem2 20490), using matrix multiplication (mamuval 20192) and multiplication of a vector with a matrix (mulmarep1gsum2 20380). By using the multiplicativity of the determinant (mdetmul 20429) it follows that det ( A ` i ) = det ( A .X. ( X ` i ) ) = det A .x. det ( X ` i ) (cramerimplem3 20491). Furthermore, it follows that det ( X ` i ) = ( x ` i ) (cramerimplem1 20489). To show this, a special case of the Laplace expansion is used (smadiadetg 20479). From these equations and the cancellation law for division in a ring (dvrcan3 18692) it follows that ( x ` i ) = det ( X ` i ) = det ( A ` i ) ./ det A. This is the right to left implication (cramerimp 20492, cramerlem1 20493, cramerlem2 20494) of Cramer's rule (cramer 20497). The left to right implication is shown by cramerlem3 20495, using the fact that a solution of the system of linear equations exists (slesolex 20488). Notice that for the special case of 0-dimensional matrices/vectors only the left to right implication is valid (see cramer0 20496), because assuming the right-hand side of the implication ( ( X .x. Z ) = Y), Z could be anything (see mavmul0g 20359).
Theorem	slesolvec 20485	Every solution of a system of linear equations represented by a matrix and a vector is a vector. (Contributed by AV, 10-Feb-2019.) (Revised by AV, 27-Feb-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- V = ( ( Base ` R ) ^m N )   &    |- .x. = ( R maVecMul <. N , N >. )   =>    |- ( ( ( N =/= (/) /\ R e. Ring ) /\ ( X e. B /\ Y e. V ) ) -> ( ( X .x. Z ) = Y -> Z e. V ) )
Theorem	slesolinv 20486	The solution of a system of linear equations represented by a matrix with a unit as determinant is the multiplication of the inverse of the matrix with the right-hand side vector. (Contributed by AV, 10-Feb-2019.) (Revised by AV, 28-Feb-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- V = ( ( Base ` R ) ^m N )   &    |- .x. = ( R maVecMul <. N , N >. )   &    |- D = ( N maDet R )   &    |- I = ( invr ` A )   =>    |- ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. (Unit ` R ) /\ ( X .x. Z ) = Y ) ) -> Z = ( ( I ` X ) .x. Y ) )
Theorem	slesolinvbi 20487	The solution of a system of linear equations represented by a matrix with a unit as determinant is the multiplication of the inverse of the matrix with the right-hand side vector. (Contributed by AV, 11-Feb-2019.) (Revised by AV, 28-Feb-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- V = ( ( Base ` R ) ^m N )   &    |- .x. = ( R maVecMul <. N , N >. )   &    |- D = ( N maDet R )   &    |- I = ( invr ` A )   =>    |- ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. (Unit ` R ) ) -> ( ( X .x. Z ) = Y <-> Z = ( ( I ` X ) .x. Y ) ) )
Theorem	slesolex 20488*	Every system of linear equations represented by a matrix with a unit as determinant has a solution. (Contributed by AV, 11-Feb-2019.) (Revised by AV, 28-Feb-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- V = ( ( Base ` R ) ^m N )   &    |- .x. = ( R maVecMul <. N , N >. )   &    |- D = ( N maDet R )   =>    |- ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. (Unit ` R ) ) -> E. z e. V ( X .x. z ) = Y )
Theorem	cramerimplem1 20489	Lemma 1 for cramerimp 20492: The determinant of the identity matrix with the ith column replaced by a (column) vector equals the ith component of the vector. (Contributed by AV, 15-Feb-2019.) (Revised by AV, 28-Feb-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- V = ( ( Base ` R ) ^m N )   &    |- E = ( ( ( 1r ` A ) ( N matRepV R ) Z ) ` I )   &    |- D = ( N maDet R )   =>    |- ( ( ( N e. Fin /\ R e. CRing /\ I e. N ) /\ Z e. V ) -> ( D ` E ) = ( Z ` I ) )
Theorem	cramerimplem2 20490	Lemma 2 for cramerimp 20492: The matrix of a system of linear equations multiplied with the identity matrix with the ith column replaced by the solution vector of the system of linear equations equals the matrix of the system of linear equations with the ith column replaced by the right-hand side vector of the system of linear equations. (Contributed by AV, 19-Feb-2019.) (Revised by AV, 1-Mar-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- V = ( ( Base ` R ) ^m N )   &    |- E = ( ( ( 1r ` A ) ( N matRepV R ) Z ) ` I )   &    |- H = ( ( X ( N matRepV R ) Y ) ` I )   &    |- .x. = ( R maVecMul <. N , N >. )   &    |- .X. = ( R maMul <. N , N , N >. )   =>    |- ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> ( X .X. E ) = H )
Theorem	cramerimplem3 20491	Lemma 3 for cramerimp 20492: The determinant of the matrix of a system of linear equations multiplied with the determinant of the identity matrix with the ith column replaced by the solution vector of the system of linear equations equals the determinant of the matrix of the system of linear equations with the ith column replaced by the right-hand side vector of the system of linear equations. (Contributed by AV, 19-Feb-2019.) (Revised by AV, 1-Mar-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- V = ( ( Base ` R ) ^m N )   &    |- E = ( ( ( 1r ` A ) ( N matRepV R ) Z ) ` I )   &    |- H = ( ( X ( N matRepV R ) Y ) ` I )   &    |- .x. = ( R maVecMul <. N , N >. )   &    |- D = ( N maDet R )   &    |- .(x) = ( .r ` R )   =>    |- ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( X .x. Z ) = Y ) -> ( ( D ` X ) .(x) ( D ` E ) ) = ( D ` H ) )
Theorem	cramerimp 20492	One direction of Cramer's rule (according to Wikipedia "Cramer's rule", 21-Feb-2019, https://en.wikipedia.org/wiki/Cramer%27s_rule: "[Cramer's rule] ... expresses the solution [of a system of linear equations] in terms of the determinants of the (square) coefficient matrix and of matrices obtained from it by replacing one column by the column vector of right-hand sides of the equations."): The ith component of the solution vector of a system of linear equations equals the determinant of the matrix of the system of linear equations with the ith column replaced by the righthand side vector of the system of linear equations divided by the determinant of the matrix of the system of linear equations. (Contributed by AV, 19-Feb-2019.) (Revised by AV, 1-Mar-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- V = ( ( Base ` R ) ^m N )   &    |- E = ( ( ( 1r ` A ) ( N matRepV R ) Z ) ` I )   &    |- H = ( ( X ( N matRepV R ) Y ) ` I )   &    |- .x. = ( R maVecMul <. N , N >. )   &    |- D = ( N maDet R )   &    |- ./ = (/r ` R )   =>    |- ( ( ( R e. CRing /\ I e. N ) /\ ( X e. B /\ Y e. V ) /\ ( ( X .x. Z ) = Y /\ ( D ` X ) e. (Unit ` R ) ) ) -> ( Z ` I ) = ( ( D ` H ) ./ ( D ` X ) ) )
Theorem	cramerlem1 20493*	Lemma 1 for cramer 20497. (Contributed by AV, 21-Feb-2019.) (Revised by AV, 1-Mar-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- V = ( ( Base ` R ) ^m N )   &    |- D = ( N maDet R )   &    |- .x. = ( R maVecMul <. N , N >. )   &    |- ./ = (/r ` R )   =>    |- ( ( R e. CRing /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. (Unit ` R ) /\ Z e. V /\ ( X .x. Z ) = Y ) ) -> Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) )
Theorem	cramerlem2 20494*	Lemma 2 for cramer 20497. (Contributed by AV, 21-Feb-2019.) (Revised by AV, 1-Mar-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- V = ( ( Base ` R ) ^m N )   &    |- D = ( N maDet R )   &    |- .x. = ( R maVecMul <. N , N >. )   &    |- ./ = (/r ` R )   =>    |- ( ( R e. CRing /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. (Unit ` R ) ) -> A. z e. V ( ( X .x. z ) = Y -> z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) ) )
Theorem	cramerlem3 20495*	Lemma 3 for cramer 20497. (Contributed by AV, 21-Feb-2019.) (Revised by AV, 1-Mar-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- V = ( ( Base ` R ) ^m N )   &    |- D = ( N maDet R )   &    |- .x. = ( R maVecMul <. N , N >. )   &    |- ./ = (/r ` R )   =>    |- ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. (Unit ` R ) ) -> ( Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) -> ( X .x. Z ) = Y ) )
Theorem	cramer0 20496*	Special case of Cramer's rule for 0-dimensional matrices/vectors. (Contributed by AV, 28-Feb-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- V = ( ( Base ` R ) ^m N )   &    |- D = ( N maDet R )   &    |- .x. = ( R maVecMul <. N , N >. )   &    |- ./ = (/r ` R )   =>    |- ( ( ( N = (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. (Unit ` R ) ) -> ( Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) -> ( X .x. Z ) = Y ) )
Theorem	cramer 20497*	Cramer's rule. According to Wikipedia "Cramer's rule", 21-Feb-2019, https://en.wikipedia.org/wiki/Cramer%27s_rule: "[Cramer's rule] ... expresses the [unique] solution [of a system of linear equations] in terms of the determinants of the (square) coefficient matrix and of matrices obtained from it by replacing one column by the column vector of right-hand sides of the equations." If it is assumed that a (unique) solution exists, it can be obtained by Cramer's rule (see also cramerimp 20492). On the other hand, if a vector can be constructed by Cramer's rule, it is a solution of the system of linear equations, so at least one solution exists. The uniqueness is ensured by considering only systems of linear equations whose matrix has a unit (of the underlying ring) as determinant, see matunit 20484 or slesolinv 20486. For fields as underlying rings, this requirement is equivalent with the determinant not being 0. Theorem 4.4 in [Lang] p. 513. This is Metamath 100 proof #97. (Contributed by Alexander van der Vekens, 21-Feb-2019.) (Revised by Alexander van der Vekens, 1-Mar-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- V = ( ( Base ` R ) ^m N )   &    |- D = ( N maDet R )   &    |- .x. = ( R maVecMul <. N , N >. )   &    |- ./ = (/r ` R )   =>    |- ( ( ( R e. CRing /\ N =/= (/) ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. (Unit ` R ) ) -> ( Z = ( i e. N |-> ( ( D ` ( ( X ( N matRepV R ) Y ) ` i ) ) ./ ( D ` X ) ) ) <-> ( X .x. Z ) = Y ) )
11.4  Polynomial matrices A polynomial matrix or matrix of polynomials is a matrix whose elements are univariate (or multivariate) polynomials. See Wikipedia "Polynomial matrix" https://en.wikipedia.org/wiki/Polynomial_matrix (18-Nov-2019). In this section, only square matrices whose elements are univariate polynomials are considered. Usually, the ring of such matrices, the ring of n x n matrices over the polynomial ring over a ring R, is denoted by M(n, R[t]). The elements of this ring are called "polynomial matrices (over the ring R)" in the following. In Metamath notation, this ring is defined by ( N Mat (Poly1 ` R ) ), usually represented by the class variable C (or Y, if C is already occupied): C = ( N Mat P ) with P = (Poly1 ` R ).
11.4.1  Basic properties
Theorem	pmatring 20498	The set of polynomial matrices over a ring is a ring. (Contributed by AV, 6-Nov-2019.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )
Theorem	pmatlmod 20499	The set of polynomial matrices over a ring is a left module. (Contributed by AV, 6-Nov-2019.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> C e. LMod )
Theorem	pmat0op 20500*	The zero polynomial matrix over a ring represented as operation. (Contributed by AV, 16-Nov-2019.)
|- P = (Poly1 ` R )   &    |- C = ( N Mat P )   &    |- .0. = ( 0g ` P )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` C ) = ( i e. N , j e. N |-> .0. ) )