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 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; 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; ( 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
; 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; ( 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
; ( 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; 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; ( [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
; 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
; verum