let n be Nat; 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; 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; ( 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
; 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; ( 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
; ( 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; 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; ( [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
; 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
; verum