let K be Field; :: thesis: for a being Element of K
for M being Matrix of K
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q holds
Det (EqSegm ((a * M),P,Q)) = ((power K) . (a,(card P))) * (Det (EqSegm (M,P,Q)))
let a be Element of K; :: thesis: for M being Matrix of K
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q holds
Det (EqSegm ((a * M),P,Q)) = ((power K) . (a,(card P))) * (Det (EqSegm (M,P,Q)))
let M be Matrix of K; :: thesis: for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q holds
Det (EqSegm ((a * M),P,Q)) = ((power K) . (a,(card P))) * (Det (EqSegm (M,P,Q)))
let P, Q be finite without_zero Subset of NAT; :: thesis: ( [:P,Q:] c= Indices M & card P = card Q implies Det (EqSegm ((a * M),P,Q)) = ((power K) . (a,(card P))) * (Det (EqSegm (M,P,Q))) )
assume that
A1: [:P,Q:] c= Indices M and
A2: card P = card Q ; :: thesis: Det (EqSegm ((a * M),P,Q)) = ((power K) . (a,(card P))) * (Det (EqSegm (M,P,Q)))
EqSegm ((a * M),P,Q) = Segm ((a * M),P,Q) by A2, Def3
.= a * (Segm (M,P,Q)) by A1, Th63
.= a * (EqSegm (M,P,Q)) by A2, Def3 ;
hence Det (EqSegm ((a * M),P,Q)) = ((power K) . (a,(card P))) * (Det (EqSegm (M,P,Q))) by Th71; :: thesis: verum