let n be Nat; :: thesis: for K being commutative Ring
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 commutative Ring; :: 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 = In ((Permutations n),(Fin (Permutations n)));
Permutations n in Fin (Permutations n) by FINSUB_1:def 5;
then A4: In ((Permutations n),(Fin (Permutations n))) = Permutations n by SUBSET_1:def 8;
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 . (In ((Permutations n),(Fin (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= In ((Permutations n),(Fin (Permutations n))) & B9 <> {} holds
for x being Element of Permutations n st x in (In ((Permutations n),(Fin (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 . (In ((Permutations n),(Fin (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= In ((Permutations n),(Fin (Permutations n))) & B9 <> {} holds
for x being Element of Permutations n st x in (In ((Permutations n),(Fin (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 . (In ((Permutations n),(Fin (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= In ((Permutations n),(Fin (Permutations n))) & B9 <> {} holds
for x being Element of Permutations n st x in (In ((Permutations n),(Fin (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 Nat st S₁[k] holds
S₁[k + 1]

proof

let k be 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 :: thesis: ( ( k = 0 & Gpq . B = (a * (Gp . B)) + (b * (Gq . B)) ) or ( k > 0 & Gpq . B = (a * (Gp . B)) + (b * (Gq . B)) ) )

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

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

then consider x being object such that
A20: B = {x} by A19, CARD_2:42;
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 object such that
A25: x in B by A19, CARD_1:27, 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 ;
then reconsider B9 = B \ {x} as Element of Fin (Permutations n) by FINSUB_1:def 5;
A26: not x in B9 by ZFMISC_1:56;
then A27: x in (In ((Permutations n),(Fin (Permutations n)))) \ B9 by A4, XBOOLE_0:def 5;
A28: {x} \/ B9 = B by A25, ZFMISC_1:116;
then A29: k + 1 = (card B9) + 1 by A19, A26, CARD_2:41;
then A30: Gpq . B9 = (a * (Gp . B9)) + (b * (Gq . B9)) by A18;
A31: B9 c= In ((Permutations n),(Fin (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:27;
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 3
.= (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 3
.= ((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 3
.= (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 7
.= (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 7
.= (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:27;
hence Gpq . B = (a * (Gp . B)) + (b * (Gq . B)) by A12, A24, A28, A29, A27, A31, A32, CARD_1:27; :: thesis: verum

end;

end;

end;

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

end;

A33: S₁[ 0 ]

proof

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 A34: B = {} ;
then A35: Gp . B = 0. K by A14, FVSUM_1:6;
A36: Gq . B = 0. K by A10, A34, FVSUM_1:6;
Gpq . B = 0. K by A6, A34, FVSUM_1:6;
hence Gpq . B = (a * (Gp . B)) + (b * (Gq . B)) by A35, A36, RLVECT_1:4; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A33, A17);
then S₁[ card (In ((Permutations n),(Fin (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