P. 225 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22401-22500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mamures 22401	Rows in a matrix product are functions only of the corresponding rows in the left argument. (Contributed by SO, 9-Jul-2018.)
⊢ 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑃⟩)    &   ⊢ 𝐺 = (𝑅 maMul ⟨𝐼, 𝑁, 𝑃⟩)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ⊆ 𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑃)))    ⇒   ⊢ (𝜑 → ((𝑋𝐹𝑌) ↾ (𝐼 × 𝑃)) = ((𝑋 ↾ (𝐼 × 𝑁))𝐺𝑌))
Theorem	grpvlinv 22402	Tuple-wise left inverse in groups. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ (𝐵 ↑m 𝐼)) → ((𝑁 ∘ 𝑋) ∘f + 𝑋) = (𝐼 × { 0 }))
Theorem	grpvrinv 22403	Tuple-wise right inverse in groups. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ (𝐵 ↑m 𝐼)) → (𝑋 ∘f + (𝑁 ∘ 𝑋)) = (𝐼 × { 0 }))
Theorem	ringvcl 22404	Tuple-wise multiplication closure in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (𝐵 ↑m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑m 𝐼)) → (𝑋 ∘f · 𝑌) ∈ (𝐵 ↑m 𝐼))
Theorem	mamucl 22405	Operation closure of matrix multiplication. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 23-Jul-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑃⟩)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑃)))    ⇒   ⊢ (𝜑 → (𝑋𝐹𝑌) ∈ (𝐵 ↑m (𝑀 × 𝑃)))
Theorem	mamuass 22406	Matrix multiplication is associative, see also statement in [Lang] p. 505. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑂 ∈ Fin)    &   ⊢ (𝜑 → 𝑃 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑂)))    &   ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m (𝑂 × 𝑃)))    &   ⊢ 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑂⟩)    &   ⊢ 𝐺 = (𝑅 maMul ⟨𝑀, 𝑂, 𝑃⟩)    &   ⊢ 𝐻 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑃⟩)    &   ⊢ 𝐼 = (𝑅 maMul ⟨𝑁, 𝑂, 𝑃⟩)    ⇒   ⊢ (𝜑 → ((𝑋𝐹𝑌)𝐺𝑍) = (𝑋𝐻(𝑌𝐼𝑍)))
Theorem	mamudi 22407	Matrix multiplication distributes over addition on the left. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Proof shortened by AV, 23-Jul-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑂⟩)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑂 ∈ Fin)    &   ⊢ + = (+g‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m (𝑁 × 𝑂)))    ⇒   ⊢ (𝜑 → ((𝑋 ∘f + 𝑌)𝐹𝑍) = ((𝑋𝐹𝑍) ∘f + (𝑌𝐹𝑍)))
Theorem	mamudir 22408	Matrix multiplication distributes over addition on the right. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Proof shortened by AV, 23-Jul-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑂⟩)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑂 ∈ Fin)    &   ⊢ + = (+g‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑁 × 𝑂)))    &   ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m (𝑁 × 𝑂)))    ⇒   ⊢ (𝜑 → (𝑋𝐹(𝑌 ∘f + 𝑍)) = ((𝑋𝐹𝑌) ∘f + (𝑋𝐹𝑍)))
Theorem	mamuvs1 22409	Matrix multiplication distributes over scalar multiplication on the left. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑂⟩)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑂 ∈ Fin)    &   ⊢ · = (.r‘𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m (𝑁 × 𝑂)))    ⇒   ⊢ (𝜑 → ((((𝑀 × 𝑁) × {𝑋}) ∘f · 𝑌)𝐹𝑍) = (((𝑀 × 𝑂) × {𝑋}) ∘f · (𝑌𝐹𝑍)))
Theorem	mamuvs2 22410	Matrix multiplication distributes over scalar multiplication on the left. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Proof shortened by AV, 22-Jul-2019.)
⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ 𝐹 = (𝑅 maMul ⟨𝑀, 𝑁, 𝑂⟩)    &   ⊢ (𝜑 → 𝑀 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑂 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁)))    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m (𝑁 × 𝑂)))    ⇒   ⊢ (𝜑 → (𝑋𝐹(((𝑁 × 𝑂) × {𝑌}) ∘f · 𝑍)) = (((𝑀 × 𝑂) × {𝑌}) ∘f · (𝑋𝐹𝑍)))
11.4.2  Square matrices In the following, the square matrix algebra is defined as extensible structure Mat. In this subsection, however, only square matrices and their basic properties are regarded. This includes showing that (𝑁 Mat 𝑅) is a left module, see matlmod 22435. That (𝑁 Mat 𝑅) is a ring and an associative algebra is shown in the next subsection, after theorems about the identity matrix are available. Nevertheless, (𝑁 Mat 𝑅) is called "matrix ring" or "matrix algebra" already in this subsection.
Syntax	cmat 22411	Syntax for the square matrix algebra.
class Mat
Definition	df-mat 22412*	Define the algebra of n x n matrices over a ring r. (Contributed by Stefan O'Rear, 31-Aug-2015.)
⊢ Mat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ ((𝑟 freeLMod (𝑛 × 𝑛)) sSet ⟨(.r‘ndx), (𝑟 maMul ⟨𝑛, 𝑛, 𝑛⟩)⟩))
Theorem	matbas0pc 22413	There is no matrix with a proper class either as dimension or as underlying ring. (Contributed by AV, 28-Dec-2018.)
⊢ (¬ (𝑁 ∈ V ∧ 𝑅 ∈ V) → (Base‘(𝑁 Mat 𝑅)) = ∅)
Theorem	matbas0 22414	There is no matrix for a not finite dimension or a proper class as the underlying ring. (Contributed by AV, 28-Dec-2018.)
⊢ (¬ (𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (Base‘(𝑁 Mat 𝑅)) = ∅)
Theorem	matval 22415	Value of the matrix algebra. (Contributed by Stefan O'Rear, 4-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐺 = (𝑅 freeLMod (𝑁 × 𝑁))    &   ⊢ · = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝐴 = (𝐺 sSet ⟨(.r‘ndx), · ⟩))
Theorem	matrcl 22416	Reverse closure for the matrix algebra. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V))
Theorem	matbas 22417	The matrix ring has the same base set as its underlying group. (Contributed by Stefan O'Rear, 4-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐺 = (𝑅 freeLMod (𝑁 × 𝑁))    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (Base‘𝐺) = (Base‘𝐴))
Theorem	matplusg 22418	The matrix ring has the same addition as its underlying group. (Contributed by Stefan O'Rear, 4-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐺 = (𝑅 freeLMod (𝑁 × 𝑁))    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (+g‘𝐺) = (+g‘𝐴))
Theorem	matsca 22419	The matrix ring has the same scalars as its underlying linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015.) (Proof shortened by AV, 12-Nov-2024.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐺 = (𝑅 freeLMod (𝑁 × 𝑁))    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (Scalar‘𝐺) = (Scalar‘𝐴))
Theorem	matscaOLD 22420	Obsolete version of matsca 22419 as of 12-Nov-2024. The matrix ring has the same scalars as its underlying linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐺 = (𝑅 freeLMod (𝑁 × 𝑁))    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (Scalar‘𝐺) = (Scalar‘𝐴))
Theorem	matvsca 22421	The matrix ring has the same scalar multiplication as its underlying linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015.) (Proof shortened by AV, 12-Nov-2024.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐺 = (𝑅 freeLMod (𝑁 × 𝑁))    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → ( ·𝑠 ‘𝐺) = ( ·𝑠 ‘𝐴))
Theorem	matvscaOLD 22422	Obsolete version of matvsca 22421 as of 12-Nov-2024. The matrix ring has the same scalar multiplication as its underlying linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐺 = (𝑅 freeLMod (𝑁 × 𝑁))    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → ( ·𝑠 ‘𝐺) = ( ·𝑠 ‘𝐴))
Theorem	mat0 22423	The matrix ring has the same zero as its underlying linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐺 = (𝑅 freeLMod (𝑁 × 𝑁))    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (0g‘𝐺) = (0g‘𝐴))
Theorem	matinvg 22424	The matrix ring has the same additive inverse as its underlying linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐺 = (𝑅 freeLMod (𝑁 × 𝑁))    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (invg‘𝐺) = (invg‘𝐴))
Theorem	mat0op 22425*	Value of a zero matrix as operation. (Contributed by AV, 2-Dec-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0g‘𝐴) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 0 ))
Theorem	matsca2 22426	The scalars of the matrix ring are the underlying ring. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑅 = (Scalar‘𝐴))
Theorem	matbas2 22427	The base set of the matrix ring as a set exponential. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Proof shortened by AV, 16-Dec-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝐾 ↑m (𝑁 × 𝑁)) = (Base‘𝐴))
Theorem	matbas2i 22428	A matrix is a function. (Contributed by Stefan O'Rear, 11-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ (𝐾 ↑m (𝑁 × 𝑁)))
Theorem	matbas2d 22429*	The base set of the matrix ring as a mapping operation. (Contributed by Stefan O'Rear, 11-Jul-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → 𝐶 ∈ 𝐾)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ 𝐶) ∈ 𝐵)
Theorem	eqmat 22430*	Two square matrices of the same dimension are equal if they have the same entries. (Contributed by AV, 25-Sep-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 = 𝑌 ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑋𝑗) = (𝑖𝑌𝑗)))
Theorem	matecl 22431	Each entry (according to Wikipedia "Matrix (mathematics)", 30-Dec-2018, https://en.wikipedia.org/wiki/Matrix_(mathematics)#Definition (or element or component or coefficient or cell) of a matrix is an element of the underlying ring. (Contributed by AV, 16-Dec-2018.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    ⇒   ⊢ ((𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (𝐼𝑀𝐽) ∈ 𝐾)
Theorem	matecld 22432	Each entry (according to Wikipedia "Matrix (mathematics)", 30-Dec-2018, https://en.wikipedia.org/wiki/Matrix_(mathematics)#Definition (or element or component or coefficient or cell) of a matrix is an element of the underlying ring, deduction form. (Contributed by AV, 27-Nov-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑁)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑁)    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐼𝑀𝐽) ∈ 𝐾)
Theorem	matplusg2 22433	Addition in the matrix ring is cell-wise. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ ✚ = (+g‘𝐴)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ✚ 𝑌) = (𝑋 ∘f + 𝑌))
Theorem	matvsca2 22434	Scalar multiplication in the matrix ring is cell-wise. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝐴)    &   ⊢ × = (.r‘𝑅)    &   ⊢ 𝐶 = (𝑁 × 𝑁)    ⇒   ⊢ ((𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) = ((𝐶 × {𝑋}) ∘f × 𝑌))
Theorem	matlmod 22435	The matrix ring is a linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ LMod)
Theorem	matgrp 22436	The matrix ring is a group. (Contributed by AV, 21-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Grp)
Theorem	matvscl 22437	Closure of the scalar multiplication in the matrix ring. (lmodvscl 20876 analog.) (Contributed by AV, 27-Nov-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ · = ( ·𝑠 ‘𝐴)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵)) → (𝐶 · 𝑋) ∈ 𝐵)
Theorem	matsubg 22438	The matrix ring has the same addition as its underlying group. (Contributed by AV, 2-Aug-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐺 = (𝑅 freeLMod (𝑁 × 𝑁))    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (-g‘𝐺) = (-g‘𝐴))
Theorem	matplusgcell 22439	Addition in the matrix ring is cell-wise. (Contributed by AV, 2-Aug-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ ✚ = (+g‘𝐴)    &   ⊢ + = (+g‘𝑅)    ⇒   ⊢ (((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑋 ✚ 𝑌)𝐽) = ((𝐼𝑋𝐽) + (𝐼𝑌𝐽)))
Theorem	matsubgcell 22440	Subtraction in the matrix ring is cell-wise. (Contributed by AV, 2-Aug-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑆 = (-g‘𝐴)    &   ⊢ − = (-g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑋𝑆𝑌)𝐽) = ((𝐼𝑋𝐽) − (𝐼𝑌𝐽)))
Theorem	matinvgcell 22441	Additive inversion in the matrix ring is cell-wise. (Contributed by AV, 17-Nov-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑉 = (invg‘𝑅)    &   ⊢ 𝑊 = (invg‘𝐴)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑊‘𝑋)𝐽) = (𝑉‘(𝐼𝑋𝐽)))
Theorem	matvscacell 22442	Scalar multiplication in the matrix ring is cell-wise. (Contributed by AV, 7-Aug-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ · = ( ·𝑠 ‘𝐴)    &   ⊢ × = (.r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑋 · 𝑌)𝐽) = (𝑋 × (𝐼𝑌𝐽)))
Theorem	matgsum 22443*	Finite commutative sums in a matrix algebra are taken componentwise. (Contributed by AV, 26-Sep-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝑈) ∈ 𝐵)    &   ⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝑈)) finSupp 0 )    ⇒   ⊢ (𝜑 → (𝐴 Σg (𝑦 ∈ 𝐽 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝑈))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈))))
11.4.3  The matrix algebra The main result of this subsection are the theorems showing that (𝑁 Mat 𝑅) is a ring (see matring 22449) and an associative algebra (see matassa 22450). Additionally, theorems for the identity matrix and transposed matrices are provided.
Theorem	matmulr 22444	Multiplication in the matrix algebra. (Contributed by Stefan O'Rear, 4-Sep-2015.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ · = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → · = (.r‘𝐴))
Theorem	mamumat1cl 22445*	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 22446*	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 22447*	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 22448*	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 22449	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 22450	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 22451*	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 22452*	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 22453*	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 22454	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 22455	The identity matrix is a matrix. (Contributed by AV, 15-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 1 = (1r‘(𝑁 Mat 𝑅))    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → 1 ∈ 𝐵)
Theorem	matsc 22456*	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 22457	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 22458	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 22459	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 22460	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 22461	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 22462	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 22463	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 22464	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 22465	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 22466*	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 22467*	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 22468*	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 22469*	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 22470*	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 22471*	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 22472, the empty set is the sole zero-dimensional matrix (also called "empty matrix", see Wikipedia https://en.wikipedia.org/wiki/Matrix_(mathematics)#Empty_matrices). 22472 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 22476. 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 22493.
Theorem	mat0dimbas0 22472	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 22473	The zero of the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019.)
⊢ 𝐴 = (∅ Mat 𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (0g‘𝐴) = ∅)
Theorem	mat0dimid 22474	The identity of the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019.)
⊢ 𝐴 = (∅ Mat 𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (1r‘𝐴) = ∅)
Theorem	mat0dimscm 22475	The scalar multiplication in the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019.)
⊢ 𝐴 = (∅ Mat 𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (Base‘𝑅)) → (𝑋( ·𝑠 ‘𝐴)∅) = ∅)
Theorem	mat0dimcrng 22476	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 22477*	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 22478	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 22479	The zero of the algebra of matrices with dimension 1. (Contributed by AV, 15-Aug-2019.)
⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (0g‘𝐴) = {⟨𝑂, (0g‘𝑅)⟩})
Theorem	mat1dimid 22480	The identity of the algebra of matrices with dimension 1. (Contributed by AV, 15-Aug-2019.)
⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (1r‘𝐴) = {⟨𝑂, (1r‘𝑅)⟩})
Theorem	mat1dimscm 22481	The scalar multiplication in the algebra of matrices with dimension 1. (Contributed by AV, 16-Aug-2019.)
⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    ⇒   ⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋( ·𝑠 ‘𝐴){⟨𝑂, 𝑌⟩}) = {⟨𝑂, (𝑋(.r‘𝑅)𝑌)⟩})
Theorem	mat1dimmul 22482	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 22483	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 22484*	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 22485*	The value of the ring homomorphism 𝐹. (Contributed by AV, 22-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {⟨𝑂, 𝑥⟩})    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾) → (𝐹‘𝑋) = {⟨𝑂, 𝑋⟩})
Theorem	mat1rhmelval 22486*	The value of the ring homomorphism 𝐹. (Contributed by AV, 22-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {⟨𝑂, 𝑥⟩})    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾) → (𝐸(𝐹‘𝑋)𝐸) = 𝑋)
Theorem	mat1rhmcl 22487*	The value of the ring homomorphism 𝐹 is a matrix with dimension 1. (Contributed by AV, 22-Dec-2019.)
⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = ({𝐸} Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑂 = ⟨𝐸, 𝐸⟩    &   ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {⟨𝑂, 𝑥⟩})    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾) → (𝐹‘𝑋) ∈ 𝐵)
Theorem	mat1f 22488*	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 22489*	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 22490*	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 22491*	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 22492*	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 22493	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 22519!]". 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 22496 and df-scmat 22497), basic properties of (elements of) these sets, and theorems showing that the diagonal matrices form a subring of the ring of square matrices (dmatsrng 22507), that the scalar matrices form a subring of the ring of square matrices (scmatsrng 22526), that the scalar matrices form a subring of the ring of diagonal matrices (scmatsrng1 22529) and that the ring of scalar matrices over a commutative ring is a commutative ring (scmatcrng 22527).
Syntax	cdmat 22494	Extend class notation for the algebra of diagonal matrices.
class DMat
Syntax	cscmat 22495	Extend class notation for the algebra of scalar matrices.
class ScMat
Definition	df-dmat 22496*	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 22497*	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 22498*	The set of 𝑁 x 𝑁 diagonal matrices over (a ring) 𝑅. (Contributed by AV, 8-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (𝑁 DMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝐷 = {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = 0 )})
Theorem	dmatel 22499*	A 𝑁 x 𝑁 diagonal matrix over (a ring) 𝑅. (Contributed by AV, 18-Dec-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 𝐷 = (𝑁 DMat 𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑀 ∈ 𝐷 ↔ (𝑀 ∈ 𝐵 ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ))))
Theorem	dmatmat 22500	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 ∧ 𝑅 ∈ 𝑉) → (𝑀 ∈ 𝐷 → 𝑀 ∈ 𝐵))