let l, n be Nat; for K being commutative Ring
for pK being FinSequence of K
for a being Element of K
for A being Matrix of n,K st l in Seg n & len pK = n holds
Det (RLine (A,l,(a * pK))) = a * (Det (RLine (A,l,pK)))
let K be commutative Ring; for pK being FinSequence of K
for a being Element of K
for A being Matrix of n,K st l in Seg n & len pK = n holds
Det (RLine (A,l,(a * pK))) = a * (Det (RLine (A,l,pK)))
let pK be FinSequence of K; for a being Element of K
for A being Matrix of n,K st l in Seg n & len pK = n holds
Det (RLine (A,l,(a * pK))) = a * (Det (RLine (A,l,pK)))
let a be Element of K; for A being Matrix of n,K st l in Seg n & len pK = n holds
Det (RLine (A,l,(a * pK))) = a * (Det (RLine (A,l,pK)))
let A be Matrix of n,K; ( l in Seg n & len pK = n implies Det (RLine (A,l,(a * pK))) = a * (Det (RLine (A,l,pK))) )
assume that
A1:
l in Seg n
and
A2:
len pK = n
; Det (RLine (A,l,(a * pK))) = a * (Det (RLine (A,l,pK)))
pK is Element of (len pK) -tuples_on the carrier of K
by FINSEQ_2:92;
then A3:
(a * pK) + ((0. K) * pK) = (a + (0. K)) * pK
by FVSUM_1:55;
a + (0. K) = a
by RLVECT_1:4;
hence Det (RLine (A,l,(a * pK))) =
(a * (Det (RLine (A,l,pK)))) + ((0. K) * (Det (RLine (A,l,pK))))
by A1, A2, A3, Th33
.=
a * (Det (RLine (A,l,pK)))
by RLVECT_1:4
;
verum