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 & x * A = <*b*> holds
( <*x*> = b * (A ~) & ( for i being Nat st i in Seg n holds
x . i = ((Det A) ") * (Det (ReplaceLine (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 & x * A = <*b*> holds
( <*x*> = b * (A ~) & ( for i being Nat st i in Seg n holds
x . i = ((Det A) ") * (Det (ReplaceLine (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 & x * A = <*b*> holds
( <*x*> = b * (A ~) & ( for i being Nat st i in Seg n holds
x . i = ((Det A) ") * (Det (ReplaceLine (A,i,b))) ) ) )
assume A1:
Det A <> 0. K
; for x, b being FinSequence of K st len x = n & x * A = <*b*> holds
( <*x*> = b * (A ~) & ( for i being Nat st i in Seg n holds
x . i = ((Det A) ") * (Det (ReplaceLine (A,i,b))) ) )
let x, b be FinSequence of K; ( len x = n & x * A = <*b*> implies ( <*x*> = b * (A ~) & ( for i being Nat st i in Seg n holds
x . i = ((Det A) ") * (Det (ReplaceLine (A,i,b))) ) ) )
assume that
A2:
len x = n
and
A3:
x * A = <*b*>
; ( <*x*> = b * (A ~) & ( for i being Nat st i in Seg n holds
x . i = ((Det A) ") * (Det (ReplaceLine (A,i,b))) ) )
set X = <*x*>;
A4:
width <*x*> = len x
by MATRIX_0:23;
hence
<*x*> = b * (A ~)
by A1, A2, A3, Th38; for i being Nat st i in Seg n holds
x . i = ((Det A) ") * (Det (ReplaceLine (A,i,b)))
A5:
[:(Seg 1),(Seg n):] = Indices <*x*>
by A2, MATRIX_0:23;
set B = <*b*>;
A6:
1 in Seg 1
;
then A7:
Line (<*x*>,1) = <*x*> . 1
by MATRIX_0:52;
let i be Nat; ( i in Seg n implies x . i = ((Det A) ") * (Det (ReplaceLine (A,i,b))) )
assume A8:
i in Seg n
; x . i = ((Det A) ") * (Det (ReplaceLine (A,i,b)))
A9:
[1,i] in [:(Seg 1),(Seg n):]
by A8, A6, ZFMISC_1:87;
A10:
Line (<*b*>,1) = <*b*> . 1
by A6, MATRIX_0:52;
<*x*> * (1,i) =
(Line (<*x*>,1)) . i
by A2, A4, A8, MATRIX_0:def 7
.=
x . i
by A7, FINSEQ_1:40
;
hence x . i =
((Det A) ") * (Det (ReplaceLine (A,i,(Line (<*b*>,1)))))
by A1, A2, A3, A4, A9, A5, Th38
.=
((Det A) ") * (Det (ReplaceLine (A,i,b)))
by A10, FINSEQ_1:40
;
verum