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 13;
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:9;
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 4
.= ((power K) . a,k) * (Det M) by A4, A3, GROUP_1:def 8 ;
:: 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 8 ;
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 8;
hence Det aM = ((power K) . a,k) * (Det M) by A14, VECTSP_1:def 19; :: 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 3;
A18: len M = n by MATRIX_1:def 3;

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 13;
then A22: i in Seg n by A20, A21;
hence aM . i = Line aM,i by MATRIX_2:10
.= 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:10 ;
:: thesis: verum

end;

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