P. 209 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20801-20900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	m2detleiblem6 20801	Lemma 6 for m2detleib 20806. (Contributed by AV, 20-Dec-2018.)
⊢ 𝑁 = {1, 2}    &   ⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑌 = (ℤRHom‘𝑅)    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invg‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑄 = {⟨1, 2⟩, ⟨2, 1⟩}) → (𝑌‘(𝑆‘𝑄)) = (𝐼‘ 1 ))
Theorem	m2detleiblem7 20802	Lemma 7 for m2detleib 20806. (Contributed by AV, 20-Dec-2018.)
⊢ 𝑁 = {1, 2}    &   ⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑌 = (ℤRHom‘𝑅)    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝐼 = (invg‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ − = (-g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (Base‘𝑅) ∧ 𝑍 ∈ (Base‘𝑅)) → (𝑋(+g‘𝑅)((𝐼‘ 1 ) · 𝑍)) = (𝑋 − 𝑍))
Theorem	m2detleiblem2 20803*	Lemma 2 for m2detleib 20806. (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 20804*	Lemma 3 for m2detleib 20806. (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 20805*	Lemma 4 for m2detleib 20806. (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 20806	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.3.3  The matrix adjugate/adjunct
Syntax	cmadu 20807	Syntax for the matrix adjugate/adjunct function.
class maAdju
Syntax	cminmar1 20808	Syntax for the minor matrices of a square matrix.
class minMatR1
Definition	df-madu 20809*	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 20810*	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 20752- note that the matrix is transposed compared with the submatrix defined in df-subma 20752, but this does not matter because the determinants are the same, see mdettpos 20786). Such matrices are used in the definition of an adjunct of a square matrix, see df-madu 20809. (Contributed by AV, 27-Dec-2018.)
⊢ minMatR1 = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, (1r‘𝑟), (0g‘𝑟)), (𝑖𝑚𝑗))))))
Theorem	mndifsplit 20811	Lemma for maducoeval2 20815. (Contributed by SO, 16-Jul-2018.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 0 = (0g‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ ((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 )))
Theorem	madufval 20812*	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 20813*	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 20814*	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 20815*	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 20816	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 20817	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 20818*	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 20819	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 20820	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 20821*	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 20822*	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 20823*	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 20824	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 20825	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	minmar1marrepOLD 20826	Obsolete version of minmar1marrep 20825 as of 4-Jul-2022. (Contributed by AV, 12-Feb-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑄 = (𝑁 matRRep 𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((𝑁 minMatR1 𝑅)‘𝑀) = (𝑀(𝑁 matRRep 𝑅) 1 ))
Theorem	minmar1cl 20827	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 20828	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.3.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 20849 or smadiadetr 20851.
Theorem	symgmatr01lem 20829*	Lemma for symgmatr01 20830. (Contributed by AV, 3-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    ⇒   ⊢ ((𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁) → (𝑄 ∈ (𝑃 ∖ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐿}) → ∃𝑘 ∈ 𝑁 if(𝑘 = 𝐾, if((𝑄‘𝑘) = 𝐿, 𝐴, 𝐵), (𝑘𝑀(𝑄‘𝑘))) = 𝐵))
Theorem	symgmatr01 20830*	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 20831*	Lemma A for gsummatr01 20835. (Contributed by AV, 8-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑅 = {𝑟 ∈ 𝑃 ∣ (𝑟‘𝐾) = 𝐿}    ⇒   ⊢ ((𝑄 ∈ 𝑅 ∧ 𝑋 ∈ 𝑁) → (𝑄‘𝑋) ∈ 𝑁)
Theorem	gsummatr01lem2 20832*	Lemma B for gsummatr01 20835. (Contributed by AV, 8-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑅 = {𝑟 ∈ 𝑃 ∣ (𝑟‘𝐾) = 𝐿}    ⇒   ⊢ ((𝑄 ∈ 𝑅 ∧ 𝑋 ∈ 𝑁) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ (Base‘𝐺) → (𝑋𝐴(𝑄‘𝑋)) ∈ (Base‘𝐺)))
Theorem	gsummatr01lem3 20833*	Lemma 1 for gsummatr01 20835. (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 20834*	Lemma 2 for gsummatr01 20835. (Contributed by AV, 8-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑅 = {𝑟 ∈ 𝑃 ∣ (𝑟‘𝐾) = 𝐿}    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑆 = (Base‘𝐺)    ⇒   ⊢ ((((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧ (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) ∧ 𝑛 ∈ (𝑁 ∖ {𝐾})) → (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)))(𝑄‘𝑛)) = (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝐴𝑗))(𝑄‘𝑛)))
Theorem	gsummatr01 20835*	Lemma 1 for smadiadetlem4 20845. (Contributed by AV, 8-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑅 = {𝑟 ∈ 𝑃 ∣ (𝑟‘𝐾) = 𝐿}    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑆 = (Base‘𝐺)    ⇒   ⊢ (((𝐺 ∈ CMnd ∧ 𝑁 ∈ Fin) ∧ (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝐴𝑗) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝑄 ∈ 𝑅)) → (𝐺 Σg (𝑛 ∈ 𝑁 ↦ (𝑛(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝐾, if(𝑗 = 𝐿, 0 , 𝐵), (𝑖𝐴𝑗)))(𝑄‘𝑛)))) = (𝐺 Σg (𝑛 ∈ (𝑁 ∖ {𝐾}) ↦ (𝑛(𝑖 ∈ (𝑁 ∖ {𝐾}), 𝑗 ∈ (𝑁 ∖ {𝐿}) ↦ (𝑖𝐴𝑗))(𝑄‘𝑛)))))
Theorem	marep01ma 20836*	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 20837*	Lemma 0 for smadiadet 20846: 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 20838*	Lemma 1 for smadiadet 20846: 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 20839*	Lemma 1a for smadiadet 20846: 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 20840*	Lemma 2 for smadiadet 20846: 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 20841*	Lemma 0 for smadiadetlem3 20844. (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 20842*	Lemma 1 for smadiadetlem3 20844. (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 20843*	Lemma 2 for smadiadetlem3 20844. (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 20844*	Lemma 3 for smadiadet 20846. (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 20845*	Lemma 4 for smadiadet 20846. (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 20846	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 20847	Lemma 1 for smadiadetg 20849. (Contributed by AV, 13-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑅 ∈ CRing    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐸 = ((𝑁 ∖ {𝐾}) maDet 𝑅)    ⇒   ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → ((𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐾) ↾ ((𝑁 ∖ {𝐾}) × 𝑁)) = ((𝐾((𝑁 minMatR1 𝑅)‘𝑀)𝐾) ↾ ((𝑁 ∖ {𝐾}) × 𝑁)))
Theorem	smadiadetglem2 20848	Lemma 2 for smadiadetg 20849. (Contributed by AV, 14-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑅 ∈ CRing    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐸 = ((𝑁 ∖ {𝐾}) maDet 𝑅)    &   ⊢ · = (.r‘𝑅)    ⇒   ⊢ ((𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝑆 ∈ (Base‘𝑅)) → ((𝐾(𝑀(𝑁 matRRep 𝑅)𝑆)𝐾) ↾ ({𝐾} × 𝑁)) = ((({𝐾} × 𝑁) × {𝑆}) ∘𝑓 · ((𝐾((𝑁 minMatR1 𝑅)‘𝑀)𝐾) ↾ ({𝐾} × 𝑁))))
Theorem	smadiadetg 20849	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 20850	Lemma for smadiadetr 20851: version of smadiadetg 20849 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 20851	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 20849. 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.3.5  Inverse matrix
Theorem	invrvald 20852	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 20853	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 20854	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.3.6  Cramer's rule In the following, Cramer's rule cramer 20868 is proven. 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." 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), 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 20861), using matrix multiplication (mamuval 20560) and multiplication of a vector with a matrix (mulmarep1gsum2 20749). By using the multiplicativity of the determinant (mdetmul 20798) it follows that det (𝐴‘𝑖) = det (𝐴 × (𝑋‘𝑖)) = det 𝐴 · det (𝑋‘𝑖) (cramerimplem3 20862). Furthermore, it follows that det (𝑋‘𝑖) = (𝑥‘𝑖) (cramerimplem1 20859). To show this, a special case of the Laplace expansion is used (smadiadetg 20849). From these equations and the cancellation law for division in a ring (dvrcan3 19047) it follows that (𝑥‘𝑖) = det (𝑋‘𝑖) = det (𝐴‘𝑖) / det 𝐴. This is the right to left implication (cramerimp 20863, cramerlem1 20864, cramerlem2 20865) of Cramer's rule (cramer 20868). The left to right implication is shown by cramerlem3 20866, using the fact that a solution of the system of linear equations exists (slesolex 20858). Notice that for the special case of 0-dimensional matrices/vectors only the left to right implication is valid (see cramer0 20867), because assuming the right-hand side of the implication ((𝑋 · 𝑍) = 𝑌), 𝑍 could be anything (see mavmul0g 20728).
Theorem	slesolvec 20855	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‘𝑅) ↑𝑚 𝑁)    &   ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    ⇒   ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ Ring) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉)) → ((𝑋 · 𝑍) = 𝑌 → 𝑍 ∈ 𝑉))
Theorem	slesolinv 20856	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‘𝑅) ↑𝑚 𝑁)    &   ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐼 = (invr‘𝐴)    ⇒   ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ ((𝐷‘𝑋) ∈ (Unit‘𝑅) ∧ (𝑋 · 𝑍) = 𝑌)) → 𝑍 = ((𝐼‘𝑋) · 𝑌))
Theorem	slesolinvbi 20857	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‘𝑅) ↑𝑚 𝑁)    &   ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ 𝐼 = (invr‘𝐴)    ⇒   ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ((𝑋 · 𝑍) = 𝑌 ↔ 𝑍 = ((𝐼‘𝑋) · 𝑌)))
Theorem	slesolex 20858*	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‘𝑅) ↑𝑚 𝑁)    &   ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    ⇒   ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ∃𝑧 ∈ 𝑉 (𝑋 · 𝑧) = 𝑌)
Theorem	cramerimplem1 20859	Lemma 1 for cramerimp 20863: 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‘𝑅) ↑𝑚 𝑁)    &   ⊢ 𝐸 = (((1r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → (𝐷‘𝐸) = (𝑍‘𝐼))
Theorem	cramerimplem1OLD 20860	Obsolete version of cramerimplem1 20859 as of 5-Jul-2022. (Contributed by AV, 15-Feb-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑉 = ((Base‘𝑅) ↑𝑚 𝑁)    &   ⊢ 𝐸 = (((1r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ 𝑍 ∈ 𝑉) → (𝐷‘𝐸) = (𝑍‘𝐼))
Theorem	cramerimplem2 20861	Lemma 2 for cramerimp 20863: 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‘𝑅) ↑𝑚 𝑁)    &   ⊢ 𝐸 = (((1r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼)    &   ⊢ 𝐻 = ((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝐼)    &   ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ × = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)    ⇒   ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → (𝑋 × 𝐸) = 𝐻)
Theorem	cramerimplem3 20862	Lemma 3 for cramerimp 20863: 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‘𝑅) ↑𝑚 𝑁)    &   ⊢ 𝐸 = (((1r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼)    &   ⊢ 𝐻 = ((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝐼)    &   ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ ⊗ = (.r‘𝑅)    ⇒   ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝑋 · 𝑍) = 𝑌) → ((𝐷‘𝑋) ⊗ (𝐷‘𝐸)) = (𝐷‘𝐻))
Theorem	cramerimp 20863	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‘𝑅) ↑𝑚 𝑁)    &   ⊢ 𝐸 = (((1r‘𝐴)(𝑁 matRepV 𝑅)𝑍)‘𝐼)    &   ⊢ 𝐻 = ((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝐼)    &   ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑁) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ ((𝑋 · 𝑍) = 𝑌 ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅))) → (𝑍‘𝐼) = ((𝐷‘𝐻) / (𝐷‘𝑋)))
Theorem	cramerlem1 20864*	Lemma 1 for cramer 20868. (Contributed by AV, 21-Feb-2019.) (Revised by AV, 1-Mar-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑉 = ((Base‘𝑅) ↑𝑚 𝑁)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ ((𝐷‘𝑋) ∈ (Unit‘𝑅) ∧ 𝑍 ∈ 𝑉 ∧ (𝑋 · 𝑍) = 𝑌)) → 𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))))
Theorem	cramerlem2 20865*	Lemma 2 for cramer 20868. (Contributed by AV, 21-Feb-2019.) (Revised by AV, 1-Mar-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑉 = ((Base‘𝑅) ↑𝑚 𝑁)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → ∀𝑧 ∈ 𝑉 ((𝑋 · 𝑧) = 𝑌 → 𝑧 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋)))))
Theorem	cramerlem3 20866*	Lemma 3 for cramer 20868. (Contributed by AV, 21-Feb-2019.) (Revised by AV, 1-Mar-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑉 = ((Base‘𝑅) ↑𝑚 𝑁)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ (((𝑁 ≠ ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌))
Theorem	cramer0 20867*	Special case of Cramer's rule for 0-dimensional matrices/vectors. (Contributed by AV, 28-Feb-2019.)
⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑉 = ((Base‘𝑅) ↑𝑚 𝑁)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ (((𝑁 = ∅ ∧ 𝑅 ∈ CRing) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) → (𝑋 · 𝑍) = 𝑌))
Theorem	cramer 20868*	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 20863). 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 20854 or slesolinv 20856. 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‘𝑅) ↑𝑚 𝑁)    &   ⊢ 𝐷 = (𝑁 maDet 𝑅)    &   ⊢ · = (𝑅 maVecMul ⟨𝑁, 𝑁⟩)    &   ⊢ / = (/r‘𝑅)    ⇒   ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ≠ ∅) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ∈ (Unit‘𝑅)) → (𝑍 = (𝑖 ∈ 𝑁 ↦ ((𝐷‘((𝑋(𝑁 matRepV 𝑅)𝑌)‘𝑖)) / (𝐷‘𝑋))) ↔ (𝑋 · 𝑍) = 𝑌))
11.4  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.4.1  Basic properties
Theorem	pmatring 20869	The set of polynomial matrices over a ring is a ring. (Contributed by AV, 6-Nov-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring)
Theorem	pmatlmod 20870	The set of polynomial matrices over a ring is a left module. (Contributed by AV, 6-Nov-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ LMod)
Theorem	pmat0op 20871*	The zero polynomial matrix over a ring represented as operation. (Contributed by AV, 16-Nov-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 0 = (0g‘𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0g‘𝐶) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 0 ))
Theorem	pmat1op 20872*	The identity polynomial matrix over a ring represented as operation. (Contributed by AV, 16-Nov-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ 1 = (1r‘𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (1r‘𝐶) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, 1 , 0 )))
Theorem	pmat1ovd 20873	Entries of the identity polynomial matrix over a ring, deduction form. (Contributed by AV, 16-Nov-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 0 = (0g‘𝑃)    &   ⊢ 1 = (1r‘𝑃)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑁)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑁)    &   ⊢ 𝑈 = (1r‘𝐶)    ⇒   ⊢ (𝜑 → (𝐼𝑈𝐽) = if(𝐼 = 𝐽, 1 , 0 ))
Theorem	pmat0opsc 20874*	The zero polynomial matrix over a ring represented as operation with "lifted scalars" (i.e. elements of the ring underlying the polynomial ring embedded into the polynomial ring by the scalar injection/algebraic scalars function algSc). (Contributed by AV, 16-Nov-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0g‘𝐶) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝐴‘ 0 )))
Theorem	pmat1opsc 20875*	The identity polynomial matrix over a ring represented as operation with "lifted scalars". (Contributed by AV, 16-Nov-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (1r‘𝐶) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ if(𝑖 = 𝑗, (𝐴‘ 1 ), (𝐴‘ 0 ))))
Theorem	pmat1ovscd 20876	Entries of the identity polynomial matrix over a ring represented with "lifted scalars", deduction form. (Contributed by AV, 16-Nov-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐴 = (algSc‘𝑃)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ (𝜑 → 𝑁 ∈ Fin)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑁)    &   ⊢ (𝜑 → 𝐽 ∈ 𝑁)    &   ⊢ 𝑈 = (1r‘𝐶)    ⇒   ⊢ (𝜑 → (𝐼𝑈𝐽) = if(𝐼 = 𝐽, (𝐴‘ 1 ), (𝐴‘ 0 )))
Theorem	pmatcoe1fsupp 20877*	For a polynomial matrix there is an upper bound for the coefficients of all the polynomials being not 0. (Contributed by AV, 3-Oct-2019.) (Proof shortened by AV, 28-Nov-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ((coe1‘(𝑖𝑀𝑗))‘𝑥) = 0 ))
Theorem	1pmatscmul 20878	The scalar product of the identity polynomial matrix with a polynomial is a polynomial matrix. (Contributed by AV, 2-Nov-2019.) (Revised by AV, 4-Dec-2019.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐸 = (Base‘𝑃)    &   ⊢ ∗ = ( ·𝑠 ‘𝐶)    &   ⊢ 1 = (1r‘𝐶)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝐸) → (𝑄 ∗ 1 ) ∈ 𝐵)
11.4.2  Constant polynomial matrices A constant polynomial matrix is a polynomial matrix whose elements are constant polynomials, i.e. polynomials with no indeterminates. Constant polynomials are obtained by "lifting" a "scalar" (i.e. an element of the underlying ring) into the polynomial ring/algebra by a "scalar injection", i.e. applying the "algebra scalar injection function" algSc (see df-ascl 19676) to a scalar 𝐴 ∈ 𝑅: ((algSc‘𝑃)‘𝐴). In an analogous way, constant polynomial matrices (over the ring 𝑅) are obtained by "lifting" matrices over the ring 𝑅 by the function matToPolyMat (see df-mat2pmat 20883), called "matrix transformation" in the following. In this section it is shown that the set 𝑆 = (𝑁 ConstPolyMat 𝑅) of constant polynomial 𝑁 x 𝑁 matrices over the ring 𝑅 is a subring of the ring of polynomial 𝑁 x 𝑁 matrices over the ring 𝑅 (cpmatsrgpmat 20897) and that 𝑇 = (𝑁 matToPolyMat 𝑅) is a ring isomorphism between the ring of matrices over a ring 𝑅 and the ring of constant polynomial matrices over the ring 𝑅 (see m2cpmrngiso 20934). By this, it is shown that the ring of matrices over a commutative ring is isomorphic to the ring of scalar matrices over the same ring, see matcpmric 20935. Finally 𝐼 = (𝑁 cPolyMatToMat 𝑅), the transformation of a constant polynomial matrix into a matrix, is the inverse function of the matrix transformation 𝑇 = (𝑁 matToPolyMat 𝑅), see m2cpminv 20936.
Syntax	ccpmat 20879	Extend class notation with the set of all constant polynomial matrices.
class ConstPolyMat
Syntax	cmat2pmat 20880	Extend class notation with the transformation of a matrix into a matrix of polynomials.
class matToPolyMat
Syntax	ccpmat2mat 20881	Extend class notation with the transformation of a constant polynomial matrix into a matrix.
class cPolyMatToMat
Definition	df-cpmat 20882*	The set of all constant polynomial matrices, which are all matrices whose entries are constant polynomials (or "scalar polynomials", see ply1sclf 20016). (Contributed by AV, 15-Nov-2019.)
⊢ ConstPolyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ {𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ∣ ∀𝑖 ∈ 𝑛 ∀𝑗 ∈ 𝑛 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑟)})
Definition	df-mat2pmat 20883*	Transformation of a matrix (over a ring) into a matrix over the corresponding polynomial ring. (Contributed by AV, 31-Jul-2019.)
⊢ matToPolyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦)))))
Definition	df-cpmat2mat 20884*	Transformation of a constant polynomial matrix (over a ring) into a matrix over the corresponding ring. Since this function is the inverse function of matToPolyMat, see m2cpminv 20936, it is also called "inverse matrix transformation" in the following. (Contributed by AV, 14-Dec-2019.)
⊢ cPolyMatToMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (𝑛 ConstPolyMat 𝑟) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦ ((coe1‘(𝑥𝑚𝑦))‘0))))
Theorem	cpmat 20885*	Value of the constructor of the set of all constant polynomial matrices, i.e. the set of all 𝑁 x 𝑁 matrices of polynomials over a ring 𝑅. (Contributed by AV, 15-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑆 = {𝑚 ∈ 𝐵 ∣ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑚𝑗))‘𝑘) = (0g‘𝑅)})
Theorem	cpmatpmat 20886	A constant polynomial matrix is a polynomial matrix. (Contributed by AV, 16-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝑆) → 𝑀 ∈ 𝐵)
Theorem	cpmatel 20887*	Property of a constant polynomial matrix. (Contributed by AV, 15-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) → (𝑀 ∈ 𝑆 ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅)))
Theorem	cpmatelimp 20888*	Implication of a set being a constant polynomial matrix. (Contributed by AV, 18-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑀 ∈ 𝑆 → (𝑀 ∈ 𝐵 ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑘 ∈ ℕ ((coe1‘(𝑖𝑀𝑗))‘𝑘) = (0g‘𝑅))))
Theorem	cpmatel2 20889*	Another property of a constant polynomial matrix. (Contributed by AV, 16-Nov-2019.) (Proof shortened by AV, 27-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑀 ∈ 𝑆 ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑘 ∈ 𝐾 (𝑖𝑀𝑗) = (𝐴‘𝑘)))
Theorem	cpmatelimp2 20890*	Another implication of a set being a constant polynomial matrix. (Contributed by AV, 17-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    &   ⊢ 𝐵 = (Base‘𝐶)    &   ⊢ 𝐾 = (Base‘𝑅)    &   ⊢ 𝐴 = (algSc‘𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑀 ∈ 𝑆 → (𝑀 ∈ 𝐵 ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑘 ∈ 𝐾 (𝑖𝑀𝑗) = (𝐴‘𝑘))))
Theorem	1elcpmat 20891	The identity of the ring of all polynomial matrices over the ring 𝑅 is a constant polynomial matrix. (Contributed by AV, 16-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (1r‘𝐶) ∈ 𝑆)
Theorem	cpmatacl 20892*	The set of all constant polynomial matrices over a ring 𝑅 is closed under addition. (Contributed by AV, 17-Nov-2019.) (Proof shortened by AV, 28-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐶)𝑦) ∈ 𝑆)
Theorem	cpmatinvcl 20893*	The set of all constant polynomial matrices over a ring 𝑅 is closed under inversion. (Contributed by AV, 17-Nov-2019.) (Proof shortened by AV, 28-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ∀𝑥 ∈ 𝑆 ((invg‘𝐶)‘𝑥) ∈ 𝑆)
Theorem	cpmatmcllem 20894*	Lemma for cpmatmcl 20895. (Contributed by AV, 18-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∀𝑐 ∈ ℕ ((coe1‘(𝑃 Σg (𝑘 ∈ 𝑁 ↦ ((𝑖𝑥𝑘)(.r‘𝑃)(𝑘𝑦𝑗)))))‘𝑐) = (0g‘𝑅))
Theorem	cpmatmcl 20895*	The set of all constant polynomial matrices over a ring 𝑅 is closed under multiplication. (Contributed by AV, 18-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(.r‘𝐶)𝑦) ∈ 𝑆)
Theorem	cpmatsubgpmat 20896	The set of all constant polynomial matrices over a ring 𝑅 is an additive subgroup of the ring of all polynomial matrices over the ring 𝑅. (Contributed by AV, 15-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑆 ∈ (SubGrp‘𝐶))
Theorem	cpmatsrgpmat 20897	The set of all constant polynomial matrices over a ring 𝑅 is a subring of the ring of all polynomial matrices over the ring 𝑅. (Contributed by AV, 18-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑆 ∈ (SubRing‘𝐶))
Theorem	0elcpmat 20898	The zero of the ring of all polynomial matrices over the ring 𝑅 is a constant polynomial matrix. (Contributed by AV, 27-Nov-2019.)
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐶 = (𝑁 Mat 𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (0g‘𝐶) ∈ 𝑆)
Theorem	mat2pmatfval 20899*	Value of the matrix transformation. (Contributed by AV, 31-Jul-2019.)
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (algSc‘𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑇 = (𝑚 ∈ 𝐵 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑚𝑦)))))
Theorem	mat2pmatval 20900*	The result of a matrix transformation. (Contributed by AV, 31-Jul-2019.)
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)    &   ⊢ 𝐴 = (𝑁 Mat 𝑅)    &   ⊢ 𝐵 = (Base‘𝐴)    &   ⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝑆 = (algSc‘𝑃)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) = (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑀𝑦))))