let n be Nat; for K being commutative Ring
for A, B, C being Matrix of n,K
for i being Nat st i in Seg n holds
ex P being FinSequence of K st
( len P = n & Det (RLine (C,i,(Line ((A * B),i)))) = the addF of K "**" P & ( for j being Nat st j in Seg n holds
P . j = (A * (i,j)) * (Det (RLine (C,i,(Line (B,j))))) ) )
let K be commutative Ring; for A, B, C being Matrix of n,K
for i being Nat st i in Seg n holds
ex P being FinSequence of K st
( len P = n & Det (RLine (C,i,(Line ((A * B),i)))) = the addF of K "**" P & ( for j being Nat st j in Seg n holds
P . j = (A * (i,j)) * (Det (RLine (C,i,(Line (B,j))))) ) )
let A, B, C be Matrix of n,K; for i being Nat st i in Seg n holds
ex P being FinSequence of K st
( len P = n & Det (RLine (C,i,(Line ((A * B),i)))) = the addF of K "**" P & ( for j being Nat st j in Seg n holds
P . j = (A * (i,j)) * (Det (RLine (C,i,(Line (B,j))))) ) )
let i be Nat; ( i in Seg n implies ex P being FinSequence of K st
( len P = n & Det (RLine (C,i,(Line ((A * B),i)))) = the addF of K "**" P & ( for j being Nat st j in Seg n holds
P . j = (A * (i,j)) * (Det (RLine (C,i,(Line (B,j))))) ) ) )
assume A1:
i in Seg n
; ex P being FinSequence of K st
( len P = n & Det (RLine (C,i,(Line ((A * B),i)))) = the addF of K "**" P & ( for j being Nat st j in Seg n holds
P . j = (A * (i,j)) * (Det (RLine (C,i,(Line (B,j))))) ) )
Seg n <> {}
by A1;
then A2:
n <> 0
;
set a = addFinS K;
A3:
len B = n
by MATRIX_0:24;
deffunc H1( Nat) -> Element of the carrier of K = (A * (i,$1)) * (Det (RLine (C,i,(Line (B,$1)))));
set aa = the addF of K;
set KK = the carrier of K;
A4:
len A = n
by MATRIX_0:24;
consider D being FinSequence of the carrier of K such that
A5:
len D = len A
and
A6:
for j being Nat st j in dom D holds
D . j = H1(j)
from FINSEQ_2:sch 1();
A7:
n <> 0
by A1;
then
len D >= 1
by A4, A5, NAT_1:14;
then consider Fd being sequence of the carrier of K such that
A8:
Fd . 1 = D . 1
and
A9:
for k being Nat st 0 <> k & k < n holds
Fd . (k + 1) = the addF of K . ((Fd . k),(D . (k + 1)))
and
A10:
the addF of K "**" D = Fd . n
by A4, A5, FINSOP_1:def 1;
A11:
dom D = Seg (len A)
by A5, FINSEQ_1:def 3;
width A = n
by MATRIX_0:24;
then consider P being FinSequence of the carrier of K * such that
A12:
len P = n
and
A13:
Line ((A * B),i) = (addFinS K) "**" P
and
A14:
for j being Nat st j in Seg (len B) holds
P . j = (A * (i,j)) * (Line (B,j))
by A1, A7, A3, A4, Th55;
len P >= 1
by A12, A2, NAT_1:14;
then consider Fp being sequence of ( the carrier of K *) such that
A15:
Fp . 1 = P . 1
and
A16:
for k being Nat st 0 <> k & k < n holds
Fp . (k + 1) = (addFinS K) . ((Fp . k),(P . (k + 1)))
and
A17:
Line ((A * B),i) = Fp . n
by A12, A13, FINSOP_1:def 1;
defpred S1[ Nat] means ( 1 <= $1 & $1 <= n implies for pK being FinSequence of K st pK = Fp . $1 holds
( len pK = n & Fd . $1 = Det (RLine (C,i,pK)) ) );
A18:
width B = n
by MATRIX_0:24;
A19:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A20:
S1[
k]
;
S1[k + 1]
set k1 =
k + 1;
set A9 =
A * (
i,
(k + 1));
set L =
Line (
B,
(k + 1));
assume that A21:
1
<= k + 1
and A22:
k + 1
<= n
;
for pK being FinSequence of K st pK = Fp . (k + 1) holds
( len pK = n & Fd . (k + 1) = Det (RLine (C,i,pK)) )
A23:
k + 1
in Seg n
by A21, A22;
let Fpk1 be
FinSequence of the
carrier of
K;
( Fpk1 = Fp . (k + 1) implies ( len Fpk1 = n & Fd . (k + 1) = Det (RLine (C,i,Fpk1)) ) )
assume A24:
Fpk1 = Fp . (k + 1)
;
( len Fpk1 = n & Fd . (k + 1) = Det (RLine (C,i,Fpk1)) )
per cases
( k = 0 or k > 0 )
;
suppose A25:
k = 0
;
( len Fpk1 = n & Fd . (k + 1) = Det (RLine (C,i,Fpk1)) )A26:
P . (k + 1) = (A * (i,(k + 1))) * (Line (B,(k + 1)))
by A3, A14, A23;
A27:
len (Line (B,(k + 1))) = n
by A18, MATRIX_0:def 7;
D . (k + 1) = H1(1)
by A4, A6, A11, A23, A25;
hence
(
len Fpk1 = n &
Fd . (k + 1) = Det (RLine (C,i,Fpk1)) )
by A1, A15, A8, A24, A25, A26, A27, Lm5, Th34;
verum end; suppose A28:
k > 0
;
( len Fpk1 = n & Fd . (k + 1) = Det (RLine (C,i,Fpk1)) )
k + 1
in dom P
by A12, A23, FINSEQ_1:def 3;
then A29:
P . (k + 1) in rng P
by FUNCT_1:def 3;
rng P c= the
carrier of
K *
by FINSEQ_1:def 4;
then reconsider Pk1 =
P . (k + 1),
Fpk =
Fp . k as
Element of the
carrier of
K * by A29, FINSEQ_1:def 11;
A30:
k + 0 < k + 1
by XREAL_1:8;
then A31:
Fd . k = Det (RLine (C,i,Fpk))
by A20, A22, A28, NAT_1:14, XXREAL_0:2;
A32:
len Fpk = n
by A20, A22, A28, A30, NAT_1:14, XXREAL_0:2;
A33:
k < n
by A22, A30, XXREAL_0:2;
then A34:
Fd . (k + 1) = the
addF of
K . (
(Fd . k),
(D . (k + 1)))
by A9, A28;
A35:
P . (k + 1) = (A * (i,(k + 1))) * (Line (B,(k + 1)))
by A3, A14, A23;
Fpk1 = (addFinS K) . (
Fpk,
Pk1)
by A16, A24, A28, A33;
then A36:
Fpk1 = Fpk + ((A * (i,(k + 1))) * (Line (B,(k + 1))))
by A35, Def5;
A37:
len (Line (B,(k + 1))) = n
by A18, MATRIX_0:def 7;
then A38:
len ((A * (i,(k + 1))) * (Line (B,(k + 1)))) = n
by Lm5;
Det (RLine (C,i,((A * (i,(k + 1))) * (Line (B,(k + 1)))))) = (A * (i,(k + 1))) * (Det (RLine (C,i,(Line (B,(k + 1))))))
by A1, A37, Th34;
then
Det (RLine (C,i,Fpk1)) = (Det (RLine (C,i,Fpk))) + ((A * (i,(k + 1))) * (Det (RLine (C,i,(Line (B,(k + 1)))))))
by A1, A32, A36, A38, Th36;
hence
(
len Fpk1 = n &
Fd . (k + 1) = Det (RLine (C,i,Fpk1)) )
by A4, A6, A11, A23, A31, A34, A32, A36, A38, Lm6;
verum end;
end;
take
D
; ( len D = n & Det (RLine (C,i,(Line ((A * B),i)))) = the addF of K "**" D & ( for j being Nat st j in Seg n holds
D . j = (A * (i,j)) * (Det (RLine (C,i,(Line (B,j))))) ) )
thus
len D = n
by A5, MATRIX_0:24; ( Det (RLine (C,i,(Line ((A * B),i)))) = the addF of K "**" D & ( for j being Nat st j in Seg n holds
D . j = (A * (i,j)) * (Det (RLine (C,i,(Line (B,j))))) ) )
A39:
S1[ 0 ]
;
for k being Nat holds S1[k]
from NAT_1:sch 2(A39, A19);
then
S1[ len P]
;
hence
( Det (RLine (C,i,(Line ((A * B),i)))) = the addF of K "**" D & ( for j being Nat st j in Seg n holds
D . j = (A * (i,j)) * (Det (RLine (C,i,(Line (B,j))))) ) )
by A4, A12, A6, A11, A17, A10, A2, NAT_1:14; verum