let n be Nat; 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; 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; 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; ( 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 )
; 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; ( 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
; 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
;
verum