P. 227 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22601-22700   *Has distinct variable group(s)

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 ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐷‘(𝐹 ∙ 𝐺)) = ((𝐷‘𝐹) · (𝐷‘𝐺)))
11.5.2  Determinants of 2 x 2 -matrices
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))))
11.5.3  The matrix adjugate/adjunct
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 𝑅)‘𝑀)𝐼)))
11.5.4  Laplace expansion of determinants (special case) 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 𝑅)‘𝑀)𝐾))))
11.5.5  Inverse matrix
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 ∧ 𝑀 ∈ 𝐵) → (𝑀 ∈ 𝑈 ↔ (𝐷‘𝑀) ∈ 𝑉))
11.5.6  Cramer's rule 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 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) ↔ (𝑋 · 𝑍) = 𝑌))
11.6  Polynomial matrices 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‘𝑅).
11.6.1  Basic properties
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)