let n be Nat; :: thesis: for K being Field
for A being Matrix of n,K st Det A <> 0. K holds
for x, b being Matrix of K st len x = n & A * x = b holds
( x = (A ~ ) * b & ( for i, j being Nat st [i,j] in Indices x holds
x * i,j = ((Det A) " ) * (Det (ReplaceCol A,i,(Col b,j))) ) )
let K be Field; :: thesis: for A being Matrix of n,K st Det A <> 0. K holds
for x, b being Matrix of K st len x = n & A * x = b holds
( x = (A ~ ) * b & ( for i, j being Nat st [i,j] in Indices x holds
x * i,j = ((Det A) " ) * (Det (ReplaceCol A,i,(Col b,j))) ) )
let A be Matrix of n,K; :: thesis: ( Det A <> 0. K implies for x, b being Matrix of K st len x = n & A * x = b holds
( x = (A ~ ) * b & ( for i, j being Nat st [i,j] in Indices x holds
x * i,j = ((Det A) " ) * (Det (ReplaceCol A,i,(Col b,j))) ) ) )
assume A1: Det A <> 0. K ; :: thesis: for x, b being Matrix of K st len x = n & A * x = b holds
( x = (A ~ ) * b & ( for i, j being Nat st [i,j] in Indices x holds
x * i,j = ((Det A) " ) * (Det (ReplaceCol A,i,(Col b,j))) ) )
let x, b be Matrix of K; :: thesis: ( len x = n & A * x = b implies ( x = (A ~ ) * b & ( for i, j being Nat st [i,j] in Indices x holds
x * i,j = ((Det A) " ) * (Det (ReplaceCol A,i,(Col b,j))) ) ) )
assume A2: ( len x = n & A * x = b ) ; :: thesis: ( x = (A ~ ) * b & ( for i, j being Nat st [i,j] in Indices x holds
x * i,j = ((Det A) " ) * (Det (ReplaceCol A,i,(Col b,j))) ) )
set D = Det A;
set MC = Matrix_of_Cofactor A;
A3: ( len (Matrix_of_Cofactor A) = n & width (Matrix_of_Cofactor A) = n & len ((Matrix_of_Cofactor A) @ ) = n & width ((Matrix_of_Cofactor A) @ ) = n & len (A ~ ) = n & width (A ~ ) = n & len A = n & width A = n ) by MATRIX_1:25;
A is invertible by A1, Th34;
then A ~ is_reverse_of A by MATRIX_6:def 4;
then ( x = (1. K,n) * x & (A ~ ) * A = 1. K,n ) by A2, MATRIXR2:68, MATRIX_6:def 2;
hence A4: x = (A ~ ) * b by A2, A3, MATRIX_3:35; :: thesis: for i, j being Nat st [i,j] in Indices x holds
x * i,j = ((Det A) " ) * (Det (ReplaceCol A,i,(Col b,j)))
let i, j be Nat; :: thesis: ( [i,j] in Indices x implies x * i,j = ((Det A) " ) * (Det (ReplaceCol A,i,(Col b,j))) )
assume A5: [i,j] in Indices x ; :: thesis: x * i,j = ((Det A) " ) * (Det (ReplaceCol A,i,(Col b,j)))
Indices x = [:(Seg n),(Seg (width x)):] by A2, FINSEQ_1:def 3;
then A6: i in Seg n by A5, ZFMISC_1:106;
then A7: ( 1 <= i & i <= n ) by FINSEQ_1:3;
A8: len b = n by A2, A3, MATRIX_3:def 4;
then A9: len (Col b,j) = n by MATRIX_1:def 9;
thus x * i,j = (Line (A ~ ),i) "*" (Col b,j) by A3, A4, A5, A8, MATRIX_3:def 4
.= (Line (((Det A) " ) * ((Matrix_of_Cofactor A) @ )),i) "*" (Col b,j) by A1, Th35
.= (((Det A) " ) * (Line ((Matrix_of_Cofactor A) @ ),i)) "*" (Col b,j) by A3, A7, MATRIXR1:20
.= Sum (((Det A) " ) * (mlt (Line ((Matrix_of_Cofactor A) @ ),i),(Col b,j))) by A3, A8, FVSUM_1:82
.= ((Det A) " ) * ((Line ((Matrix_of_Cofactor A) @ ),i) "*" (Col b,j)) by FVSUM_1:92
.= ((Det A) " ) * ((Col (Matrix_of_Cofactor A),i) "*" (Col b,j)) by A3, A6, MATRIX_2:17
.= ((Det A) " ) * (Sum (LaplaceExpL (RLine (A @ ),i,(Col b,j)),i)) by A6, A9, Th31
.= ((Det A) " ) * (Det (RLine (A @ ),i,(Col b,j))) by A6, Th25
.= ((Det A) " ) * (Det ((RLine (A @ ),i,(Col b,j)) @ )) by MATRIXR2:43
.= ((Det A) " ) * (Det (RCol A,i,(Col b,j))) by Th19 ; :: thesis: verum