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]
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
A3: k = m + 1 and
A4: 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 A3, A4, NAT_1:13;
then consider aM being Matrix of n,K such that
A5: Det aM = ((power K) . (a,m)) * (Det M) and
A6: 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 A3, XREAL_1:7;
then k in Seg n by A4;
hence Det R = a * (((power K) . (a,m)) * (Det M)) by A5, MATRIX11:35
.= (((power K) . (a,m)) * a) * (Det M) by GROUP_1:def 3
.= ((power K) . (a,k)) * (Det M) by 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 A7: 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 A8: ( 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 A9: ( ( i <= m & i < k ) or ( i > m & i > k ) ) by A3, NAT_1:13;
Line (R,i) = Line (aM,i) by A7, A8, MATRIX11:28;
hence ( ( i <= k implies Line (R,i) = a * (Line (M,i)) ) & ( i > k implies Line (R,i) = Line (M,i) ) ) by A6, A7, A9; :: thesis: verum

end;

suppose A10: 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_0:def 7 ;
then A11: Line (R,i) = a * (Line (aM,k)) by A7, A10, MATRIX11:28;
i > m by A3, A10, NAT_1:13;
hence ( ( i <= k implies Line (R,i) = a * (Line (M,i)) ) & ( i > k implies Line (R,i) = Line (M,i) ) ) by A6, A7, A10, A11; :: thesis: verum

end;

end;

end;

A12: 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
A13: 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 A13; :: 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 A13; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A12, A1);
then consider aM being Matrix of n,K such that
A14: Det aM = ((power K) . (a,n)) * (Det M) and
A15: 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;
A16: len (a * M) = n by MATRIX_0:def 2;
A17: len M = n by MATRIX_0:def 2;

A18: now :: thesis: for i being Nat st 1 <= i & i <= n holds
aM . i = (a * M) . i

let i be Nat; :: thesis: ( 1 <= i & i <= n implies aM . i = (a * M) . i )
assume that
A19: 1 <= i and
A20: i <= n ; :: thesis: aM . i = (a * M) . i
A21: i in Seg n by A19, A20;
hence aM . i = Line (aM,i) by MATRIX_0:52
.= a * (Line (M,i)) by A15, A20, A21
.= Line ((a * M),i) by A17, A19, A20, MATRIXR1:20
.= (a * M) . i by A21, MATRIX_0:52 ;
:: thesis: verum

end;

len aM = n by MATRIX_0:def 2;
hence Det (a * M) = ((power K) . (a,n)) * (Det M) by A14, A16, A18, FINSEQ_1:14; :: thesis: verum