let n be Nat; :: thesis: for K being Field
for a being Element of K
for A being Matrix of n,K
for i, j being Nat st i in Seg n & j in Seg n & i <> j holds
Det A = Det (RLine A,i,((Line A,i) + (a * (Line A,j))))
let K be Field; :: thesis: for a being Element of K
for A being Matrix of n,K
for i, j being Nat st i in Seg n & j in Seg n & i <> j holds
Det A = Det (RLine A,i,((Line A,i) + (a * (Line A,j))))
let a be Element of K; :: thesis: for A being Matrix of n,K
for i, j being Nat st i in Seg n & j in Seg n & i <> j holds
Det A = Det (RLine A,i,((Line A,i) + (a * (Line A,j))))
let A be Matrix of n,K; :: thesis: for i, j being Nat st i in Seg n & j in Seg n & i <> j holds
Det A = Det (RLine A,i,((Line A,i) + (a * (Line A,j))))
let i, j be Nat; :: thesis: ( i in Seg n & j in Seg n & i <> j implies Det A = Det (RLine A,i,((Line A,i) + (a * (Line A,j)))) )
assume that
A1: i in Seg n and
A2: j in Seg n and
A3: i <> j ; :: thesis: Det A = Det (RLine A,i,((Line A,i) + (a * (Line A,j))))
A4: width A = n by MATRIX_1:25;
then A5: len (Line A,j) = n by MATRIX_1:def 8;
A6: len (Line A,j) = len (a * (Line A,j)) by Lm5;
len (Line A,i) = n by A4, MATRIX_1:def 8;
hence Det (RLine A,i,((Line A,i) + (a * (Line A,j)))) = (Det (RLine A,i,(Line A,i))) + (Det (RLine A,i,(a * (Line A,j)))) by A1, A5, A6, Th36
.= (Det A) + (Det (RLine A,i,(a * (Line A,j)))) by Th30
.= (Det A) + (0. K) by A1, A2, A3, Th52
.= Det A by RLVECT_1:10 ;
:: thesis: verum