let n be Nat; :: thesis: for K being commutative Ring
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 commutative Ring; :: 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_0:24;
then A5: len (Line (A,j)) = n by MATRIX_0:def 7;
A6: len (Line (A,j)) = len (a * (Line (A,j))) by Lm5;
len (Line (A,i)) = n by A4, MATRIX_0:def 7;
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:4 ;
:: thesis: verum