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 width x = n & x * A = b holds
( x = b * (A ~ ) & ( for i, j being Nat st [i,j] in Indices x holds
x * i,j = ((Det A) " ) * (Det (ReplaceLine A,j,(Line b,i))) ) )
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 width x = n & x * A = b holds
( x = b * (A ~ ) & ( for i, j being Nat st [i,j] in Indices x holds
x * i,j = ((Det A) " ) * (Det (ReplaceLine A,j,(Line b,i))) ) )
let A be Matrix of n,K; :: thesis: ( Det A <> 0. K implies for x, b being Matrix of K st width x = n & x * A = b holds
( x = b * (A ~ ) & ( for i, j being Nat st [i,j] in Indices x holds
x * i,j = ((Det A) " ) * (Det (ReplaceLine A,j,(Line b,i))) ) ) )
assume A1: Det A <> 0. K ; :: thesis: for x, b being Matrix of K st width x = n & x * A = b holds
( x = b * (A ~ ) & ( for i, j being Nat st [i,j] in Indices x holds
x * i,j = ((Det A) " ) * (Det (ReplaceLine A,j,(Line b,i))) ) )
A is invertible by A1, Th34;
then A ~ is_reverse_of A by MATRIX_6:def 4;
then A2: A * (A ~ ) = 1. K,n by MATRIX_6:def 2;
A3: width A = n by MATRIX_1:25;
let x, b be Matrix of K; :: thesis: ( width x = n & x * A = b implies ( x = b * (A ~ ) & ( for i, j being Nat st [i,j] in Indices x holds
x * i,j = ((Det A) " ) * (Det (ReplaceLine A,j,(Line b,i))) ) ) )
assume that
A4: width x = n and
A5: x * A = b ; :: thesis: ( x = b * (A ~ ) & ( for i, j being Nat st [i,j] in Indices x holds
x * i,j = ((Det A) " ) * (Det (ReplaceLine A,j,(Line b,i))) ) )
A6: len A = n by MATRIX_1:25;
then A7: width b = n by A4, A5, A3, MATRIX_3:def 4;
set MC = Matrix_of_Cofactor A;
set D = Det A;
A8: len ((Matrix_of_Cofactor A) @ ) = n by MATRIX_1:25;
A9: width ((Matrix_of_Cofactor A) @ ) = n by MATRIX_1:25;
len (Matrix_of_Cofactor A) = n by MATRIX_1:25;
then A10: Seg n = dom (Matrix_of_Cofactor A) by FINSEQ_1:def 3;
A11: len (A ~ ) = n by MATRIX_1:25;
x = x * (1. K,n) by A4, MATRIXR2:67;
hence A12: x = b * (A ~ ) by A4, A5, A11, A6, A3, A2, MATRIX_3:35; :: thesis: for i, j being Nat st [i,j] in Indices x holds
x * i,j = ((Det A) " ) * (Det (ReplaceLine A,j,(Line b,i)))
let i, j be Nat; :: thesis: ( [i,j] in Indices x implies x * i,j = ((Det A) " ) * (Det (ReplaceLine A,j,(Line b,i))) )
assume A13: [i,j] in Indices x ; :: thesis: x * i,j = ((Det A) " ) * (Det (ReplaceLine A,j,(Line b,i)))
A14: j in Seg n by A4, A13, ZFMISC_1:106;
then A15: 1 <= j by FINSEQ_1:3;
A16: len (Line b,i) = n by A7, MATRIX_1:def 8;
A17: j <= n by A14, FINSEQ_1:3;
thus x * i,j = (Line b,i) "*" (Col (A ~ ),j) by A11, A12, A13, A7, MATRIX_3:def 4
.= (Line b,i) "*" (Col (((Det A) " ) * ((Matrix_of_Cofactor A) @ )),j) by A1, Th35
.= (Line b,i) "*" (((Det A) " ) * (Col ((Matrix_of_Cofactor A) @ ),j)) by A9, A15, A17, MATRIXR1:19
.= (((Det A) " ) * (Col ((Matrix_of_Cofactor A) @ ),j)) "*" (Line b,i) by FVSUM_1:115
.= Sum (((Det A) " ) * (mlt (Col ((Matrix_of_Cofactor A) @ ),j),(Line b,i))) by A8, A7, FVSUM_1:83
.= ((Det A) " ) * ((Col ((Matrix_of_Cofactor A) @ ),j) "*" (Line b,i)) by FVSUM_1:92
.= ((Det A) " ) * ((Line (Matrix_of_Cofactor A),j) "*" (Line b,i)) by A14, A10, MATRIX_2:16
.= ((Det A) " ) * (Sum (LaplaceExpL (RLine A,j,(Line b,i)),j)) by A14, A16, Th28
.= ((Det A) " ) * (Det (RLine A,j,(Line b,i))) by A14, Th25 ; :: thesis: verum