let i, j, m9, n9 be Nat; :: thesis: for K being Field
for a being Element of K
for M9 being Matrix of n9,m9,K st j in Seg (len M9) & ( i = j implies a <> - (1_ K) ) holds
the_rank_of M9 = the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j))))))
let K be Field; :: thesis: for a being Element of K
for M9 being Matrix of n9,m9,K st j in Seg (len M9) & ( i = j implies a <> - (1_ K) ) holds
the_rank_of M9 = the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j))))))
let a be Element of K; :: thesis: for M9 being Matrix of n9,m9,K st j in Seg (len M9) & ( i = j implies a <> - (1_ K) ) holds
the_rank_of M9 = the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j))))))
let M9 be Matrix of n9,m9,K; :: thesis: ( j in Seg (len M9) & ( i = j implies a <> - (1_ K) ) implies the_rank_of M9 = the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) )
assume that
A1: j in Seg (len M9) and
A2: ( i = j implies a <> - (1_ K) ) ; :: thesis: the_rank_of M9 = the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j))))))
per cases ( not i in Seg (len M9) or i in Seg (len M9) ) ;
suppose not i in Seg (len M9) ; :: thesis: the_rank_of M9 = the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j))))))
hence the_rank_of M9 = the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) by Th40; :: thesis: verum
end;
suppose A3: i in Seg (len M9) ; :: thesis: the_rank_of M9 = the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j))))))
set KK = the carrier of K;
set W = width M9;
set Lj = Line (M9,j);
set Li = Line (M9,i);
set R = RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))));
reconsider Li9 = Line (M9,i), Lj9 = Line (M9,j), LL = (Line (M9,i)) + (a * (Line (M9,j))) as Element of the carrier of K * by FINSEQ_1:def 11;
A4: len (Line (M9,i)) = width M9 by CARD_1:def 7;
then A5: dom (Line (M9,i)) = Seg (width M9) by FINSEQ_1:def 3;
A6: len ((Line (M9,i)) + (a * (Line (M9,j)))) = width M9 by CARD_1:def 7;
then A7: width M9 = width (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) by MATRIX11:def 3;
then A8: RLine ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),i,(Line (M9,i))) = Replace ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),i,Li9) by A4, MATRIX11:29
.= Replace ((Replace (M9,i,LL)),i,Li9) by A6, MATRIX11:29
.= Replace (M9,i,Li9) by FUNCT_7:34
.= RLine (M9,i,(Line (M9,i))) by A4, MATRIX11:29
.= M9 by MATRIX11:30 ;
A9: len M9 = n9 by MATRIX_0:def 2;
then A10: Line ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),i) = (Line (M9,i)) + (a * (Line (M9,j))) by A3, A6, MATRIX11:28;
A11: len (Line (M9,j)) = width M9 by CARD_1:def 7;
then A12: dom (Line (M9,j)) = Seg (width M9) by FINSEQ_1:def 3;
len (a * (Line (M9,j))) = width M9 by CARD_1:def 7;
then A13: dom (a * (Line (M9,j))) = Seg (width M9) by FINSEQ_1:def 3;
A14: Indices (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) = Indices M9 by MATRIX_0:26;
consider P1, Q1 being finite without_zero Subset of NAT such that
A15: [:P1,Q1:] c= Indices M9 and
A16: card P1 = card Q1 and
A17: card P1 = the_rank_of M9 and
A18: Det (EqSegm (M9,P1,Q1)) <> 0. K by Def4;
A19: EqSegm (M9,P1,Q1) = Segm (M9,P1,Q1) by A16, Def3;
A20: EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P1,Q1) = Segm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P1,Q1) by A16, Def3;
A21: RLine ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),i,(Line (M9,j))) = Replace ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),i,Lj9) by A11, A7, MATRIX11:29
.= Replace ((Replace (M9,i,LL)),i,Lj9) by A6, MATRIX11:29
.= Replace (M9,i,Lj9) by FUNCT_7:34
.= RLine (M9,i,(Line (M9,j))) by A11, MATRIX11:29 ;
A22: now :: thesis: the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) >= the_rank_of M9
per cases ( not i in P1 or i in P1 ) ;
suppose not i in P1 ; :: thesis: the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) >= the_rank_of M9
then Segm (M9,P1,Q1) = Segm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P1,Q1) by A15, Th60;
hence the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) >= the_rank_of M9 by A14, A15, A16, A17, A18, A20, A19, Def4; :: thesis: verum
end;
suppose A23: i in P1 ; :: thesis: the_rank_of M9 <= the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j))))))
set SM = EqSegm (M9,P1,Q1);
set SR = EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P1,Q1);
A24: rng (Line (M9,j)) c= the carrier of K by FINSEQ_1:def 4;
A25: ex k being Nat st P1 c= Seg k by Th43;
then A26: dom (Sgm P1) = Seg (card P1) by FINSEQ_3:40;
A27: Q1 c= Seg (width M9) by A15, A16, Th67;
then A28: dom (Sgm Q1) = Seg (card Q1) by FINSEQ_3:40;
A29: rng (Sgm Q1) c= Seg (width M9) by A27, FINSEQ_1:def 13;
then A30: dom ((Line (M9,j)) * (Sgm Q1)) = dom (Sgm Q1) by A12, RELAT_1:27;
then reconsider LjQ = (Line (M9,j)) * (Sgm Q1) as FinSequence by A28, FINSEQ_1:def 2;
rng LjQ c= rng (Line (M9,j)) by RELAT_1:26;
then rng LjQ c= the carrier of K by A24;
then reconsider LjQ = LjQ as FinSequence of K by FINSEQ_1:def 4;
A31: len LjQ = card P1 by A16, A30, A28, FINSEQ_1:def 3;
rng (Sgm P1) = P1 by A25, FINSEQ_1:def 13;
then consider m being object such that
A32: m in dom (Sgm P1) and
A33: (Sgm P1) . m = i by A23, FUNCT_1:def 3;
reconsider m = m as Element of NAT by A32;
A34: len (Line ((EqSegm (M9,P1,Q1)),m)) = width (EqSegm (M9,P1,Q1)) by MATRIX_0:def 7;
A35: Line ((EqSegm (M9,P1,Q1)),m) = (Line (M9,i)) * (Sgm Q1) by A19, A32, A33, A26, A27, Th47;
then A36: RLine ((EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P1,Q1)),m,(Line ((EqSegm (M9,P1,Q1)),m))) = Segm (M9,P1,Q1) by A4, A7, A8, A14, A15, A16, A20, A33, Th59;
Q1 c= Seg (width (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j))))))) by A14, A15, A16, Th67;
then A37: Line ((EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P1,Q1)),m) = (Line ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),i)) * (Sgm Q1) by A20, A32, A33, A26, Th47;
A38: RLine ((EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P1,Q1)),m,LjQ) = Segm ((RLine (M9,i,(Line (M9,j)))),P1,Q1) by A11, A7, A21, A14, A15, A16, A20, A33, Th59;
A39: a * LjQ = (a * (Line (M9,j))) * (Sgm Q1) by A12, A29, Th87;
A40: len LjQ = len (a * LjQ) by MATRIXR1:16;
A41: width (EqSegm (M9,P1,Q1)) = card P1 by MATRIX_0:24;
A42: Segm ((RLine (M9,i,(Line (M9,j)))),P1,Q1) = EqSegm ((RLine (M9,i,(Line (M9,j)))),P1,Q1) by A16, Def3;
EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P1,Q1) = RLine ((EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P1,Q1)),m,(Line ((EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P1,Q1)),m))) by MATRIX11:30
.= RLine ((EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P1,Q1)),m,((Line ((EqSegm (M9,P1,Q1)),m)) + (a * LjQ))) by A10, A5, A13, A29, A37, A35, A39, Th88 ;
then A43: Det (EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P1,Q1)) = (Det (RLine ((EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P1,Q1)),m,(Line ((EqSegm (M9,P1,Q1)),m))))) + (Det (RLine ((EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P1,Q1)),m,(a * LjQ)))) by A32, A26, A31, A40, A34, A41, MATRIX11:36
.= (Det (RLine ((EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P1,Q1)),m,(Line ((EqSegm (M9,P1,Q1)),m))))) + (a * (Det (RLine ((EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P1,Q1)),m,LjQ)))) by A32, A26, A31, MATRIX11:34
.= (Det (EqSegm (M9,P1,Q1))) + (a * (Det (EqSegm ((RLine (M9,i,(Line (M9,j)))),P1,Q1)))) by A16, A36, A38, A42, Def3 ;
per cases ( Det (EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P1,Q1)) <> 0. K or Det (EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P1,Q1)) = 0. K ) ;
suppose Det (EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P1,Q1)) <> 0. K ; :: thesis: the_rank_of M9 <= the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j))))))
hence the_rank_of M9 <= the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) by A14, A15, A16, A17, Def4; :: thesis: verum
end;
suppose A44: Det (EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P1,Q1)) = 0. K ; :: thesis: the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) >= the_rank_of M9
reconsider j0 = j as non zero Element of NAT by A1;
per cases ( i = j or ( i <> j & j in P1 ) or ( i <> j & not j in P1 ) ) ;
suppose A45: i = j ; :: thesis: the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) >= the_rank_of M9
then Det (EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P1,Q1)) = (Det (EqSegm (M9,P1,Q1))) + (a * (Det (EqSegm (M9,P1,Q1)))) by A43, MATRIX11:30
.= ((1_ K) * (Det (EqSegm (M9,P1,Q1)))) + (a * (Det (EqSegm (M9,P1,Q1))))
.= ((1_ K) + a) * (Det (EqSegm (M9,P1,Q1))) by VECTSP_1:def 7 ;
then (1_ K) + a = 0. K by A18, A44, VECTSP_1:12;
then a = (0. K) - (1_ K) by VECTSP_2:2
.= (0. K) + (- (1_ K))
.= - (1_ K) by RLVECT_1:def 4 ;
hence the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) >= the_rank_of M9 by A2, A45; :: thesis: verum
end;
suppose A46: ( i <> j & j in P1 ) ; :: thesis: the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) >= the_rank_of M9
rng (Sgm P1) = P1 by A25, FINSEQ_1:def 13;
then consider l being object such that
A47: l in dom (Sgm P1) and
A48: (Sgm P1) . l = j0 by A46, FUNCT_1:def 3;
reconsider l = l as Element of NAT by A47;
0. K = Det (RLine ((EqSegm (M9,P1,Q1)),m,(Line ((EqSegm (M9,P1,Q1)),l)))) by A32, A33, A26, A46, A47, A48, MATRIX11:51;
then A49: 0. K = a * (Det (RLine ((EqSegm (M9,P1,Q1)),m,(Line ((EqSegm (M9,P1,Q1)),l))))) ;
RLine ((EqSegm (M9,P1,Q1)),m,(Line ((EqSegm (M9,P1,Q1)),l))) = EqSegm ((RLine (M9,i,(Line (M9,j)))),P1,Q1) by A11, A15, A16, A19, A33, A26, A27, A38, A42, A47, A48, Th47, Th59;
hence the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) >= the_rank_of M9 by A18, A43, A44, A49, RLVECT_1:def 4; :: thesis: verum
end;
suppose A50: ( i <> j & not j in P1 ) ; :: thesis: the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) >= the_rank_of M9
set Pij = (P1 \ {i}) \/ {j0};
A51: not i in P1 \ {i} by ZFMISC_1:56;
A52: [:((P1 \ {i}) \/ {j0}),Q1:] c= Indices (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) by A1, A9, A14, A15, A16, A23, A50, Th68;
a * (Det (EqSegm ((RLine (M9,i,(Line (M9,j)))),P1,Q1))) <> 0. K by A18, A43, A44, RLVECT_1:def 4;
then A53: Det (EqSegm ((RLine (M9,i,(Line (M9,j)))),P1,Q1)) <> 0. K ;
( Det (EqSegm ((RLine (M9,i,(Line (M9,j)))),P1,Q1)) = Det (EqSegm (M9,((P1 \ {i}) \/ {j0}),Q1)) or Det (EqSegm ((RLine (M9,i,(Line (M9,j)))),P1,Q1)) = - (Det (EqSegm (M9,((P1 \ {i}) \/ {j0}),Q1))) ) by A1, A9, A15, A16, A23, A50, Th68;
then A54: Det (EqSegm (M9,((P1 \ {i}) \/ {j0}),Q1)) <> 0. K by A53, VECTSP_2:3;
not i in {j} by A50, TARSKI:def 1;
then A55: not i in (P1 \ {i}) \/ {j0} by A51, XBOOLE_0:def 3;
A56: card P1 = card ((P1 \ {i}) \/ {j0}) by A1, A9, A15, A16, A23, A50, Th68;
then EqSegm (M9,((P1 \ {i}) \/ {j0}),Q1) = Segm (M9,((P1 \ {i}) \/ {j0}),Q1) by A16, Def3
.= Segm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),((P1 \ {i}) \/ {j0}),Q1) by A14, A52, A55, Th60
.= EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),((P1 \ {i}) \/ {j0}),Q1) by A16, A56, Def3 ;
hence the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) >= the_rank_of M9 by A16, A17, A54, A56, A52, Def4; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
consider P, Q being finite without_zero Subset of NAT such that
A57: [:P,Q:] c= Indices (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) and
A58: card P = card Q and
A59: card P = the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) and
A60: Det (EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P,Q)) <> 0. K by Def4;
A61: EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P,Q) = Segm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P,Q) by A58, Def3;
A62: EqSegm (M9,P,Q) = Segm (M9,P,Q) by A58, Def3;
now :: thesis: the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) <= the_rank_of M9
per cases ( not i in P or i in P ) ;
suppose not i in P ; :: thesis: the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) <= the_rank_of M9
then Segm (M9,P,Q) = Segm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P,Q) by A57, A14, Th60;
hence the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) <= the_rank_of M9 by A57, A58, A59, A60, A61, A62, A14, Def4; :: thesis: verum
end;
suppose A63: i in P ; :: thesis: the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) <= the_rank_of M9
set SM = EqSegm (M9,P,Q);
set SR = EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P,Q);
A64: rng (Line (M9,j)) c= the carrier of K by FINSEQ_1:def 4;
A65: ex k being Nat st P c= Seg k by Th43;
then A66: dom (Sgm P) = Seg (card P) by FINSEQ_3:40;
A67: Q c= Seg (width M9) by A57, A58, A14, Th67;
then A68: dom (Sgm Q) = Seg (card Q) by FINSEQ_3:40;
A69: rng (Sgm Q) c= Seg (width M9) by A67, FINSEQ_1:def 13;
then A70: dom ((Line (M9,j)) * (Sgm Q)) = dom (Sgm Q) by A12, RELAT_1:27;
then reconsider LjQ = (Line (M9,j)) * (Sgm Q) as FinSequence by A68, FINSEQ_1:def 2;
rng LjQ c= rng (Line (M9,j)) by RELAT_1:26;
then rng LjQ c= the carrier of K by A64;
then reconsider LjQ = LjQ as FinSequence of K by FINSEQ_1:def 4;
A71: len LjQ = card P by A58, A70, A68, FINSEQ_1:def 3;
rng (Sgm P) = P by A65, FINSEQ_1:def 13;
then consider m being object such that
A72: m in dom (Sgm P) and
A73: (Sgm P) . m = i by A63, FUNCT_1:def 3;
reconsider m = m as Element of NAT by A72;
A74: len (Line ((EqSegm (M9,P,Q)),m)) = width (EqSegm (M9,P,Q)) by MATRIX_0:def 7;
A75: Line ((EqSegm (M9,P,Q)),m) = (Line (M9,i)) * (Sgm Q) by A62, A72, A73, A66, A67, Th47;
then A76: RLine ((EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P,Q)),m,(Line ((EqSegm (M9,P,Q)),m))) = Segm (M9,P,Q) by A4, A7, A8, A57, A58, A61, A73, Th59;
Q c= Seg (width (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j))))))) by A57, A58, Th67;
then A77: Line ((EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P,Q)),m) = (Line ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),i)) * (Sgm Q) by A61, A72, A73, A66, Th47;
A78: RLine ((EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P,Q)),m,LjQ) = Segm ((RLine (M9,i,(Line (M9,j)))),P,Q) by A11, A7, A21, A57, A58, A61, A73, Th59;
A79: a * LjQ = (a * (Line (M9,j))) * (Sgm Q) by A12, A69, Th87;
A80: len LjQ = len (a * LjQ) by MATRIXR1:16;
A81: width (EqSegm (M9,P,Q)) = card P by MATRIX_0:24;
A82: Segm ((RLine (M9,i,(Line (M9,j)))),P,Q) = EqSegm ((RLine (M9,i,(Line (M9,j)))),P,Q) by A58, Def3;
EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P,Q) = RLine ((EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P,Q)),m,(Line ((EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P,Q)),m))) by MATRIX11:30
.= RLine ((EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P,Q)),m,((Line ((EqSegm (M9,P,Q)),m)) + (a * LjQ))) by A10, A5, A13, A69, A77, A75, A79, Th88 ;
then A83: Det (EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P,Q)) = (Det (RLine ((EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P,Q)),m,(Line ((EqSegm (M9,P,Q)),m))))) + (Det (RLine ((EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P,Q)),m,(a * LjQ)))) by A72, A66, A71, A80, A74, A81, MATRIX11:36
.= (Det (RLine ((EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P,Q)),m,(Line ((EqSegm (M9,P,Q)),m))))) + (a * (Det (RLine ((EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P,Q)),m,LjQ)))) by A72, A66, A71, MATRIX11:34
.= (Det (EqSegm (M9,P,Q))) + (a * (Det (EqSegm ((RLine (M9,i,(Line (M9,j)))),P,Q)))) by A58, A76, A78, A82, Def3 ;
per cases ( Det (EqSegm (M9,P,Q)) <> 0. K or Det (EqSegm (M9,P,Q)) = 0. K ) ;
suppose Det (EqSegm (M9,P,Q)) <> 0. K ; :: thesis: the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) <= the_rank_of M9
hence the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) <= the_rank_of M9 by A57, A58, A59, A14, Def4; :: thesis: verum
end;
suppose A84: Det (EqSegm (M9,P,Q)) = 0. K ; :: thesis: the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) <= the_rank_of M9
reconsider j0 = j as non zero Element of NAT by A1;
per cases ( i = j or ( i <> j & j in P ) or ( i <> j & not j in P ) ) ;
suppose i = j ; :: thesis: the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) <= the_rank_of M9
then Det (EqSegm ((RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))),P,Q)) = (Det (EqSegm (M9,P,Q))) + (a * (Det (EqSegm (M9,P,Q)))) by A83, MATRIX11:30
.= ((1_ K) * (Det (EqSegm (M9,P,Q)))) + (a * (Det (EqSegm (M9,P,Q))))
.= ((1_ K) + a) * (Det (EqSegm (M9,P,Q))) by VECTSP_1:def 7 ;
hence the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) <= the_rank_of M9 by A60, A84; :: thesis: verum
end;
suppose A85: ( i <> j & j in P ) ; :: thesis: the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) <= the_rank_of M9
rng (Sgm P) = P by A65, FINSEQ_1:def 13;
then consider l being object such that
A86: l in dom (Sgm P) and
A87: (Sgm P) . l = j0 by A85, FUNCT_1:def 3;
reconsider l = l as Element of NAT by A86;
A88: RLine ((EqSegm (M9,P,Q)),m,(Line ((EqSegm (M9,P,Q)),l))) = EqSegm ((RLine (M9,i,(Line (M9,j)))),P,Q) by A11, A57, A58, A62, A14, A73, A66, A67, A78, A82, A86, A87, Th47, Th59;
0. K = Det (RLine ((EqSegm (M9,P,Q)),m,(Line ((EqSegm (M9,P,Q)),l)))) by A72, A73, A66, A85, A86, A87, MATRIX11:51;
then 0. K = a * (Det (RLine ((EqSegm (M9,P,Q)),m,(Line ((EqSegm (M9,P,Q)),l)))))
.= (Det (EqSegm (M9,P,Q))) + (a * (Det (EqSegm ((RLine (M9,i,(Line (M9,j)))),P,Q)))) by A84, A88, RLVECT_1:def 4 ;
hence the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) <= the_rank_of M9 by A60, A83; :: thesis: verum
end;
suppose A89: ( i <> j & not j in P ) ; :: thesis: the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) <= the_rank_of M9
set Pij = (P \ {i}) \/ {j0};
A90: card P = card ((P \ {i}) \/ {j0}) by A1, A9, A57, A58, A63, A89, Th68;
a * (Det (EqSegm ((RLine (M9,i,(Line (M9,j)))),P,Q))) <> 0. K by A60, A83, A84, RLVECT_1:def 4;
then A91: Det (EqSegm ((RLine (M9,i,(Line (M9,j)))),P,Q)) <> 0. K ;
( Det (EqSegm ((RLine (M9,i,(Line (M9,j)))),P,Q)) = Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q)) or Det (EqSegm ((RLine (M9,i,(Line (M9,j)))),P,Q)) = - (Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q))) ) by A1, A9, A57, A58, A14, A63, A89, Th68;
then A92: Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q)) <> 0. K by A91, VECTSP_2:3;
[:((P \ {i}) \/ {j0}),Q:] c= Indices M9 by A1, A9, A57, A58, A14, A63, A89, Th68;
hence the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) <= the_rank_of M9 by A58, A59, A92, A90, Def4; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
hence the_rank_of M9 = the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j)))))) by A22, XXREAL_0:1; :: thesis: verum
end;
end;