Home | Metamath
Proof Explorer Theorem List (p. 204 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dmatid 20301 | 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 20302 | 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 20303* | 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 20304 | 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 20305 | 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 20306 | 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 20307 | 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 20308 | 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 20309 | 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 20310* | 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 20311* | An 𝑁 x 𝑁 scalar matrix over (a ring) 𝑅. (Contributed by AV, 18-Dec-2019.) |
⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 1 = (1r‘𝐴) & ⊢ · = ( ·𝑠 ‘𝐴) & ⊢ 𝑆 = (𝑁 ScMat 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑀 ∈ 𝑆 ↔ (𝑀 ∈ 𝐵 ∧ ∃𝑐 ∈ 𝐾 𝑀 = (𝑐 · 1 )))) | ||
Theorem | scmatscmid 20312* | 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 20313 | 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 20314 | 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 20315 | 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 20316* | 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 20317* | 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 20318* | Alternate proof of scmate 20316: An entry of an 𝑁 x 𝑁 scalar matrix over the ring 𝑅. This prove makes use of scmatmats 20317 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 20319* | 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 20320 | 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 20321 | 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 20322 | 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 20323 | 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 20324 | 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 20325 | 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 20326 | 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 20327 | 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 20328 | 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 20329 | 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 20330 | Closure of the scalar multiplication in the ring of scalar matrices. (matvscl 20237 analog.) (Contributed by AV, 24-Dec-2019.) |
⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑆 = (𝑁 ScMat 𝑅) & ⊢ ∗ = ( ·𝑠 ‘𝐴) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑆)) → (𝐶 ∗ 𝑋) ∈ 𝑆) | ||
Theorem | scmatlss 20331 | 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 20332 | 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 20333* | The value of the ring homomorphism 𝐹. (Contributed by AV, 22-Dec-2019.) |
⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 1 = (1r‘𝐴) & ⊢ ∗ = ( ·𝑠 ‘𝐴) & ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ (𝑥 ∗ 1 )) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾) → (𝐹‘𝑋) = (𝑋 ∗ 1 )) | ||
Theorem | scmatrhmcl 20334* | 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 20335* | 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 20336* | 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 20337* | 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 20338* | 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 20339* | 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 20340* | 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 20341* | 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 20342* | 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 20343 | 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 20344 | The empty matrix over a ring is a scalar matrix (and therefore, by scmatdmat 20321, also a diagonal matrix). (Contributed by AV, 21-Dec-2019.) |
⊢ (𝑅 ∈ Ring → ∅ ∈ (∅ ScMat 𝑅)) | ||
Theorem | mat1scmat 20345 | A 1-dimensional matrix over a ring is always a scalar matrix (and therefore, by scmatdmat 20321, 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 20190 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 20347 for the multiplication of a matrix with a column vector. In most cases, it is sufficient to regard members of ((Base‘𝑅) ↑𝑚 𝑁) as "column vectors", because ((Base‘𝑅) ↑𝑚 𝑁) is the base set of (𝑅 freeLMod 𝑁), see frlmbasmap 20103. See also the statements in [Lang] p. 508. | ||
Syntax | cmvmul 20346 | Syntax for the operator for the multiplication of a vector with a matrix. |
class maVecMul | ||
Definition | df-mvmul 20347* | 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‘𝑟) ↑𝑚 (𝑚 × 𝑛)), 𝑦 ∈ ((Base‘𝑟) ↑𝑚 𝑛) ↦ (𝑖 ∈ 𝑚 ↦ (𝑟 Σg (𝑗 ∈ 𝑛 ↦ ((𝑖𝑥𝑗)(.r‘𝑟)(𝑦‘𝑗))))))) | ||
Theorem | mvmulfval 20348* | Functional value of the matrix vector multiplication operator. (Contributed by AV, 23-Feb-2019.) |
⊢ × = (𝑅 maVecMul 〈𝑀, 𝑁〉) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ Fin) & ⊢ (𝜑 → 𝑁 ∈ Fin) ⇒ ⊢ (𝜑 → × = (𝑥 ∈ (𝐵 ↑𝑚 (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑𝑚 𝑁) ↦ (𝑖 ∈ 𝑀 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑦‘𝑗))))))) | ||
Theorem | mvmulval 20349* | Multiplication of a vector with a matrix. (Contributed by AV, 23-Feb-2019.) |
⊢ × = (𝑅 maVecMul 〈𝑀, 𝑁〉) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ Fin) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑𝑚 (𝑀 × 𝑁))) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑𝑚 𝑁)) ⇒ ⊢ (𝜑 → (𝑋 × 𝑌) = (𝑖 ∈ 𝑀 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗) · (𝑌‘𝑗)))))) | ||
Theorem | mvmulfv 20350* | 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) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑𝑚 (𝑀 × 𝑁))) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑𝑚 𝑁)) & ⊢ (𝜑 → 𝐼 ∈ 𝑀) ⇒ ⊢ (𝜑 → ((𝑋 × 𝑌)‘𝐼) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝐼𝑋𝑗) · (𝑌‘𝑗))))) | ||
Theorem | mavmulval 20351* | Multiplication of a vector with a square matrix. (Contributed by AV, 23-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ × = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐴)) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑𝑚 𝑁)) ⇒ ⊢ (𝜑 → (𝑋 × 𝑌) = (𝑖 ∈ 𝑁 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗) · (𝑌‘𝑗)))))) | ||
Theorem | mavmulfv 20352* | 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‘𝐴)) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑𝑚 𝑁)) & ⊢ (𝜑 → 𝐼 ∈ 𝑁) ⇒ ⊢ (𝜑 → ((𝑋 × 𝑌)‘𝐼) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝐼𝑋𝑗) · (𝑌‘𝑗))))) | ||
Theorem | mavmulcl 20353 | 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‘𝐴)) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑𝑚 𝑁)) ⇒ ⊢ (𝜑 → (𝑋 × 𝑌) ∈ (𝐵 ↑𝑚 𝑁)) | ||
Theorem | 1mavmul 20354 | 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) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑𝑚 𝑁)) ⇒ ⊢ (𝜑 → ((1r‘𝐴) · 𝑌) = 𝑌) | ||
Theorem | mavmulass 20355 | 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) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑𝑚 𝑁)) & ⊢ × = (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐴)) & ⊢ (𝜑 → 𝑍 ∈ (Base‘𝐴)) ⇒ ⊢ (𝜑 → ((𝑋 × 𝑍) · 𝑌) = (𝑋 · (𝑍 · 𝑌))) | ||
Theorem | mavmuldm 20356 | The domain of the matrix vector multiplication function. (Contributed by AV, 27-Feb-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (𝐵 ↑𝑚 (𝑀 × 𝑁)) & ⊢ 𝐷 = (𝐵 ↑𝑚 𝑁) & ⊢ · = (𝑅 maVecMul 〈𝑀, 𝑁〉) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin) → dom · = (𝐶 × 𝐷)) | ||
Theorem | mavmulsolcl 20357 | Every solution of the equation 𝐴∗𝑋 = 𝑌 for a matrix 𝐴 and a vector 𝐵 is a vector. (Contributed by AV, 27-Feb-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (𝐵 ↑𝑚 (𝑀 × 𝑁)) & ⊢ 𝐷 = (𝐵 ↑𝑚 𝑁) & ⊢ · = (𝑅 maVecMul 〈𝑀, 𝑁〉) & ⊢ 𝐸 = (𝐵 ↑𝑚 𝑀) ⇒ ⊢ (((𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑀 ≠ ∅) ∧ (𝑅 ∈ 𝑉 ∧ 𝑌 ∈ 𝐸)) → ((𝐴 · 𝑋) = 𝑌 → 𝑋 ∈ 𝐷)) | ||
Theorem | mavmul0 20358 | Multiplication of a 0-dimensional matrix with a 0-dimensional vector. (Contributed by AV, 28-Feb-2019.) |
⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) ⇒ ⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ 𝑉) → (∅ · ∅) = ∅) | ||
Theorem | mavmul0g 20359 | 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 20360* | 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) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑𝑚 (𝑀 × 𝑁))) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑𝑚 𝑁)) & ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑𝑚 (𝑁 × {∅}))) ⇒ ⊢ (𝜑 → (∀𝑗 ∈ 𝑁 (𝑌‘𝑗) = (𝑗𝑍∅) → ∀𝑖 ∈ 𝑀 ((𝐴 · 𝑌)‘𝑖) = (𝑖(𝐴 × 𝑍)∅))) | ||
Theorem | mavmumamul1 20361* | 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‘𝐴)) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑𝑚 𝑁)) & ⊢ (𝜑 → 𝑍 ∈ (𝐵 ↑𝑚 (𝑁 × {∅}))) ⇒ ⊢ (𝜑 → (∀𝑗 ∈ 𝑁 (𝑌‘𝑗) = (𝑗𝑍∅) → ∀𝑖 ∈ 𝑁 ((𝑋 · 𝑌)‘𝑖) = (𝑖(𝑋 × 𝑍)∅))) | ||
Syntax | cmarrep 20362 | Syntax for the row replacing function for a square matrix. |
class matRRep | ||
Syntax | cmatrepV 20363 | Syntax for the function replacing a column of a matrix by a vector. |
class matRepV | ||
Definition | df-marrep 20364* | 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 20365* | 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‘𝑟) ↑𝑚 𝑛) ↦ (𝑘 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑗 = 𝑘, (𝑣‘𝑖), (𝑖𝑚𝑗)))))) | ||
Theorem | marrepfval 20366* | First 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 | marrepval0 20367* | 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 20368* | 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 20369 | 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 20370 | Closure of the row replacement function for square matrices. (Contributed by AV, 13-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ (Base‘𝑅)) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁)) → (𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐿) ∈ 𝐵) | ||
Theorem | marepvfval 20371* | 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.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑄 = (𝑁 matRepV 𝑅) & ⊢ 𝑉 = ((Base‘𝑅) ↑𝑚 𝑁) ⇒ ⊢ 𝑄 = (𝑚 ∈ 𝐵, 𝑣 ∈ 𝑉 ↦ (𝑘 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑗 = 𝑘, (𝑣‘𝑖), (𝑖𝑚𝑗))))) | ||
Theorem | marepvval0 20372* | 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‘𝑅) ↑𝑚 𝑁) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉) → (𝑀𝑄𝐶) = (𝑘 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑗 = 𝑘, (𝐶‘𝑖), (𝑖𝑀𝑗))))) | ||
Theorem | marepvval 20373* | 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‘𝑅) ↑𝑚 𝑁) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁) → ((𝑀𝑄𝐶)‘𝐾) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑗 = 𝐾, (𝐶‘𝑖), (𝑖𝑀𝑗)))) | ||
Theorem | marepveval 20374 | 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‘𝑅) ↑𝑚 𝑁) ⇒ ⊢ (((𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼((𝑀𝑄𝐶)‘𝐾)𝐽) = if(𝐽 = 𝐾, (𝐶‘𝐼), (𝐼𝑀𝐽))) | ||
Theorem | marepvcl 20375 | Closure of the column replacement function for square matrices. (Contributed by AV, 14-Feb-2019.) (Revised by AV, 26-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑𝑚 𝑁) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁)) → ((𝑀(𝑁 matRepV 𝑅)𝐶)‘𝐾) ∈ 𝐵) | ||
Theorem | ma1repvcl 20376 | Closure of the column replacement function for identity matrices. (Contributed by AV, 15-Feb-2019.) (Revised by AV, 26-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑𝑚 𝑁) & ⊢ 1 = (1r‘𝐴) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) ∧ (𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁)) → (( 1 (𝑁 matRepV 𝑅)𝐶)‘𝐾) ∈ 𝐵) | ||
Theorem | ma1repveval 20377 | 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‘𝑅) ↑𝑚 𝑁) & ⊢ 1 = (1r‘𝐴) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐸 = (( 1 (𝑁 matRepV 𝑅)𝐶)‘𝐾) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑀 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼𝐸𝐽) = if(𝐽 = 𝐾, (𝐶‘𝐼), if(𝐽 = 𝐼, (1r‘𝑅), 0 ))) | ||
Theorem | mulmarep1el 20378 | 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‘𝑅) ↑𝑚 𝑁) & ⊢ 1 = (1r‘𝐴) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐸 = (( 1 (𝑁 matRepV 𝑅)𝐶)‘𝐾) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁)) → ((𝐼𝑋𝐿)(.r‘𝑅)(𝐿𝐸𝐽)) = if(𝐽 = 𝐾, ((𝐼𝑋𝐿)(.r‘𝑅)(𝐶‘𝐿)), if(𝐽 = 𝐿, (𝐼𝑋𝐿), 0 ))) | ||
Theorem | mulmarep1gsum1 20379* | 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‘𝑅) ↑𝑚 𝑁) & ⊢ 1 = (1r‘𝐴) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐸 = (( 1 (𝑁 matRepV 𝑅)𝐶)‘𝐾) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝐽 ≠ 𝐾)) → (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝐼𝑋𝑙)(.r‘𝑅)(𝑙𝐸𝐽)))) = (𝐼𝑋𝐽)) | ||
Theorem | mulmarep1gsum2 20380* | 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‘𝑅) ↑𝑚 𝑁) & ⊢ 1 = (1r‘𝐴) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐸 = (( 1 (𝑁 matRepV 𝑅)𝐶)‘𝐾) & ⊢ × = (𝑅 maVecMul 〈𝑁, 𝑁〉) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ (𝑋 × 𝐶) = 𝑍)) → (𝑅 Σg (𝑙 ∈ 𝑁 ↦ ((𝐼𝑋𝑙)(.r‘𝑅)(𝑙𝐸𝐽)))) = if(𝐽 = 𝐾, (𝑍‘𝐼), (𝐼𝑋𝐽))) | ||
Theorem | 1marepvmarrepid 20381 | 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‘𝑅) ↑𝑚 𝑁) & ⊢ 1 = (1r‘(𝑁 Mat 𝑅)) & ⊢ 𝑋 = (( 1 (𝑁 matRepV 𝑅)𝑍)‘𝐼) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) ∧ (𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉)) → (𝐼(𝑋(𝑁 matRRep 𝑅)(𝑍‘𝐼))𝐼) = 𝑋) | ||
Syntax | csubma 20382 | Syntax for submatrices of a square matrix. |
class subMat | ||
Definition | df-subma 20383* | 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 20384* | 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 20385* | First substitution for a submatrix. (Contributed by AV, 28-Dec-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (𝑁 subMat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ 𝑄 = (𝑚 ∈ 𝐵 ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ (𝑁 ∖ {𝑘}), 𝑗 ∈ (𝑁 ∖ {𝑙}) ↦ (𝑖𝑚𝑗)))) | ||
Theorem | submaval0 20386* | Second substitution for a submatrix. (Contributed by AV, 28-Dec-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (𝑁 subMat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ (𝑀 ∈ 𝐵 → (𝑄‘𝑀) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ (𝑁 ∖ {𝑘}), 𝑗 ∈ (𝑁 ∖ {𝑙}) ↦ (𝑖𝑀𝑗)))) | ||
Theorem | submaval 20387* | Third substitution for a submatrix. (Contributed by AV, 28-Dec-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (𝑁 subMat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → (𝐾(𝑄‘𝑀)𝐿) = (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝑀𝑗))) | ||
Theorem | submaeval 20388 | An entry of a submatrix of a square matrix. (Contributed by AV, 28-Dec-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (𝑁 subMat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) ∧ (𝐼 ∈ (𝑁 ∖ {𝐾}) ∧ 𝐽 ∈ (𝑁 ∖ {𝐿}))) → (𝐼(𝐾(𝑄‘𝑀)𝐿)𝐽) = (𝐼𝑀𝐽)) | ||
Theorem | 1marepvsma1 20389 | The submatrix of the identity matrix with the ith column replaced by the vector obtained by removing the ith row and the ith column is an identity matrix. (Contributed by AV, 14-Feb-2019.) (Revised by AV, 27-Feb-2019.) |
⊢ 𝑉 = ((Base‘𝑅) ↑𝑚 𝑁) & ⊢ 1 = (1r‘(𝑁 Mat 𝑅)) & ⊢ 𝑋 = (( 1 (𝑁 matRepV 𝑅)𝑍)‘𝐼) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) ∧ (𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉)) → (𝐼((𝑁 subMat 𝑅)‘𝑋)𝐼) = (1r‘((𝑁 ∖ {𝐼}) Mat 𝑅))) | ||
Syntax | cmdat 20390 | Syntax for the matrix determinant function. |
class maDet | ||
Definition | df-mdet 20391* | Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib 20393). The properties of the axiomatic definition of a determinant according to [Weierstrass] p. 272 are derived from this definition as theorems: "The determinant function is the unique multilinear, alternating and normalized function from the algebra of square matrices of the same dimension over a commutative ring to this ring". The functionality is shown by mdetf 20401. Multilineary means "linear for each row" - the additivity is shown by mdetrlin 20408, the homogeneity by mdetrsca 20409. Furthermore, it is shown that the determinant function is alternating (see mdetralt 20414) and normalized (see mdet1 20407). Finally, the uniqueness is shown by mdetuni 20428. As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib 20393. (Contributed by Stefan O'Rear, 9-Sep-2015.) (Revised by SO, 10-Jul-2018.) |
⊢ maDet = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑟 Σg (𝑝 ∈ (Base‘(SymGrp‘𝑛)) ↦ ((((ℤRHom‘𝑟) ∘ (pmSgn‘𝑛))‘𝑝)(.r‘𝑟)((mulGrp‘𝑟) Σg (𝑥 ∈ 𝑛 ↦ ((𝑝‘𝑥)𝑚𝑥)))))))) | ||
Theorem | mdetfval 20392* | First substitution for the determinant definition. (Contributed by Stefan O'Rear, 9-Sep-2015.) (Revised by SO, 9-Jul-2018.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ · = (.r‘𝑅) & ⊢ 𝑈 = (mulGrp‘𝑅) ⇒ ⊢ 𝐷 = (𝑚 ∈ 𝐵 ↦ (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥))))))) | ||
Theorem | mdetleib 20393* | Full substitution of our determinant definition (also known as Leibniz' Formula, expanding by columns). Proposition 4.6 in [Lang] p. 514. (Contributed by Stefan O'Rear, 3-Oct-2015.) (Revised by SO, 9-Jul-2018.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ · = (.r‘𝑅) & ⊢ 𝑈 = (mulGrp‘𝑅) ⇒ ⊢ (𝑀 ∈ 𝐵 → (𝐷‘𝑀) = (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥))))))) | ||
Theorem | mdetleib2 20394* | Leibniz' formula can also be expanded by rows. (Contributed by Stefan O'Rear, 9-Jul-2018.) (Proof shortened by AV, 23-Jul-2019.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ · = (.r‘𝑅) & ⊢ 𝑈 = (mulGrp‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (𝑅 Σg (𝑝 ∈ 𝑃 ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ (𝑥𝑀(𝑝‘𝑥)))))))) | ||
Theorem | nfimdetndef 20395 | The determinant is not defined for an infinite matrix. (Contributed by AV, 27-Dec-2018.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) ⇒ ⊢ (𝑁 ∉ Fin → 𝐷 = ∅) | ||
Theorem | mdetfval1 20396* | First substitution of an alternative determinant definition. (Contributed by Stefan O'Rear, 9-Sep-2015.) (Revised by AV, 27-Dec-2018.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ · = (.r‘𝑅) & ⊢ 𝑈 = (mulGrp‘𝑅) ⇒ ⊢ 𝐷 = (𝑚 ∈ 𝐵 ↦ (𝑅 Σg (𝑝 ∈ 𝑃 ↦ ((𝑌‘(𝑆‘𝑝)) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑚𝑥))))))) | ||
Theorem | mdetleib1 20397* | Full substitution of an alternative determinant definition (also known as Leibniz' Formula). (Contributed by Stefan O'Rear, 3-Oct-2015.) (Revised by AV, 26-Dec-2018.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ · = (.r‘𝑅) & ⊢ 𝑈 = (mulGrp‘𝑅) ⇒ ⊢ (𝑀 ∈ 𝐵 → (𝐷‘𝑀) = (𝑅 Σg (𝑝 ∈ 𝑃 ↦ ((𝑌‘(𝑆‘𝑝)) · (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)𝑀𝑥))))))) | ||
Theorem | mdet0pr 20398 | The determinant for 0-dimensional matrices is a singleton containing an ordered pair with the singleton containing the empty set as first component, and the singleton containing the 1 element of the underlying ring as second component. (Contributed by AV, 28-Feb-2019.) |
⊢ (𝑅 ∈ Ring → (∅ maDet 𝑅) = {〈∅, (1r‘𝑅)〉}) | ||
Theorem | mdet0f1o 20399 | The determinant for 0-dimensional matrices is a one-to-one function from the singleton containing the empty set onto the singleton containing the 1 element of the underlying ring.function x is . (Contributed by AV, 28-Feb-2019.) |
⊢ (𝑅 ∈ Ring → (∅ maDet 𝑅):{∅}–1-1-onto→{(1r‘𝑅)}) | ||
Theorem | mdet0fv0 20400 | The determinant of a 0-dimensional matrix is the 1 element of the underlying ring . (Contributed by AV, 28-Feb-2019.) |
⊢ (𝑅 ∈ Ring → ((∅ maDet 𝑅)‘∅) = (1r‘𝑅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |