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_0:24;

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_0:24;

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_0:24;

A9: width ((Matrix_of_Cofactor A) @) = n by MATRIX_0:24;

len (Matrix_of_Cofactor A) = n by MATRIX_0:24;

then A10: Seg n = dom (Matrix_of_Cofactor A) by FINSEQ_1:def 3;

A11: len (A ~) = n by MATRIX_0:24;

x = x * (1. (K,n)) by A4, MATRIXR2:67;

hence A12: x = b * (A ~) by A4, A5, A11, A6, A3, A2, MATRIX_3:33; :: 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:87;

then A15: 1 <= j by FINSEQ_1:1;

A16: len (Line (b,i)) = n by A7, MATRIX_0:def 7;

A17: j <= n by A14, FINSEQ_1:1;

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:90

.= Sum (((Det A) ") * (mlt ((Col (((Matrix_of_Cofactor A) @),j)),(Line (b,i))))) by A8, A7, FVSUM_1:69

.= ((Det A) ") * ((Col (((Matrix_of_Cofactor A) @),j)) "*" (Line (b,i))) by FVSUM_1:73

.= ((Det A) ") * ((Line ((Matrix_of_Cofactor A),j)) "*" (Line (b,i))) by A14, A10, MATRIX_0:58

.= ((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

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_0:24;

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_0:24;

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_0:24;

A9: width ((Matrix_of_Cofactor A) @) = n by MATRIX_0:24;

len (Matrix_of_Cofactor A) = n by MATRIX_0:24;

then A10: Seg n = dom (Matrix_of_Cofactor A) by FINSEQ_1:def 3;

A11: len (A ~) = n by MATRIX_0:24;

x = x * (1. (K,n)) by A4, MATRIXR2:67;

hence A12: x = b * (A ~) by A4, A5, A11, A6, A3, A2, MATRIX_3:33; :: 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:87;

then A15: 1 <= j by FINSEQ_1:1;

A16: len (Line (b,i)) = n by A7, MATRIX_0:def 7;

A17: j <= n by A14, FINSEQ_1:1;

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:90

.= Sum (((Det A) ") * (mlt ((Col (((Matrix_of_Cofactor A) @),j)),(Line (b,i))))) by A8, A7, FVSUM_1:69

.= ((Det A) ") * ((Col (((Matrix_of_Cofactor A) @),j)) "*" (Line (b,i))) by FVSUM_1:73

.= ((Det A) ") * ((Line ((Matrix_of_Cofactor A),j)) "*" (Line (b,i))) by A14, A10, MATRIX_0:58

.= ((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