let n be Nat; :: thesis: for K being commutative Ring
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 (RLine (A,i,(Line (A,j)))) = 0. K
let K be commutative Ring; :: 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 (RLine (A,i,(Line (A,j)))) = 0. K
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 (RLine (A,i,(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,(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,(Line (A,j)))) = 0. K
A4: ( i < j or j < i ) by A3, XXREAL_0:1;
len (Line (A,j)) = width A by MATRIX_0:def 7;
then A5: Line ((RLine (A,i,(Line (A,j)))),i) = Line (A,j) by A1, Th28;
Line ((RLine (A,i,(Line (A,j)))),j) = Line (A,j) by A2, A3, Th28;
hence Det (RLine (A,i,(Line (A,j)))) = 0. K by A1, A2, A5, A4, Th50; :: thesis: verum