let n be Nat; :: thesis: for K being Field
for a being Element of K
for M being Matrix of n,K holds Det (a * M) = ((power K) . (a,n)) * (Det M)
let K be Field; :: thesis: for a being Element of K
for M being Matrix of n,K holds Det (a * M) = ((power K) . (a,n)) * (Det M)
let a be Element of K; :: thesis: for M being Matrix of n,K holds Det (a * M) = ((power K) . (a,n)) * (Det M)
let M be Matrix of n,K; :: thesis: Det (a * M) = ((power K) . (a,n)) * (Det M)
defpred S₁[ Nat] means for k being Nat st k = $1 & k <= n holds
ex aM being Matrix of n,K st
( Det aM = ((power K) . (a,k)) * (Det M) & ( for i being Nat st i in Seg n holds
( ( i <= k implies Line (aM,i) = a * (Line (M,i)) ) & ( i > k implies Line (aM,i) = Line (M,i) ) ) ) );
A1: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A2: S₁[m] ; :: thesis: S₁[m + 1]
A3: m in NAT by ORDINAL1:def 12;
let k be Nat; :: thesis: ( k = m + 1 & k <= n implies ex aM being Matrix of n,K st
( Det aM = ((power K) . (a,k)) * (Det M) & ( for i being Nat st i in Seg n holds
( ( i <= k implies Line (aM,i) = a * (Line (M,i)) ) & ( i > k implies Line (aM,i) = Line (M,i) ) ) ) ) )
assume that
A4: k = m + 1 and
A5: k <= n ; :: thesis: ex aM being Matrix of n,K st
( Det aM = ((power K) . (a,k)) * (Det M) & ( for i being Nat st i in Seg n holds
( ( i <= k implies Line (aM,i) = a * (Line (M,i)) ) & ( i > k implies Line (aM,i) = Line (M,i) ) ) ) )
m <= n by A4, A5, NAT_1:13;
then consider aM being Matrix of n,K such that
A6: Det aM = ((power K) . (a,m)) * (Det M) and
A7: for i being Nat st i in Seg n holds
( ( i <= m implies Line (aM,i) = a * (Line (M,i)) ) & ( i > m implies Line (aM,i) = Line (M,i) ) ) by A2;
take R = RLine (aM,k,(a * (Line (aM,k)))); :: thesis: ( Det R = ((power K) . (a,k)) * (Det M) & ( for i being Nat st i in Seg n holds
( ( i <= k implies Line (R,i) = a * (Line (M,i)) ) & ( i > k implies Line (R,i) = Line (M,i) ) ) ) )
0 + 1 <= k by A4, XREAL_1:7;
then k in Seg n by A4, A5;
hence Det R = a * (((power K) . (a,m)) * (Det M)) by A6, MATRIX11:35
.= (((power K) . (a,m)) * a) * (Det M) by GROUP_1:def 3
.= ((power K) . (a,k)) * (Det M) by A4, A3, GROUP_1:def 7 ;
:: thesis: for i being Nat st i in Seg n holds
( ( i <= k implies Line (R,i) = a * (Line (M,i)) ) & ( i > k implies Line (R,i) = Line (M,i) ) )
let i be Nat; :: thesis: ( i in Seg n implies ( ( i <= k implies Line (R,i) = a * (Line (M,i)) ) & ( i > k implies Line (R,i) = Line (M,i) ) ) )
assume A8: i in Seg n ; :: thesis: ( ( i <= k implies Line (R,i) = a * (Line (M,i)) ) & ( i > k implies Line (R,i) = Line (M,i) ) )

per cases ( i < k or i > k or i = k ) by XXREAL_0:1;

suppose A9: ( i < k or i > k ) ; :: thesis: ( ( i <= k implies Line (R,i) = a * (Line (M,i)) ) & ( i > k implies Line (R,i) = Line (M,i) ) )

then A10: ( ( i <= m & i < k ) or ( i > m & i > k ) ) by A4, NAT_1:13;
Line (R,i) = Line (aM,i) by A8, A9, MATRIX11:28;
hence ( ( i <= k implies Line (R,i) = a * (Line (M,i)) ) & ( i > k implies Line (R,i) = Line (M,i) ) ) by A7, A8, A10; :: thesis: verum

end;

suppose A11: i = k ; :: thesis: ( ( i <= k implies Line (R,i) = a * (Line (M,i)) ) & ( i > k implies Line (R,i) = Line (M,i) ) )

len (a * (Line (aM,k))) = len (Line (aM,k)) by MATRIXR1:16
.= width aM by MATRIX_1:def 7 ;
then A12: Line (R,i) = a * (Line (aM,k)) by A8, A11, MATRIX11:28;
i > m by A4, A11, NAT_1:13;
hence ( ( i <= k implies Line (R,i) = a * (Line (M,i)) ) & ( i > k implies Line (R,i) = Line (M,i) ) ) by A7, A8, A11, A12; :: thesis: verum

end;

end;

end;

A13: S₁[ 0 ]

proof

let k be Nat; :: thesis: ( k = 0 & k <= n implies ex aM being Matrix of n,K st
( Det aM = ((power K) . (a,k)) * (Det M) & ( for i being Nat st i in Seg n holds
( ( i <= k implies Line (aM,i) = a * (Line (M,i)) ) & ( i > k implies Line (aM,i) = Line (M,i) ) ) ) ) )
assume that
A14: k = 0 and
k <= n ; :: thesis: ex aM being Matrix of n,K st
( Det aM = ((power K) . (a,k)) * (Det M) & ( for i being Nat st i in Seg n holds
( ( i <= k implies Line (aM,i) = a * (Line (M,i)) ) & ( i > k implies Line (aM,i) = Line (M,i) ) ) ) )
take aM = M; :: thesis: ( Det aM = ((power K) . (a,k)) * (Det M) & ( for i being Nat st i in Seg n holds
( ( i <= k implies Line (aM,i) = a * (Line (M,i)) ) & ( i > k implies Line (aM,i) = Line (M,i) ) ) ) )
(power K) . (a,0) = 1_ K by GROUP_1:def 7;
hence Det aM = ((power K) . (a,k)) * (Det M) by A14, VECTSP_1:def 8; :: thesis: for i being Nat st i in Seg n holds
( ( i <= k implies Line (aM,i) = a * (Line (M,i)) ) & ( i > k implies Line (aM,i) = Line (M,i) ) )
let i be Nat; :: thesis: ( i in Seg n implies ( ( i <= k implies Line (aM,i) = a * (Line (M,i)) ) & ( i > k implies Line (aM,i) = Line (M,i) ) ) )
assume i in Seg n ; :: thesis: ( ( i <= k implies Line (aM,i) = a * (Line (M,i)) ) & ( i > k implies Line (aM,i) = Line (M,i) ) )
hence ( ( i <= k implies Line (aM,i) = a * (Line (M,i)) ) & ( i > k implies Line (aM,i) = Line (M,i) ) ) by A14; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A13, A1);
then consider aM being Matrix of n,K such that
A15: Det aM = ((power K) . (a,n)) * (Det M) and
A16: for i being Nat st i in Seg n holds
( ( i <= n implies Line (aM,i) = a * (Line (M,i)) ) & ( i > n implies Line (aM,i) = Line (M,i) ) ) ;
set AM = a * M;
A17: len (a * M) = n by MATRIX_1:def 2;
A18: len M = n by MATRIX_1:def 2;

A19: now

let i be Nat; :: thesis: ( 1 <= i & i <= n implies aM . i = (a * M) . i )
assume that
A20: 1 <= i and
A21: i <= n ; :: thesis: aM . i = (a * M) . i
i in NAT by ORDINAL1:def 12;
then A22: i in Seg n by A20, A21;
hence aM . i = Line (aM,i) by MATRIX_2:8
.= a * (Line (M,i)) by A16, A21, A22
.= Line ((a * M),i) by A18, A20, A21, MATRIXR1:20
.= (a * M) . i by A22, MATRIX_2:8 ;
:: thesis: verum

end;

len aM = n by MATRIX_1:def 2;
hence Det (a * M) = ((power K) . (a,n)) * (Det M) by A15, A17, A19, FINSEQ_1:14; :: thesis: verum