let n be Nat; :: thesis: for K being Field
for a, b being Element of
for l being Nat
for pK, qK being FinSequence of st l in Seg n & len pK = n & len qK = n holds
for M being Matrix of n, holds Det (RLine M,l,((a * pK) + (b * qK))) = (a * (Det (RLine M,l,pK))) + (b * (Det (RLine M,l,qK)))
let K be Field; :: thesis: for a, b being Element of
for l being Nat
for pK, qK being FinSequence of st l in Seg n & len pK = n & len qK = n holds
for M being Matrix of n, holds Det (RLine M,l,((a * pK) + (b * qK))) = (a * (Det (RLine M,l,pK))) + (b * (Det (RLine M,l,qK)))
let a, b be Element of ; :: thesis: for l being Nat
for pK, qK being FinSequence of st l in Seg n & len pK = n & len qK = n holds
for M being Matrix of n, holds Det (RLine M,l,((a * pK) + (b * qK))) = (a * (Det (RLine M,l,pK))) + (b * (Det (RLine M,l,qK)))
let l be Nat; :: thesis: for pK, qK being FinSequence of st l in Seg n & len pK = n & len qK = n holds
for M being Matrix of n, holds Det (RLine M,l,((a * pK) + (b * qK))) = (a * (Det (RLine M,l,pK))) + (b * (Det (RLine M,l,qK)))
let pK, qK be FinSequence of ; :: thesis: ( l in Seg n & len pK = n & len qK = n implies for M being Matrix of n, holds Det (RLine M,l,((a * pK) + (b * qK))) = (a * (Det (RLine M,l,pK))) + (b * (Det (RLine M,l,qK))) )
assume that
A1: l in Seg n and
A2: len pK = n and
A3: len qK = n ; :: thesis: for M being Matrix of n, holds Det (RLine M,l,((a * pK) + (b * qK))) = (a * (Det (RLine M,l,pK))) + (b * (Det (RLine M,l,qK)))
set P = Permutations n;
set KK = the carrier of K;
set aa = the addF of K;
let M be Matrix of n,; :: thesis: Det (RLine M,l,((a * pK) + (b * qK))) = (a * (Det (RLine M,l,pK))) + (b * (Det (RLine M,l,qK)))
set Rpq = RLine M,l,((a * pK) + (b * qK));
set Rp = RLine M,l,pK;
set Rq = RLine M,l,qK;
set Pathpq = Path_product (RLine M,l,((a * pK) + (b * qK)));
set Pathp = Path_product (RLine M,l,pK);
set Pathq = Path_product (RLine M,l,qK);
set F = FinOmega (Permutations n);
A4: FinOmega (Permutations n) = Permutations n by MATRIX_2:30, MATRIX_2:def 17;
then consider Gpq being Function of Fin (Permutations n),the carrier of K such that
A5: Det (RLine M,l,((a * pK) + (b * qK))) = Gpq . (FinOmega (Permutations n)) and
A6: for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
Gpq . {} = e and
A7: for x being Element of Permutations n holds Gpq . {x} = (Path_product (RLine M,l,((a * pK) + (b * qK)))) . x and
A8: for B' being Element of Fin (Permutations n) st B' c= FinOmega (Permutations n) & B' <> {} holds
for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B' holds
Gpq . (B' \/ {x}) = the addF of K . (Gpq . B'),((Path_product (RLine M,l,((a * pK) + (b * qK)))) . x) by SETWISEO:def 3;
consider Gq being Function of Fin (Permutations n),the carrier of K such that
A9: Det (RLine M,l,qK) = Gq . (FinOmega (Permutations n)) and
A10: for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
Gq . {} = e and
A11: for x being Element of Permutations n holds Gq . {x} = (Path_product (RLine M,l,qK)) . x and
A12: for B' being Element of Fin (Permutations n) st B' c= FinOmega (Permutations n) & B' <> {} holds
for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B' holds
Gq . (B' \/ {x}) = the addF of K . (Gq . B'),((Path_product (RLine M,l,qK)) . x) by A4, SETWISEO:def 3;
consider Gp being Function of Fin (Permutations n),the carrier of K such that
A13: Det (RLine M,l,pK) = Gp . (FinOmega (Permutations n)) and
A14: for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
Gp . {} = e and
A15: for x being Element of Permutations n holds Gp . {x} = (Path_product (RLine M,l,pK)) . x and
A16: for B' being Element of Fin (Permutations n) st B' c= FinOmega (Permutations n) & B' <> {} holds
for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B' holds
Gp . (B' \/ {x}) = the addF of K . (Gp . B'),((Path_product (RLine M,l,pK)) . x) by A4, SETWISEO:def 3;
defpred S₁[ Nat] means for B being Element of Fin (Permutations n) st card B = $1 holds
Gpq . B = (a * (Gp . B)) + (b * (Gq . B));
A17: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A18: S₁[k] ; :: thesis: S₁[k + 1]
let B be Element of Fin (Permutations n); :: thesis: ( card B = k + 1 implies Gpq . B = (a * (Gp . B)) + (b * (Gq . B)) )
assume A19: card B = k + 1 ; :: thesis: Gpq . B = (a * (Gp . B)) + (b * (Gq . B))

now

per cases ( k = 0 or k > 0 ) ;

case k = 0 ; :: thesis: Gpq . B = (a * (Gp . B)) + (b * (Gq . B))

then consider x being set such that
A20: B = {x} by A19, CARD_2:60;
A21: x in B by A20, TARSKI:def 1;
B c= Permutations n by FINSUB_1:def 5;
then reconsider x = x as Element of Permutations n by A21;
A22: Gp . B = (Path_product (RLine M,l,pK)) . x by A15, A20;
A23: Gq . B = (Path_product (RLine M,l,qK)) . x by A11, A20;
Gpq . B = (Path_product (RLine M,l,((a * pK) + (b * qK)))) . x by A7, A20;
hence Gpq . B = (a * (Gp . B)) + (b * (Gq . B)) by A1, A2, A3, A22, A23, Th32; :: thesis: verum

end;

case A24: k > 0 ; :: thesis: Gpq . B = (a * (Gp . B)) + (b * (Gq . B))

consider x being set such that
A25: x in B by A19, CARD_1:47, XBOOLE_0:def 1;
B c= Permutations n by FINSUB_1:def 5;
then reconsider x = x as Element of Permutations n by A25;
B c= Permutations n by FINSUB_1:def 5;
then B \ {x} c= Permutations n by XBOOLE_1:1;
then reconsider B' = B \ {x} as Element of Fin (Permutations n) by FINSUB_1:def 5;
A26: not x in B' by ZFMISC_1:64;
then A27: x in (FinOmega (Permutations n)) \ B' by A4, XBOOLE_0:def 5;
A28: {x} \/ B' = B by A25, ZFMISC_1:140;
then A29: k + 1 = (card B') + 1 by A19, A26, CARD_2:54;
then A30: Gpq . B' = (a * (Gp . B')) + (b * (Gq . B')) by A18;
A31: B' c= FinOmega (Permutations n) by A4, FINSUB_1:def 5;
then Gpq . B = the addF of K . (Gpq . B'),((Path_product (RLine M,l,((a * pK) + (b * qK)))) . x) by A8, A24, A28, A29, A27, CARD_1:47;
then A32: Gpq . B = ((a * (Gp . B')) + (b * (Gq . B'))) + ((a * ((Path_product (RLine M,l,pK)) . x)) + (b * ((Path_product (RLine M,l,qK)) . x))) by A1, A2, A3, A30, Th32
.= (a * (Gp . B')) + ((b * (Gq . B')) + ((a * ((Path_product (RLine M,l,pK)) . x)) + (b * ((Path_product (RLine M,l,qK)) . x)))) by RLVECT_1:def 6
.= (a * (Gp . B')) + ((a * ((Path_product (RLine M,l,pK)) . x)) + ((b * (Gq . B')) + (b * ((Path_product (RLine M,l,qK)) . x)))) by RLVECT_1:def 6
.= ((a * (Gp . B')) + (a * ((Path_product (RLine M,l,pK)) . x))) + ((b * (Gq . B')) + (b * ((Path_product (RLine M,l,qK)) . x))) by RLVECT_1:def 6
.= (a * ((Gp . B') + ((Path_product (RLine M,l,pK)) . x))) + ((b * (Gq . B')) + (b * ((Path_product (RLine M,l,qK)) . x))) by VECTSP_1:def 18
.= (a * (the addF of K . (Gp . B'),((Path_product (RLine M,l,pK)) . x))) + (b * ((Gq . B') + ((Path_product (RLine M,l,qK)) . x))) by VECTSP_1:def 18
.= (a * (the addF of K . (Gp . B'),((Path_product (RLine M,l,pK)) . x))) + (b * (the addF of K . (Gq . B'),((Path_product (RLine M,l,qK)) . x))) ;
Gp . B = the addF of K . (Gp . B'),((Path_product (RLine M,l,pK)) . x) by A16, A24, A28, A29, A27, A31, CARD_1:47;
hence Gpq . B = (a * (Gp . B)) + (b * (Gq . B)) by A12, A24, A28, A29, A27, A31, A32, CARD_1:47; :: thesis: verum

end;

end;

end;

hence Gpq . B = (a * (Gp . B)) + (b * (Gq . B)) ; :: thesis: verum

end;

A33: S₁[ 0 ]

proof

A34: b * (0. K) = 0. K by VECTSP_1:36;
A35: a * (0. K) = 0. K by VECTSP_1:36;
let B be Element of Fin (Permutations n); :: thesis: ( card B = 0 implies Gpq . B = (a * (Gp . B)) + (b * (Gq . B)) )
assume card B = 0 ; :: thesis: Gpq . B = (a * (Gp . B)) + (b * (Gq . B))
then A36: B = {} ;
then A37: Gp . B = 0. K by A14, FVSUM_1:8;
A38: Gq . B = 0. K by A10, A36, FVSUM_1:8;
Gpq . B = 0. K by A6, A36, FVSUM_1:8;
hence Gpq . B = (a * (Gp . B)) + (b * (Gq . B)) by A37, A38, A35, A34, RLVECT_1:10; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A33, A17);
then S₁[ card (FinOmega (Permutations n))] ;
hence Det (RLine M,l,((a * pK) + (b * qK))) = (a * (Det (RLine M,l,pK))) + (b * (Det (RLine M,l,qK))) by A5, A13, A9; :: thesis: verum