Home | Metamath
Proof Explorer Theorem List (p. 211 of 450) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44955) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mamures 21001 | 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 | mndvcl 21002 | Tuple-wise additive closure in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) ⇒ ⊢ ((𝑀 ∈ Mnd ∧ 𝑋 ∈ (𝐵 ↑m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑m 𝐼)) → (𝑋 ∘f + 𝑌) ∈ (𝐵 ↑m 𝐼)) | ||
Theorem | mndvass 21003 | Tuple-wise associativity in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) ⇒ ⊢ ((𝑀 ∈ Mnd ∧ (𝑋 ∈ (𝐵 ↑m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑m 𝐼) ∧ 𝑍 ∈ (𝐵 ↑m 𝐼))) → ((𝑋 ∘f + 𝑌) ∘f + 𝑍) = (𝑋 ∘f + (𝑌 ∘f + 𝑍))) | ||
Theorem | mndvlid 21004 | Tuple-wise left identity in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 0 = (0g‘𝑀) ⇒ ⊢ ((𝑀 ∈ Mnd ∧ 𝑋 ∈ (𝐵 ↑m 𝐼)) → ((𝐼 × { 0 }) ∘f + 𝑋) = 𝑋) | ||
Theorem | mndvrid 21005 | Tuple-wise right identity in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 0 = (0g‘𝑀) ⇒ ⊢ ((𝑀 ∈ Mnd ∧ 𝑋 ∈ (𝐵 ↑m 𝐼)) → (𝑋 ∘f + (𝐼 × { 0 })) = 𝑋) | ||
Theorem | grpvlinv 21006 | 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 21007 | Tuple-wise right inverse in groups. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ (𝐵 ↑m 𝐼)) → (𝑋 ∘f + (𝑁 ∘ 𝑋)) = (𝐼 × { 0 })) | ||
Theorem | mhmvlin 21008 | Tuple extension of monoid homomorphisms. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ ⨣ = (+g‘𝑁) ⇒ ⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑m 𝐼)) → (𝐹 ∘ (𝑋 ∘f + 𝑌)) = ((𝐹 ∘ 𝑋) ∘f ⨣ (𝐹 ∘ 𝑌))) | ||
Theorem | ringvcl 21009 | Tuple-wise multiplication closure in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (𝐵 ↑m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑m 𝐼)) → (𝑋 ∘f · 𝑌) ∈ (𝐵 ↑m 𝐼)) | ||
Theorem | mamucl 21010 | 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 21011 | 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 21012 | 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 21013 | 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 21014 | 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 21015 | 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 · (𝑋𝐹𝑍))) | ||
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 21038. 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 21016 | Syntax for the square matrix algebra. |
class Mat | ||
Definition | df-mat 21017* | 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 21018 | 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 21019 | 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 21020 | Value of the matrix algebra. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐺 = (𝑅 freeLMod (𝑁 × 𝑁)) & ⊢ · = (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝐴 = (𝐺 sSet 〈(.r‘ndx), · 〉)) | ||
Theorem | matrcl 21021 | Reverse closure for the matrix algebra. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) | ||
Theorem | matbas 21022 | 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 21023 | 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 21024 | The matrix ring has the same scalars as its underlying linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐺 = (𝑅 freeLMod (𝑁 × 𝑁)) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (Scalar‘𝐺) = (Scalar‘𝐴)) | ||
Theorem | matvsca 21025 | The matrix ring has the same scalar multiplication as its underlying linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐺 = (𝑅 freeLMod (𝑁 × 𝑁)) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → ( ·𝑠 ‘𝐺) = ( ·𝑠 ‘𝐴)) | ||
Theorem | mat0 21026 | 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 21027 | 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 21028* | Value of a zero matrix as operation. (Contributed by AV, 2-Dec-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0g‘𝐴) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 0 )) | ||
Theorem | matsca2 21029 | The scalars of the matrix ring are the underlying ring. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑅 = (Scalar‘𝐴)) | ||
Theorem | matbas2 21030 | 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 21031 | A matrix is a function. (Contributed by Stefan O'Rear, 11-Sep-2015.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ (𝐾 ↑m (𝑁 × 𝑁))) | ||
Theorem | matbas2d 21032* | 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 21033* | 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 21034 | 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 21035 | 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 21036 | Addition in the matrix ring is cell-wise. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ ✚ = (+g‘𝐴) & ⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ✚ 𝑌) = (𝑋 ∘f + 𝑌)) | ||
Theorem | matvsca2 21037 | Scalar multiplication in the matrix ring is cell-wise. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ · = ( ·𝑠 ‘𝐴) & ⊢ × = (.r‘𝑅) & ⊢ 𝐶 = (𝑁 × 𝑁) ⇒ ⊢ ((𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) = ((𝐶 × {𝑋}) ∘f × 𝑌)) | ||
Theorem | matlmod 21038 | The matrix ring is a linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ LMod) | ||
Theorem | matgrp 21039 | The matrix ring is a group. (Contributed by AV, 21-Dec-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Grp) | ||
Theorem | matvscl 21040 | Closure of the scalar multiplication in the matrix ring. (lmodvscl 19651 analog.) (Contributed by AV, 27-Nov-2019.) |
⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = ( ·𝑠 ‘𝐴) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵)) → (𝐶 · 𝑋) ∈ 𝐵) | ||
Theorem | matsubg 21041 | The matrix ring has the same addition as its underlying group. (Contributed by AV, 2-Aug-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐺 = (𝑅 freeLMod (𝑁 × 𝑁)) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (-g‘𝐺) = (-g‘𝐴)) | ||
Theorem | matplusgcell 21042 | Addition in the matrix ring is cell-wise. (Contributed by AV, 2-Aug-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ ✚ = (+g‘𝐴) & ⊢ + = (+g‘𝑅) ⇒ ⊢ (((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑋 ✚ 𝑌)𝐽) = ((𝐼𝑋𝐽) + (𝐼𝑌𝐽))) | ||
Theorem | matsubgcell 21043 | Subtraction in the matrix ring is cell-wise. (Contributed by AV, 2-Aug-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑆 = (-g‘𝐴) & ⊢ − = (-g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑋𝑆𝑌)𝐽) = ((𝐼𝑋𝐽) − (𝐼𝑌𝐽))) | ||
Theorem | matinvgcell 21044 | Additive inversion in the matrix ring is cell-wise. (Contributed by AV, 17-Nov-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = (invg‘𝑅) & ⊢ 𝑊 = (invg‘𝐴) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑊‘𝑋)𝐽) = (𝑉‘(𝐼𝑋𝐽))) | ||
Theorem | matvscacell 21045 | Scalar multiplication in the matrix ring is cell-wise. (Contributed by AV, 7-Aug-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ · = ( ·𝑠 ‘𝐴) & ⊢ × = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑋 · 𝑌)𝐽) = (𝑋 × (𝐼𝑌𝐽))) | ||
Theorem | matgsum 21046* | 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 (𝑦 ∈ 𝐽 ↦ 𝑈)))) | ||
The main result of this subsection are the theorems showing that (𝑁 Mat 𝑅) is a ring (see matring 21052) and an associative algebra (see matassa 21053). Additionally, theorems for the identity matrix and transposed matrices are provided. | ||
Theorem | matmulr 21047 | Multiplication in the matrix algebra. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ · = (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → · = (.r‘𝐴)) | ||
Theorem | mamumat1cl 21048* | 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 21049* | 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 21050* | 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 21051* | 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 21052 | 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 21053 | 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 21054* | 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 21055* | 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 21056* | 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 21057 | 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 21058 | The identity matrix is a matrix. (Contributed by AV, 15-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 1 = (1r‘(𝑁 Mat 𝑅)) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) → 1 ∈ 𝐵) | ||
Theorem | matsc 21059* | 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 21060 | 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 21061 | 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 21062 | 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 21063 | 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 21064 | 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 21065 | 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 21066 | 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 21067 | 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 21068 | 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 21069* | 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 21070* | 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 21071* | 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 21072* | 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 21073* | 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 21074* | 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‘𝑅)) | ||
As already mentioned before, and shown in mat0dimbas0 21075, the empty set is the sole zero-dimensional matrix (also called "empty matrix", see Wikipedia https://en.wikipedia.org/wiki/Matrix_(mathematics)#Empty_matrices). 21075 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 21079. 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 21096. | ||
Theorem | mat0dimbas0 21075 | 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 21076 | The zero of the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019.) |
⊢ 𝐴 = (∅ Mat 𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (0g‘𝐴) = ∅) | ||
Theorem | mat0dimid 21077 | The identity of the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019.) |
⊢ 𝐴 = (∅ Mat 𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (1r‘𝐴) = ∅) | ||
Theorem | mat0dimscm 21078 | The scalar multiplication in the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019.) |
⊢ 𝐴 = (∅ Mat 𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (Base‘𝑅)) → (𝑋( ·𝑠 ‘𝐴)∅) = ∅) | ||
Theorem | mat0dimcrng 21079 | 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 21080* | 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 21081 | 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 21082 | The zero of the algebra of matrices with dimension 1. (Contributed by AV, 15-Aug-2019.) |
⊢ 𝐴 = ({𝐸} Mat 𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑂 = 〈𝐸, 𝐸〉 ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (0g‘𝐴) = {〈𝑂, (0g‘𝑅)〉}) | ||
Theorem | mat1dimid 21083 | The identity of the algebra of matrices with dimension 1. (Contributed by AV, 15-Aug-2019.) |
⊢ 𝐴 = ({𝐸} Mat 𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑂 = 〈𝐸, 𝐸〉 ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (1r‘𝐴) = {〈𝑂, (1r‘𝑅)〉}) | ||
Theorem | mat1dimscm 21084 | The scalar multiplication in the algebra of matrices with dimension 1. (Contributed by AV, 16-Aug-2019.) |
⊢ 𝐴 = ({𝐸} Mat 𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑂 = 〈𝐸, 𝐸〉 ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋( ·𝑠 ‘𝐴){〈𝑂, 𝑌〉}) = {〈𝑂, (𝑋(.r‘𝑅)𝑌)〉}) | ||
Theorem | mat1dimmul 21085 | 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 21086 | 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 21087* | 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 21088* | The value of the ring homomorphism 𝐹. (Contributed by AV, 22-Dec-2019.) |
⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = ({𝐸} Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑂 = 〈𝐸, 𝐸〉 & ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {〈𝑂, 𝑥〉}) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾) → (𝐹‘𝑋) = {〈𝑂, 𝑋〉}) | ||
Theorem | mat1rhmelval 21089* | The value of the ring homomorphism 𝐹. (Contributed by AV, 22-Dec-2019.) |
⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = ({𝐸} Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑂 = 〈𝐸, 𝐸〉 & ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {〈𝑂, 𝑥〉}) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾) → (𝐸(𝐹‘𝑋)𝐸) = 𝑋) | ||
Theorem | mat1rhmcl 21090* | The value of the ring homomorphism 𝐹 is a matrix with dimension 1. (Contributed by AV, 22-Dec-2019.) |
⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = ({𝐸} Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑂 = 〈𝐸, 𝐸〉 & ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {〈𝑂, 𝑥〉}) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾) → (𝐹‘𝑋) ∈ 𝐵) | ||
Theorem | mat1f 21091* | 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 21092* | 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 21093* | 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 21094* | 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 21095* | 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 21096 | A ring is isomorphic to the ring of matrices with dimension 1 over this ring. (Contributed by AV, 30-Dec-2019.) |
⊢ 𝐴 = ({𝐸} Mat 𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝑅 ≃𝑟 𝐴) | ||
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 21122!]". 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 21099 and df-scmat 21100), basic properties of (elements of) these sets, and theorems showing that the diagonal matrices are a subring of the ring of square matrices (dmatsrng 21110), that the scalar matrices are a subring of the ring of square matrices (scmatsrng 21129), that the scalar matrices are a subring of the ring of diagonal matrices (scmatsrng1 21132) and that the ring of scalar matrices (over a commutative ring) is a commutative ring (scmatcrng 21130). | ||
Syntax | cdmat 21097 | Extend class notation for the algebra of diagonal matrices. |
class DMat | ||
Syntax | cscmat 21098 | Extend class notation for the algebra of scalar matrices. |
class ScMat | ||
Definition | df-dmat 21099* | 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 21100* | 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‘𝑎))}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |