P. 216 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21501-21600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	matassa 21501	Existence of the matrix algebra, see also the statement in [Lang] p. 505: "Then Matn(R) is an algebra over R" . (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ AssAlg)
Theorem	matmulcell 21502*	Multiplication in the matrix ring for a single cell of a matrix. (Contributed by AV, 17-Nov-2019.) (Revised by AV, 3-Jul-2022.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ × = (.r‘𝐴)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑋 × 𝑌)𝐽) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝐼𝑋𝑗)(.r‘𝑅)(𝑗𝑌𝐽)))))
Theorem	mpomatmul 21503*	Multiplication of two N x N matrices given in maps-to notation. (Contributed by AV, 29-Oct-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ × = (.r‘𝐴)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ 𝑋 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝐶)    &   ⊢ 𝑌 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝐸)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝐶 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝐸 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑘 = 𝑖 ∧ 𝑚 = 𝑗)) → 𝐷 = 𝐶)    &   ⊢ ((𝜑 ∧ (𝑚 = 𝑖 ∧ 𝑙 = 𝑗)) → 𝐹 = 𝐸)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑚 ∈ 𝑁) → 𝐷 ∈ 𝑈)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝐹 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝑋 × 𝑌) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑅 Σg (𝑚 ∈ 𝑁 ↦ (𝐷 · 𝐹)))))
Theorem	mat1 21504*	Value of an identity matrix, see also the statement in [Lang] p. 504: "The unit element of the ring of n x n matrices is the matrix In ... whose components are equal to 0 except on the diagonal, in which case they are equal to 1.". (Contributed by Stefan O'Rear, 7-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (1r‘𝐴) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, 1 , 0 )))
Theorem	mat1ov 21505	Entries of an identity matrix, deduction form. (Contributed by Stefan O'Rear, 10-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑁)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑁)    &   ⊢ 𝑈 = (1r‘𝐴)    ⇒   ⊢ (𝜑 → (𝐼𝑈𝐽) = if(𝐼 = 𝐽, 1 , 0 ))
Theorem	mat1bas 21506	The identity matrix is a matrix. (Contributed by AV, 15-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 1 = (1r‘(𝑁 Mat 𝑅))    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → 1 ∈ 𝐵)
Theorem	matsc 21507*	The identity matrix multiplied with a scalar. (Contributed by Stefan O'Rear, 16-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐿 ∈ 𝐾) → (𝐿 · (1r‘𝐴)) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, 𝐿, 0 )))
Theorem	ofco2 21508	Distribution law for the function operation and the composition of functions. (Contributed by Stefan O'Rear, 17-Jul-2018.)
⊢ (((𝐹 ∈ V ∧ 𝐺 ∈ V) ∧ (Fun 𝐻 ∧ (𝐹 ∘ 𝐻) ∈ V ∧ (𝐺 ∘ 𝐻) ∈ V)) → ((𝐹 ∘f 𝑅𝐺) ∘ 𝐻) = ((𝐹 ∘ 𝐻) ∘f 𝑅(𝐺 ∘ 𝐻)))
Theorem	oftpos 21509	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 21510	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 21511	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 21512	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 21513	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 21514	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 21515	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 21516	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 21517*	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 21518*	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 21519*	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 21520*	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 21521*	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 21522*	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 21523, the empty set is the sole zero-dimensional matrix (also called "empty matrix", see Wikipedia https://en.wikipedia.org/wiki/Matrix_(mathematics)#Empty_matrices). 21523 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 21527. 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 21544.
Theorem	mat0dimbas0 21523	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 21524	The zero of the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019.)
⊢ 𝐴 = (∅ Mat 𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (0g‘𝐴) = ∅)
Theorem	mat0dimid 21525	The identity of the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019.)
⊢ 𝐴 = (∅ Mat 𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (1r‘𝐴) = ∅)
Theorem	mat0dimscm 21526	The scalar multiplication in the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019.)
⊢ 𝐴 = (∅ Mat 𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (Base‘𝑅)) → (𝑋( ·𝑠 ‘𝐴)∅) = ∅)
Theorem	mat0dimcrng 21527	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 21528*	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 21529	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 21530	The zero of the algebra of matrices with dimension 1. (Contributed by AV, 15-Aug-2019.)
⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (0g‘𝐴) = {⟨𝑂, (0g‘𝑅)⟩})
Theorem	mat1dimid 21531	The identity of the algebra of matrices with dimension 1. (Contributed by AV, 15-Aug-2019.)
⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (1r‘𝐴) = {⟨𝑂, (1r‘𝑅)⟩})
Theorem	mat1dimscm 21532	The scalar multiplication in the algebra of matrices with dimension 1. (Contributed by AV, 16-Aug-2019.)
⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    ⇒   ⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋( ·𝑠 ‘𝐴){⟨𝑂, 𝑌⟩}) = {⟨𝑂, (𝑋(.r‘𝑅)𝑌)⟩})
Theorem	mat1dimmul 21533	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 21534	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 21535*	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 21536*	The value of the ring homomorphism 𝐹. (Contributed by AV, 22-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {⟨𝑂, 𝑥⟩})    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾) → (𝐹‘𝑋) = {⟨𝑂, 𝑋⟩})
Theorem	mat1rhmelval 21537*	The value of the ring homomorphism 𝐹. (Contributed by AV, 22-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {⟨𝑂, 𝑥⟩})    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾) → (𝐸(𝐹‘𝑋)𝐸) = 𝑋)
Theorem	mat1rhmcl 21538*	The value of the ring homomorphism 𝐹 is a matrix with dimension 1. (Contributed by AV, 22-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {⟨𝑂, 𝑥⟩})    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾) → (𝐹‘𝑋) ∈ 𝐵)
Theorem	mat1f 21539*	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 21540*	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 21541*	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 21542*	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 21543*	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 21544	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 21570!]". 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 21547 and df-scmat 21548), basic properties of (elements of) these sets, and theorems showing that the diagonal matrices form a subring of the ring of square matrices (dmatsrng 21558), that the scalar matrices form a subring of the ring of square matrices (scmatsrng 21577), that the scalar matrices form a subring of the ring of diagonal matrices (scmatsrng1 21580) and that the ring of scalar matrices over a commutative ring is a commutative ring (scmatcrng 21578).
Syntax	cdmat 21545	Extend class notation for the algebra of diagonal matrices.
class DMat
Syntax	cscmat 21546	Extend class notation for the algebra of scalar matrices.
class ScMat
Definition	df-dmat 21547*	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 21548*	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 21549*	The set of 𝑁 x 𝑁 diagonal matrices over (a ring) 𝑅. (Contributed by AV, 8-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (𝑁 DMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝐷 = {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = 0 )})
Theorem	dmatel 21550*	A 𝑁 x 𝑁 diagonal matrix over (a ring) 𝑅. (Contributed by AV, 18-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (𝑁 DMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑀 ∈ 𝐷 ↔ (𝑀 ∈ 𝐵 ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ))))
Theorem	dmatmat 21551	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 21552	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 21553	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 21554*	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 21555	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 21556	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 21557	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 21558	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 21559	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 21560	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 21561*	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 21562*	An 𝑁 x 𝑁 scalar matrix over (a ring) 𝑅. (Contributed by AV, 18-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐴)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑀 ∈ 𝑆 ↔ (𝑀 ∈ 𝐵 ∧ ∃𝑐 ∈ 𝐾 𝑀 = (𝑐 · 1 ))))
Theorem	scmatscmid 21563*	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 21564	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 21565	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 21566	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 21567*	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 21568*	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 21569*	Alternate proof of scmate 21567: An entry of an 𝑁 x 𝑁 scalar matrix over the ring 𝑅. This prove makes use of scmatmats 21568 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 21570*	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 21571	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 21572	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 21573	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 21574	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 21575	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 21576	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 21577	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 21578	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 21579	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 21580	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 21581	Closure of the scalar multiplication in the ring of scalar matrices. (matvscl 21488 analog.) (Contributed by AV, 24-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑅)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑆)) → (𝐶 ∗ 𝑋) ∈ 𝑆)
Theorem	scmatlss 21582	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 21583	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 21584*	The value of the ring homomorphism 𝐹. (Contributed by AV, 22-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ (𝑥 ∗ 1 ))    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾) → (𝐹‘𝑋) = (𝑋 ∗ 1 ))
Theorem	scmatrhmcl 21585*	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 21586*	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 21587*	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 21588*	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 21589*	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 21590*	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 21591*	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 21592*	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 21593*	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 21594	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 21595	The empty matrix over a ring is a scalar matrix (and therefore, by scmatdmat 21572, also a diagonal matrix). (Contributed by AV, 21-Dec-2019.)
⊢ (𝑅 ∈ Ring → ∅ ∈ (∅ ScMat 𝑅))
Theorem	mat1scmat 21596	A 1-dimensional matrix over a ring is always a scalar matrix (and therefore, by scmatdmat 21572, 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 21443 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 21598 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 20876. See also the statements in [Lang] p. 508.
Syntax	cmvmul 21597	Syntax for the operator for the multiplication of a vector with a matrix.
class maVecMul
Definition	df-mvmul 21598*	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 21599*	Functional value of the matrix vector multiplication operator. (Contributed by AV, 23-Feb-2019.)
⊢ × = (𝑅 maVecMul ⟨𝑀, 𝑁⟩)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    ⇒   ⊢ (𝜑 → × = (𝑥 ∈ (𝐵 ↑m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑m 𝑁) ↦ (𝑖 ∈ 𝑀 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑦‘𝑗)))))))
Theorem	mvmulval 21600*	Multiplication of a vector with a matrix. (Contributed by AV, 23-Feb-2019.)
⊢ × = (𝑅 maVecMul ⟨𝑀, 𝑁⟩)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m 𝑁))    ⇒   ⊢ (𝜑 → (𝑋 × 𝑌) = (𝑖 ∈ 𝑀 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗) · (𝑌‘𝑗))))))