P. 224 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22301-22400   *Has distinct variable group(s)

Type	Label	Description
Statement
11.4.3  The matrix algebra The main result of this subsection are the theorems showing that (𝑁 Mat 𝑅) is a ring (see matring 22306) and an associative algebra (see matassa 22307). Additionally, theorems for the identity matrix and transposed matrices are provided.
Theorem	matmulr 22301	Multiplication in the matrix algebra. (Contributed by Stefan O'Rear, 4-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ · = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → · = (.r‘𝐴))
Theorem	mamumat1cl 22302*	The identity matrix (as operation in maps-to notation) is a matrix. (Contributed by Stefan O'Rear, 2-Sep-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (𝑖 ∈ 𝑀, 𝑗 ∈ 𝑀 ↦ if(𝑖 = 𝑗, 1 , 0 ))    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    ⇒   ⊢ (𝜑 → 𝐼 ∈ (𝐵 ↑m (𝑀 × 𝑀)))
Theorem	mat1comp 22303*	The components of the identity matrix (as operation in maps-to notation). (Contributed by AV, 22-Jul-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (𝑖 ∈ 𝑀, 𝑗 ∈ 𝑀 ↦ if(𝑖 = 𝑗, 1 , 0 ))    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    ⇒   ⊢ ((𝐴 ∈ 𝑀 ∧ 𝐽 ∈ 𝑀) → (𝐴𝐼𝐽) = if(𝐴 = 𝐽, 1 , 0 ))
Theorem	mamulid 22304*	The identity matrix (as operation in maps-to notation) is a left identity (for any matrix with the same number of rows). (Contributed by Stefan O'Rear, 3-Sep-2015.) (Proof shortened by AV, 22-Jul-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (𝑖 ∈ 𝑀, 𝑗 ∈ 𝑀 ↦ if(𝑖 = 𝑗, 1 , 0 ))    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ 𝐹 = (𝑅 maMul ⟨𝑀, 𝑀, 𝑁⟩)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    ⇒   ⊢ (𝜑 → (𝐼𝐹𝑋) = 𝑋)
Theorem	mamurid 22305*	The identity matrix (as operation in maps-to notation) is a right identity (for any matrix with the same number of columns). (Contributed by Stefan O'Rear, 3-Sep-2015.) (Proof shortened by AV, 22-Jul-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐼 = (𝑖 ∈ 𝑀, 𝑗 ∈ 𝑀 ↦ if(𝑖 = 𝑗, 1 , 0 ))    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ 𝐹 = (𝑅 maMul ⟨𝑁, 𝑀, 𝑀⟩)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑁 × 𝑀)))    ⇒   ⊢ (𝜑 → (𝑋𝐹𝐼) = 𝑋)
Theorem	matring 22306	Existence of the matrix ring, see also the statement in [Lang] p. 504: "For a given integer n > 0 the set of square n x n matrices form a ring." (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring)
Theorem	matassa 22307	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 22308*	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 22309*	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 22310*	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 22311	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 22312	The identity matrix is a matrix. (Contributed by AV, 15-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 1 = (1r‘(𝑁 Mat 𝑅))    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → 1 ∈ 𝐵)
Theorem	matsc 22313*	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 22314	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 22315	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 22316	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 22317	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 22318	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 22319	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 22320	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 22321	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 22322	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 22323*	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 22324*	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 22325*	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 22326*	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 22327*	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 22328*	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 22329, the empty set is the sole zero-dimensional matrix (also called "empty matrix", see Wikipedia https://en.wikipedia.org/wiki/Matrix_(mathematics)#Empty_matrices). 22329 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 22333. 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 22350.
Theorem	mat0dimbas0 22329	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 22330	The zero of the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019.)
⊢ 𝐴 = (∅ Mat 𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (0g‘𝐴) = ∅)
Theorem	mat0dimid 22331	The identity of the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019.)
⊢ 𝐴 = (∅ Mat 𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (1r‘𝐴) = ∅)
Theorem	mat0dimscm 22332	The scalar multiplication in the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019.)
⊢ 𝐴 = (∅ Mat 𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (Base‘𝑅)) → (𝑋( ·𝑠 ‘𝐴)∅) = ∅)
Theorem	mat0dimcrng 22333	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 22334*	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 22335	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 22336	The zero of the algebra of matrices with dimension 1. (Contributed by AV, 15-Aug-2019.)
⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (0g‘𝐴) = {⟨𝑂, (0g‘𝑅)⟩})
Theorem	mat1dimid 22337	The identity of the algebra of matrices with dimension 1. (Contributed by AV, 15-Aug-2019.)
⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (1r‘𝐴) = {⟨𝑂, (1r‘𝑅)⟩})
Theorem	mat1dimscm 22338	The scalar multiplication in the algebra of matrices with dimension 1. (Contributed by AV, 16-Aug-2019.)
⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    ⇒   ⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋( ·𝑠 ‘𝐴){⟨𝑂, 𝑌⟩}) = {⟨𝑂, (𝑋(.r‘𝑅)𝑌)⟩})
Theorem	mat1dimmul 22339	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 22340	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 22341*	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 22342*	The value of the ring homomorphism 𝐹. (Contributed by AV, 22-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {⟨𝑂, 𝑥⟩})    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾) → (𝐹‘𝑋) = {⟨𝑂, 𝑋⟩})
Theorem	mat1rhmelval 22343*	The value of the ring homomorphism 𝐹. (Contributed by AV, 22-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {⟨𝑂, 𝑥⟩})    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾) → (𝐸(𝐹‘𝑋)𝐸) = 𝑋)
Theorem	mat1rhmcl 22344*	The value of the ring homomorphism 𝐹 is a matrix with dimension 1. (Contributed by AV, 22-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {⟨𝑂, 𝑥⟩})    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾) → (𝐹‘𝑋) ∈ 𝐵)
Theorem	mat1f 22345*	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 22346*	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 22347*	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 22348*	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 22349*	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 22350	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 22376!]". 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 22353 and df-scmat 22354), basic properties of (elements of) these sets, and theorems showing that the diagonal matrices form a subring of the ring of square matrices (dmatsrng 22364), that the scalar matrices form a subring of the ring of square matrices (scmatsrng 22383), that the scalar matrices form a subring of the ring of diagonal matrices (scmatsrng1 22386) and that the ring of scalar matrices over a commutative ring is a commutative ring (scmatcrng 22384).
Syntax	cdmat 22351	Extend class notation for the algebra of diagonal matrices.
class DMat
Syntax	cscmat 22352	Extend class notation for the algebra of scalar matrices.
class ScMat
Definition	df-dmat 22353*	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 22354*	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 22355*	The set of 𝑁 x 𝑁 diagonal matrices over (a ring) 𝑅. (Contributed by AV, 8-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (𝑁 DMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝐷 = {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = 0 )})
Theorem	dmatel 22356*	A 𝑁 x 𝑁 diagonal matrix over (a ring) 𝑅. (Contributed by AV, 18-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (𝑁 DMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑀 ∈ 𝐷 ↔ (𝑀 ∈ 𝐵 ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ))))
Theorem	dmatmat 22357	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 22358	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 22359	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 22360*	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 22361	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 22362	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 22363	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 22364	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 22365	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 22366	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 22367*	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 22368*	An 𝑁 x 𝑁 scalar matrix over (a ring) 𝑅. (Contributed by AV, 18-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐴)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑀 ∈ 𝑆 ↔ (𝑀 ∈ 𝐵 ∧ ∃𝑐 ∈ 𝐾 𝑀 = (𝑐 · 1 ))))
Theorem	scmatscmid 22369*	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 22370	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 22371	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 22372	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 22373*	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 22374*	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 22375*	Alternate proof of scmate 22373: An entry of an 𝑁 x 𝑁 scalar matrix over the ring 𝑅. This prove makes use of scmatmats 22374 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 22376*	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 22377	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 22378	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 22379	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 22380	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 22381	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 22382	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 22383	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 22384	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 22385	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 22386	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 22387	Closure of the scalar multiplication in the ring of scalar matrices. (matvscl 22294 analog.) (Contributed by AV, 24-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝑆 = (𝑁 ScMat 𝑅)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑆)) → (𝐶 ∗ 𝑋) ∈ 𝑆)
Theorem	scmatlss 22388	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 22389	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 22390*	The value of the ring homomorphism 𝐹. (Contributed by AV, 22-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 1 = (1r‘𝐴)    &   ⊢ ∗ = ( ·𝑠 ‘𝐴)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ (𝑥 ∗ 1 ))    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾) → (𝐹‘𝑋) = (𝑋 ∗ 1 ))
Theorem	scmatrhmcl 22391*	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 22392*	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 22393*	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 22394*	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 22395*	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 22396*	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 22397*	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 22398*	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 22399*	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 22400	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) → 𝑅 ≃𝑟 𝑆)