![]() |
Metamath
Proof Explorer Theorem List (p. 226 of 491) | < 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: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mat1rhmelval 22501* | The value of the ring homomorphism 𝐹. (Contributed by AV, 22-Dec-2019.) |
⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = ({𝐸} Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑂 = 〈𝐸, 𝐸〉 & ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {〈𝑂, 𝑥〉}) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾) → (𝐸(𝐹‘𝑋)𝐸) = 𝑋) | ||
Theorem | mat1rhmcl 22502* | The value of the ring homomorphism 𝐹 is a matrix with dimension 1. (Contributed by AV, 22-Dec-2019.) |
⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = ({𝐸} Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑂 = 〈𝐸, 𝐸〉 & ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {〈𝑂, 𝑥〉}) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾) → (𝐹‘𝑋) ∈ 𝐵) | ||
Theorem | mat1f 22503* | 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 22504* | 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 22505* | 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 22506* | 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 22507* | 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 22508 | 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 22534!]". 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 22511 and df-scmat 22512), basic properties of (elements of) these sets, and theorems showing that the diagonal matrices form a subring of the ring of square matrices (dmatsrng 22522), that the scalar matrices form a subring of the ring of square matrices (scmatsrng 22541), that the scalar matrices form a subring of the ring of diagonal matrices (scmatsrng1 22544) and that the ring of scalar matrices over a commutative ring is a commutative ring (scmatcrng 22542). | ||
Syntax | cdmat 22509 | Extend class notation for the algebra of diagonal matrices. |
class DMat | ||
Syntax | cscmat 22510 | Extend class notation for the algebra of scalar matrices. |
class ScMat | ||
Definition | df-dmat 22511* | 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 22512* | 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 22513* | The set of 𝑁 x 𝑁 diagonal matrices over (a ring) 𝑅. (Contributed by AV, 8-Dec-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐷 = (𝑁 DMat 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝐷 = {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑚𝑗) = 0 )}) | ||
Theorem | dmatel 22514* | A 𝑁 x 𝑁 diagonal matrix over (a ring) 𝑅. (Contributed by AV, 18-Dec-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐷 = (𝑁 DMat 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑀 ∈ 𝐷 ↔ (𝑀 ∈ 𝐵 ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )))) | ||
Theorem | dmatmat 22515 | 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 22516 | 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 22517 | 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 22518* | 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 22519 | 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 22520 | 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 22521 | 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 22522 | 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 22523 | 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 22524 | 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 22525* | 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 22526* | An 𝑁 x 𝑁 scalar matrix over (a ring) 𝑅. (Contributed by AV, 18-Dec-2019.) |
⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 1 = (1r‘𝐴) & ⊢ · = ( ·𝑠 ‘𝐴) & ⊢ 𝑆 = (𝑁 ScMat 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑀 ∈ 𝑆 ↔ (𝑀 ∈ 𝐵 ∧ ∃𝑐 ∈ 𝐾 𝑀 = (𝑐 · 1 )))) | ||
Theorem | scmatscmid 22527* | 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 22528 | 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 22529 | 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 22530 | 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 22531* | 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 22532* | 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 22533* | Alternate proof of scmate 22531: An entry of an 𝑁 x 𝑁 scalar matrix over the ring 𝑅. This prove makes use of scmatmats 22532 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 22534* | 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 22535 | 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 22536 | 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 22537 | 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 22538 | 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 22539 | 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 22540 | 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 22541 | 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 22542 | 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 22543 | 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 22544 | 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 22545 | Closure of the scalar multiplication in the ring of scalar matrices. (matvscl 22452 analog.) (Contributed by AV, 24-Dec-2019.) |
⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑆 = (𝑁 ScMat 𝑅) & ⊢ ∗ = ( ·𝑠 ‘𝐴) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑆)) → (𝐶 ∗ 𝑋) ∈ 𝑆) | ||
Theorem | scmatlss 22546 | 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 22547 | 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 22548* | The value of the ring homomorphism 𝐹. (Contributed by AV, 22-Dec-2019.) |
⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 1 = (1r‘𝐴) & ⊢ ∗ = ( ·𝑠 ‘𝐴) & ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ (𝑥 ∗ 1 )) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾) → (𝐹‘𝑋) = (𝑋 ∗ 1 )) | ||
Theorem | scmatrhmcl 22549* | 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 22550* | 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 22551* | 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 22552* | 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 22553* | 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 22554* | 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 22555* | 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 22556* | 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 22557* | 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 22558 | A ring is isomorphic to every ring of scalar matrices over this ring with positive dimension. (Contributed by AV, 29-Dec-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐶 = (𝑁 ScMat 𝑅) & ⊢ 𝑆 = (𝐴 ↾s 𝐶) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring) → 𝑅 ≃𝑟 𝑆) | ||
Theorem | mat0scmat 22559 | The empty matrix over a ring is a scalar matrix (and therefore, by scmatdmat 22536, also a diagonal matrix). (Contributed by AV, 21-Dec-2019.) |
⊢ (𝑅 ∈ Ring → ∅ ∈ (∅ ScMat 𝑅)) | ||
Theorem | mat1scmat 22560 | A 1-dimensional matrix over a ring is always a scalar matrix (and therefore, by scmatdmat 22536, also a diagonal matrix). (Contributed by AV, 21-Dec-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ ((𝑁 ∈ 𝑉 ∧ (♯‘𝑁) = 1 ∧ 𝑅 ∈ Ring) → (𝑀 ∈ 𝐵 → 𝑀 ∈ (𝑁 ScMat 𝑅))) | ||
The module of 𝑛-dimensional "column vectors" over a ring 𝑟 is the 𝑛-dimensional free module over a ring 𝑟, which is the product of 𝑛 -many copies of the ring with componentwise addition and multiplication. Although a "column vector" could also be defined as n x 1 -matrix (according to Wikipedia "Row and column vectors", 22-Feb-2019, https://en.wikipedia.org/wiki/Row_and_column_vectors: "In linear algebra, a column vector [... ] is an m x 1 matrix, that is, a matrix consisting of a single column of m elements"), which would allow for using the matrix multiplication df-mamu 22410 for multiplying a matrix with a column vector, it seems more natural to use the definition of a free (left) module, avoiding to provide a singleton as 1-dimensional index set for the column, and to introduce a new operator df-mvmul 22562 for the multiplication of a matrix with a column vector. In most cases, it is sufficient to regard members of ((Base‘𝑅) ↑m 𝑁) as "column vectors", because ((Base‘𝑅) ↑m 𝑁) is the base set of (𝑅 freeLMod 𝑁), see frlmbasmap 21796. See also the statements in [Lang] p. 508. | ||
Syntax | cmvmul 22561 | Syntax for the operator for the multiplication of a vector with a matrix. |
class maVecMul | ||
Definition | df-mvmul 22562* | The operator which multiplies an M x N -matrix with an N-dimensional vector. (Contributed by AV, 23-Feb-2019.) |
⊢ maVecMul = (𝑟 ∈ V, 𝑜 ∈ V ↦ ⦋(1st ‘𝑜) / 𝑚⦌⦋(2nd ‘𝑜) / 𝑛⦌(𝑥 ∈ ((Base‘𝑟) ↑m (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑖 ∈ 𝑚 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗))))))) | ||
Theorem | mvmulfval 22563* | Functional value of the matrix vector multiplication operator. (Contributed by AV, 23-Feb-2019.) |
⊢ × = (𝑅 maVecMul 〈𝑀, 𝑁〉) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ Fin) & ⊢ (𝜑 → 𝑁 ∈ Fin) ⇒ ⊢ (𝜑 → × = (𝑥 ∈ (𝐵 ↑m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑m 𝑁) ↦ (𝑖 ∈ 𝑀 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑦‘𝑗))))))) | ||
Theorem | mvmulval 22564* | Multiplication of a vector with a matrix. (Contributed by AV, 23-Feb-2019.) |
⊢ × = (𝑅 maVecMul 〈𝑀, 𝑁〉) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ Fin) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁))) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m 𝑁)) ⇒ ⊢ (𝜑 → (𝑋 × 𝑌) = (𝑖 ∈ 𝑀 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗) · (𝑌‘𝑗)))))) | ||
Theorem | mvmulfv 22565* | A cell/element in the vector resulting from a multiplication of a vector with a matrix. (Contributed by AV, 23-Feb-2019.) |
⊢ × = (𝑅 maVecMul 〈𝑀, 𝑁〉) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ Fin) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁))) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m 𝑁)) & ⊢ (𝜑 → 𝐼 ∈ 𝑀) ⇒ ⊢ (𝜑 → ((𝑋 × 𝑌)‘𝐼) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝐼𝑋𝑗) · (𝑌‘𝑗))))) | ||
Theorem | mavmulval 22566* | Multiplication of a vector with a square matrix. (Contributed by AV, 23-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ × = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐴)) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m 𝑁)) ⇒ ⊢ (𝜑 → (𝑋 × 𝑌) = (𝑖 ∈ 𝑁 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗) · (𝑌‘𝑗)))))) | ||
Theorem | mavmulfv 22567* | A cell/element in the vector resulting from a multiplication of a vector with a square matrix. (Contributed by AV, 6-Dec-2018.) (Revised by AV, 18-Feb-2019.) (Revised by AV, 23-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ × = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐴)) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m 𝑁)) & ⊢ (𝜑 → 𝐼 ∈ 𝑁) ⇒ ⊢ (𝜑 → ((𝑋 × 𝑌)‘𝐼) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝐼𝑋𝑗) · (𝑌‘𝑗))))) | ||
Theorem | mavmulcl 22568 | Multiplication of an NxN matrix with an N-dimensional vector results in an N-dimensional vector. (Contributed by AV, 6-Dec-2018.) (Revised by AV, 23-Feb-2019.) (Proof shortened by AV, 23-Jul-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ × = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐴)) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m 𝑁)) ⇒ ⊢ (𝜑 → (𝑋 × 𝑌) ∈ (𝐵 ↑m 𝑁)) | ||
Theorem | 1mavmul 22569 | Multiplication of the identity NxN matrix with an N-dimensional vector results in the vector itself. (Contributed by AV, 9-Feb-2019.) (Revised by AV, 23-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m 𝑁)) ⇒ ⊢ (𝜑 → ((1r‘𝐴) · 𝑌) = 𝑌) | ||
Theorem | mavmulass 22570 | Associativity of the multiplication of two NxN matrices with an N-dimensional vector. (Contributed by AV, 9-Feb-2019.) (Revised by AV, 25-Feb-2019.) (Proof shortened by AV, 22-Jul-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m 𝑁)) & ⊢ × = (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐴)) & ⊢ (𝜑 → 𝑍 ∈ (Base‘𝐴)) ⇒ ⊢ (𝜑 → ((𝑋 × 𝑍) · 𝑌) = (𝑋 · (𝑍 · 𝑌))) | ||
Theorem | mavmuldm 22571 | The domain of the matrix vector multiplication function. (Contributed by AV, 27-Feb-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (𝐵 ↑m (𝑀 × 𝑁)) & ⊢ 𝐷 = (𝐵 ↑m 𝑁) & ⊢ · = (𝑅 maVecMul 〈𝑀, 𝑁〉) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin) → dom · = (𝐶 × 𝐷)) | ||
Theorem | mavmulsolcl 22572 | Every solution of the equation 𝐴∗𝑋 = 𝑌 for a matrix 𝐴 and a vector 𝐵 is a vector. (Contributed by AV, 27-Feb-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (𝐵 ↑m (𝑀 × 𝑁)) & ⊢ 𝐷 = (𝐵 ↑m 𝑁) & ⊢ · = (𝑅 maVecMul 〈𝑀, 𝑁〉) & ⊢ 𝐸 = (𝐵 ↑m 𝑀) ⇒ ⊢ (((𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅) ∧ (𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸)) → ((𝐴 · 𝑋) = 𝑌 → 𝑋 ∈ 𝐷)) | ||
Theorem | mavmul0 22573 | Multiplication of a 0-dimensional matrix with a 0-dimensional vector. (Contributed by AV, 28-Feb-2019.) |
⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) ⇒ ⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ 𝑉) → (∅ · ∅) = ∅) | ||
Theorem | mavmul0g 22574 | The result of the 0-dimensional multiplication of a matrix with a vector is always the empty set. (Contributed by AV, 1-Mar-2019.) |
⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) ⇒ ⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ 𝑉) → (𝑋 · 𝑌) = ∅) | ||
Theorem | mvmumamul1 22575* | The multiplication of an MxN matrix with an N-dimensional vector corresponds to the matrix multiplication of an MxN matrix with an Nx1 matrix. (Contributed by AV, 14-Mar-2019.) |
⊢ × = (𝑅 maMul 〈𝑀, 𝑁, {∅}〉) & ⊢ · = (𝑅 maVecMul 〈𝑀, 𝑁〉) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ Fin) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m (𝑀 × 𝑁))) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m 𝑁)) & ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m (𝑁 × {∅}))) ⇒ ⊢ (𝜑 → (∀𝑗 ∈ 𝑁 (𝑌‘𝑗) = (𝑗𝑍∅) → ∀𝑖 ∈ 𝑀 ((𝐴 · 𝑌)‘𝑖) = (𝑖(𝐴 × 𝑍)∅))) | ||
Theorem | mavmumamul1 22576* | The multiplication of an NxN matrix with an N-dimensional vector corresponds to the matrix multiplication of an NxN matrix with an Nx1 matrix. (Contributed by AV, 14-Mar-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ × = (𝑅 maMul 〈𝑁, 𝑁, {∅}〉) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐴)) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m 𝑁)) & ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑m (𝑁 × {∅}))) ⇒ ⊢ (𝜑 → (∀𝑗 ∈ 𝑁 (𝑌‘𝑗) = (𝑗𝑍∅) → ∀𝑖 ∈ 𝑁 ((𝑋 · 𝑌)‘𝑖) = (𝑖(𝑋 × 𝑍)∅))) | ||
Syntax | cmarrep 22577 | Syntax for the row replacing function for a square matrix. |
class matRRep | ||
Syntax | cmatrepV 22578 | Syntax for the function replacing a column of a matrix by a vector. |
class matRepV | ||
Definition | df-marrep 22579* | Define the matrices whose k-th row is replaced by 0's and an arbitrary element of the underlying ring at the l-th column. (Contributed by AV, 12-Feb-2019.) |
⊢ matRRep = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)), 𝑠 ∈ (Base‘𝑟) ↦ (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, (0g‘𝑟)), (𝑖𝑚𝑗)))))) | ||
Definition | df-marepv 22580* | Function replacing a column of a matrix by a vector. (Contributed by AV, 9-Feb-2019.) (Revised by AV, 26-Feb-2019.) |
⊢ matRepV = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)), 𝑣 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑘 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑗 = 𝑘, (𝑣‘𝑖), (𝑖𝑚𝑗)))))) | ||
Theorem | marrepfval 22581* | First substitution for the definition of the matrix row replacement function. (Contributed by AV, 12-Feb-2019.) (Proof shortened by AV, 2-Mar-2024.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑄 = (𝑁 matRRep 𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ 𝑄 = (𝑚 ∈ 𝐵, 𝑠 ∈ (Base‘𝑅) ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, 0 ), (𝑖𝑚𝑗))))) | ||
Theorem | marrepval0 22582* | Second substitution for the definition of the matrix row replacement function. (Contributed by AV, 12-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑄 = (𝑁 matRRep 𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝑆 ∈ (Base‘𝑅)) → (𝑀𝑄𝑆) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑆, 0 ), (𝑖𝑀𝑗))))) | ||
Theorem | marrepval 22583* | Third substitution for the definition of the matrix row replacement function. (Contributed by AV, 12-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑄 = (𝑁 matRRep 𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (((𝑀 ∈ 𝐵 ∧ 𝑆 ∈ (Base‘𝑅)) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁)) → (𝐾(𝑀𝑄𝑆)𝐿) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 𝑆, 0 ), (𝑖𝑀𝑗)))) | ||
Theorem | marrepeval 22584 | An entry of a matrix with a replaced row. (Contributed by AV, 12-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑄 = (𝑁 matRRep 𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (((𝑀 ∈ 𝐵 ∧ 𝑆 ∈ (Base‘𝑅)) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝐾(𝑀𝑄𝑆)𝐿)𝐽) = if(𝐼 = 𝐾, if(𝐽 = 𝐿, 𝑆, 0 ), (𝐼𝑀𝐽))) | ||
Theorem | marrepcl 22585 | Closure of the row replacement function for square matrices. (Contributed by AV, 13-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ (Base‘𝑅)) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁)) → (𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐿) ∈ 𝐵) | ||
Theorem | marepvfval 22586* | First substitution for the definition of the function replacing a column of a matrix by a vector. (Contributed by AV, 14-Feb-2019.) (Revised by AV, 26-Feb-2019.) (Proof shortened by AV, 2-Mar-2024.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑄 = (𝑁 matRepV 𝑅) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) ⇒ ⊢ 𝑄 = (𝑚 ∈ 𝐵, 𝑣 ∈ 𝑉 ↦ (𝑘 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑗 = 𝑘, (𝑣‘𝑖), (𝑖𝑚𝑗))))) | ||
Theorem | marepvval0 22587* | Second substitution for the definition of the function replacing a column of a matrix by a vector. (Contributed by AV, 14-Feb-2019.) (Revised by AV, 26-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑄 = (𝑁 matRepV 𝑅) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉) → (𝑀𝑄𝐶) = (𝑘 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑗 = 𝑘, (𝐶‘𝑖), (𝑖𝑀𝑗))))) | ||
Theorem | marepvval 22588* | Third substitution for the definition of the function replacing a column of a matrix by a vector. (Contributed by AV, 14-Feb-2019.) (Revised by AV, 26-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑄 = (𝑁 matRepV 𝑅) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁) → ((𝑀𝑄𝐶)‘𝐾) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑗 = 𝐾, (𝐶‘𝑖), (𝑖𝑀𝑗)))) | ||
Theorem | marepveval 22589 | An entry of a matrix with a replaced column. (Contributed by AV, 14-Feb-2019.) (Revised by AV, 26-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑄 = (𝑁 matRepV 𝑅) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) ⇒ ⊢ (((𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼((𝑀𝑄𝐶)‘𝐾)𝐽) = if(𝐽 = 𝐾, (𝐶‘𝐼), (𝐼𝑀𝐽))) | ||
Theorem | marepvcl 22590 | Closure of the column replacement function for square matrices. (Contributed by AV, 14-Feb-2019.) (Revised by AV, 26-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁)) → ((𝑀(𝑁 matRepV 𝑅)𝐶)‘𝐾) ∈ 𝐵) | ||
Theorem | ma1repvcl 22591 | Closure of the column replacement function for identity matrices. (Contributed by AV, 15-Feb-2019.) (Revised by AV, 26-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 1 = (1r‘𝐴) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) ∧ (𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁)) → (( 1 (𝑁 matRepV 𝑅)𝐶)‘𝐾) ∈ 𝐵) | ||
Theorem | ma1repveval 22592 | An entry of an identity matrix with a replaced column. (Contributed by AV, 16-Feb-2019.) (Revised by AV, 26-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 1 = (1r‘𝐴) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐸 = (( 1 (𝑁 matRepV 𝑅)𝐶)‘𝐾) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼𝐸𝐽) = if(𝐽 = 𝐾, (𝐶‘𝐼), if(𝐽 = 𝐼, (1r‘𝑅), 0 ))) | ||
Theorem | mulmarep1el 22593 | Element by element multiplication of a matrix with an identity matrix with a column replaced by a vector. (Contributed by AV, 16-Feb-2019.) (Revised by AV, 26-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 1 = (1r‘𝐴) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐸 = (( 1 (𝑁 matRepV 𝑅)𝐶)‘𝐾) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁)) → ((𝐼𝑋𝐿)(.r‘𝑅)(𝐿𝐸𝐽)) = if(𝐽 = 𝐾, ((𝐼𝑋𝐿)(.r‘𝑅)(𝐶‘𝐿)), if(𝐽 = 𝐿, (𝐼𝑋𝐿), 0 ))) | ||
Theorem | mulmarep1gsum1 22594* | The sum of element by element multiplications of a matrix with an identity matrix with a column replaced by a vector. (Contributed by AV, 16-Feb-2019.) (Revised by AV, 26-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 1 = (1r‘𝐴) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐸 = (( 1 (𝑁 matRepV 𝑅)𝐶)‘𝐾) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾)) → (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝐼𝑋𝑙)(.r‘𝑅)(𝑙𝐸𝐽)))) = (𝐼𝑋𝐽)) | ||
Theorem | mulmarep1gsum2 22595* | The sum of element by element multiplications of a matrix with an identity matrix with a column replaced by a vector. (Contributed by AV, 18-Feb-2019.) (Revised by AV, 26-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 1 = (1r‘𝐴) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐸 = (( 1 (𝑁 matRepV 𝑅)𝐶)‘𝐾) & ⊢ × = (𝑅 maVecMul 〈𝑁, 𝑁〉) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ (𝑋 × 𝐶) = 𝑍)) → (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝐼𝑋𝑙)(.r‘𝑅)(𝑙𝐸𝐽)))) = if(𝐽 = 𝐾, (𝑍‘𝐼), (𝐼𝑋𝐽))) | ||
Theorem | 1marepvmarrepid 22596 | Replacing the ith row by 0's and the ith component of a (column) vector at the diagonal position for the identity matrix with the ith column replaced by the vector results in the matrix itself. (Contributed by AV, 14-Feb-2019.) (Revised by AV, 27-Feb-2019.) |
⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 1 = (1r‘(𝑁 Mat 𝑅)) & ⊢ 𝑋 = (( 1 (𝑁 matRepV 𝑅)𝑍)‘𝐼) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) ∧ (𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉)) → (𝐼(𝑋(𝑁 matRRep 𝑅)(𝑍‘𝐼))𝐼) = 𝑋) | ||
Syntax | csubma 22597 | Syntax for submatrices of a square matrix. |
class subMat | ||
Definition | df-subma 22598* | Define the submatrices of a square matrix. A submatrix is obtained by deleting a row and a column of the original matrix. Since the indices of a matrix need not to be sequential integers, it does not matter that there may be gaps in the numbering of the indices for the submatrix. The determinants of such submatrices are called the "minors" of the original matrix. (Contributed by AV, 27-Dec-2018.) |
⊢ subMat = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ (𝑛 ∖ {𝑘}), 𝑗 ∈ (𝑛 ∖ {𝑙}) ↦ (𝑖𝑚𝑗))))) | ||
Theorem | submabas 22599* | Any subset of the index set of a square matrix defines a submatrix of the matrix. (Contributed by AV, 1-Jan-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐷 ⊆ 𝑁) → (𝑖 ∈ 𝐷, 𝑗 ∈ 𝐷 ↦ (𝑖𝑀𝑗)) ∈ (Base‘(𝐷 Mat 𝑅))) | ||
Theorem | submafval 22600* | First substitution for a submatrix. (Contributed by AV, 28-Dec-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (𝑁 subMat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ 𝑄 = (𝑚 ∈ 𝐵 ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ (𝑁 ∖ {𝑘}), 𝑗 ∈ (𝑁 ∖ {𝑙}) ↦ (𝑖𝑚𝑗)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |