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 FinSequence of K st len x = n & A * x = <*b*> @ holds
( <*x*> @ = (A ~ ) * b & ( for i being Nat st i in Seg n holds
x . i = ((Det A) " ) * (Det (ReplaceCol A,i,b)) ) )
let K be Field; for A being Matrix of n,K st Det A <> 0. K holds
for x, b being FinSequence of K st len x = n & A * x = <*b*> @ holds
( <*x*> @ = (A ~ ) * b & ( for i being Nat st i in Seg n holds
x . i = ((Det A) " ) * (Det (ReplaceCol A,i,b)) ) )
let A be Matrix of n,K; ( Det A <> 0. K implies for x, b being FinSequence of K st len x = n & A * x = <*b*> @ holds
( <*x*> @ = (A ~ ) * b & ( for i being Nat st i in Seg n holds
x . i = ((Det A) " ) * (Det (ReplaceCol A,i,b)) ) ) )
assume A1:
Det A <> 0. K
; for x, b being FinSequence of K st len x = n & A * x = <*b*> @ holds
( <*x*> @ = (A ~ ) * b & ( for i being Nat st i in Seg n holds
x . i = ((Det A) " ) * (Det (ReplaceCol A,i,b)) ) )
let x, b be FinSequence of K; ( len x = n & A * x = <*b*> @ implies ( <*x*> @ = (A ~ ) * b & ( for i being Nat st i in Seg n holds
x . i = ((Det A) " ) * (Det (ReplaceCol A,i,b)) ) ) )
assume that
A2:
len x = n
and
A3:
A * x = <*b*> @
; ( <*x*> @ = (A ~ ) * b & ( for i being Nat st i in Seg n holds
x . i = ((Det A) " ) * (Det (ReplaceCol A,i,b)) ) )
set X = <*x*>;
len <*x*> = 1
by MATRIX_1:def 3;
then A4:
len x = width <*x*>
by MATRIX_1:20;
then A5:
len (<*x*> @ ) = len x
by MATRIX_1:def 7;
hence
<*x*> @ = (A ~ ) * b
by A1, A2, A3, Th37; for i being Nat st i in Seg n holds
x . i = ((Det A) " ) * (Det (ReplaceCol A,i,b))
set B = <*b*>;
A6:
1 in Seg 1
;
then A7:
Line <*x*>,1 = <*x*> . 1
by MATRIX_2:10;
len <*b*> = 1
by MATRIX_1:def 3;
then A8:
1 in dom <*b*>
by A6, FINSEQ_1:def 3;
A9:
Line <*b*>,1 = <*b*> . 1
by A6, MATRIX_2:10;
let i be Nat; ( i in Seg n implies x . i = ((Det A) " ) * (Det (ReplaceCol A,i,b)) )
assume A10:
i in Seg n
; x . i = ((Det A) " ) * (Det (ReplaceCol A,i,b))
n > 0
by A10;
then width (<*x*> @ ) =
len <*x*>
by A2, A4, MATRIX_2:12
.=
1
by MATRIX_1:def 3
;
then
Indices (<*x*> @ ) = [:(Seg n),(Seg 1):]
by A2, A5, FINSEQ_1:def 3;
then A11:
[i,1] in Indices (<*x*> @ )
by A10, A6, ZFMISC_1:106;
then
[1,i] in Indices <*x*>
by MATRIX_1:def 7;
then (<*x*> @ ) * i,1 =
<*x*> * 1,i
by MATRIX_1:def 7
.=
(Line <*x*>,1) . i
by A2, A4, A10, MATRIX_1:def 8
.=
x . i
by A7, FINSEQ_1:57
;
hence x . i =
((Det A) " ) * (Det (ReplaceCol A,i,(Col (<*b*> @ ),1)))
by A1, A2, A3, A5, A11, Th37
.=
((Det A) " ) * (Det (ReplaceCol A,i,(Line <*b*>,1)))
by A8, MATRIX_2:16
.=
((Det A) " ) * (Det (ReplaceCol A,i,b))
by A9, FINSEQ_1:57
;
verum