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))))) ) )

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;

set MC = Matrix_of_Cofactor A;

set D = Det A;

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

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

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

A6: width (A ~) = n by MATRIX_0:24;

A7: width A = n by MATRIX_0:24;

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 that

A8: len x = n and

A9: 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))))) ) )

A10: len A = n by MATRIX_0:24;

then A11: len b = n by A8, A9, A7, MATRIX_3:def 4;

x = (1. (K,n)) * x by A8, MATRIXR2:68;

hence A12: x = (A ~) * b by A8, A9, A6, A10, A7, A2, MATRIX_3:33; :: 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 A13: [i,j] in Indices x ; :: thesis: x * (i,j) = ((Det A) ") * (Det (ReplaceCol (A,i,(Col (b,j)))))

A14: len (Col (b,j)) = n by A11, MATRIX_0:def 8;

Indices x = [:(Seg n),(Seg (width x)):] by A8, FINSEQ_1:def 3;

then A15: i in Seg n by A13, ZFMISC_1:87;

then A16: 1 <= i by FINSEQ_1:1;

A17: i <= n by A15, FINSEQ_1:1;

thus x * (i,j) = (Line ((A ~),i)) "*" (Col (b,j)) by A6, A12, A13, A11, 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 A4, A16, A17, MATRIXR1:20

.= Sum (((Det A) ") * (mlt ((Line (((Matrix_of_Cofactor A) @),i)),(Col (b,j))))) by A5, A11, FVSUM_1:68

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

.= ((Det A) ") * ((Col ((Matrix_of_Cofactor A),i)) "*" (Col (b,j))) by A3, A15, MATRIX_0:59

.= ((Det A) ") * (Sum (LaplaceExpL ((RLine ((A @),i,(Col (b,j)))),i))) by A15, A14, Th31

.= ((Det A) ") * (Det (RLine ((A @),i,(Col (b,j))))) by A15, 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

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))))) ) )

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;

set MC = Matrix_of_Cofactor A;

set D = Det A;

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

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

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

A6: width (A ~) = n by MATRIX_0:24;

A7: width A = n by MATRIX_0:24;

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 that

A8: len x = n and

A9: 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))))) ) )

A10: len A = n by MATRIX_0:24;

then A11: len b = n by A8, A9, A7, MATRIX_3:def 4;

x = (1. (K,n)) * x by A8, MATRIXR2:68;

hence A12: x = (A ~) * b by A8, A9, A6, A10, A7, A2, MATRIX_3:33; :: 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 A13: [i,j] in Indices x ; :: thesis: x * (i,j) = ((Det A) ") * (Det (ReplaceCol (A,i,(Col (b,j)))))

A14: len (Col (b,j)) = n by A11, MATRIX_0:def 8;

Indices x = [:(Seg n),(Seg (width x)):] by A8, FINSEQ_1:def 3;

then A15: i in Seg n by A13, ZFMISC_1:87;

then A16: 1 <= i by FINSEQ_1:1;

A17: i <= n by A15, FINSEQ_1:1;

thus x * (i,j) = (Line ((A ~),i)) "*" (Col (b,j)) by A6, A12, A13, A11, 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 A4, A16, A17, MATRIXR1:20

.= Sum (((Det A) ") * (mlt ((Line (((Matrix_of_Cofactor A) @),i)),(Col (b,j))))) by A5, A11, FVSUM_1:68

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

.= ((Det A) ") * ((Col ((Matrix_of_Cofactor A),i)) "*" (Col (b,j))) by A3, A15, MATRIX_0:59

.= ((Det A) ") * (Sum (LaplaceExpL ((RLine ((A @),i,(Col (b,j)))),i))) by A15, A14, Th31

.= ((Det A) ") * (Det (RLine ((A @),i,(Col (b,j))))) by A15, 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