![]() |
Metamath
Proof Explorer Theorem List (p. 226 of 486) | < 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-30851) |
![]() (30852-32374) |
![]() (32375-48553) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | scmatscmiddistr 22501 | 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 22502 | 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 22503* | 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 22504* | 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 22505* | Alternate proof of scmate 22503: An entry of an 𝑁 x 𝑁 scalar matrix over the ring 𝑅. This prove makes use of scmatmats 22504 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 22506* | 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 22507 | 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 22508 | 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 22509 | 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 22510 | 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 22511 | 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 22512 | 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 22513 | 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 22514 | 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 22515 | 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 22516 | 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 22517 | Closure of the scalar multiplication in the ring of scalar matrices. (matvscl 22424 analog.) (Contributed by AV, 24-Dec-2019.) |
⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑆 = (𝑁 ScMat 𝑅) & ⊢ ∗ = ( ·𝑠 ‘𝐴) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑆)) → (𝐶 ∗ 𝑋) ∈ 𝑆) | ||
Theorem | scmatlss 22518 | 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 22519 | 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 22520* | The value of the ring homomorphism 𝐹. (Contributed by AV, 22-Dec-2019.) |
⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 1 = (1r‘𝐴) & ⊢ ∗ = ( ·𝑠 ‘𝐴) & ⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ (𝑥 ∗ 1 )) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾) → (𝐹‘𝑋) = (𝑋 ∗ 1 )) | ||
Theorem | scmatrhmcl 22521* | 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 22522* | 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 22523* | 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 22524* | 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 22525* | 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 22526* | 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 22527* | 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 22528* | 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 22529* | 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 22530 | 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 22531 | The empty matrix over a ring is a scalar matrix (and therefore, by scmatdmat 22508, also a diagonal matrix). (Contributed by AV, 21-Dec-2019.) |
⊢ (𝑅 ∈ Ring → ∅ ∈ (∅ ScMat 𝑅)) | ||
Theorem | mat1scmat 22532 | A 1-dimensional matrix over a ring is always a scalar matrix (and therefore, by scmatdmat 22508, 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 22382 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 22534 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 21757. See also the statements in [Lang] p. 508. | ||
Syntax | cmvmul 22533 | Syntax for the operator for the multiplication of a vector with a matrix. |
class maVecMul | ||
Definition | df-mvmul 22534* | 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 22535* | Functional value of the matrix vector multiplication operator. (Contributed by AV, 23-Feb-2019.) |
⊢ × = (𝑅 maVecMul 〈𝑀, 𝑁〉) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ Fin) & ⊢ (𝜑 → 𝑁 ∈ Fin) ⇒ ⊢ (𝜑 → × = (𝑥 ∈ (𝐵 ↑m (𝑀 × 𝑁)), 𝑦 ∈ (𝐵 ↑m 𝑁) ↦ (𝑖 ∈ 𝑀 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑥𝑗) · (𝑦‘𝑗))))))) | ||
Theorem | mvmulval 22536* | Multiplication of a vector with a matrix. (Contributed by AV, 23-Feb-2019.) |
⊢ × = (𝑅 maVecMul 〈𝑀, 𝑁〉) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ Fin) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m (𝑀 × 𝑁))) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m 𝑁)) ⇒ ⊢ (𝜑 → (𝑋 × 𝑌) = (𝑖 ∈ 𝑀 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗) · (𝑌‘𝑗)))))) | ||
Theorem | mvmulfv 22537* | 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 22538* | Multiplication of a vector with a square matrix. (Contributed by AV, 23-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ × = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐴)) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 ↑m 𝑁)) ⇒ ⊢ (𝜑 → (𝑋 × 𝑌) = (𝑖 ∈ 𝑁 ↦ (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝑖𝑋𝑗) · (𝑌‘𝑗)))))) | ||
Theorem | mavmulfv 22539* | 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 22540 | 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 22541 | 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 22542 | 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 22543 | The domain of the matrix vector multiplication function. (Contributed by AV, 27-Feb-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐶 = (𝐵 ↑m (𝑀 × 𝑁)) & ⊢ 𝐷 = (𝐵 ↑m 𝑁) & ⊢ · = (𝑅 maVecMul 〈𝑀, 𝑁〉) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin) → dom · = (𝐶 × 𝐷)) | ||
Theorem | mavmulsolcl 22544 | 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 22545 | Multiplication of a 0-dimensional matrix with a 0-dimensional vector. (Contributed by AV, 28-Feb-2019.) |
⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) ⇒ ⊢ ((𝑁 = ∅ ∧ 𝑅 ∈ 𝑉) → (∅ · ∅) = ∅) | ||
Theorem | mavmul0g 22546 | 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 22547* | 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 22548* | 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 22549 | Syntax for the row replacing function for a square matrix. |
class matRRep | ||
Syntax | cmatrepV 22550 | Syntax for the function replacing a column of a matrix by a vector. |
class matRepV | ||
Definition | df-marrep 22551* | 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 22552* | 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 22553* | 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 22554* | 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 22555* | 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 22556 | 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 22557 | Closure of the row replacement function for square matrices. (Contributed by AV, 13-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ (Base‘𝑅)) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁)) → (𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐿) ∈ 𝐵) | ||
Theorem | marepvfval 22558* | 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 22559* | 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 22560* | 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 22561 | 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 22562 | 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 22563 | 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 22564 | 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 22565 | 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 22566* | 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 22567* | 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 22568 | 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 22569 | Syntax for submatrices of a square matrix. |
class subMat | ||
Definition | df-subma 22570* | 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 22571* | 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 22572* | First substitution for a submatrix. (Contributed by AV, 28-Dec-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (𝑁 subMat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ 𝑄 = (𝑚 ∈ 𝐵 ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ (𝑁 ∖ {𝑘}), 𝑗 ∈ (𝑁 ∖ {𝑙}) ↦ (𝑖𝑚𝑗)))) | ||
Theorem | submaval0 22573* | Second substitution for a submatrix. (Contributed by AV, 28-Dec-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (𝑁 subMat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ (𝑀 ∈ 𝐵 → (𝑄‘𝑀) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ (𝑁 ∖ {𝑘}), 𝑗 ∈ (𝑁 ∖ {𝑙}) ↦ (𝑖𝑀𝑗)))) | ||
Theorem | submaval 22574* | Third substitution for a submatrix. (Contributed by AV, 28-Dec-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (𝑁 subMat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → (𝐾(𝑄‘𝑀)𝐿) = (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝑀𝑗))) | ||
Theorem | submaeval 22575 | An entry of a submatrix of a square matrix. (Contributed by AV, 28-Dec-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (𝑁 subMat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) ∧ (𝐼 ∈ (𝑁 ∖ {𝐾}) ∧ 𝐽 ∈ (𝑁 ∖ {𝐿}))) → (𝐼(𝐾(𝑄‘𝑀)𝐿)𝐽) = (𝐼𝑀𝐽)) | ||
Theorem | 1marepvsma1 22576 | 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‘𝑅) ↑m 𝑁) & ⊢ 1 = (1r‘(𝑁 Mat 𝑅)) & ⊢ 𝑋 = (( 1 (𝑁 matRepV 𝑅)𝑍)‘𝐼) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin) ∧ (𝐼 ∈ 𝑁 ∧ 𝑍 ∈ 𝑉)) → (𝐼((𝑁 subMat 𝑅)‘𝑋)𝐼) = (1r‘((𝑁 ∖ {𝐼}) Mat 𝑅))) | ||
Syntax | cmdat 22577 | Syntax for the matrix determinant function. |
class maDet | ||
Definition | df-mdet 22578* | Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib 22580). 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". Functionality is shown by mdetf 22588. Multilineary means "linear for each row" - the additivity is shown by mdetrlin 22595, the homogeneity by mdetrsca 22596. Furthermore, it is shown that the determinant function is alternating (see mdetralt 22601) and normalized (see mdet1 22594). Finally, uniqueness is shown by mdetuni 22615. As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib 22580. (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 22579* | 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 22580* | 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 22581* | 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 22582 | The determinant is not defined for an infinite matrix. (Contributed by AV, 27-Dec-2018.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) ⇒ ⊢ (𝑁 ∉ Fin → 𝐷 = ∅) | ||
Theorem | mdetfval1 22583* | 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 22584* | 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 22585 | The determinant function for 0-dimensional matrices on a given ring is the function mapping the empty set to the unity element of that ring. (Contributed by AV, 28-Feb-2019.) |
⊢ (𝑅 ∈ Ring → (∅ maDet 𝑅) = {〈∅, (1r‘𝑅)〉}) | ||
Theorem | mdet0f1o 22586 | The determinant function for 0-dimensional matrices on a given ring is a bijection from the singleton containing the empty set (empty matrix) onto the singleton containing the unity element of that ring. (Contributed by AV, 28-Feb-2019.) |
⊢ (𝑅 ∈ Ring → (∅ maDet 𝑅):{∅}–1-1-onto→{(1r‘𝑅)}) | ||
Theorem | mdet0fv0 22587 | The determinant of the empty matrix on a given ring is the unity element of that ring. (Contributed by AV, 28-Feb-2019.) |
⊢ (𝑅 ∈ Ring → ((∅ maDet 𝑅)‘∅) = (1r‘𝑅)) | ||
Theorem | mdetf 22588 | Functionality of the determinant, see also definition in [Lang] p. 513. (Contributed by Stefan O'Rear, 9-Jul-2018.) (Proof shortened by AV, 23-Jul-2019.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐾 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → 𝐷:𝐵⟶𝐾) | ||
Theorem | mdetcl 22589 | The determinant evaluates to an element of the base ring. (Contributed by Stefan O'Rear, 9-Sep-2015.) (Revised by AV, 7-Feb-2019.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐾 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) ∈ 𝐾) | ||
Theorem | m1detdiag 22590 | The determinant of a 1-dimensional matrix equals its (single) entry. (Contributed by AV, 6-Aug-2019.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (𝐼𝑀𝐼)) | ||
Theorem | mdetdiaglem 22591* | Lemma for mdetdiag 22592. Previously part of proof for mdet1 22594. (Contributed by SO, 10-Jul-2018.) (Revised by AV, 17-Aug-2019.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐻 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) ∧ (𝑃 ∈ 𝐻 ∧ 𝑃 ≠ ( I ↾ 𝑁))) → (((𝑍 ∘ 𝑆)‘𝑃) · (𝐺 Σg (𝑘 ∈ 𝑁 ↦ ((𝑃‘𝑘)𝑀𝑘)))) = 0 ) | ||
Theorem | mdetdiag 22592* | The determinant of a diagonal matrix is the product of the entries in the diagonal. (Contributed by AV, 17-Aug-2019.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑀 ∈ 𝐵) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 ) → (𝐷‘𝑀) = (𝐺 Σg (𝑘 ∈ 𝑁 ↦ (𝑘𝑀𝑘))))) | ||
Theorem | mdetdiagid 22593* | The determinant of a diagonal matrix with identical entries is the power of the entry in the diagonal. (Contributed by AV, 17-Aug-2019.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐶 = (Base‘𝑅) & ⊢ · = (.g‘𝐺) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑋 ∈ 𝐶)) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑀𝑗) = if(𝑖 = 𝑗, 𝑋, 0 ) → (𝐷‘𝑀) = ((♯‘𝑁) · 𝑋))) | ||
Theorem | mdet1 22594 | The determinant of the identity matrix is 1, i.e. the determinant function is normalized, see also definition in [Lang] p. 513. (Contributed by SO, 10-Jul-2018.) (Proof shortened by AV, 25-Nov-2019.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐼 = (1r‘𝐴) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) → (𝐷‘𝐼) = 1 ) | ||
Theorem | mdetrlin 22595 | The determinant function is additive for each row: The matrices X, Y, Z are identical except for the I's row, and the I's row of the matrix X is the componentwise sum of the I's row of the matrices Y and Z. In this case the determinant of X is the sum of the determinants of Y and Z. (Contributed by SO, 9-Jul-2018.) (Proof shortened by AV, 23-Jul-2019.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ + = (+g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐼 ∈ 𝑁) & ⊢ (𝜑 → (𝑋 ↾ ({𝐼} × 𝑁)) = ((𝑌 ↾ ({𝐼} × 𝑁)) ∘f + (𝑍 ↾ ({𝐼} × 𝑁)))) & ⊢ (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑌 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))) & ⊢ (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))) ⇒ ⊢ (𝜑 → (𝐷‘𝑋) = ((𝐷‘𝑌) + (𝐷‘𝑍))) | ||
Theorem | mdetrsca 22596 | The determinant function is homogeneous for each row: If the matrices 𝑋 and 𝑍 are identical except for the 𝐼-th row, and the 𝐼-th row of the matrix 𝑋 is the componentwise product of the 𝐼-th row of the matrix 𝑍 and the scalar 𝑌, then the determinant of 𝑋 is the determinant of 𝑍 multiplied by 𝑌. (Contributed by SO, 9-Jul-2018.) (Proof shortened by AV, 23-Jul-2019.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐾) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐼 ∈ 𝑁) & ⊢ (𝜑 → (𝑋 ↾ ({𝐼} × 𝑁)) = ((({𝐼} × 𝑁) × {𝑌}) ∘f · (𝑍 ↾ ({𝐼} × 𝑁)))) & ⊢ (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))) ⇒ ⊢ (𝜑 → (𝐷‘𝑋) = (𝑌 · (𝐷‘𝑍))) | ||
Theorem | mdetrsca2 22597* | The determinant function is homogeneous for each row (matrices are given explicitly by their entries). (Contributed by SO, 16-Jul-2018.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑋 ∈ 𝐾) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑌 ∈ 𝐾) & ⊢ (𝜑 → 𝐹 ∈ 𝐾) & ⊢ (𝜑 → 𝐼 ∈ 𝑁) ⇒ ⊢ (𝜑 → (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝐹 · 𝑋), 𝑌))) = (𝐹 · (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, 𝑌))))) | ||
Theorem | mdetr0 22598* | The determinant of a matrix with a row containing only 0's is 0. (Contributed by SO, 16-Jul-2018.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝐼 ∈ 𝑁) ⇒ ⊢ (𝜑 → (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 0 , 𝑋))) = 0 ) | ||
Theorem | mdet0 22599 | The determinant of the zero matrix (of dimension greater 0!) is 0. (Contributed by AV, 17-Aug-2019.) (Revised by AV, 3-Jul-2022.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑍 = (0g‘𝐴) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ∧ 𝑁 ≠ ∅) → (𝐷‘𝑍) = 0 ) | ||
Theorem | mdetrlin2 22600* | The determinant function is additive for each row (matrices are given explicitly by their entries). (Contributed by SO, 16-Jul-2018.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑋 ∈ 𝐾) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑌 ∈ 𝐾) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑍 ∈ 𝐾) & ⊢ (𝜑 → 𝐼 ∈ 𝑁) ⇒ ⊢ (𝜑 → (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑋 + 𝑌), 𝑍))) = ((𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, 𝑍))) + (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑌, 𝑍))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |