let n be Nat; :: thesis: for K being commutative Ring
for a being Element of K
for A being Matrix of n,K st not K is degenerated & K is well-unital & K is domRing-like holds
for i, j being Nat st i in Seg n & j in Seg n & i <> j holds
Det (RLine (A,i,(a * (Line (A,j))))) = 0. K
let K be commutative Ring; :: thesis: for a being Element of K
for A being Matrix of n,K st not K is degenerated & K is well-unital & K is domRing-like holds
for i, j being Nat st i in Seg n & j in Seg n & i <> j holds
Det (RLine (A,i,(a * (Line (A,j))))) = 0. K
let a be Element of K; :: thesis: for A being Matrix of n,K st not K is degenerated & K is well-unital & K is domRing-like holds
for i, j being Nat st i in Seg n & j in Seg n & i <> j holds
Det (RLine (A,i,(a * (Line (A,j))))) = 0. K
let A be Matrix of n,K; :: thesis: ( not K is degenerated & K is well-unital & K is domRing-like implies for i, j being Nat st i in Seg n & j in Seg n & i <> j holds
Det (RLine (A,i,(a * (Line (A,j))))) = 0. K )
assume A0: ( not K is degenerated & K is well-unital & K is domRing-like ) ; :: thesis: for i, j being Nat st i in Seg n & j in Seg n & i <> j holds
Det (RLine (A,i,(a * (Line (A,j))))) = 0. K
let i, j be Nat; :: thesis: ( i in Seg n & j in Seg n & i <> j implies Det (RLine (A,i,(a * (Line (A,j))))) = 0. K )
assume that
A1: i in Seg n and
A2: j in Seg n and
A3: i <> j ; :: thesis: Det (RLine (A,i,(a * (Line (A,j))))) = 0. K
width A = n by MATRIX_0:24;
then len (Line (A,j)) = n by MATRIX_0:def 7;
hence Det (RLine (A,i,(a * (Line (A,j))))) = a * (Det (RLine (A,i,(Line (A,j))))) by A1, Th34
.= a * (0. K) by A0, A1, A2, A3, Th51
.= 0. K ;
:: thesis: verum