P. 219 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21801-21900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	oftpos 21801	The transposition of the value of a function operation for two functions is the value of the function operation for the two functions transposed. (Contributed by Stefan O'Rear, 17-Jul-2018.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → tpos (𝐹 ∘f 𝑅𝐺) = (tpos 𝐹 ∘f 𝑅tpos 𝐺))
Theorem	mattposcl 21802	The transpose of a square matrix is a square matrix of the same size. (Contributed by SO, 9-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ (𝑀 ∈ 𝐵 → tpos 𝑀 ∈ 𝐵)
Theorem	mattpostpos 21803	The transpose of the transpose of a square matrix is the square matrix itself. (Contributed by SO, 17-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ (𝑀 ∈ 𝐵 → tpos tpos 𝑀 = 𝑀)
Theorem	mattposvs 21804	The transposition of a matrix multiplied with a scalar equals the transposed matrix multiplied with the scalar, see also the statement in [Lang] p. 505. (Contributed by Stefan O'Rear, 17-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝐴)    ⇒   ⊢ ((𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵) → tpos (𝑋 · 𝑌) = (𝑋 · tpos 𝑌))
Theorem	mattpos1 21805	The transposition of the identity matrix is the identity matrix. (Contributed by Stefan O'Rear, 17-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 1 = (1r‘𝐴)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → tpos 1 = 1 )
Theorem	tposmap 21806	The transposition of an I X J -matrix is a J X I -matrix, see also the statement in [Lang] p. 505. (Contributed by Stefan O'Rear, 9-Jul-2018.)
⊢ (𝐴 ∈ (𝐵 ↑m (𝐼 × 𝐽)) → tpos 𝐴 ∈ (𝐵 ↑m (𝐽 × 𝐼)))
Theorem	mamutpos 21807	Behavior of transposes in matrix products, see also the statement in [Lang] p. 505. (Contributed by Stefan O'Rear, 9-Jul-2018.)
⊢ 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑃⟩)    &   ⊢ 𝐺 = (𝑅 maMul ⟨𝑃, 𝑁, 𝑀⟩)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑃)))    ⇒   ⊢ (𝜑 → tpos (𝑋𝐹𝑌) = (tpos 𝑌𝐺tpos 𝑋))
Theorem	mattposm 21808	Multiplying two transposed matrices results in the transposition of the product of the two matrices. (Contributed by Stefan O'Rear, 17-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = (.r‘𝐴)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → tpos (𝑋 · 𝑌) = (tpos 𝑌 · tpos 𝑋))
Theorem	matgsumcl 21809*	Closure of a group sum over the diagonal coefficients of a square matrix over a commutative ring. (Contributed by AV, 29-Dec-2018.) (Proof shortened by AV, 23-Jul-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑈 = (mulGrp‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑈 Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑀𝑟))) ∈ (Base‘𝑅))
Theorem	madetsumid 21810*	The identity summand in the Leibniz' formula of a determinant for a square matrix over a commutative ring. (Contributed by AV, 29-Dec-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑈 = (mulGrp‘𝑅)    &   ⊢ 𝑌 = (ℤRHom‘𝑅)    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑃 = ( I ↾ 𝑁)) → (((𝑌 ∘ 𝑆)‘𝑃) · (𝑈 Σg (𝑟 ∈ 𝑁 ↦ ((𝑃‘𝑟)𝑀𝑟)))) = (𝑈 Σg (𝑟 ∈ 𝑁 ↦ (𝑟𝑀𝑟))))
Theorem	matepmcl 21811*	Each entry of a matrix with an index as permutation of the other is an element of the underlying ring. (Contributed by AV, 1-Jan-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵) → ∀𝑛 ∈ 𝑁 ((𝑄‘𝑛)𝑀𝑛) ∈ (Base‘𝑅))
Theorem	matepm2cl 21812*	Each entry of a matrix with an index as permutation of the other is an element of the underlying ring. (Contributed by AV, 1-Jan-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵) → ∀𝑛 ∈ 𝑁 (𝑛𝑀(𝑄‘𝑛)) ∈ (Base‘𝑅))
Theorem	madetsmelbas 21813*	A summand of the determinant of a matrix belongs to the underlying ring. (Contributed by AV, 1-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ 𝑌 = (ℤRHom‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑄 ∈ 𝑃) → (((𝑌 ∘ 𝑆)‘𝑄)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛)))) ∈ (Base‘𝑅))
Theorem	madetsmelbas2 21814*	A summand of the determinant of a matrix belongs to the underlying ring. (Contributed by AV, 1-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ 𝑌 = (ℤRHom‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐺 = (mulGrp‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑄 ∈ 𝑃) → (((𝑌 ∘ 𝑆)‘𝑄)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ 𝑁 ↦ (𝑛𝑀(𝑄‘𝑛))))) ∈ (Base‘𝑅))
11.4.4  Matrices of dimension 0 and 1 As already mentioned before, and shown in mat0dimbas0 21815, the empty set is the sole zero-dimensional matrix (also called "empty matrix", see Wikipedia https://en.wikipedia.org/wiki/Matrix_(mathematics)#Empty_matrices). 21815 In the following, some properties of the empty matrix are shown, especially that the empty matrix over an arbitrary ring forms a commutative ring, see mat0dimcrng 21819. For the one-dimensional case, it can be shown that a ring of matrices with dimension 1 is isomorphic to the underlying ring, see mat1ric 21836.
Theorem	mat0dimbas0 21815	The empty set is the one and only matrix of dimension 0, called "the empty matrix". (Contributed by AV, 27-Feb-2019.)
⊢ (𝑅 ∈ 𝑉 → (Base‘(∅ Mat 𝑅)) = {∅})
Theorem	mat0dim0 21816	The zero of the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019.)
⊢ 𝐴 = (∅ Mat 𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (0g‘𝐴) = ∅)
Theorem	mat0dimid 21817	The identity of the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019.)
⊢ 𝐴 = (∅ Mat 𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (1r‘𝐴) = ∅)
Theorem	mat0dimscm 21818	The scalar multiplication in the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019.)
⊢ 𝐴 = (∅ Mat 𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (Base‘𝑅)) → (𝑋( ·𝑠 ‘𝐴)∅) = ∅)
Theorem	mat0dimcrng 21819	The algebra of matrices with dimension 0 (over an arbitrary ring!) is a commutative ring. (Contributed by AV, 10-Aug-2019.)
⊢ 𝐴 = (∅ Mat 𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → 𝐴 ∈ CRing)
Theorem	mat1dimelbas 21820*	A matrix with dimension 1 is an ordered pair with an ordered pair (of the one and only pair of indices) as first component. (Contributed by AV, 15-Aug-2019.)
⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀 ∈ (Base‘𝐴) ↔ ∃𝑟 ∈ 𝐵 𝑀 = {⟨𝑂, 𝑟⟩}))
Theorem	mat1dimbas 21821	A matrix with dimension 1 is an ordered pair with an ordered pair (of the one and only pair of indices) as first component. (Contributed by AV, 15-Aug-2019.)
⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → {⟨𝑂, 𝑋⟩} ∈ (Base‘𝐴))
Theorem	mat1dim0 21822	The zero of the algebra of matrices with dimension 1. (Contributed by AV, 15-Aug-2019.)
⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (0g‘𝐴) = {⟨𝑂, (0g‘𝑅)⟩})
Theorem	mat1dimid 21823	The identity of the algebra of matrices with dimension 1. (Contributed by AV, 15-Aug-2019.)
⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (1r‘𝐴) = {⟨𝑂, (1r‘𝑅)⟩})
Theorem	mat1dimscm 21824	The scalar multiplication in the algebra of matrices with dimension 1. (Contributed by AV, 16-Aug-2019.)
⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    ⇒   ⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋( ·𝑠 ‘𝐴){⟨𝑂, 𝑌⟩}) = {⟨𝑂, (𝑋(.r‘𝑅)𝑌)⟩})
Theorem	mat1dimmul 21825	The ring multiplication in the algebra of matrices with dimension 1. (Contributed by AV, 16-Aug-2019.) (Proof shortened by AV, 18-Apr-2021.)
⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    ⇒   ⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ({⟨𝑂, 𝑋⟩} (.r‘𝐴){⟨𝑂, 𝑌⟩}) = {⟨𝑂, (𝑋(.r‘𝑅)𝑌)⟩})
Theorem	mat1dimcrng 21826	The algebra of matrices with dimension 1 over a commutative ring is a commutative ring. (Contributed by AV, 16-Aug-2019.)
⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝐸 ∈ 𝑉) → 𝐴 ∈ CRing)
Theorem	mat1f1o 21827*	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.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {⟨𝑂, 𝑥⟩})    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝐹:𝐾–1-1-onto→𝐵)
Theorem	mat1rhmval 21828*	The value of the ring homomorphism 𝐹. (Contributed by AV, 22-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {⟨𝑂, 𝑥⟩})    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾) → (𝐹‘𝑋) = {⟨𝑂, 𝑋⟩})
Theorem	mat1rhmelval 21829*	The value of the ring homomorphism 𝐹. (Contributed by AV, 22-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {⟨𝑂, 𝑥⟩})    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾) → (𝐸(𝐹‘𝑋)𝐸) = 𝑋)
Theorem	mat1rhmcl 21830*	The value of the ring homomorphism 𝐹 is a matrix with dimension 1. (Contributed by AV, 22-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {⟨𝑂, 𝑥⟩})    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾) → (𝐹‘𝑋) ∈ 𝐵)
Theorem	mat1f 21831*	There is a function from a ring to the ring of matrices with dimension 1 over this ring. (Contributed by AV, 22-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {⟨𝑂, 𝑥⟩})    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝐹:𝐾⟶𝐵)
Theorem	mat1ghm 21832*	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.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {⟨𝑂, 𝑥⟩})    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝐹 ∈ (𝑅 GrpHom 𝐴))
Theorem	mat1mhm 21833*	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.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {⟨𝑂, 𝑥⟩})    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑁 = (mulGrp‘𝐴)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝐹 ∈ (𝑀 MndHom 𝑁))
Theorem	mat1rhm 21834*	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.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {⟨𝑂, 𝑥⟩})    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝐹 ∈ (𝑅 RingHom 𝐴))
Theorem	mat1rngiso 21835*	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.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {⟨𝑂, 𝑥⟩})    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝐹 ∈ (𝑅 RingIso 𝐴))
Theorem	mat1ric 21836	A ring is isomorphic to the ring of matrices with dimension 1 over this ring. (Contributed by AV, 30-Dec-2019.)
⊢ 𝐴 = ({𝐸} Mat 𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝑅 ≃𝑟 𝐴)
11.4.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 𝜆 ∗ 𝐼 of the identity matrix 𝐼. Its effect on a vector is scalar multiplication by 𝜆 [see scmatscm 21862!]". 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 21839 and df-scmat 21840), basic properties of (elements of) these sets, and theorems showing that the diagonal matrices form a subring of the ring of square matrices (dmatsrng 21850), that the scalar matrices form a subring of the ring of square matrices (scmatsrng 21869), that the scalar matrices form a subring of the ring of diagonal matrices (scmatsrng1 21872) and that the ring of scalar matrices over a commutative ring is a commutative ring (scmatcrng 21870).
Syntax	cdmat 21837	Extend class notation for the algebra of diagonal matrices.
class DMat
Syntax	cscmat 21838	Extend class notation for the algebra of scalar matrices.
class ScMat
Definition	df-dmat 21839*	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 = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = (0g‘𝑟))})
Definition	df-scmat 21840*	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 = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌{𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠 ‘𝑎)(1r‘𝑎))})
Theorem	dmatval 21841*	The set of 𝑁 x 𝑁 diagonal matrices over (a ring) 𝑅. (Contributed by AV, 8-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (𝑁 DMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝐷 = {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = 0 )})
Theorem	dmatel 21842*	A 𝑁 x 𝑁 diagonal matrix over (a ring) 𝑅. (Contributed by AV, 18-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (𝑁 DMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑀 ∈ 𝐷 ↔ (𝑀 ∈ 𝐵 ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ))))
Theorem	dmatmat 21843	An 𝑁 x 𝑁 diagonal matrix over (the ring) 𝑅 is an 𝑁 x 𝑁 matrix over (the ring) 𝑅. (Contributed by AV, 18-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (𝑁 DMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑀 ∈ 𝐷 → 𝑀 ∈ 𝐵))
Theorem	dmatid 21844	The identity matrix is a diagonal matrix. (Contributed by AV, 19-Aug-2019.) (Revised by AV, 18-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (𝑁 DMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (1r‘𝐴) ∈ 𝐷)
Theorem	dmatelnd 21845	An extradiagonal entry of a diagonal matrix is equal to zero. (Contributed by AV, 19-Aug-2019.) (Revised by AV, 18-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (𝑁 DMat 𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐷) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐼 ≠ 𝐽)) → (𝐼𝑋𝐽) = 0 )
Theorem	dmatmul 21846*	The product of two diagonal matrices. (Contributed by AV, 19-Aug-2019.) (Revised by AV, 18-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (𝑁 DMat 𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) → (𝑋(.r‘𝐴)𝑌) = (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ if(𝑥 = 𝑦, ((𝑥𝑋𝑦)(.r‘𝑅)(𝑥𝑌𝑦)), 0 )))
Theorem	dmatsubcl 21847	The difference of two diagonal matrices is a diagonal matrix. (Contributed by AV, 19-Aug-2019.) (Revised by AV, 18-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (𝑁 DMat 𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) → (𝑋(-g‘𝐴)𝑌) ∈ 𝐷)
Theorem	dmatsgrp 21848	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.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (𝑁 DMat 𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → 𝐷 ∈ (SubGrp‘𝐴))
Theorem	dmatmulcl 21849	The product of two diagonal matrices is a diagonal matrix. (Contributed by AV, 20-Aug-2019.) (Revised by AV, 18-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (𝑁 DMat 𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷)) → (𝑋(.r‘𝐴)𝑌) ∈ 𝐷)
Theorem	dmatsrng 21850	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.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (𝑁 DMat 𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → 𝐷 ∈ (SubRing‘𝐴))
Theorem	dmatcrng 21851	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.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (𝑁 DMat 𝑅)    &   ⊢ 𝐶 = (𝐴 ↾s 𝐷)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → 𝐶 ∈ CRing)
Theorem	dmatscmcl 21852	The multiplication of a diagonal matrix with a scalar is a diagonal matrix. (Contributed by AV, 19-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    &   ⊢ 𝐷 = (𝑁 DMat 𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐷)) → (𝐶 ∗ 𝑀) ∈ 𝐷)
Theorem	scmatval 21853*	The set of 𝑁 x 𝑁 scalar matrices over (a ring) 𝑅. (Contributed by AV, 18-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐴)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑆 = {𝑚 ∈ 𝐵 ∣ ∃𝑐 ∈ 𝐾 𝑚 = (𝑐 · 1 )})
Theorem	scmatel 21854*	An 𝑁 x 𝑁 scalar matrix over (a ring) 𝑅. (Contributed by AV, 18-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐴)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑀 ∈ 𝑆 ↔ (𝑀 ∈ 𝐵 ∧ ∃𝑐 ∈ 𝐾 𝑀 = (𝑐 · 1 ))))
Theorem	scmatscmid 21855*	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.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐴)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆) → ∃𝑐 ∈ 𝐾 𝑀 = (𝑐 · 1 ))
Theorem	scmatscmide 21856	An entry of a scalar matrix expressed as a multiplication of a scalar with the identity matrix. (Contributed by AV, 30-Oct-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝐶 ∗ 1 )𝐽) = if(𝐼 = 𝐽, 𝐶, 0 ))
Theorem	scmatscmiddistr 21857	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.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    &   ⊢ · = (.r‘𝑅)    &   ⊢ × = (.r‘𝐴)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵)) → ((𝑆 ∗ 1 ) × (𝑇 ∗ 1 )) = ((𝑆 · 𝑇) ∗ 1 ))
Theorem	scmatmat 21858	An 𝑁 x 𝑁 scalar matrix over (the ring) 𝑅 is an 𝑁 x 𝑁 matrix over (the ring) 𝑅. (Contributed by AV, 18-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑀 ∈ 𝑆 → 𝑀 ∈ 𝐵))
Theorem	scmate 21859*	An entry of an 𝑁 x 𝑁 scalar matrix over the ring 𝑅. (Contributed by AV, 18-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → ∃𝑐 ∈ 𝐾 (𝐼𝑀𝐽) = if(𝐼 = 𝐽, 𝑐, 0 ))
Theorem	scmatmats 21860*	The set of an 𝑁 x 𝑁 scalar matrices over the ring 𝑅 expressed as a subset of 𝑁 x 𝑁 matrices over the ring 𝑅 with certain properties for their entries. (Contributed by AV, 31-Oct-2019.) (Revised by AV, 19-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑆 = {𝑚 ∈ 𝐵 ∣ ∃𝑐 ∈ 𝐾 ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, 0 )})
Theorem	scmateALT 21861*	Alternate proof of scmate 21859: An entry of an 𝑁 x 𝑁 scalar matrix over the ring 𝑅. This prove makes use of scmatmats 21860 but is longer and requires more distinct variables. (Contributed by AV, 19-Dec-2019.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → ∃𝑐 ∈ 𝐾 (𝐼𝑀𝐽) = if(𝐼 = 𝐽, 𝑐, 0 ))
Theorem	scmatscm 21862*	The multiplication of a matrix with a scalar matrix corresponds to a scalar multiplication. (Contributed by AV, 28-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    &   ⊢ × = (.r‘𝐴)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐶 ∈ 𝑆) → ∃𝑐 ∈ 𝐾 ∀𝑚 ∈ 𝐵 (𝐶 × 𝑚) = (𝑐 ∗ 𝑚))
Theorem	scmatid 21863	The identity matrix is a scalar matrix. (Contributed by AV, 20-Aug-2019.) (Revised by AV, 18-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (1r‘𝐴) ∈ 𝑆)
Theorem	scmatdmat 21864	A scalar matrix is a diagonal matrix. (Contributed by AV, 20-Aug-2019.) (Revised by AV, 19-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑅)    &   ⊢ 𝐷 = (𝑁 DMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑀 ∈ 𝑆 → 𝑀 ∈ 𝐷))
Theorem	scmataddcl 21865	The sum of two scalar matrices is a scalar matrix. (Contributed by AV, 25-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆)) → (𝑋(+g‘𝐴)𝑌) ∈ 𝑆)
Theorem	scmatsubcl 21866	The difference of two scalar matrices is a scalar matrix. (Contributed by AV, 20-Aug-2019.) (Revised by AV, 19-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆)) → (𝑋(-g‘𝐴)𝑌) ∈ 𝑆)
Theorem	scmatmulcl 21867	The product of two scalar matrices is a scalar matrix. (Contributed by AV, 21-Aug-2019.) (Revised by AV, 19-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆)) → (𝑋(.r‘𝐴)𝑌) ∈ 𝑆)
Theorem	scmatsgrp 21868	The set of scalar matrices is a subgroup of the matrix group/algebra. (Contributed by AV, 20-Aug-2019.) (Revised by AV, 19-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑆 ∈ (SubGrp‘𝐴))
Theorem	scmatsrng 21869	The set of scalar matrices is a subring of the matrix ring/algebra. (Contributed by AV, 21-Aug-2019.) (Revised by AV, 19-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑆 ∈ (SubRing‘𝐴))
Theorem	scmatcrng 21870	The subring of scalar matrices (over a commutative ring) is a commutative ring. (Contributed by AV, 21-Aug-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑅)    &   ⊢ 𝐶 = (𝐴 ↾s 𝑆)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐶 ∈ CRing)
Theorem	scmatsgrp1 21871	The set of scalar matrices is a subgroup of the group/ring of diagonal matrices. (Contributed by AV, 21-Aug-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑅)    &   ⊢ 𝐷 = (𝑁 DMat 𝑅)    &   ⊢ 𝐶 = (𝐴 ↾s 𝐷)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑆 ∈ (SubGrp‘𝐶))
Theorem	scmatsrng1 21872	The set of scalar matrices is a subring of the ring of diagonal matrices. (Contributed by AV, 21-Aug-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐸 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑅)    &   ⊢ 𝐷 = (𝑁 DMat 𝑅)    &   ⊢ 𝐶 = (𝐴 ↾s 𝐷)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑆 ∈ (SubRing‘𝐶))
Theorem	smatvscl 21873	Closure of the scalar multiplication in the ring of scalar matrices. (matvscl 21780 analog.) (Contributed by AV, 24-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑅)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑆)) → (𝐶 ∗ 𝑋) ∈ 𝑆)
Theorem	scmatlss 21874	The set of scalar matrices is a linear subspace of the matrix algebra. (Contributed by AV, 25-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑆 ∈ (LSubSp‘𝐴))
Theorem	scmatstrbas 21875	The set of scalar matrices is the base set of the ring of corresponding scalar matrices. (Contributed by AV, 26-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐶 = (𝑁 ScMat 𝑅)    &   ⊢ 𝑆 = (𝐴 ↾s 𝐶)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (Base‘𝑆) = 𝐶)
Theorem	scmatrhmval 21876*	The value of the ring homomorphism 𝐹. (Contributed by AV, 22-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ (𝑥 ∗ 1 ))    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾) → (𝐹‘𝑋) = (𝑋 ∗ 1 ))
Theorem	scmatrhmcl 21877*	The value of the ring homomorphism 𝐹 is a scalar matrix. (Contributed by AV, 22-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ (𝑥 ∗ 1 ))    &   ⊢ 𝐶 = (𝑁 ScMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾) → (𝐹‘𝑋) ∈ 𝐶)
Theorem	scmatf 21878*	There is a function from a ring to any ring of scalar matrices over this ring. (Contributed by AV, 25-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ (𝑥 ∗ 1 ))    &   ⊢ 𝐶 = (𝑁 ScMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐹:𝐾⟶𝐶)
Theorem	scmatfo 21879*	There is a function from a ring onto any ring of scalar matrices over this ring. (Contributed by AV, 26-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ (𝑥 ∗ 1 ))    &   ⊢ 𝐶 = (𝑁 ScMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐹:𝐾–onto→𝐶)
Theorem	scmatf1 21880*	There is a 1-1 function from a ring to any ring of scalar matrices with positive dimension over this ring. (Contributed by AV, 25-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ (𝑥 ∗ 1 ))    &   ⊢ 𝐶 = (𝑁 ScMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring) → 𝐹:𝐾–1-1→𝐶)
Theorem	scmatf1o 21881*	There is a bijection between a ring and any ring of scalar matrices with positive dimension over this ring. (Contributed by AV, 26-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ (𝑥 ∗ 1 ))    &   ⊢ 𝐶 = (𝑁 ScMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring) → 𝐹:𝐾–1-1-onto→𝐶)
Theorem	scmatghm 21882*	There is a group homomorphism from the additive group of a ring to the additive group of the ring of scalar matrices over this ring. (Contributed by AV, 22-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ (𝑥 ∗ 1 ))    &   ⊢ 𝐶 = (𝑁 ScMat 𝑅)    &   ⊢ 𝑆 = (𝐴 ↾s 𝐶)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
Theorem	scmatmhm 21883*	There is a monoid homomorphism from the multiplicative group of a ring to the multiplicative group of the ring of scalar matrices over this ring. (Contributed by AV, 29-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ (𝑥 ∗ 1 ))    &   ⊢ 𝐶 = (𝑁 ScMat 𝑅)    &   ⊢ 𝑆 = (𝐴 ↾s 𝐶)    &   ⊢ 𝑀 = (mulGrp‘𝑅)    &   ⊢ 𝑇 = (mulGrp‘𝑆)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐹 ∈ (𝑀 MndHom 𝑇))
Theorem	scmatrhm 21884*	There is a ring homomorphism from a ring to the ring of scalar matrices over this ring. (Contributed by AV, 29-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ (𝑥 ∗ 1 ))    &   ⊢ 𝐶 = (𝑁 ScMat 𝑅)    &   ⊢ 𝑆 = (𝐴 ↾s 𝐶)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐹 ∈ (𝑅 RingHom 𝑆))
Theorem	scmatrngiso 21885*	There is a ring isomorphism from a ring to the ring of scalar matrices over this ring with positive dimension. (Contributed by AV, 29-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ (𝑥 ∗ 1 ))    &   ⊢ 𝐶 = (𝑁 ScMat 𝑅)    &   ⊢ 𝑆 = (𝐴 ↾s 𝐶)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring) → 𝐹 ∈ (𝑅 RingIso 𝑆))
Theorem	scmatric 21886	A ring is isomorphic to every ring of scalar matrices over this ring with positive dimension. (Contributed by AV, 29-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐶 = (𝑁 ScMat 𝑅)    &   ⊢ 𝑆 = (𝐴 ↾s 𝐶)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring) → 𝑅 ≃𝑟 𝑆)
Theorem	mat0scmat 21887	The empty matrix over a ring is a scalar matrix (and therefore, by scmatdmat 21864, also a diagonal matrix). (Contributed by AV, 21-Dec-2019.)
⊢ (𝑅 ∈ Ring → ∅ ∈ (∅ ScMat 𝑅))
Theorem	mat1scmat 21888	A 1-dimensional matrix over a ring is always a scalar matrix (and therefore, by scmatdmat 21864, also a diagonal matrix). (Contributed by AV, 21-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ ((𝑁 ∈ 𝑉 ∧ (♯‘𝑁) = 1 ∧ 𝑅 ∈ Ring) → (𝑀 ∈ 𝐵 → 𝑀 ∈ (𝑁 ScMat 𝑅)))
11.4.6  Multiplication of a matrix with a "column vector" The module of 𝑛-dimensional "column vectors" over a ring 𝑟 is the 𝑛-dimensional free module over a ring 𝑟, which is the product of 𝑛 -many copies of the ring with componentwise addition and multiplication. Although a "column vector" could also be defined as n x 1 -matrix (according to Wikipedia "Row and column vectors", 22-Feb-2019, https://en.wikipedia.org/wiki/Row_and_column_vectors: "In linear algebra, a column vector [... ] is an m x 1 matrix, that is, a matrix consisting of a single column of m elements"), which would allow for using the matrix multiplication df-mamu 21733 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 21890 for the multiplication of a matrix with a column vector. In most cases, it is sufficient to regard members of ((Base‘𝑅) ↑m 𝑁) as "column vectors", because ((Base‘𝑅) ↑m 𝑁) is the base set of (𝑅 freeLMod 𝑁), see frlmbasmap 21165. See also the statements in [Lang] p. 508.
Syntax	cmvmul 21889	Syntax for the operator for the multiplication of a vector with a matrix.
class maVecMul
Definition	df-mvmul 21890*	The operator which multiplies an M x N -matrix with an N-dimensional vector. (Contributed by AV, 23-Feb-2019.)
⊢ maVecMul = (𝑟 ∈ V, 𝑜 ∈ V ↦ ⦋(1st ‘𝑜) / 𝑚⦌⦋(2nd ‘𝑜) / 𝑛⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑖 ∈ 𝑚 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗)))))))
Theorem	mvmulfval 21891*	Functional value of the matrix vector multiplication operator. (Contributed by AV, 23-Feb-2019.)
⊢ × = (𝑅 maVecMul ⟨𝑀, 𝑁⟩)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    ⇒   ⊢ (𝜑 → × = (𝑥 ∈ (𝐵 ↑m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑m 𝑁) ↦ (𝑖 ∈ 𝑀 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑦‘𝑗)))))))
Theorem	mvmulval 21892*	Multiplication of a vector with a matrix. (Contributed by AV, 23-Feb-2019.)
⊢ × = (𝑅 maVecMul ⟨𝑀, 𝑁⟩)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m 𝑁))    ⇒   ⊢ (𝜑 → (𝑋 × 𝑌) = (𝑖 ∈ 𝑀 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗) · (𝑌‘𝑗))))))
Theorem	mvmulfv 21893*	A cell/element in the vector resulting from a multiplication of a vector with a matrix. (Contributed by AV, 23-Feb-2019.)
⊢ × = (𝑅 maVecMul ⟨𝑀, 𝑁⟩)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m 𝑁))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑀)    ⇒   ⊢ (𝜑 → ((𝑋 × 𝑌)‘𝐼) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝐼𝑋𝑗) · (𝑌‘𝑗)))))
Theorem	mavmulval 21894*	Multiplication of a vector with a square matrix. (Contributed by AV, 23-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ × = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐴))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m 𝑁))    ⇒   ⊢ (𝜑 → (𝑋 × 𝑌) = (𝑖 ∈ 𝑁 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗) · (𝑌‘𝑗))))))
Theorem	mavmulfv 21895*	A cell/element in the vector resulting from a multiplication of a vector with a square matrix. (Contributed by AV, 6-Dec-2018.) (Revised by AV, 18-Feb-2019.) (Revised by AV, 23-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ × = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐴))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m 𝑁))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑁)    ⇒   ⊢ (𝜑 → ((𝑋 × 𝑌)‘𝐼) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝐼𝑋𝑗) · (𝑌‘𝑗)))))
Theorem	mavmulcl 21896	Multiplication of an NxN matrix with an N-dimensional vector results in an N-dimensional vector. (Contributed by AV, 6-Dec-2018.) (Revised by AV, 23-Feb-2019.) (Proof shortened by AV, 23-Jul-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ × = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐴))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m 𝑁))    ⇒   ⊢ (𝜑 → (𝑋 × 𝑌) ∈ (𝐵 ↑m 𝑁))
Theorem	1mavmul 21897	Multiplication of the identity NxN matrix with an N-dimensional vector results in the vector itself. (Contributed by AV, 9-Feb-2019.) (Revised by AV, 23-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m 𝑁))    ⇒   ⊢ (𝜑 → ((1r‘𝐴) · 𝑌) = 𝑌)
Theorem	mavmulass 21898	Associativity of the multiplication of two NxN matrices with an N-dimensional vector. (Contributed by AV, 9-Feb-2019.) (Revised by AV, 25-Feb-2019.) (Proof shortened by AV, 22-Jul-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m 𝑁))    &   ⊢ × = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐴))    &   ⊢ (𝜑 → 𝑍 ∈ (Base‘𝐴))    ⇒   ⊢ (𝜑 → ((𝑋 × 𝑍) · 𝑌) = (𝑋 · (𝑍 · 𝑌)))
Theorem	mavmuldm 21899	The domain of the matrix vector multiplication function. (Contributed by AV, 27-Feb-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (𝐵 ↑m (𝑀 × 𝑁))    &   ⊢ 𝐷 = (𝐵 ↑m 𝑁)    &   ⊢ · = (𝑅 maVecMul ⟨𝑀, 𝑁⟩)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin) → dom · = (𝐶 × 𝐷))
Theorem	mavmulsolcl 21900	Every solution of the equation 𝐴∗𝑋 = 𝑌 for a matrix 𝐴 and a vector 𝐵 is a vector. (Contributed by AV, 27-Feb-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (𝐵 ↑m (𝑀 × 𝑁))    &   ⊢ 𝐷 = (𝐵 ↑m 𝑁)    &   ⊢ · = (𝑅 maVecMul ⟨𝑀, 𝑁⟩)    &   ⊢ 𝐸 = (𝐵 ↑m 𝑀)    ⇒   ⊢ (((𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅) ∧ (𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸)) → ((𝐴 · 𝑋) = 𝑌 → 𝑋 ∈ 𝐷))