P. 196 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19501-19600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mat1f1o 19501*	There is a 1-1 function from a ring onto the ring of matrices with dimension 1 over this ring. (Contributed by AV, 22-Dec-2019.)
|- K = ( Base ` R )   &    |- A = ( { E } Mat R )   &    |- B = ( Base ` A )   &    |- O = <. E , E >.   &    |- F = ( x e. K |-> { <. O , x >. } )   =>    |- ( ( R e. Ring /\ E e. V ) -> F : K -1-1-onto-> B )
Theorem	mat1rhmval 19502*	The value of the ring homomorphism F. (Contributed by AV, 22-Dec-2019.)
|- K = ( Base ` R )   &    |- A = ( { E } Mat R )   &    |- B = ( Base ` A )   &    |- O = <. E , E >.   &    |- F = ( x e. K |-> { <. O , x >. } )   =>    |- ( ( R e. Ring /\ E e. V /\ X e. K ) -> ( F ` X ) = { <. O , X >. } )
Theorem	mat1rhmelval 19503*	The value of the ring homomorphism F. (Contributed by AV, 22-Dec-2019.)
|- K = ( Base ` R )   &    |- A = ( { E } Mat R )   &    |- B = ( Base ` A )   &    |- O = <. E , E >.   &    |- F = ( x e. K |-> { <. O , x >. } )   =>    |- ( ( R e. Ring /\ E e. V /\ X e. K ) -> ( E ( F ` X ) E ) = X )
Theorem	mat1rhmcl 19504*	The value of the ring homomorphism F is a matrix with dimension 1. (Contributed by AV, 22-Dec-2019.)
|- K = ( Base ` R )   &    |- A = ( { E } Mat R )   &    |- B = ( Base ` A )   &    |- O = <. E , E >.   &    |- F = ( x e. K |-> { <. O , x >. } )   =>    |- ( ( R e. Ring /\ E e. V /\ X e. K ) -> ( F ` X ) e. B )
Theorem	mat1f 19505*	There is a function from a ring to the ring of matrices with dimension 1 over this ring. (Contributed by AV, 22-Dec-2019.)
|- K = ( Base ` R )   &    |- A = ( { E } Mat R )   &    |- B = ( Base ` A )   &    |- O = <. E , E >.   &    |- F = ( x e. K |-> { <. O , x >. } )   =>    |- ( ( R e. Ring /\ E e. V ) -> F : K --> B )
Theorem	mat1ghm 19506*	There is a group homomorphism from the additive group of a ring to the additive group of the ring of matrices with dimension 1 over this ring. (Contributed by AV, 22-Dec-2019.)
|- K = ( Base ` R )   &    |- A = ( { E } Mat R )   &    |- B = ( Base ` A )   &    |- O = <. E , E >.   &    |- F = ( x e. K |-> { <. O , x >. } )   =>    |- ( ( R e. Ring /\ E e. V ) -> F e. ( R GrpHom A ) )
Theorem	mat1mhm 19507*	There is a monoid homomorphism from the multiplicative group of a ring to the multiplicative group of the ring of matrices with dimension 1 over this ring. (Contributed by AV, 22-Dec-2019.)
|- K = ( Base ` R )   &    |- A = ( { E } Mat R )   &    |- B = ( Base ` A )   &    |- O = <. E , E >.   &    |- F = ( x e. K |-> { <. O , x >. } )   &    |- M = (mulGrp ` R )   &    |- N = (mulGrp ` A )   =>    |- ( ( R e. Ring /\ E e. V ) -> F e. ( M MndHom N ) )
Theorem	mat1rhm 19508*	There is a ring homomorphism from a ring to the ring of matrices with dimension 1 over this ring. (Contributed by AV, 22-Dec-2019.)
|- K = ( Base ` R )   &    |- A = ( { E } Mat R )   &    |- B = ( Base ` A )   &    |- O = <. E , E >.   &    |- F = ( x e. K |-> { <. O , x >. } )   =>    |- ( ( R e. Ring /\ E e. V ) -> F e. ( R RingHom A ) )
Theorem	mat1rngiso 19509*	There is a ring isomorphism from a ring to the ring of matrices with dimension 1 over this ring. (Contributed by AV, 22-Dec-2019.)
|- K = ( Base ` R )   &    |- A = ( { E } Mat R )   &    |- B = ( Base ` A )   &    |- O = <. E , E >.   &    |- F = ( x e. K |-> { <. O , x >. } )   =>    |- ( ( R e. Ring /\ E e. V ) -> F e. ( R RingIso A ) )
Theorem	mat1ric 19510	A ring is isomorphic to the ring of matrices with dimension 1 over this ring. (Contributed by AV, 30-Dec-2019.)
|- A = ( { E } Mat R )   =>    |- ( ( R e. Ring /\ E e. V ) -> R ~=r A )
11.2.5  The subalgebras of diagonal and scalar matrices According to Wikipedia ("Diagonal Matrix", 8-Dec-2019, https://en.wikipedia.org/wiki/Diagonal_matrix): "In linear algebra, a diagonal matrix is a matrix in which the entries outside the main diagonal are all zero; the term usually refers to square matrices." The diagonal matrices are mentioned in [Lang] p. 576, but without giving them a dedicated definition. Furthermore, "A diagonal matrix with all its main diagonal entries equal is a scalar matrix, that is, a scalar multiple la .* I of the identity matrix I. Its effect on a vector is scalar multiplication by la [see scmatscm 19536!]". The scalar multiples of the identity matrix are mentioned in [Lang] p. 504, but without giving them a special name. The main results of this subsection are the definitions of the sets of diagonal and scalar matrices (df-dmat 19513 and df-scmat 19514), basic properties of (elements of) these sets, and theorems showing that the diagonal matrices are a subring of the ring of square matrices (dmatsrng 19524), that the scalar matrices are a subring of the ring of square matrices (scmatsrng 19543), that the scalar matrices are a subring of the ring of diagonal matrices (scmatsrng1 19546) and that the ring of scalar matrices (over a commutative ring) is a commutative ring (scmatcrng 19544).
Syntax	cdmat 19511	Extend class notation for the algebra of diagonal matrices.
class DMat
Syntax	cscmat 19512	Extend class notation for the algebra of scalar matrices.
class ScMat
Definition	df-dmat 19513*	Define the set of n x n diagonal (square) matrices over a set (usually a ring) r, see definition in [Roman] p. 4 or Definition 3.12 in [Hefferon] p. 240. (Contributed by AV, 8-Dec-2019.)
|- DMat = ( n e. Fin , r e. _V |-> { m e. ( Base ` ( n Mat r ) ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) } )
Definition	df-scmat 19514*	Define the algebra of n x n scalar matrices over a set (usually a ring) r, see definition in [Connell] p. 57: "A scalar matrix is a diagonal matrix for which all the diagonal terms are equal, i.e., a matrix of the form cIn";. (Contributed by AV, 8-Dec-2019.)
|- ScMat = ( n e. Fin , r e. _V |-> [_ ( n Mat r ) / a ]_ { m e. ( Base ` a ) | E. c e. ( Base ` r ) m = ( c ( .s ` a ) ( 1r ` a ) ) } )
Theorem	dmatval 19515*	The set of N x N diagonal matrices over (a ring) R. (Contributed by AV, 8-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- .0. = ( 0g ` R )   &    |- D = ( N DMat R )   =>    |- ( ( N e. Fin /\ R e. V ) -> D = { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } )
Theorem	dmatel 19516*	A N x N diagonal matrix over (a ring) R. (Contributed by AV, 18-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- .0. = ( 0g ` R )   &    |- D = ( N DMat R )   =>    |- ( ( N e. Fin /\ R e. V ) -> ( M e. D <-> ( M e. B /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) ) )
Theorem	dmatmat 19517	An N x N diagonal matrix over (the ring) R is an N x N matrix over (the ring) R. (Contributed by AV, 18-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- .0. = ( 0g ` R )   &    |- D = ( N DMat R )   =>    |- ( ( N e. Fin /\ R e. V ) -> ( M e. D -> M e. B ) )
Theorem	dmatid 19518	The identity matrix is a diagonal matrix. (Contributed by AV, 19-Aug-2019.) (Revised by AV, 18-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- .0. = ( 0g ` R )   &    |- D = ( N DMat R )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. D )
Theorem	dmatelnd 19519	An extradiagonal entry of a diagonal matrix is equal to zero. (Contributed by AV, 19-Aug-2019.) (Revised by AV, 18-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- .0. = ( 0g ` R )   &    |- D = ( N DMat R )   =>    |- ( ( ( N e. Fin /\ R e. Ring /\ X e. D ) /\ ( I e. N /\ J e. N /\ I =/= J ) ) -> ( I X J ) = .0. )
Theorem	dmatmul 19520*	The product of two diagonal matrices. (Contributed by AV, 19-Aug-2019.) (Revised by AV, 18-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- .0. = ( 0g ` R )   &    |- D = ( N DMat R )   =>    |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( X ( .r ` A ) Y ) = ( x e. N , y e. N |-> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) ) )
Theorem	dmatsubcl 19521	The difference of two diagonal matrices is a diagonal matrix. (Contributed by AV, 19-Aug-2019.) (Revised by AV, 18-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- .0. = ( 0g ` R )   &    |- D = ( N DMat R )   =>    |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( X ( -g ` A ) Y ) e. D )
Theorem	dmatsgrp 19522	The set of diagonal matrices is a subgroup of the matrix group/algebra. (Contributed by AV, 19-Aug-2019.) (Revised by AV, 18-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- .0. = ( 0g ` R )   &    |- D = ( N DMat R )   =>    |- ( ( R e. Ring /\ N e. Fin ) -> D e. (SubGrp ` A ) )
Theorem	dmatmulcl 19523	The product of two diagonal matrices is a diagonal matrix. (Contributed by AV, 20-Aug-2019.) (Revised by AV, 18-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- .0. = ( 0g ` R )   &    |- D = ( N DMat R )   =>    |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( X ( .r ` A ) Y ) e. D )
Theorem	dmatsrng 19524	The set of diagonal matrices is a subring of the matrix ring/algebra. (Contributed by AV, 20-Aug-2019.) (Revised by AV, 18-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- .0. = ( 0g ` R )   &    |- D = ( N DMat R )   =>    |- ( ( R e. Ring /\ N e. Fin ) -> D e. (SubRing ` A ) )
Theorem	dmatcrng 19525	The subring of diagonal matrices (over a commutative ring) is a commutative ring . (Contributed by AV, 20-Aug-2019.) (Revised by AV, 18-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- .0. = ( 0g ` R )   &    |- D = ( N DMat R )   &    |- C = ( A ↾s D )   =>    |- ( ( R e. CRing /\ N e. Fin ) -> C e. CRing )
Theorem	dmatscmcl 19526	The multiplication of a diagonal matrix with a scalar is a diagonal matrix. (Contributed by AV, 19-Dec-2019.)
|- K = ( Base ` R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- .* = ( .s ` A )   &    |- D = ( N DMat R )   =>    |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( C e. K /\ M e. D ) ) -> ( C .* M ) e. D )
Theorem	scmatval 19527*	The set of N x N scalar matrices over (a ring) R. (Contributed by AV, 18-Dec-2019.)
|- K = ( Base ` R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- .1. = ( 1r ` A )   &    |- .x. = ( .s ` A )   &    |- S = ( N ScMat R )   =>    |- ( ( N e. Fin /\ R e. V ) -> S = { m e. B | E. c e. K m = ( c .x. .1. ) } )
Theorem	scmatel 19528*	An N x N scalar matrix over (a ring) R. (Contributed by AV, 18-Dec-2019.)
|- K = ( Base ` R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- .1. = ( 1r ` A )   &    |- .x. = ( .s ` A )   &    |- S = ( N ScMat R )   =>    |- ( ( N e. Fin /\ R e. V ) -> ( M e. S <-> ( M e. B /\ E. c e. K M = ( c .x. .1. ) ) ) )
Theorem	scmatscmid 19529*	A scalar matrix can be expressed as a multiplication of a scalar with the identity matrix. (Contributed by AV, 30-Oct-2019.) (Revised by AV, 18-Dec-2019.)
|- K = ( Base ` R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- .1. = ( 1r ` A )   &    |- .x. = ( .s ` A )   &    |- S = ( N ScMat R )   =>    |- ( ( N e. Fin /\ R e. V /\ M e. S ) -> E. c e. K M = ( c .x. .1. ) )
Theorem	scmatscmide 19530	An entry of a scalar matrix expressed as a multiplication of a scalar with the identity matrix. (Contributed by AV, 30-Oct-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` A )   &    |- .* = ( .s ` A )   =>    |- ( ( ( N e. Fin /\ R e. Ring /\ C e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I ( C .* .1. ) J ) = if ( I = J , C , .0. ) )
Theorem	scmatscmiddistr 19531	Distributive law for scalar and ring multiplication for scalar matrices expressed as multiplications of a scalar with the identity matrix. (Contributed by AV, 19-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` A )   &    |- .* = ( .s ` A )   &    |- .x. = ( .r ` R )   &    |- .X. = ( .r ` A )   =>    |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> ( ( S .* .1. ) .X. ( T .* .1. ) ) = ( ( S .x. T ) .* .1. ) )
Theorem	scmatmat 19532	An N x N scalar matrix over (the ring) R is an N x N matrix over (the ring) R. (Contributed by AV, 18-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- S = ( N ScMat R )   =>    |- ( ( N e. Fin /\ R e. V ) -> ( M e. S -> M e. B ) )
Theorem	scmate 19533*	An entry of an N x N scalar matrix over the ring R. (Contributed by AV, 18-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- S = ( N ScMat R )   &    |- K = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( I e. N /\ J e. N ) ) -> E. c e. K ( I M J ) = if ( I = J , c , .0. ) )
Theorem	scmatmats 19534*	The set of an N x N scalar matrices over the ring R expressed as a subset of N x N matrices over the ring R with certain properties for their entries. (Contributed by AV, 31-Oct-2019.) (Revised by AV, 19-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- S = ( N ScMat R )   &    |- K = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> S = { m e. B | E. c e. K A. i e. N A. j e. N ( i m j ) = if ( i = j , c , .0. ) } )
Theorem	scmateALT 19535*	Alternate proof of scmate 19533: An entry of an N x N scalar matrix over the ring R. This prove makes use of scmatmats 19534 but is longer and requires more distinct variables. (Contributed by AV, 19-Dec-2019.) (New usage is discouraged.) (Proof modification is discouraged.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- S = ( N ScMat R )   &    |- K = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( I e. N /\ J e. N ) ) -> E. c e. K ( I M J ) = if ( I = J , c , .0. ) )
Theorem	scmatscm 19536*	The multiplication of a matrix with a scalar matrix corresponds to a scalar multiplication. (Contributed by AV, 28-Dec-2019.)
|- K = ( Base ` R )   &    |- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- .* = ( .s ` A )   &    |- .X. = ( .r ` A )   &    |- S = ( N ScMat R )   =>    |- ( ( ( N e. Fin /\ R e. Ring ) /\ C e. S ) -> E. c e. K A. m e. B ( C .X. m ) = ( c .* m ) )
Theorem	scmatid 19537	The identity matrix is a scalar matrix. (Contributed by AV, 20-Aug-2019.) (Revised by AV, 18-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- E = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- S = ( N ScMat R )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. S )
Theorem	scmatdmat 19538	A scalar matrix is a diagonal matrix. (Contributed by AV, 20-Aug-2019.) (Revised by AV, 19-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- E = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- S = ( N ScMat R )   &    |- D = ( N DMat R )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> ( M e. S -> M e. D ) )
Theorem	scmataddcl 19539	The sum of two scalar matrices is a scalar matrix. (Contributed by AV, 25-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- E = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- S = ( N ScMat R )   =>    |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. S /\ Y e. S ) ) -> ( X ( +g ` A ) Y ) e. S )
Theorem	scmatsubcl 19540	The difference of two scalar matrices is a scalar matrix. (Contributed by AV, 20-Aug-2019.) (Revised by AV, 19-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- E = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- S = ( N ScMat R )   =>    |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. S /\ Y e. S ) ) -> ( X ( -g ` A ) Y ) e. S )
Theorem	scmatmulcl 19541	The product of two scalar matrices is a scalar matrix. (Contributed by AV, 21-Aug-2019.) (Revised by AV, 19-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- E = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- S = ( N ScMat R )   =>    |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. S /\ Y e. S ) ) -> ( X ( .r ` A ) Y ) e. S )
Theorem	scmatsgrp 19542	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.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- E = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- S = ( N ScMat R )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> S e. (SubGrp ` A ) )
Theorem	scmatsrng 19543	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.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- E = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- S = ( N ScMat R )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> S e. (SubRing ` A ) )
Theorem	scmatcrng 19544	The subring of scalar matrices (over a commutative ring) is a commutative ring. (Contributed by AV, 21-Aug-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- E = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- S = ( N ScMat R )   &    |- C = ( A ↾s S )   =>    |- ( ( N e. Fin /\ R e. CRing ) -> C e. CRing )
Theorem	scmatsgrp1 19545	The set of scalar matrices is a subgroup of the group/ring of diagonal matrices. (Contributed by AV, 21-Aug-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- E = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- S = ( N ScMat R )   &    |- D = ( N DMat R )   &    |- C = ( A ↾s D )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> S e. (SubGrp ` C ) )
Theorem	scmatsrng1 19546	The set of scalar matrices is a subring of the ring of diagonal matrices. (Contributed by AV, 21-Aug-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- E = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- S = ( N ScMat R )   &    |- D = ( N DMat R )   &    |- C = ( A ↾s D )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> S e. (SubRing ` C ) )
Theorem	smatvscl 19547	Closure of the scalar multiplication in the ring of scalar matrices. (matvscl 19454 analog.) (Contributed by AV, 24-Dec-2019.)
|- K = ( Base ` R )   &    |- A = ( N Mat R )   &    |- S = ( N ScMat R )   &    |- .* = ( .s ` A )   =>    |- ( ( ( N e. Fin /\ R e. Ring ) /\ ( C e. K /\ X e. S ) ) -> ( C .* X ) e. S )
Theorem	scmatlss 19548	The set of scalar matrices is a linear subspace of the matrix algebra. (Contributed by AV, 25-Dec-2019.)
|- A = ( N Mat R )   &    |- S = ( N ScMat R )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> S e. ( LSubSp ` A ) )
Theorem	scmatstrbas 19549	The set of scalar matrices is the base set of the ring of corresponding scalar matrices. (Contributed by AV, 26-Dec-2019.)
|- A = ( N Mat R )   &    |- C = ( N ScMat R )   &    |- S = ( A ↾s C )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> ( Base ` S ) = C )
Theorem	scmatrhmval 19550*	The value of the ring homomorphism F. (Contributed by AV, 22-Dec-2019.)
|- K = ( Base ` R )   &    |- A = ( N Mat R )   &    |- .1. = ( 1r ` A )   &    |- .* = ( .s ` A )   &    |- F = ( x e. K |-> ( x .* .1. ) )   =>    |- ( ( R e. V /\ X e. K ) -> ( F ` X ) = ( X .* .1. ) )
Theorem	scmatrhmcl 19551*	The value of the ring homomorphism F is a scalar matrix. (Contributed by AV, 22-Dec-2019.)
|- K = ( Base ` R )   &    |- A = ( N Mat R )   &    |- .1. = ( 1r ` A )   &    |- .* = ( .s ` A )   &    |- F = ( x e. K |-> ( x .* .1. ) )   &    |- C = ( N ScMat R )   =>    |- ( ( N e. Fin /\ R e. Ring /\ X e. K ) -> ( F ` X ) e. C )
Theorem	scmatf 19552*	There is a function from a ring to any ring of scalar matrices over this ring. (Contributed by AV, 25-Dec-2019.)
|- K = ( Base ` R )   &    |- A = ( N Mat R )   &    |- .1. = ( 1r ` A )   &    |- .* = ( .s ` A )   &    |- F = ( x e. K |-> ( x .* .1. ) )   &    |- C = ( N ScMat R )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> F : K --> C )
Theorem	scmatfo 19553*	There is a function from a ring onto any ring of scalar matrices over this ring. (Contributed by AV, 26-Dec-2019.)
|- K = ( Base ` R )   &    |- A = ( N Mat R )   &    |- .1. = ( 1r ` A )   &    |- .* = ( .s ` A )   &    |- F = ( x e. K |-> ( x .* .1. ) )   &    |- C = ( N ScMat R )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> F : K -onto-> C )
Theorem	scmatf1 19554*	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.)
|- K = ( Base ` R )   &    |- A = ( N Mat R )   &    |- .1. = ( 1r ` A )   &    |- .* = ( .s ` A )   &    |- F = ( x e. K |-> ( x .* .1. ) )   &    |- C = ( N ScMat R )   =>    |- ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> F : K -1-1-> C )
Theorem	scmatf1o 19555*	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.)
|- K = ( Base ` R )   &    |- A = ( N Mat R )   &    |- .1. = ( 1r ` A )   &    |- .* = ( .s ` A )   &    |- F = ( x e. K |-> ( x .* .1. ) )   &    |- C = ( N ScMat R )   =>    |- ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> F : K -1-1-onto-> C )
Theorem	scmatghm 19556*	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.)
|- K = ( Base ` R )   &    |- A = ( N Mat R )   &    |- .1. = ( 1r ` A )   &    |- .* = ( .s ` A )   &    |- F = ( x e. K |-> ( x .* .1. ) )   &    |- C = ( N ScMat R )   &    |- S = ( A ↾s C )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> F e. ( R GrpHom S ) )
Theorem	scmatmhm 19557*	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.)
|- K = ( Base ` R )   &    |- A = ( N Mat R )   &    |- .1. = ( 1r ` A )   &    |- .* = ( .s ` A )   &    |- F = ( x e. K |-> ( x .* .1. ) )   &    |- C = ( N ScMat R )   &    |- S = ( A ↾s C )   &    |- M = (mulGrp ` R )   &    |- T = (mulGrp ` S )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> F e. ( M MndHom T ) )
Theorem	scmatrhm 19558*	There is a ring homomorphism from a ring to the ring of scalar matrices over this ring. (Contributed by AV, 29-Dec-2019.)
|- K = ( Base ` R )   &    |- A = ( N Mat R )   &    |- .1. = ( 1r ` A )   &    |- .* = ( .s ` A )   &    |- F = ( x e. K |-> ( x .* .1. ) )   &    |- C = ( N ScMat R )   &    |- S = ( A ↾s C )   =>    |- ( ( N e. Fin /\ R e. Ring ) -> F e. ( R RingHom S ) )
Theorem	scmatrngiso 19559*	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.)
|- K = ( Base ` R )   &    |- A = ( N Mat R )   &    |- .1. = ( 1r ` A )   &    |- .* = ( .s ` A )   &    |- F = ( x e. K |-> ( x .* .1. ) )   &    |- C = ( N ScMat R )   &    |- S = ( A ↾s C )   =>    |- ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> F e. ( R RingIso S ) )
Theorem	scmatric 19560	A ring is isomorphic to every ring of scalar matrices over this ring with positive dimension. (Contributed by AV, 29-Dec-2019.)
|- A = ( N Mat R )   &    |- C = ( N ScMat R )   &    |- S = ( A ↾s C )   =>    |- ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> R ~=r S )
Theorem	mat0scmat 19561	The empty matrix over a ring is a scalar matrix (and therefore, by scmatdmat 19538, also a diagonal matrix). (Contributed by AV, 21-Dec-2019.)
|- ( R e. Ring -> (/) e. ( (/) ScMat R ) )
Theorem	mat1scmat 19562	A 1-dimensional matrix over a ring is always a scalar matrix (and therefore, by scmatdmat 19538, also a diagonal matrix). (Contributed by AV, 21-Dec-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   =>    |- ( ( N e. V /\ ( # ` N ) = 1 /\ R e. Ring ) -> ( M e. B -> M e. ( N ScMat R ) ) )
11.2.6  Multiplication of a matrix with a "column vector" The module of n-dimensional "column vectors" over a ring r is the n-dimensional free module over a ring r, which is the product of n -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 19407 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 19564 for the multiplication of a matrix with a column vector. In most cases, it is sufficient to regard members of ( ( Base ` R ) ^m N ) as "column vectors", because ( ( Base ` R ) ^m N ) is the base set of ( R freeLMod N ), see frlmbasmap 19320. See also the statements in [Lang] p. 508.
Syntax	cmvmul 19563	Syntax for the operator for the multiplication of a vector with a matrix.
class maVecMul
Definition	df-mvmul 19564*	The operator which multiplies an M x N -matrix with an N-dimensional vector. (Contributed by AV, 23-Feb-2019.)
|- maVecMul = ( r e. _V , o e. _V |-> [_ ( 1st ` o ) / m ]_ [_ ( 2nd ` o ) / n ]_ ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m n ) |-> ( i e. m |-> ( r gsumg ( j e. n |-> ( ( i x j ) ( .r ` r ) ( y ` j ) ) ) ) ) ) )
Theorem	mvmulfval 19565*	Functional value of the matrix vector multiplication operator. (Contributed by AV, 23-Feb-2019.)
|- .X. = ( R maVecMul <. M , N >. )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> R e. V )   &    |- ( ph -> M e. Fin )   &    |- ( ph -> N e. Fin )   =>    |- ( ph -> .X. = ( x e. ( B ^m ( M X. N ) ) , y e. ( B ^m N ) |-> ( i e. M |-> ( R gsumg ( j e. N |-> ( ( i x j ) .x. ( y ` j ) ) ) ) ) ) )
Theorem	mvmulval 19566*	Multiplication of a vector with a matrix. (Contributed by AV, 23-Feb-2019.)
|- .X. = ( R maVecMul <. M , N >. )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> R e. V )   &    |- ( ph -> M e. Fin )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> X e. ( B ^m ( M X. N ) ) )   &    |- ( ph -> Y e. ( B ^m N ) )   =>    |- ( ph -> ( X .X. Y ) = ( i e. M |-> ( R gsumg ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) ) ) )
Theorem	mvmulfv 19567*	A cell/element in the vector resulting from a multiplication of a vector with a matrix. (Contributed by AV, 23-Feb-2019.)
|- .X. = ( R maVecMul <. M , N >. )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> R e. V )   &    |- ( ph -> M e. Fin )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> X e. ( B ^m ( M X. N ) ) )   &    |- ( ph -> Y e. ( B ^m N ) )   &    |- ( ph -> I e. M )   =>    |- ( ph -> ( ( X .X. Y ) ` I ) = ( R gsumg ( j e. N |-> ( ( I X j ) .x. ( Y ` j ) ) ) ) )
Theorem	mavmulval 19568*	Multiplication of a vector with a square matrix. (Contributed by AV, 23-Feb-2019.)
|- A = ( N Mat R )   &    |- .X. = ( R maVecMul <. N , N >. )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> R e. V )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> X e. ( Base ` A ) )   &    |- ( ph -> Y e. ( B ^m N ) )   =>    |- ( ph -> ( X .X. Y ) = ( i e. N |-> ( R gsumg ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) ) ) )
Theorem	mavmulfv 19569*	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.)
|- A = ( N Mat R )   &    |- .X. = ( R maVecMul <. N , N >. )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> R e. V )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> X e. ( Base ` A ) )   &    |- ( ph -> Y e. ( B ^m N ) )   &    |- ( ph -> I e. N )   =>    |- ( ph -> ( ( X .X. Y ) ` I ) = ( R gsumg ( j e. N |-> ( ( I X j ) .x. ( Y ` j ) ) ) ) )
Theorem	mavmulcl 19570	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.)
|- A = ( N Mat R )   &    |- .X. = ( R maVecMul <. N , N >. )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> X e. ( Base ` A ) )   &    |- ( ph -> Y e. ( B ^m N ) )   =>    |- ( ph -> ( X .X. Y ) e. ( B ^m N ) )
Theorem	1mavmul 19571	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.)
|- A = ( N Mat R )   &    |- B = ( Base ` R )   &    |- .x. = ( R maVecMul <. N , N >. )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> Y e. ( B ^m N ) )   =>    |- ( ph -> ( ( 1r ` A ) .x. Y ) = Y )
Theorem	mavmulass 19572	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.)
|- A = ( N Mat R )   &    |- B = ( Base ` R )   &    |- .x. = ( R maVecMul <. N , N >. )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> Y e. ( B ^m N ) )   &    |- .X. = ( R maMul <. N , N , N >. )   &    |- ( ph -> X e. ( Base ` A ) )   &    |- ( ph -> Z e. ( Base ` A ) )   =>    |- ( ph -> ( ( X .X. Z ) .x. Y ) = ( X .x. ( Z .x. Y ) ) )
Theorem	mavmuldm 19573	The domain of the matrix vector multiplication function. (Contributed by AV, 27-Feb-2019.)
|- B = ( Base ` R )   &    |- C = ( B ^m ( M X. N ) )   &    |- D = ( B ^m N )   &    |- .x. = ( R maVecMul <. M , N >. )   =>    |- ( ( R e. V /\ M e. Fin /\ N e. Fin ) -> dom .x. = ( C X. D ) )
Theorem	mavmulsolcl 19574	Every solution of the equation A * X = Y for a matrix A and a vector B is a vector. (Contributed by AV, 27-Feb-2019.)
|- B = ( Base ` R )   &    |- C = ( B ^m ( M X. N ) )   &    |- D = ( B ^m N )   &    |- .x. = ( R maVecMul <. M , N >. )   &    |- E = ( B ^m M )   =>    |- ( ( ( M e. Fin /\ N e. Fin /\ M =/= (/) ) /\ ( R e. V /\ Y e. E ) ) -> ( ( A .x. X ) = Y -> X e. D ) )
Theorem	mavmul0 19575	Multiplication of a 0-dimensional matrix with a 0-dimensional vector. (Contributed by AV, 28-Feb-2019.)
|- .x. = ( R maVecMul <. N , N >. )   =>    |- ( ( N = (/) /\ R e. V ) -> ( (/) .x. (/) ) = (/) )
Theorem	mavmul0g 19576	The result of the 0-dimensional multiplication of a matrix with a vector is always the empty set. (Contributed by AV, 1-Mar-2019.)
|- .x. = ( R maVecMul <. N , N >. )   =>    |- ( ( N = (/) /\ R e. V ) -> ( X .x. Y ) = (/) )
Theorem	mvmumamul1 19577*	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.)
|- .X. = ( R maMul <. M , N , { (/) } >. )   &    |- .x. = ( R maVecMul <. M , N >. )   &    |- B = ( Base ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> M e. Fin )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> A e. ( B ^m ( M X. N ) ) )   &    |- ( ph -> Y e. ( B ^m N ) )   &    |- ( ph -> Z e. ( B ^m ( N X. { (/) } ) ) )   =>    |- ( ph -> ( A. j e. N ( Y ` j ) = ( j Z (/) ) -> A. i e. M ( ( A .x. Y ) ` i ) = ( i ( A .X. Z ) (/) ) ) )
Theorem	mavmumamul1 19578*	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.)
|- A = ( N Mat R )   &    |- .X. = ( R maMul <. N , N , { (/) } >. )   &    |- .x. = ( R maVecMul <. N , N >. )   &    |- B = ( Base ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> X e. ( Base ` A ) )   &    |- ( ph -> Y e. ( B ^m N ) )   &    |- ( ph -> Z e. ( B ^m ( N X. { (/) } ) ) )   =>    |- ( ph -> ( A. j e. N ( Y ` j ) = ( j Z (/) ) -> A. i e. N ( ( X .x. Y ) ` i ) = ( i ( X .X. Z ) (/) ) ) )
11.2.7  Replacement functions for a square matrix
Syntax	cmarrep 19579	Syntax for the row replacing function for a square matrix.
class matRRep
Syntax	cmatrepV 19580	Syntax for the function replacing a column of a matrix by a vector.
class matRepV
Definition	df-marrep 19581*	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 = ( n e. _V , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) , s e. ( Base ` r ) |-> ( k e. n , l e. n |-> ( i e. n , j e. n |-> if ( i = k , if ( j = l , s , ( 0g ` r ) ) , ( i m j ) ) ) ) ) )
Definition	df-marepv 19582*	Function replacing a column of a matrix by a vector. (Contributed by AV, 9-Feb-2019.) (Revised by AV, 26-Feb-2019.)
|- matRepV = ( n e. _V , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) , v e. ( ( Base ` r ) ^m n ) |-> ( k e. n |-> ( i e. n , j e. n |-> if ( j = k , ( v ` i ) , ( i m j ) ) ) ) ) )
Theorem	marrepfval 19583*	First substitution for the definition of the matrix row replacement function. (Contributed by AV, 12-Feb-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- Q = ( N matRRep R )   &    |- .0. = ( 0g ` R )   =>    |- Q = ( m e. B , s e. ( Base ` R ) |-> ( k e. N , l e. N |-> ( i e. N , j e. N |-> if ( i = k , if ( j = l , s , .0. ) , ( i m j ) ) ) ) )
Theorem	marrepval0 19584*	Second substitution for the definition of the matrix row replacement function. (Contributed by AV, 12-Feb-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- Q = ( N matRRep R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( M e. B /\ S e. ( Base ` R ) ) -> ( M Q S ) = ( k e. N , l e. N |-> ( i e. N , j e. N |-> if ( i = k , if ( j = l , S , .0. ) , ( i M j ) ) ) ) )
Theorem	marrepval 19585*	Third substitution for the definition of the matrix row replacement function. (Contributed by AV, 12-Feb-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- Q = ( N matRRep R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( ( M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) ) -> ( K ( M Q S ) L ) = ( i e. N , j e. N |-> if ( i = K , if ( j = L , S , .0. ) , ( i M j ) ) ) )
Theorem	marrepeval 19586	An entry of a matrix with a replaced row. (Contributed by AV, 12-Feb-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- Q = ( N matRRep R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( ( M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) /\ ( I e. N /\ J e. N ) ) -> ( I ( K ( M Q S ) L ) J ) = if ( I = K , if ( J = L , S , .0. ) , ( I M J ) ) )
Theorem	marrepcl 19587	Closure of the row replacement function for square matrices. (Contributed by AV, 13-Feb-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   =>    |- ( ( ( R e. Ring /\ M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) ) -> ( K ( M ( N matRRep R ) S ) L ) e. B )
Theorem	marepvfval 19588*	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.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- Q = ( N matRepV R )   &    |- V = ( ( Base ` R ) ^m N )   =>    |- Q = ( m e. B , v e. V |-> ( k e. N |-> ( i e. N , j e. N |-> if ( j = k , ( v ` i ) , ( i m j ) ) ) ) )
Theorem	marepvval0 19589*	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.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- Q = ( N matRepV R )   &    |- V = ( ( Base ` R ) ^m N )   =>    |- ( ( M e. B /\ C e. V ) -> ( M Q C ) = ( k e. N |-> ( i e. N , j e. N |-> if ( j = k , ( C ` i ) , ( i M j ) ) ) ) )
Theorem	marepvval 19590*	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.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- Q = ( N matRepV R )   &    |- V = ( ( Base ` R ) ^m N )   =>    |- ( ( M e. B /\ C e. V /\ K e. N ) -> ( ( M Q C ) ` K ) = ( i e. N , j e. N |-> if ( j = K , ( C ` i ) , ( i M j ) ) ) )
Theorem	marepveval 19591	An entry of a matrix with a replaced column. (Contributed by AV, 14-Feb-2019.) (Revised by AV, 26-Feb-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- Q = ( N matRepV R )   &    |- V = ( ( Base ` R ) ^m N )   =>    |- ( ( ( M e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) -> ( I ( ( M Q C ) ` K ) J ) = if ( J = K , ( C ` I ) , ( I M J ) ) )
Theorem	marepvcl 19592	Closure of the column replacement function for square matrices. (Contributed by AV, 14-Feb-2019.) (Revised by AV, 26-Feb-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- V = ( ( Base ` R ) ^m N )   =>    |- ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) -> ( ( M ( N matRepV R ) C ) ` K ) e. B )
Theorem	ma1repvcl 19593	Closure of the column replacement function for identity matrices. (Contributed by AV, 15-Feb-2019.) (Revised by AV, 26-Feb-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- V = ( ( Base ` R ) ^m N )   &    |- .1. = ( 1r ` A )   =>    |- ( ( ( R e. Ring /\ N e. Fin ) /\ ( C e. V /\ K e. N ) ) -> ( ( .1. ( N matRepV R ) C ) ` K ) e. B )
Theorem	ma1repveval 19594	An entry of an identity matrix with a replaced column. (Contributed by AV, 16-Feb-2019.) (Revised by AV, 26-Feb-2019.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- V = ( ( Base ` R ) ^m N )   &    |- .1. = ( 1r ` A )   &    |- .0. = ( 0g ` R )   &    |- E = ( ( .1. ( N matRepV R ) C ) ` K )   =>    |- ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) -> ( I E J ) = if ( J = K , ( C ` I ) , if ( J = I , ( 1r ` R ) , .0. ) ) )
Theorem	mulmarep1el 19595	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.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- V = ( ( Base ` R ) ^m N )   &    |- .1. = ( 1r ` A )   &    |- .0. = ( 0g ` R )   &    |- E = ( ( .1. ( N matRepV R ) C ) ` K )   =>    |- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ L e. N ) ) -> ( ( I X L ) ( .r ` R ) ( L E J ) ) = if ( J = K , ( ( I X L ) ( .r ` R ) ( C ` L ) ) , if ( J = L , ( I X L ) , .0. ) ) )
Theorem	mulmarep1gsum1 19596*	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.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- V = ( ( Base ` R ) ^m N )   &    |- .1. = ( 1r ` A )   &    |- .0. = ( 0g ` R )   &    |- E = ( ( .1. ( N matRepV R ) C ) ` K )   =>    |- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) -> ( R gsumg ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) ) = ( I X J ) )
Theorem	mulmarep1gsum2 19597*	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.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- V = ( ( Base ` R ) ^m N )   &    |- .1. = ( 1r ` A )   &    |- .0. = ( 0g ` R )   &    |- E = ( ( .1. ( N matRepV R ) C ) ` K )   &    |- .X. = ( R maVecMul <. N , N >. )   =>    |- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) -> ( R gsumg ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) ) = if ( J = K , ( Z ` I ) , ( I X J ) ) )
Theorem	1marepvmarrepid 19598	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.)
|- V = ( ( Base ` R ) ^m N )   &    |- .1. = ( 1r ` ( N Mat R ) )   &    |- X = ( ( .1. ( N matRepV R ) Z ) ` I )   =>    |- ( ( ( R e. Ring /\ N e. Fin ) /\ ( I e. N /\ Z e. V ) ) -> ( I ( X ( N matRRep R ) ( Z ` I ) ) I ) = X )
11.2.8  Submatrices
Syntax	csubma 19599	Syntax for submatrices of a square matrix.
class subMat
Definition	df-subma 19600*	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 = ( n e. _V , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) |-> ( k e. n , l e. n |-> ( i e. ( n \ { k } ) , j e. ( n \ { l } ) |-> ( i m j ) ) ) ) )