Home | Metamath
Proof Explorer Theorem List (p. 212 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | marrepval 21101* | 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 21102 | 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 21103 | Closure of the row replacement function for square matrices. (Contributed by AV, 13-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑆 ∈ (Base‘𝑅)) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁)) → (𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐿) ∈ 𝐵) | ||
Theorem | marepvfval 21104* | 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 21105* | 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 21106* | 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 21107 | 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 21108 | 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 21109 | 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 21110 | 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 21111 | 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 21112* | 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 21113* | 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 21114 | 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 21115 | Syntax for submatrices of a square matrix. |
class subMat | ||
Definition | df-subma 21116* | 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 21117* | 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 21118* | First substitution for a submatrix. (Contributed by AV, 28-Dec-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (𝑁 subMat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ 𝑄 = (𝑚 ∈ 𝐵 ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ (𝑁 ∖ {𝑘}), 𝑗 ∈ (𝑁 ∖ {𝑙}) ↦ (𝑖𝑚𝑗)))) | ||
Theorem | submaval0 21119* | Second substitution for a submatrix. (Contributed by AV, 28-Dec-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (𝑁 subMat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ (𝑀 ∈ 𝐵 → (𝑄‘𝑀) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ (𝑁 ∖ {𝑘}), 𝑗 ∈ (𝑁 ∖ {𝑙}) ↦ (𝑖𝑀𝑗)))) | ||
Theorem | submaval 21120* | Third substitution for a submatrix. (Contributed by AV, 28-Dec-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (𝑁 subMat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → (𝐾(𝑄‘𝑀)𝐿) = (𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝑀𝑗))) | ||
Theorem | submaeval 21121 | An entry of a submatrix of a square matrix. (Contributed by AV, 28-Dec-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (𝑁 subMat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) ∧ (𝐼 ∈ (𝑁 ∖ {𝐾}) ∧ 𝐽 ∈ (𝑁 ∖ {𝐿}))) → (𝐼(𝐾(𝑄‘𝑀)𝐿)𝐽) = (𝐼𝑀𝐽)) | ||
Theorem | 1marepvsma1 21122 | 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 21123 | Syntax for the matrix determinant function. |
class maDet | ||
Definition | df-mdet 21124* | Determinant of a square matrix. This definition is based on Leibniz' Formula (see mdetleib 21126). 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 21134. Multilineary means "linear for each row" - the additivity is shown by mdetrlin 21141, the homogeneity by mdetrsca 21142. Furthermore, it is shown that the determinant function is alternating (see mdetralt 21147) and normalized (see mdet1 21140). Finally, the uniqueness is shown by mdetuni 21161. As a consequence, the "determinant of a square matrix" is the function value of the determinant function for this square matrix, see mdetleib 21126. (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 21125* | 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 21126* | 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 21127* | 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 21128 | The determinant is not defined for an infinite matrix. (Contributed by AV, 27-Dec-2018.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) ⇒ ⊢ (𝑁 ∉ Fin → 𝐷 = ∅) | ||
Theorem | mdetfval1 21129* | 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 21130* | 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 21131 | 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 21132 | 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 21133 | The determinant of a 0-dimensional matrix is the 1 element of the underlying ring . (Contributed by AV, 28-Feb-2019.) |
⊢ (𝑅 ∈ Ring → ((∅ maDet 𝑅)‘∅) = (1r‘𝑅)) | ||
Theorem | mdetf 21134 | 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 21135 | 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 21136 | The determinant of a 1-dimensional matrix equals its (single) entry. (Contributed by AV, 6-Aug-2019.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (𝐼𝑀𝐼)) | ||
Theorem | mdetdiaglem 21137* | Lemma for mdetdiag 21138. Previously part of proof for mdet1 21140. (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 21138* | 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 21139* | 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 21140 | 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 21141 | 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 21142 | The determinant function is homogeneous for each row: The matrices X and Z are identical except for the I's row, and the I's row of the matrix X is the componentwise product of the I's row of the matrix Z and the scalar Y. In this case the determinant of X is the determinant of Z multiplied by Y. (Contributed by SO, 9-Jul-2018.) (Proof shortened by AV, 23-Jul-2019.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐾) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐼 ∈ 𝑁) & ⊢ (𝜑 → (𝑋 ↾ ({𝐼} × 𝑁)) = ((({𝐼} × 𝑁) × {𝑌}) ∘f · (𝑍 ↾ ({𝐼} × 𝑁)))) & ⊢ (𝜑 → (𝑋 ↾ ((𝑁 ∖ {𝐼}) × 𝑁)) = (𝑍 ↾ ((𝑁 ∖ {𝐼}) × 𝑁))) ⇒ ⊢ (𝜑 → (𝐷‘𝑋) = (𝑌 · (𝐷‘𝑍))) | ||
Theorem | mdetrsca2 21143* | 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 21144* | 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 21145 | 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 21146* | 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(𝑖 = 𝐼, 𝑌, 𝑍))))) | ||
Theorem | mdetralt 21147* | The determinant function is alternating regarding rows: if a matrix has two identical rows, its determinant is 0. Corollary 4.9 in [Lang] p. 515. (Contributed by SO, 10-Jul-2018.) (Proof shortened by AV, 23-Jul-2018.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐼 ∈ 𝑁) & ⊢ (𝜑 → 𝐽 ∈ 𝑁) & ⊢ (𝜑 → 𝐼 ≠ 𝐽) & ⊢ (𝜑 → ∀𝑎 ∈ 𝑁 (𝐼𝑋𝑎) = (𝐽𝑋𝑎)) ⇒ ⊢ (𝜑 → (𝐷‘𝑋) = 0 ) | ||
Theorem | mdetralt2 21148* | The determinant function is alternating regarding rows (matrix is given explicitly by its entries). (Contributed by SO, 16-Jul-2018.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑁) → 𝑋 ∈ 𝐾) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑌 ∈ 𝐾) & ⊢ (𝜑 → 𝐼 ∈ 𝑁) & ⊢ (𝜑 → 𝐽 ∈ 𝑁) & ⊢ (𝜑 → 𝐼 ≠ 𝐽) ⇒ ⊢ (𝜑 → (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, if(𝑖 = 𝐽, 𝑋, 𝑌)))) = 0 ) | ||
Theorem | mdetero 21149* | The determinant function is multilinear (additive and homogeneous for each row (matrices are given explicitly by their entries). Corollary 4.9 in [Lang] p. 515. (Contributed by SO, 16-Jul-2018.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑁) → 𝑋 ∈ 𝐾) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑁) → 𝑌 ∈ 𝐾) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑍 ∈ 𝐾) & ⊢ (𝜑 → 𝑊 ∈ 𝐾) & ⊢ (𝜑 → 𝐼 ∈ 𝑁) & ⊢ (𝜑 → 𝐽 ∈ 𝑁) & ⊢ (𝜑 → 𝐼 ≠ 𝐽) ⇒ ⊢ (𝜑 → (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, (𝑋 + (𝑊 · 𝑌)), if(𝑖 = 𝐽, 𝑌, 𝑍)))) = (𝐷‘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐼, 𝑋, if(𝑖 = 𝐽, 𝑌, 𝑍))))) | ||
Theorem | mdettpos 21150 | Determinant is invariant under transposition. Proposition 4.8 in [Lang] p. 514. (Contributed by Stefan O'Rear, 9-Jul-2018.) |
⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐷‘tpos 𝑀) = (𝐷‘𝑀)) | ||
Theorem | mdetunilem1 21151* | Lemma for mdetuni 21161. (Contributed by SO, 14-Jul-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐷:𝐵⟶𝐾) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 )) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧)))) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧)))) ⇒ ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝐺𝐸𝑤)) ∧ (𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺)) → (𝐷‘𝐸) = 0 ) | ||
Theorem | mdetunilem2 21152* | Lemma for mdetuni 21161. (Contributed by SO, 15-Jul-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐷:𝐵⟶𝐾) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 )) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧)))) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧)))) & ⊢ (𝜓 → 𝜑) & ⊢ (𝜓 → (𝐸 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐸 ≠ 𝐺)) & ⊢ ((𝜓 ∧ 𝑏 ∈ 𝑁) → 𝐹 ∈ 𝐾) & ⊢ ((𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝐻 ∈ 𝐾) ⇒ ⊢ (𝜓 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, 𝐹, if(𝑎 = 𝐺, 𝐹, 𝐻)))) = 0 ) | ||
Theorem | mdetunilem3 21153* | Lemma for mdetuni 21161. (Contributed by SO, 15-Jul-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐷:𝐵⟶𝐾) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 )) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧)))) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧)))) ⇒ ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵) ∧ (𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘f + (𝐺 ↾ ({𝐻} × 𝑁)))) ∧ ((𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐷‘𝐸) = ((𝐷‘𝐹) + (𝐷‘𝐺))) | ||
Theorem | mdetunilem4 21154* | Lemma for mdetuni 21161. (Contributed by SO, 15-Jul-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐷:𝐵⟶𝐾) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 )) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧)))) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧)))) ⇒ ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ (𝐻 ∈ 𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘f · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝐺))) | ||
Theorem | mdetunilem5 21155* | Lemma for mdetuni 21161. (Contributed by SO, 15-Jul-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐷:𝐵⟶𝐾) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 )) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧)))) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧)))) & ⊢ (𝜓 → 𝜑) & ⊢ (𝜓 → 𝐸 ∈ 𝑁) & ⊢ ((𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → (𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐾 ∧ 𝐻 ∈ 𝐾)) ⇒ ⊢ (𝜓 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, (𝐹 + 𝐺), 𝐻))) = ((𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, 𝐹, 𝐻))) + (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, 𝐺, 𝐻))))) | ||
Theorem | mdetunilem6 21156* | Lemma for mdetuni 21161. (Contributed by SO, 15-Jul-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐷:𝐵⟶𝐾) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 )) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧)))) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧)))) & ⊢ (𝜓 → 𝜑) & ⊢ (𝜓 → (𝐸 ∈ 𝑁 ∧ 𝐹 ∈ 𝑁 ∧ 𝐸 ≠ 𝐹)) & ⊢ ((𝜓 ∧ 𝑏 ∈ 𝑁) → (𝐺 ∈ 𝐾 ∧ 𝐻 ∈ 𝐾)) & ⊢ ((𝜓 ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → 𝐼 ∈ 𝐾) ⇒ ⊢ (𝜓 → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, 𝐺, if(𝑎 = 𝐹, 𝐻, 𝐼)))) = ((invg‘𝑅)‘(𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if(𝑎 = 𝐸, 𝐻, if(𝑎 = 𝐹, 𝐺, 𝐼)))))) | ||
Theorem | mdetunilem7 21157* | Lemma for mdetuni 21161. (Contributed by SO, 15-Jul-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐷:𝐵⟶𝐾) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 )) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧)))) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧)))) ⇒ ⊢ ((𝜑 ∧ 𝐸:𝑁–1-1-onto→𝑁 ∧ 𝐹 ∈ 𝐵) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ ((𝐸‘𝑎)𝐹𝑏))) = ((((ℤRHom‘𝑅) ∘ (pmSgn‘𝑁))‘𝐸) · (𝐷‘𝐹))) | ||
Theorem | mdetunilem8 21158* | Lemma for mdetuni 21161. (Contributed by SO, 15-Jul-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐷:𝐵⟶𝐾) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 )) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧)))) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧)))) & ⊢ (𝜑 → (𝐷‘(1r‘𝐴)) = 0 ) ⇒ ⊢ ((𝜑 ∧ 𝐸:𝑁⟶𝑁) → (𝐷‘(𝑎 ∈ 𝑁, 𝑏 ∈ 𝑁 ↦ if((𝐸‘𝑎) = 𝑏, 1 , 0 ))) = 0 ) | ||
Theorem | mdetunilem9 21159* | Lemma for mdetuni 21161. (Contributed by SO, 15-Jul-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐷:𝐵⟶𝐾) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 )) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧)))) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧)))) & ⊢ (𝜑 → (𝐷‘(1r‘𝐴)) = 0 ) & ⊢ 𝑌 = {𝑥 ∣ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ (𝑁 ↑m 𝑁)(∀𝑤 ∈ 𝑥 (𝑦‘𝑤) = if(𝑤 ∈ 𝑧, 1 , 0 ) → (𝐷‘𝑦) = 0 )} ⇒ ⊢ (𝜑 → 𝐷 = (𝐵 × { 0 })) | ||
Theorem | mdetuni0 21160* | Lemma for mdetuni 21161. (Contributed by SO, 15-Jul-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐷:𝐵⟶𝐾) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 )) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧)))) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧)))) & ⊢ 𝐸 = (𝑁 maDet 𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐷‘𝐹) = ((𝐷‘(1r‘𝐴)) · (𝐸‘𝐹))) | ||
Theorem | mdetuni 21161* | According to the definition in [Weierstrass] p. 272, 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. So for any multilinear (mdetuni.li and mdetuni.sc), alternating (mdetuni.al) and normalized (mdetuni.no) function D (mdetuni.ff) from the algebra of square matrices (mdetuni.a) to their underlying commutative ring (mdetuni.cr), the function value of this function D for a matrix F (mdetuni.f) is the determinant of this matrix. (Contributed by Stefan O'Rear, 15-Jul-2018.) (Revised by Alexander van der Vekens, 8-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐷:𝐵⟶𝐾) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 )) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧)))) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧)))) & ⊢ 𝐸 = (𝑁 maDet 𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → (𝐷‘(1r‘𝐴)) = 1 ) ⇒ ⊢ (𝜑 → (𝐷‘𝐹) = (𝐸‘𝐹)) | ||
Theorem | mdetmul 21162 | Multiplicativity of the determinant function: the determinant of a matrix product of square matrices equals the product of their determinants. Proposition 4.15 in [Lang] p. 517. (Contributed by Stefan O'Rear, 16-Jul-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ · = (.r‘𝑅) & ⊢ ∙ = (.r‘𝐴) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐷‘(𝐹 ∙ 𝐺)) = ((𝐷‘𝐹) · (𝐷‘𝐺))) | ||
Theorem | m2detleiblem1 21163 | Lemma 1 for m2detleib 21170. (Contributed by AV, 12-Dec-2018.) |
⊢ 𝑁 = {1, 2} & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃) → (𝑌‘(𝑆‘𝑄)) = (((pmSgn‘𝑁)‘𝑄)(.g‘𝑅) 1 )) | ||
Theorem | m2detleiblem5 21164 | Lemma 5 for m2detleib 21170. (Contributed by AV, 20-Dec-2018.) |
⊢ 𝑁 = {1, 2} & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {〈1, 1〉, 〈2, 2〉}) → (𝑌‘(𝑆‘𝑄)) = 1 ) | ||
Theorem | m2detleiblem6 21165 | Lemma 6 for m2detleib 21170. (Contributed by AV, 20-Dec-2018.) |
⊢ 𝑁 = {1, 2} & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {〈1, 2〉, 〈2, 1〉}) → (𝑌‘(𝑆‘𝑄)) = (𝐼‘ 1 )) | ||
Theorem | m2detleiblem7 21166 | Lemma 7 for m2detleib 21170. (Contributed by AV, 20-Dec-2018.) |
⊢ 𝑁 = {1, 2} & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ − = (-g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (Base‘𝑅) ∧ 𝑍 ∈ (Base‘𝑅)) → (𝑋(+g‘𝑅)((𝐼‘ 1 ) · 𝑍)) = (𝑋 − 𝑍)) | ||
Theorem | m2detleiblem2 21167* | Lemma 2 for m2detleib 21170. (Contributed by AV, 16-Dec-2018.) (Proof shortened by AV, 1-Jan-2019.) |
⊢ 𝑁 = {1, 2} & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐺 = (mulGrp‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵) → (𝐺 Σg (𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))) ∈ (Base‘𝑅)) | ||
Theorem | m2detleiblem3 21168* | Lemma 3 for m2detleib 21170. (Contributed by AV, 16-Dec-2018.) (Proof shortened by AV, 2-Jan-2019.) |
⊢ 𝑁 = {1, 2} & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ · = (+g‘𝐺) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {〈1, 1〉, 〈2, 2〉} ∧ 𝑀 ∈ 𝐵) → (𝐺 Σg (𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))) = ((1𝑀1) · (2𝑀2))) | ||
Theorem | m2detleiblem4 21169* | Lemma 4 for m2detleib 21170. (Contributed by AV, 20-Dec-2018.) (Proof shortened by AV, 2-Jan-2019.) |
⊢ 𝑁 = {1, 2} & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ · = (+g‘𝐺) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {〈1, 2〉, 〈2, 1〉} ∧ 𝑀 ∈ 𝐵) → (𝐺 Σg (𝑛 ∈ 𝑁 ↦ ((𝑄‘𝑛)𝑀𝑛))) = ((2𝑀1) · (1𝑀2))) | ||
Theorem | m2detleib 21170 | Leibniz' Formula for 2x2-matrices. (Contributed by AV, 21-Dec-2018.) (Revised by AV, 26-Dec-2018.) (Proof shortened by AV, 23-Jul-2019.) |
⊢ 𝑁 = {1, 2} & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ − = (-g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (((1𝑀1) · (2𝑀2)) − ((2𝑀1) · (1𝑀2)))) | ||
Syntax | cmadu 21171 | Syntax for the matrix adjugate/adjunct function. |
class maAdju | ||
Syntax | cminmar1 21172 | Syntax for the minor matrices of a square matrix. |
class minMatR1 | ||
Definition | df-madu 21173* | Define the adjugate or adjunct (matrix of cofactors) of a square matrix. This definition gives the standard cofactors, however the internal minors are not the standard minors, see definition in [Lang] p. 518. (Contributed by Stefan O'Rear, 7-Sep-2015.) (Revised by SO, 10-Jul-2018.) |
⊢ maAdju = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r‘𝑟), (0g‘𝑟)), (𝑘𝑚𝑙))))))) | ||
Definition | df-minmar1 21174* | Define the matrices whose determinants are the minors of a square matrix. In contrast to the standard definition of minors, a row is replaced by 0's and one 1 instead of deleting the column and row (e.g., definition in [Lang] p. 515). By this, the determinant of such a matrix is equal to the minor determined in the standard way (as determinant of a submatrix, see df-subma 21116- note that the matrix is transposed compared with the submatrix defined in df-subma 21116, but this does not matter because the determinants are the same, see mdettpos 21150). Such matrices are used in the definition of an adjunct of a square matrix, see df-madu 21173. (Contributed by AV, 27-Dec-2018.) |
⊢ minMatR1 = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, (1r‘𝑟), (0g‘𝑟)), (𝑖𝑚𝑗)))))) | ||
Theorem | mndifsplit 21175 | Lemma for maducoeval2 21179. (Contributed by SO, 16-Jul-2018.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 0 = (0g‘𝑀) & ⊢ + = (+g‘𝑀) ⇒ ⊢ ((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 ))) | ||
Theorem | madufval 21176* | First substitution for the adjunct (cofactor) matrix. (Contributed by SO, 11-Jul-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐽 = (𝑁 maAdju 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ 𝐽 = (𝑚 ∈ 𝐵 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝐷‘(𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, 1 , 0 ), (𝑘𝑚𝑙)))))) | ||
Theorem | maduval 21177* | Second substitution for the adjunct (cofactor) matrix. (Contributed by SO, 11-Jul-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐽 = (𝑁 maAdju 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑀 ∈ 𝐵 → (𝐽‘𝑀) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝐷‘(𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, 1 , 0 ), (𝑘𝑀𝑙)))))) | ||
Theorem | maducoeval 21178* | An entry of the adjunct (cofactor) matrix. (Contributed by SO, 11-Jul-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐽 = (𝑁 maAdju 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁 ∧ 𝐻 ∈ 𝑁) → (𝐼(𝐽‘𝑀)𝐻) = (𝐷‘(𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ if(𝑘 = 𝐻, if(𝑙 = 𝐼, 1 , 0 ), (𝑘𝑀𝑙))))) | ||
Theorem | maducoeval2 21179* | An entry of the adjunct (cofactor) matrix. (Contributed by SO, 17-Jul-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐽 = (𝑁 maAdju 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝐼 ∈ 𝑁 ∧ 𝐻 ∈ 𝑁) → (𝐼(𝐽‘𝑀)𝐻) = (𝐷‘(𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ if((𝑘 = 𝐻 ∨ 𝑙 = 𝐼), if((𝑙 = 𝐼 ∧ 𝑘 = 𝐻), 1 , 0 ), (𝑘𝑀𝑙))))) | ||
Theorem | maduf 21180 | Creating the adjunct of matrices is a function from the set of matrices into the set of matrices. (Contributed by Stefan O'Rear, 11-Jul-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐽 = (𝑁 maAdju 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ (𝑅 ∈ CRing → 𝐽:𝐵⟶𝐵) | ||
Theorem | madutpos 21181 | The adjuct of a transposed matrix is the transposition of the adjunct of the matrix. (Contributed by Stefan O'Rear, 17-Jul-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐽 = (𝑁 maAdju 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐽‘tpos 𝑀) = tpos (𝐽‘𝑀)) | ||
Theorem | madugsum 21182* | The determinant of a matrix with a row 𝐿 consisting of the same element 𝑋 is the sum of the elements of the 𝐿-th column of the adjunct of the matrix multiplied with 𝑋. (Contributed by Stefan O'Rear, 16-Jul-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐽 = (𝑁 maAdju 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑁) → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝐿 ∈ 𝑁) ⇒ ⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ 𝑁 ↦ (𝑋 · (𝑖(𝐽‘𝑀)𝐿)))) = (𝐷‘(𝑗 ∈ 𝑁, 𝑖 ∈ 𝑁 ↦ if(𝑗 = 𝐿, 𝑋, (𝑗𝑀𝑖))))) | ||
Theorem | madurid 21183 | Multiplying a matrix with its adjunct results in the identity matrix multiplied with the determinant of the matrix. See Proposition 4.16 in [Lang] p. 518. (Contributed by Stefan O'Rear, 16-Jul-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐽 = (𝑁 maAdju 𝑅) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 1 = (1r‘𝐴) & ⊢ · = (.r‘𝐴) & ⊢ ∙ = ( ·𝑠 ‘𝐴) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → (𝑀 · (𝐽‘𝑀)) = ((𝐷‘𝑀) ∙ 1 )) | ||
Theorem | madulid 21184 | Multiplying the adjunct of a matrix with the matrix results in the identity matrix multiplied with the determinant of the matrix. See Proposition 4.16 in [Lang] p. 518. (Contributed by Stefan O'Rear, 17-Jul-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐽 = (𝑁 maAdju 𝑅) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 1 = (1r‘𝐴) & ⊢ · = (.r‘𝐴) & ⊢ ∙ = ( ·𝑠 ‘𝐴) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝑅 ∈ CRing) → ((𝐽‘𝑀) · 𝑀) = ((𝐷‘𝑀) ∙ 1 )) | ||
Theorem | minmar1fval 21185* | First substitution for the definition of a matrix for a minor. (Contributed by AV, 31-Dec-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑄 = (𝑁 minMatR1 𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ 𝑄 = (𝑚 ∈ 𝐵 ↦ (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 1 , 0 ), (𝑖𝑚𝑗))))) | ||
Theorem | minmar1val0 21186* | Second substitution for the definition of a matrix for a minor. (Contributed by AV, 31-Dec-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑄 = (𝑁 minMatR1 𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑀 ∈ 𝐵 → (𝑄‘𝑀) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 1 , 0 ), (𝑖𝑀𝑗))))) | ||
Theorem | minmar1val 21187* | Third substitution for the definition of a matrix for a minor. (Contributed by AV, 31-Dec-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑄 = (𝑁 minMatR1 𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → (𝐾(𝑄‘𝑀)𝐿) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 1 , 0 ), (𝑖𝑀𝑗)))) | ||
Theorem | minmar1eval 21188 | An entry of a matrix for a minor. (Contributed by AV, 31-Dec-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑄 = (𝑁 minMatR1 𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝐾(𝑄‘𝑀)𝐿)𝐽) = if(𝐼 = 𝐾, if(𝐽 = 𝐿, 1 , 0 ), (𝐼𝑀𝐽))) | ||
Theorem | minmar1marrep 21189 | The minor matrix is a special case of a matrix with a replaced row. (Contributed by AV, 12-Feb-2019.) (Revised by AV, 4-Jul-2022.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((𝑁 minMatR1 𝑅)‘𝑀) = (𝑀(𝑁 matRRep 𝑅) 1 )) | ||
Theorem | minmar1cl 21190 | Closure of the row replacement function for square matrices: The matrix for a minor is a matrix. (Contributed by AV, 13-Feb-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁)) → (𝐾((𝑁 minMatR1 𝑅)‘𝑀)𝐿) ∈ 𝐵) | ||
Theorem | maducoevalmin1 21191 | The coefficients of an adjunct (matrix of cofactors) expressed as determinants of the minor matrices (alternative definition) of the original matrix. (Contributed by AV, 31-Dec-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐽 = (𝑁 maAdju 𝑅) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁 ∧ 𝐻 ∈ 𝑁) → (𝐼(𝐽‘𝑀)𝐻) = (𝐷‘(𝐻((𝑁 minMatR1 𝑅)‘𝑀)𝐼))) | ||
According to Wikipedia ("Laplace expansion", 08-Mar-2019, https://en.wikipedia.org/wiki/Laplace_expansion) "In linear algebra, the Laplace expansion, named after Pierre-Simon Laplace, also called cofactor expansion, is an expression for the determinant det(B) of an n x n -matrix B that is a weighted sum of the determinants of n sub-matrices of B, each of size (n-1) x (n-1)". The expansion is usually performed for a row of matrix B (alternately for a column of matrix B). The mentioned "sub-matrices" are the matrices resultung from deleting the i-th row and the j-th column of matrix B. The mentioned "weights" (factors/coefficients) are the elements at position i and j in matrix B. If the expansion is performed for a row, the coefficients are the elements of the selected row. In the following, only the case where the row for the expansion contains only the zero element of the underlying ring except at the diagonal position. By this, the sum for the Laplace expansion is reduced to one summand, consisting of the element at the diagonal position multiplied with the determinant of the corresponding submatrix, see smadiadetg 21212 or smadiadetr 21214. | ||
Theorem | symgmatr01lem 21192* | Lemma for symgmatr01 21193. (Contributed by AV, 3-Jan-2019.) |
⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) ⇒ ⊢ ((𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → (𝑄 ∈ (𝑃 ∖ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐿}) → ∃𝑘 ∈ 𝑁 if(𝑘 = 𝐾, if((𝑄‘𝑘) = 𝐿, 𝐴, 𝐵), (𝑘𝑀(𝑄‘𝑘))) = 𝐵)) | ||
Theorem | symgmatr01 21193* | Applying a permutation that does not fix a certain element of a set to a second element to an index of a matrix a row with 0's and a 1. (Contributed by AV, 3-Jan-2019.) |
⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → (𝑄 ∈ (𝑃 ∖ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐿}) → ∃𝑘 ∈ 𝑁 (𝑘(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 1 , 0 ), (𝑖𝑀𝑗)))(𝑄‘𝑘)) = 0 )) | ||
Theorem | gsummatr01lem1 21194* | Lemma A for gsummatr01 21198. (Contributed by AV, 8-Jan-2019.) |
⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑅 = {𝑟 ∈ 𝑃 ∣ (𝑟‘𝐾) = 𝐿} ⇒ ⊢ ((𝑄 ∈ 𝑅 ∧ 𝑋 ∈ 𝑁) → (𝑄‘𝑋) ∈ 𝑁) | ||
Theorem | gsummatr01lem2 21195* | Lemma B for gsummatr01 21198. (Contributed by AV, 8-Jan-2019.) |
⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑅 = {𝑟 ∈ 𝑃 ∣ (𝑟‘𝐾) = 𝐿} ⇒ ⊢ ((𝑄 ∈ 𝑅 ∧ 𝑋 ∈ 𝑁) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ (Base‘𝐺) → (𝑋𝐴(𝑄‘𝑋)) ∈ (Base‘𝐺))) | ||
Theorem | gsummatr01lem3 21196* | Lemma 1 for gsummatr01 21198. (Contributed by AV, 8-Jan-2019.) |
⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑅 = {𝑟 ∈ 𝑃 ∣ (𝑟‘𝐾) = 𝐿} & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑆 = (Base‘𝐺) ⇒ ⊢ (((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧ (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) → (𝐺 Σg (𝑛 ∈ ((𝑁 ∖ {𝐾}) ∪ {𝐾}) ↦ (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)))(𝑄‘𝑛)))) = ((𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)))(𝑄‘𝑛))))(+g‘𝐺)(𝐾(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)))(𝑄‘𝐾)))) | ||
Theorem | gsummatr01lem4 21197* | Lemma 2 for gsummatr01 21198. (Contributed by AV, 8-Jan-2019.) |
⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑅 = {𝑟 ∈ 𝑃 ∣ (𝑟‘𝐾) = 𝐿} & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑆 = (Base‘𝐺) ⇒ ⊢ ((((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧ (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)))(𝑄‘𝑛)) = (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝐴𝑗))(𝑄‘𝑛))) | ||
Theorem | gsummatr01 21198* | Lemma 1 for smadiadetlem4 21208. (Contributed by AV, 8-Jan-2019.) |
⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑅 = {𝑟 ∈ 𝑃 ∣ (𝑟‘𝐾) = 𝐿} & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑆 = (Base‘𝐺) ⇒ ⊢ (((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧ (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) → (𝐺 Σg (𝑛 ∈ 𝑁 ↦ (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)))(𝑄‘𝑛)))) = (𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝐴𝑗))(𝑄‘𝑛))))) | ||
Theorem | marep01ma 21199* | Replacing a row of a square matrix by a row with 0's and a 1 results in a square matrix of the same dimension. (Contributed by AV, 30-Dec-2018.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑀 ∈ 𝐵 → (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ if(𝑘 = 𝐻, if(𝑙 = 𝐼, 1 , 0 ), (𝑘𝑀𝑙))) ∈ 𝐵) | ||
Theorem | smadiadetlem0 21200* | Lemma 0 for smadiadet 21209: The products of the Leibniz' formula vanish for all permutations fixing the index of the row containing the 0's and the 1 to the column with the 1. (Contributed by AV, 3-Jan-2019.) |
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝐺 = (mulGrp‘𝑅) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → (𝑄 ∈ (𝑃 ∖ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐿}) → (𝐺 Σg (𝑛 ∈ 𝑁 ↦ (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 1 , 0 ), (𝑖𝑀𝑗)))(𝑄‘𝑛)))) = 0 )) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |