let n be Nat; :: thesis: for K being Field
for a, b being Element of K
for l being Nat
for pK, qK being FinSequence of K st l in Seg n & len pK = n & len qK = n holds
for M being Matrix of n,K 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 K
for l being Nat
for pK, qK being FinSequence of K st l in Seg n & len pK = n & len qK = n holds
for M being Matrix of n,K 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 K; :: thesis: for l being Nat
for pK, qK being FinSequence of K st l in Seg n & len pK = n & len qK = n holds
for M being Matrix of n,K 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 K st l in Seg n & len pK = n & len qK = n holds
for M being Matrix of n,K 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 K; :: thesis: ( l in Seg n & len pK = n & len qK = n implies for M being Matrix of n,K 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,K 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,K; :: 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 B9 being Element of Fin (Permutations n) st B9 c= FinOmega (Permutations n) & B9 <> {} holds
for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
Gpq . (B9 \/ {x}) = the addF of K . (Gpq . B9),((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 B9 being Element of Fin (Permutations n) st B9 c= FinOmega (Permutations n) & B9 <> {} holds
for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
Gq . (B9 \/ {x}) = the addF of K . (Gq . B9),((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 B9 being Element of Fin (Permutations n) st B9 c= FinOmega (Permutations n) & B9 <> {} holds
for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
Gp . (B9 \/ {x}) = the addF of K . (Gp . B9),((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 B9 = B \ {x} as Element of Fin (Permutations n) by FINSUB_1:def 5;
A26: not x in B9 by ZFMISC_1:64;
then A27: x in (FinOmega (Permutations n)) \ B9 by A4, XBOOLE_0:def 5;
A28: {x} \/ B9 = B by A25, ZFMISC_1:140;
then A29: k + 1 = (card B9) + 1 by A19, A26, CARD_2:54;
then A30: Gpq . B9 = (a * (Gp . B9)) + (b * (Gq . B9)) by A18;
A31: B9 c= FinOmega (Permutations n) by A4, FINSUB_1:def 5;
then Gpq . B = the addF of K . (Gpq . B9),((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 . B9)) + (b * (Gq . B9))) + ((a * ((Path_product (RLine M,l,pK)) . x)) + (b * ((Path_product (RLine M,l,qK)) . x))) by A1, A2, A3, A30, Th32
.= (a * (Gp . B9)) + ((b * (Gq . B9)) + ((a * ((Path_product (RLine M,l,pK)) . x)) + (b * ((Path_product (RLine M,l,qK)) . x)))) by RLVECT_1:def 6
.= (a * (Gp . B9)) + ((a * ((Path_product (RLine M,l,pK)) . x)) + ((b * (Gq . B9)) + (b * ((Path_product (RLine M,l,qK)) . x)))) by RLVECT_1:def 6
.= ((a * (Gp . B9)) + (a * ((Path_product (RLine M,l,pK)) . x))) + ((b * (Gq . B9)) + (b * ((Path_product (RLine M,l,qK)) . x))) by RLVECT_1:def 6
.= (a * ((Gp . B9) + ((Path_product (RLine M,l,pK)) . x))) + ((b * (Gq . B9)) + (b * ((Path_product (RLine M,l,qK)) . x))) by VECTSP_1:def 18
.= (a * (the addF of K . (Gp . B9),((Path_product (RLine M,l,pK)) . x))) + (b * ((Gq . B9) + ((Path_product (RLine M,l,qK)) . x))) by VECTSP_1:def 18
.= (a * (the addF of K . (Gp . B9),((Path_product (RLine M,l,pK)) . x))) + (b * (the addF of K . (Gq . B9),((Path_product (RLine M,l,qK)) . x))) ;
Gp . B = the addF of K . (Gp . B9),((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