| Metamath
Proof Explorer Theorem List (p. 227 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | mdetf 22601 | 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 22602 | 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 22603 | The determinant of a 1-dimensional matrix equals its (single) entry. (Contributed by AV, 6-Aug-2019.) |
| ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐷‘𝑀) = (𝐼𝑀𝐼)) | ||
| Theorem | mdetdiaglem 22604* | Lemma for mdetdiag 22605. Previously part of proof for mdet1 22607. (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 22605* | 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 22606* | 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 22607 | 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 22608 | 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 22609 | 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 22610* | 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 22611* | 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 22612 | 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 22613* | 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 22614* | 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 22615* | 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 22616* | 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 22617 | 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 22618* | Lemma for mdetuni 22628. (Contributed by SO, 14-Jul-2018.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐷:𝐵⟶𝐾) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 )) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧)))) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧)))) ⇒ ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ ∀𝑤 ∈ 𝑁 (𝐹𝐸𝑤) = (𝐺𝐸𝑤)) ∧ (𝐹 ∈ 𝑁 ∧ 𝐺 ∈ 𝑁 ∧ 𝐹 ≠ 𝐺)) → (𝐷‘𝐸) = 0 ) | ||
| Theorem | mdetunilem2 22619* | Lemma for mdetuni 22628. (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 22620* | Lemma for mdetuni 22628. (Contributed by SO, 15-Jul-2018.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐷:𝐵⟶𝐾) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 )) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧)))) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧)))) ⇒ ⊢ (((𝜑 ∧ 𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐵) ∧ (𝐺 ∈ 𝐵 ∧ 𝐻 ∈ 𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((𝐹 ↾ ({𝐻} × 𝑁)) ∘f + (𝐺 ↾ ({𝐻} × 𝑁)))) ∧ ((𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐹 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐷‘𝐸) = ((𝐷‘𝐹) + (𝐷‘𝐺))) | ||
| Theorem | mdetunilem4 22621* | Lemma for mdetuni 22628. (Contributed by SO, 15-Jul-2018.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐷:𝐵⟶𝐾) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝑁 ∀𝑧 ∈ 𝑁 ((𝑦 ≠ 𝑧 ∧ ∀𝑤 ∈ 𝑁 (𝑦𝑥𝑤) = (𝑧𝑥𝑤)) → (𝐷‘𝑥) = 0 )) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((𝑦 ↾ ({𝑤} × 𝑁)) ∘f + (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑦 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = ((𝐷‘𝑦) + (𝐷‘𝑧)))) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝑁 (((𝑥 ↾ ({𝑤} × 𝑁)) = ((({𝑤} × 𝑁) × {𝑦}) ∘f · (𝑧 ↾ ({𝑤} × 𝑁))) ∧ (𝑥 ↾ ((𝑁 ∖ {𝑤}) × 𝑁)) = (𝑧 ↾ ((𝑁 ∖ {𝑤}) × 𝑁))) → (𝐷‘𝑥) = (𝑦 · (𝐷‘𝑧)))) ⇒ ⊢ ((𝜑 ∧ (𝐸 ∈ 𝐵 ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ (𝐻 ∈ 𝑁 ∧ (𝐸 ↾ ({𝐻} × 𝑁)) = ((({𝐻} × 𝑁) × {𝐹}) ∘f · (𝐺 ↾ ({𝐻} × 𝑁))) ∧ (𝐸 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)) = (𝐺 ↾ ((𝑁 ∖ {𝐻}) × 𝑁)))) → (𝐷‘𝐸) = (𝐹 · (𝐷‘𝐺))) | ||
| Theorem | mdetunilem5 22622* | Lemma for mdetuni 22628. (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 22623* | Lemma for mdetuni 22628. (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 22624* | Lemma for mdetuni 22628. (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 22625* | Lemma for mdetuni 22628. (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 22626* | Lemma for mdetuni 22628. (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 22627* | Lemma for mdetuni 22628. (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 22628* | 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 22629 | 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 22630 | Lemma 1 for m2detleib 22637. (Contributed by AV, 12-Dec-2018.) |
| ⊢ 𝑁 = {1, 2} & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃) → (𝑌‘(𝑆‘𝑄)) = (((pmSgn‘𝑁)‘𝑄)(.g‘𝑅) 1 )) | ||
| Theorem | m2detleiblem5 22631 | Lemma 5 for m2detleib 22637. (Contributed by AV, 20-Dec-2018.) |
| ⊢ 𝑁 = {1, 2} & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {〈1, 1〉, 〈2, 2〉}) → (𝑌‘(𝑆‘𝑄)) = 1 ) | ||
| Theorem | m2detleiblem6 22632 | Lemma 6 for m2detleib 22637. (Contributed by AV, 20-Dec-2018.) |
| ⊢ 𝑁 = {1, 2} & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {〈1, 2〉, 〈2, 1〉}) → (𝑌‘(𝑆‘𝑄)) = (𝐼‘ 1 )) | ||
| Theorem | m2detleiblem7 22633 | Lemma 7 for m2detleib 22637. (Contributed by AV, 20-Dec-2018.) |
| ⊢ 𝑁 = {1, 2} & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ − = (-g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (Base‘𝑅) ∧ 𝑍 ∈ (Base‘𝑅)) → (𝑋(+g‘𝑅)((𝐼‘ 1 ) · 𝑍)) = (𝑋 − 𝑍)) | ||
| Theorem | m2detleiblem2 22634* | Lemma 2 for m2detleib 22637. (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 22635* | Lemma 3 for m2detleib 22637. (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 22636* | Lemma 4 for m2detleib 22637. (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 22637 | 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 22638 | Syntax for the matrix adjugate/adjunct function. |
| class maAdju | ||
| Syntax | cminmar1 22639 | Syntax for the minor matrices of a square matrix. |
| class minMatR1 | ||
| Definition | df-madu 22640* | 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 22641* | 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 22583- note that the matrix is transposed compared with the submatrix defined in df-subma 22583, but this does not matter because the determinants are the same, see mdettpos 22617). Such matrices are used in the definition of an adjunct of a square matrix, see df-madu 22640. (Contributed by AV, 27-Dec-2018.) |
| ⊢ minMatR1 = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, (1r‘𝑟), (0g‘𝑟)), (𝑖𝑚𝑗)))))) | ||
| Theorem | mndifsplit 22642 | Lemma for maducoeval2 22646. (Contributed by SO, 16-Jul-2018.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ 0 = (0g‘𝑀) & ⊢ + = (+g‘𝑀) ⇒ ⊢ ((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 ))) | ||
| Theorem | madufval 22643* | 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 22644* | 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 22645* | 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 22646* | 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 22647 | 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 22648 | 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 22649* | 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 22650 | 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 22651 | 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 22652* | 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 22653* | 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 22654* | 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 22655 | 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 22656 | 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 22657 | 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 22658 | 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 22679 or smadiadetr 22681. | ||
| Theorem | symgmatr01lem 22659* | Lemma for symgmatr01 22660. (Contributed by AV, 3-Jan-2019.) |
| ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) ⇒ ⊢ ((𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → (𝑄 ∈ (𝑃 ∖ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐿}) → ∃𝑘 ∈ 𝑁 if(𝑘 = 𝐾, if((𝑄‘𝑘) = 𝐿, 𝐴, 𝐵), (𝑘𝑀(𝑄‘𝑘))) = 𝐵)) | ||
| Theorem | symgmatr01 22660* | 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 22661* | Lemma A for gsummatr01 22665. (Contributed by AV, 8-Jan-2019.) |
| ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑅 = {𝑟 ∈ 𝑃 ∣ (𝑟‘𝐾) = 𝐿} ⇒ ⊢ ((𝑄 ∈ 𝑅 ∧ 𝑋 ∈ 𝑁) → (𝑄‘𝑋) ∈ 𝑁) | ||
| Theorem | gsummatr01lem2 22662* | Lemma B for gsummatr01 22665. (Contributed by AV, 8-Jan-2019.) |
| ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑅 = {𝑟 ∈ 𝑃 ∣ (𝑟‘𝐾) = 𝐿} ⇒ ⊢ ((𝑄 ∈ 𝑅 ∧ 𝑋 ∈ 𝑁) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ (Base‘𝐺) → (𝑋𝐴(𝑄‘𝑋)) ∈ (Base‘𝐺))) | ||
| Theorem | gsummatr01lem3 22663* | Lemma 1 for gsummatr01 22665. (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 22664* | Lemma 2 for gsummatr01 22665. (Contributed by AV, 8-Jan-2019.) |
| ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑅 = {𝑟 ∈ 𝑃 ∣ (𝑟‘𝐾) = 𝐿} & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑆 = (Base‘𝐺) ⇒ ⊢ ((((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧ (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)))(𝑄‘𝑛)) = (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝐴𝑗))(𝑄‘𝑛))) | ||
| Theorem | gsummatr01 22665* | Lemma 1 for smadiadetlem4 22675. (Contributed by AV, 8-Jan-2019.) |
| ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑅 = {𝑟 ∈ 𝑃 ∣ (𝑟‘𝐾) = 𝐿} & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑆 = (Base‘𝐺) ⇒ ⊢ (((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧ (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) → (𝐺 Σg (𝑛 ∈ 𝑁 ↦ (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)))(𝑄‘𝑛)))) = (𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝐴𝑗))(𝑄‘𝑛))))) | ||
| Theorem | marep01ma 22666* | 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 22667* | Lemma 0 for smadiadet 22676: 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 )) | ||
| Theorem | smadiadetlem1 22668* | Lemma 1 for smadiadet 22676: A summand of the determinant of a matrix belongs to the underlying ring. (Contributed by AV, 1-Jan-2019.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) ∧ 𝑝 ∈ 𝑃) → (((𝑌 ∘ 𝑆)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ 𝑁 ↦ (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 1 , 0 ), (𝑖𝑀𝑗)))(𝑝‘𝑛))))) ∈ (Base‘𝑅)) | ||
| Theorem | smadiadetlem1a 22669* | Lemma 1a for smadiadet 22676: The summands 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‘𝑅) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → (𝑅 Σg (𝑝 ∈ (𝑃 ∖ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐿}) ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝐺 Σg (𝑛 ∈ 𝑁 ↦ (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 1 , 0 ), (𝑖𝑀𝑗)))(𝑝‘𝑛))))))) = 0 ) | ||
| Theorem | smadiadetlem2 22670* | Lemma 2 for smadiadet 22676: The summands of the Leibniz' formula vanish for all permutations fixing the index of the row containing the 0's and the 1 to itself. (Contributed by AV, 31-Dec-2018.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → (𝑅 Σg (𝑝 ∈ (𝑃 ∖ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) ↦ (((𝑌 ∘ 𝑆)‘𝑝) · (𝐺 Σg (𝑛 ∈ 𝑁 ↦ (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 1 , 0 ), (𝑖𝑀𝑗)))(𝑝‘𝑛))))))) = 0 ) | ||
| Theorem | smadiadetlem3lem0 22671* | Lemma 0 for smadiadetlem3 22674. (Contributed by AV, 12-Jan-2019.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ · = (.r‘𝑅) & ⊢ 𝑊 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) & ⊢ 𝑍 = (pmSgn‘(𝑁 ∖ {𝐾})) ⇒ ⊢ (((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ 𝑊) → (((𝑌 ∘ 𝑍)‘𝑄)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑄‘𝑛))))) ∈ (Base‘𝑅)) | ||
| Theorem | smadiadetlem3lem1 22672* | Lemma 1 for smadiadetlem3 22674. (Contributed by AV, 12-Jan-2019.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ · = (.r‘𝑅) & ⊢ 𝑊 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) & ⊢ 𝑍 = (pmSgn‘(𝑁 ∖ {𝐾})) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → (𝑝 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))):𝑊⟶(Base‘𝑅)) | ||
| Theorem | smadiadetlem3lem2 22673* | Lemma 2 for smadiadetlem3 22674. (Contributed by AV, 12-Jan-2019.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ · = (.r‘𝑅) & ⊢ 𝑊 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) & ⊢ 𝑍 = (pmSgn‘(𝑁 ∖ {𝐾})) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → ran (𝑝 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))) ⊆ ((Cntz‘𝑅)‘ran (𝑝 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))))) | ||
| Theorem | smadiadetlem3 22674* | Lemma 3 for smadiadet 22676. (Contributed by AV, 31-Jan-2019.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ · = (.r‘𝑅) & ⊢ 𝑊 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) & ⊢ 𝑍 = (pmSgn‘(𝑁 ∖ {𝐾})) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → (𝑅 Σg (𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ↦ (((𝑌 ∘ 𝑆)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛))))))) = (𝑅 Σg (𝑝 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))))) | ||
| Theorem | smadiadetlem4 22675* | Lemma 4 for smadiadet 22676. (Contributed by AV, 31-Jan-2019.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 0 = (0g‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ 𝑌 = (ℤRHom‘𝑅) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ · = (.r‘𝑅) & ⊢ 𝑊 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) & ⊢ 𝑍 = (pmSgn‘(𝑁 ∖ {𝐾})) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → (𝑅 Σg (𝑝 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ↦ (((𝑌 ∘ 𝑆)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ 𝑁 ↦ (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐾, 1 , 0 ), (𝑖𝑀𝑗)))(𝑝‘𝑛))))))) = (𝑅 Σg (𝑝 ∈ 𝑊 ↦ (((𝑌 ∘ 𝑍)‘𝑝)(.r‘𝑅)(𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑖𝑀𝑗))(𝑝‘𝑛)))))))) | ||
| Theorem | smadiadet 22676 | The determinant of a submatrix of a square matrix obtained by removing a row and a column at the same index equals the determinant of the original matrix with the row replaced with 0's and a 1 at the diagonal position. (Contributed by AV, 31-Jan-2019.) (Proof shortened by AV, 24-Jul-2019.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐸 = ((𝑁 ∖ {𝐾}) maDet 𝑅) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁) → (𝐸‘(𝐾((𝑁 subMat 𝑅)‘𝑀)𝐾)) = (𝐷‘(𝐾((𝑁 minMatR1 𝑅)‘𝑀)𝐾))) | ||
| Theorem | smadiadetglem1 22677 | Lemma 1 for smadiadetg 22679. (Contributed by AV, 13-Feb-2019.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐸 = ((𝑁 ∖ {𝐾}) maDet 𝑅) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → ((𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐾) ↾ ((𝑁 ∖ {𝐾}) × 𝑁)) = ((𝐾((𝑁 minMatR1 𝑅)‘𝑀)𝐾) ↾ ((𝑁 ∖ {𝐾}) × 𝑁))) | ||
| Theorem | smadiadetglem2 22678 | Lemma 2 for smadiadetg 22679. (Contributed by AV, 14-Feb-2019.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐸 = ((𝑁 ∖ {𝐾}) maDet 𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → ((𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐾) ↾ ({𝐾} × 𝑁)) = ((({𝐾} × 𝑁) × {𝑆}) ∘f · ((𝐾((𝑁 minMatR1 𝑅)‘𝑀)𝐾) ↾ ({𝐾} × 𝑁)))) | ||
| Theorem | smadiadetg 22679 | The determinant of a square matrix with one row replaced with 0's and an arbitrary element of the underlying ring at the diagonal position equals the ring element multiplied with the determinant of a submatrix of the square matrix obtained by removing the row and the column at the same index. (Contributed by AV, 14-Feb-2019.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑅 ∈ CRing & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐸 = ((𝑁 ∖ {𝐾}) maDet 𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → (𝐷‘(𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐾)) = (𝑆 · (𝐸‘(𝐾((𝑁 subMat 𝑅)‘𝑀)𝐾)))) | ||
| Theorem | smadiadetg0 22680 | Lemma for smadiadetr 22681: version of smadiadetg 22679 with all hypotheses defining class variables removed, i.e. all class variables defined in the hypotheses replaced in the theorem by their definition. (Contributed by AV, 15-Feb-2019.) |
| ⊢ 𝑅 ∈ CRing ⇒ ⊢ ((𝑀 ∈ (Base‘(𝑁 Mat 𝑅)) ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → ((𝑁 maDet 𝑅)‘(𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐾)) = (𝑆(.r‘𝑅)(((𝑁 ∖ {𝐾}) maDet 𝑅)‘(𝐾((𝑁 subMat 𝑅)‘𝑀)𝐾)))) | ||
| Theorem | smadiadetr 22681 | The determinant of a square matrix with one row replaced with 0's and an arbitrary element of the underlying ring at the diagonal position equals the ring element multiplied with the determinant of a submatrix of the square matrix obtained by removing the row and the column at the same index. Closed form of smadiadetg 22679. Special case of the "Laplace expansion", see definition in [Lang] p. 515. (Contributed by AV, 15-Feb-2019.) |
| ⊢ (((𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘(𝑁 Mat 𝑅))) ∧ (𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅))) → ((𝑁 maDet 𝑅)‘(𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐾)) = (𝑆(.r‘𝑅)(((𝑁 ∖ {𝐾}) maDet 𝑅)‘(𝐾((𝑁 subMat 𝑅)‘𝑀)𝐾)))) | ||
| Theorem | invrvald 22682 | If a matrix multiplied with a given matrix (from the left as well as from the right) results in the identity matrix, this matrix is the inverse (matrix) of the given matrix. (Contributed by Stefan O'Rear, 17-Jul-2018.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑋 · 𝑌) = 1 ) & ⊢ (𝜑 → (𝑌 · 𝑋) = 1 ) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝑈 ∧ (𝐼‘𝑋) = 𝑌)) | ||
| Theorem | matinv 22683 | The inverse of a matrix is the adjunct of the matrix multiplied with the inverse of the determinant of the matrix if the determinant is a unit in the underlying ring. Proposition 4.16 in [Lang] p. 518. (Contributed by Stefan O'Rear, 17-Jul-2018.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐽 = (𝑁 maAdju 𝑅) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑈 = (Unit‘𝐴) & ⊢ 𝑉 = (Unit‘𝑅) & ⊢ 𝐻 = (invr‘𝑅) & ⊢ 𝐼 = (invr‘𝐴) & ⊢ ∙ = ( ·𝑠 ‘𝐴) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ (𝐷‘𝑀) ∈ 𝑉) → (𝑀 ∈ 𝑈 ∧ (𝐼‘𝑀) = ((𝐻‘(𝐷‘𝑀)) ∙ (𝐽‘𝑀)))) | ||
| Theorem | matunit 22684 | A matrix is a unit in the ring of matrices iff its determinant is a unit in the underlying ring. (Contributed by Stefan O'Rear, 17-Jul-2018.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑈 = (Unit‘𝐴) & ⊢ 𝑉 = (Unit‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑀 ∈ 𝑈 ↔ (𝐷‘𝑀) ∈ 𝑉)) | ||
In the following, Cramer's rule cramer 22697 is proven. According to Wikipedia "Cramer's rule", 21-Feb-2019, https://en.wikipedia.org/wiki/Cramer%27s_rule 22697: "[Cramer's rule] ... expresses the [unique] solution [of a system of linear equations] in terms of the determinants of the (square) coefficient matrix and of matrices obtained from it by replacing one column by the column vector of right-hand sides of the equations." The outline of the proof for systems of linear equations with coefficients from a commutative ring, according to the proof in Wikipedia (https://en.wikipedia.org/wiki/Cramer's_rule#A_short_proof), 22697 is as follows: The system of linear equations 𝐴 × 𝑋 = 𝐵 to be solved shall be given by the N x N coefficient matrix 𝐴 and the N-dimensional vector 𝐵. Let (𝐴‘𝑖) be the matrix obtained by replacing the i-th column of the coefficient matrix 𝐴 by the right-hand side vector 𝐵. Additionally, let (𝑋‘𝑖) be the matrix obtained by replacing the i-th column of the identity matrix by the solution vector 𝑋, with 𝑋 = (𝑥‘𝑖). Finally, it is assumed that det 𝐴 is a unit in the underlying ring. With these definitions, it follows that 𝐴 × (𝑋‘𝑖) = (𝐴‘𝑖) (cramerimplem2 22690), using matrix multiplication (mamuval 22397) and multiplication of a vector with a matrix (mulmarep1gsum2 22580). By using the multiplicativity of the determinant (mdetmul 22629) it follows that det (𝐴‘𝑖) = det (𝐴 × (𝑋‘𝑖)) = det 𝐴 · det (𝑋‘𝑖) (cramerimplem3 22691). Furthermore, it follows that det (𝑋‘𝑖) = (𝑥‘𝑖) (cramerimplem1 22689). To show this, a special case of the Laplace expansion is used (smadiadetg 22679). From these equations and the cancellation law for division in a ring (dvrcan3 20410) it follows that (𝑥‘𝑖) = det (𝑋‘𝑖) = det (𝐴‘𝑖) / det 𝐴. This is the right to left implication (cramerimp 22692, cramerlem1 22693, cramerlem2 22694) of Cramer's rule (cramer 22697). The left to right implication is shown by cramerlem3 22695, using the fact that a solution of the system of linear equations exists (slesolex 22688). Notice that for the special case of 0-dimensional matrices/vectors only the left to right implication is valid (see cramer0 22696), because assuming the right-hand side of the implication ((𝑋 · 𝑍) = 𝑌), 𝑍 could be anything (see mavmul0g 22559). | ||
| Theorem | slesolvec 22685 | Every solution of a system of linear equations represented by a matrix and a vector is a vector. (Contributed by AV, 10-Feb-2019.) (Revised by AV, 27-Feb-2019.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) ⇒ ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → ((𝑋 · 𝑍) = 𝑌 → 𝑍 ∈ 𝑉)) | ||
| Theorem | slesolinv 22686 | The solution of a system of linear equations represented by a matrix with a unit as determinant is the multiplication of the inverse of the matrix with the right-hand side vector. (Contributed by AV, 10-Feb-2019.) (Revised by AV, 28-Feb-2019.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐼 = (invr‘𝐴) ⇒ ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ ((𝐷‘𝑋) ∈ (Unit‘𝑅) ∧ (𝑋 · 𝑍) = 𝑌)) → 𝑍 = ((𝐼‘𝑋) · 𝑌)) | ||
| Theorem | slesolinvbi 22687 | The solution of a system of linear equations represented by a matrix with a unit as determinant is the multiplication of the inverse of the matrix with the right-hand side vector. (Contributed by AV, 11-Feb-2019.) (Revised by AV, 28-Feb-2019.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐼 = (invr‘𝐴) ⇒ ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ((𝑋 · 𝑍) = 𝑌 ↔ 𝑍 = ((𝐼‘𝑋) · 𝑌))) | ||
| Theorem | slesolex 22688* | Every system of linear equations represented by a matrix with a unit as determinant has a solution. (Contributed by AV, 11-Feb-2019.) (Revised by AV, 28-Feb-2019.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ 𝐷 = (𝑁 maDet 𝑅) ⇒ ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ∃𝑧 ∈ 𝑉 (𝑋 · 𝑧) = 𝑌) | ||
| Theorem | cramerimplem1 22689 | Lemma 1 for cramerimp 22692: The determinant of the identity matrix with the ith column replaced by a (column) vector equals the ith component of the vector. (Contributed by AV, 15-Feb-2019.) (Revised by AV, 5-Jul-2022.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 𝐸 = (((1r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼) & ⊢ 𝐷 = (𝑁 maDet 𝑅) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → (𝐷‘𝐸) = (𝑍‘𝐼)) | ||
| Theorem | cramerimplem2 22690 | Lemma 2 for cramerimp 22692: The matrix of a system of linear equations multiplied with the identity matrix with the ith column replaced by the solution vector of the system of linear equations equals the matrix of the system of linear equations with the ith column replaced by the right-hand side vector of the system of linear equations. (Contributed by AV, 19-Feb-2019.) (Revised by AV, 1-Mar-2019.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 𝐸 = (((1r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼) & ⊢ 𝐻 = ((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝐼) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ × = (𝑅 maMul 〈𝑁, 𝑁, 𝑁〉) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑋 × 𝐸) = 𝐻) | ||
| Theorem | cramerimplem3 22691 | Lemma 3 for cramerimp 22692: The determinant of the matrix of a system of linear equations multiplied with the determinant of the identity matrix with the ith column replaced by the solution vector of the system of linear equations equals the determinant of the matrix of the system of linear equations with the ith column replaced by the right-hand side vector of the system of linear equations. (Contributed by AV, 19-Feb-2019.) (Revised by AV, 1-Mar-2019.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 𝐸 = (((1r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼) & ⊢ 𝐻 = ((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝐼) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ ⊗ = (.r‘𝑅) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → ((𝐷‘𝑋) ⊗ (𝐷‘𝐸)) = (𝐷‘𝐻)) | ||
| Theorem | cramerimp 22692 | One direction of Cramer's rule (according to Wikipedia "Cramer's rule", 21-Feb-2019, https://en.wikipedia.org/wiki/Cramer%27s_rule: "[Cramer's rule] ... expresses the solution [of a system of linear equations] in terms of the determinants of the (square) coefficient matrix and of matrices obtained from it by replacing one column by the column vector of right-hand sides of the equations."): The ith component of the solution vector of a system of linear equations equals the determinant of the matrix of the system of linear equations with the ith column replaced by the righthand side vector of the system of linear equations divided by the determinant of the matrix of the system of linear equations. (Contributed by AV, 19-Feb-2019.) (Revised by AV, 1-Mar-2019.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 𝐸 = (((1r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼) & ⊢ 𝐻 = ((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝐼) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ / = (/r‘𝑅) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ ((𝑋 · 𝑍) = 𝑌 ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅))) → (𝑍‘𝐼) = ((𝐷‘𝐻) / (𝐷‘𝑋))) | ||
| Theorem | cramerlem1 22693* | Lemma 1 for cramer 22697. (Contributed by AV, 21-Feb-2019.) (Revised by AV, 1-Mar-2019.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ / = (/r‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ ((𝐷‘𝑋) ∈ (Unit‘𝑅) ∧ 𝑍 ∈ 𝑉 ∧ (𝑋 · 𝑍) = 𝑌)) → 𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋)))) | ||
| Theorem | cramerlem2 22694* | Lemma 2 for cramer 22697. (Contributed by AV, 21-Feb-2019.) (Revised by AV, 1-Mar-2019.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ / = (/r‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ∀𝑧 ∈ 𝑉 ((𝑋 · 𝑧) = 𝑌 → 𝑧 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))))) | ||
| Theorem | cramerlem3 22695* | Lemma 3 for cramer 22697. (Contributed by AV, 21-Feb-2019.) (Revised by AV, 1-Mar-2019.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ / = (/r‘𝑅) ⇒ ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌)) | ||
| Theorem | cramer0 22696* | Special case of Cramer's rule for 0-dimensional matrices/vectors. (Contributed by AV, 28-Feb-2019.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ / = (/r‘𝑅) ⇒ ⊢ (((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌)) | ||
| Theorem | cramer 22697* | Cramer's rule. According to Wikipedia "Cramer's rule", 21-Feb-2019, https://en.wikipedia.org/wiki/Cramer%27s_rule: "[Cramer's rule] ... expresses the [unique] solution [of a system of linear equations] in terms of the determinants of the (square) coefficient matrix and of matrices obtained from it by replacing one column by the column vector of right-hand sides of the equations." If it is assumed that a (unique) solution exists, it can be obtained by Cramer's rule (see also cramerimp 22692). On the other hand, if a vector can be constructed by Cramer's rule, it is a solution of the system of linear equations, so at least one solution exists. The uniqueness is ensured by considering only systems of linear equations whose matrix has a unit (of the underlying ring) as determinant, see matunit 22684 or slesolinv 22686. For fields as underlying rings, this requirement is equivalent to the determinant not being 0. Theorem 4.4 in [Lang] p. 513. This is Metamath 100 proof #97. (Contributed by Alexander van der Vekens, 21-Feb-2019.) (Revised by Alexander van der Vekens, 1-Mar-2019.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑉 = ((Base‘𝑅) ↑m 𝑁) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ · = (𝑅 maVecMul 〈𝑁, 𝑁〉) & ⊢ / = (/r‘𝑅) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) ↔ (𝑋 · 𝑍) = 𝑌)) | ||
A polynomial matrix or matrix of polynomials is a matrix whose elements are univariate (or multivariate) polynomials. See Wikipedia "Polynomial matrix" https://en.wikipedia.org/wiki/Polynomial_matrix (18-Nov-2019). In this section, only square matrices whose elements are univariate polynomials are considered. Usually, the ring of such matrices, the ring of n x n matrices over the polynomial ring over a ring 𝑅, is denoted by M(n, R[t]). The elements of this ring are called "polynomial matrices (over the ring 𝑅)" in the following. In Metamath notation, this ring is defined by (𝑁 Mat (Poly1‘𝑅)), usually represented by the class variable 𝐶 (or 𝑌, if 𝐶 is already occupied): 𝐶 = (𝑁 Mat 𝑃) with 𝑃 = (Poly1‘𝑅). | ||
| Theorem | pmatring 22698 | The set of polynomial matrices over a ring is a ring. (Contributed by AV, 6-Nov-2019.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring) | ||
| Theorem | pmatlmod 22699 | The set of polynomial matrices over a ring is a left module. (Contributed by AV, 6-Nov-2019.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ LMod) | ||
| Theorem | pmatassa 22700 | The set of polynomial matrices over a commutative ring is an associative algebra. (Contributed by AV, 16-Jun-2024.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐶 ∈ AssAlg) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |