defpred S1[ FinSequence of NAT , Nat, Nat, Matrix of F2(),F3(),F1()] means ( $4 * $2,($1 /. $2) <> 0. F1() & ( $3 in dom $1 & $2 < $3 implies $1 /. $2 < $1 /. $3 ) & ( $3 in (dom $1) \ {$2} implies $4 * $3,($1 /. $2) = 0. F1() ) & ( $3 in Seg (width $4) & $3 < $1 /. $2 implies $4 * $2,$3 = 0. F1() ) );
set r = the_rank_of F5();
ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & ( for i being Nat st i in dom A' & i > the_rank_of F5() holds
Line A',i = F3() |-> (0. F1()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) ) )
proof
per cases ( F2() = 0 or F2() > 0 ) ;
suppose A3: F2() = 0 ; :: thesis: ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & ( for i being Nat st i in dom A' & i > the_rank_of F5() holds
Line A',i = F3() |-> (0. F1()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) ) )
take A' = F5(); :: thesis: ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & ( for i being Nat st i in dom A' & i > the_rank_of F5() holds
Line A',i = F3() |-> (0. F1()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) ) )
take B' = F6(); :: thesis: ( P1[A',B'] & the_rank_of F5() = the_rank_of A' & ( for i being Nat st i in dom A' & i > the_rank_of F5() holds
Line A',i = F3() |-> (0. F1()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) ) )
( dom A' = Seg (len A') & len A' = 0 ) by A3, FINSEQ_1:def 3, MATRIX_1:def 3;
hence ( P1[A',B'] & the_rank_of F5() = the_rank_of A' & ( for i being Nat st i in dom A' & i > the_rank_of F5() holds
Line A',i = F3() |-> (0. F1()) ) ) by A1; :: thesis: ex f being FinSequence of NAT st
( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) )
take f = <*> NAT ; :: thesis: ( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) )
len A' = 0 by A3, MATRIX_1:23;
hence ( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) ) by MATRIX13:74, XBOOLE_1:2; :: thesis: verum
end;
suppose A4: F2() > 0 ; :: thesis: ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & ( for i being Nat st i in dom A' & i > the_rank_of F5() holds
Line A',i = F3() |-> (0. F1()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) ) )
defpred S2[ Nat] means ( $1 <= F3() implies ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= $1 holds
A' * i,j = 0. F1() ) & f is one-to-one & len f <= $1 & len f <= F2() & rng f c= Seg $1 & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) ) ) );
A5: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A6: S2[n] ; :: thesis: S2[n + 1]
set n1 = n + 1;
assume A7: n + 1 <= F3() ; :: thesis: ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n + 1 holds
A' * i,j = 0. F1() ) & f is one-to-one & len f <= n + 1 & len f <= F2() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) ) )
then consider A' being Matrix of F2(),F3(),F1(), B' being Matrix of F2(),F4(),F1() such that
A8: ( P1[A',B'] & the_rank_of F5() = the_rank_of A' ) and
A9: ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F1() ) & f is one-to-one & len f <= n & len f <= F2() & rng f c= Seg n & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) ) by A6, NAT_1:13;
consider f being FinSequence of NAT such that
A10: for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F1() and
A11: f is one-to-one and
A12: len f <= n and
A13: len f <= F2() and
A14: rng f c= Seg n and
A15: for i, j being Nat st i in dom f holds
S1[f,i,j,A'] by A9;
per cases ( for i, j being Nat st [i,j] in Indices A' & i > len f & j = n + 1 holds
A' * i,j = 0. F1() or ex i, j being Nat st
( [i,j] in Indices A' & i > len f & j = n + 1 & A' * i,j <> 0. F1() ) ) ;
suppose A16: for i, j being Nat st [i,j] in Indices A' & i > len f & j = n + 1 holds
A' * i,j = 0. F1() ; :: thesis: ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n + 1 holds
A' * i,j = 0. F1() ) & f is one-to-one & len f <= n + 1 & len f <= F2() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) ) )
A17: now
let i, j be Nat; :: thesis: ( [i,j] in Indices A' & i > len f & j <= n + 1 implies A' * i,j = 0. F1() )
assume that
A18: ( [i,j] in Indices A' & i > len f ) and
A19: j <= n + 1 ; :: thesis: A' * i,j = 0. F1()
( j <= n or j = n + 1 ) by A19, NAT_1:8;
hence A' * i,j = 0. F1() by A10, A16, A18; :: thesis: verum
end;
n <= n + 1 by NAT_1:13;
then Seg n c= Seg (n + 1) by FINSEQ_1:7;
then A20: rng f c= Seg (n + 1) by A14, XBOOLE_1:1;
len f <= n + 1 by A12, NAT_1:12;
hence ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n + 1 holds
A' * i,j = 0. F1() ) & f is one-to-one & len f <= n + 1 & len f <= F2() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) ) ) by A8, A11, A13, A15, A17, A20; :: thesis: verum
end;
suppose ex i, j being Nat st
( [i,j] in Indices A' & i > len f & j = n + 1 & A' * i,j <> 0. F1() ) ; :: thesis: ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n + 1 holds
A' * i,j = 0. F1() ) & f is one-to-one & len f <= n + 1 & len f <= F2() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) ) )
then consider i0, j0 being Nat such that
A21: [i0,j0] in Indices A' and
A22: i0 > len f and
A23: j0 = n + 1 and
A24: A' * i0,j0 <> 0. F1() ;
A25: Indices A' = [:(Seg F2()),(Seg F3()):] by A4, MATRIX_1:24;
then A26: n + 1 in Seg F3() by A21, A23, ZFMISC_1:106;
A27: i0 in Seg F2() by A21, A25, ZFMISC_1:106;
then A28: i0 <= F2() by FINSEQ_1:3;
A29: (len f) + 1 <= i0 by A22, NAT_1:13;
then ( 0 + 1 <= (len f) + 1 & (len f) + 1 <= F2() ) by A28, XREAL_1:9, XXREAL_0:2;
then A30: (len f) + 1 in Seg F2() ;
defpred S3[ Nat] means ( $1 <= F2() implies ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) & ( for j being Nat st j in (dom A') \ {((len f) + 1)} & j <= $1 holds
A' * j,(n + 1) = 0. F1() ) ) );
A31: dom f = Seg (len f) by FINSEQ_1:def 3;
n <= F3() by A7, NAT_1:13;
then A32: Seg n c= Seg F3() by FINSEQ_1:7;
A33: Seg (len f) c= Seg F2() by A13, FINSEQ_1:7;
A34: for k being Nat st S3[k] holds
S3[k + 1]
proof
let k be Nat; :: thesis: ( S3[k] implies S3[k + 1] )
assume A35: S3[k] ; :: thesis: S3[k + 1]
set k1 = k + 1;
assume k + 1 <= F2() ; :: thesis: ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) & ( for j being Nat st j in (dom A') \ {((len f) + 1)} & j <= k + 1 holds
A' * j,(n + 1) = 0. F1() ) )
then consider AA being Matrix of F2(),F3(),F1(), BB being Matrix of F2(),F4(),F1() such that
A36: P1[AA,BB] and
A37: the_rank_of F5() = the_rank_of AA and
A38: AA * ((len f) + 1),(n + 1) <> 0. F1() and
A39: for i, j being Nat st [i,j] in Indices AA & i > len f & j <= n holds
AA * i,j = 0. F1() and
A40: for i, j being Nat st i in dom f holds
S1[f,i,j,AA] and
A41: for j being Nat st j in (dom AA) \ {((len f) + 1)} & j <= k holds
AA * j,(n + 1) = 0. F1() by A35, NAT_1:13;
now
per cases ( k + 1 = (len f) + 1 or k + 1 <> (len f) + 1 ) ;
suppose A42: k + 1 = (len f) + 1 ; :: thesis: ex RA being Matrix of F2(),F3(),F1() ex RB being Matrix of F2(),F4(),F1() ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) & ( for j being Nat st j in (dom A') \ {((len f) + 1)} & j <= k + 1 holds
A' * j,(n + 1) = 0. F1() ) )
take RA = AA; :: thesis: ex RB being Matrix of F2(),F4(),F1() ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) & ( for j being Nat st j in (dom A') \ {((len f) + 1)} & j <= k + 1 holds
A' * j,(n + 1) = 0. F1() ) )
take RB = BB; :: thesis: ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) & ( for j being Nat st j in (dom A') \ {((len f) + 1)} & j <= k + 1 holds
A' * j,(n + 1) = 0. F1() ) )
now
let j be Nat; :: thesis: ( j in (dom RA) \ {((len f) + 1)} & j <= k + 1 implies RA * j,(n + 1) = 0. F1() )
assume that
A43: j in (dom RA) \ {((len f) + 1)} and
A44: j <= k + 1 ; :: thesis: RA * j,(n + 1) = 0. F1()
j <> (len f) + 1 by A43, ZFMISC_1:64;
then j < k + 1 by A42, A44, XXREAL_0:1;
then j <= k by NAT_1:13;
hence RA * j,(n + 1) = 0. F1() by A41, A43; :: thesis: verum
end;
hence ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) & ( for j being Nat st j in (dom A') \ {((len f) + 1)} & j <= k + 1 holds
A' * j,(n + 1) = 0. F1() ) ) by A36, A37, A38, A39, A40; :: thesis: verum
end;
suppose A45: k + 1 <> (len f) + 1 ; :: thesis: ex RA being Matrix of F2(),F3(),the carrier of F1() ex RB being Matrix of F2(),F4(),F1() ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) & ( for j being Nat st j in (dom A') \ {((len f) + 1)} & j <= k + 1 holds
A' * j,(n + 1) = 0. F1() ) )
set LA = Line AA,(k + 1);
set LAf = Line AA,((len f) + 1);
set a = AA * ((len f) + 1),(n + 1);
set RA = RLine AA,(k + 1),((Line AA,(k + 1)) + ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1))));
A46: width AA = F3() by A4, MATRIX_1:24;
then A47: len ((Line AA,(k + 1)) + ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1)))) = F3() by FINSEQ_1:def 18;
A48: Indices A' = Indices AA by MATRIX_1:27;
then [((len f) + 1),(n + 1)] in Indices AA by A25, A30, A26, ZFMISC_1:106;
then A49: (RLine AA,(k + 1),((Line AA,(k + 1)) + ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1))))) * ((len f) + 1),(n + 1) <> 0. F1() by A38, A45, A46, A47, MATRIX11:def 3;
A50: Indices A' = Indices (RLine AA,(k + 1),((Line AA,(k + 1)) + ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1))))) by MATRIX_1:27;
A51: now
let i, j be Nat; :: thesis: ( [i,j] in Indices (RLine AA,(k + 1),((Line AA,(k + 1)) + ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1))))) & i > len f & j <= n implies (RLine AA,(k + 1),((Line AA,(k + 1)) + ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1))))) * i,j = 0. F1() )
assume that
A52: [i,j] in Indices (RLine AA,(k + 1),((Line AA,(k + 1)) + ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1))))) and
A53: i > len f and
A54: j <= n ; :: thesis: (RLine AA,(k + 1),((Line AA,(k + 1)) + ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1))))) * i,j = 0. F1()
now
per cases ( i = k + 1 or i <> k + 1 ) ;
suppose A55: i = k + 1 ; :: thesis: (RLine AA,(k + 1),((Line AA,(k + 1)) + ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1))))) * i,j = 0. F1()
A56: j in Seg F3() by A25, A50, A52, ZFMISC_1:106;
then ( (len f) + 1 > len f & [((len f) + 1),j] in Indices A' ) by A25, A30, NAT_1:13, ZFMISC_1:106;
then AA * ((len f) + 1),j = 0. F1() by A39, A48, A54;
then (Line AA,((len f) + 1)) . j = 0. F1() by A46, A56, MATRIX_1:def 8;
then A57: ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1))) . j = (- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (0. F1()) by A46, A56, FVSUM_1:63
.= 0. F1() by VECTSP_1:36 ;
(Line AA,(k + 1)) . j = AA * (k + 1),j by A46, A56, MATRIX_1:def 8
.= 0. F1() by A39, A48, A50, A52, A53, A54, A55 ;
then (0. F1()) + (0. F1()) = ((Line AA,(k + 1)) + ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1)))) . j by A46, A56, A57, FVSUM_1:22
.= (RLine AA,(k + 1),((Line AA,(k + 1)) + ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1))))) * i,j by A48, A50, A46, A47, A52, A55, MATRIX11:def 3 ;
hence (RLine AA,(k + 1),((Line AA,(k + 1)) + ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1))))) * i,j = 0. F1() by RLVECT_1:def 7; :: thesis: verum
end;
suppose i <> k + 1 ; :: thesis: (RLine AA,(k + 1),((Line AA,(k + 1)) + ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1))))) * i,j = 0. F1()
hence (RLine AA,(k + 1),((Line AA,(k + 1)) + ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1))))) * i,j = AA * i,j by A48, A50, A46, A47, A52, MATRIX11:def 3
.= 0. F1() by A39, A48, A50, A52, A53, A54 ;
:: thesis: verum
end;
end;
end;
hence (RLine AA,(k + 1),((Line AA,(k + 1)) + ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1))))) * i,j = 0. F1() ; :: thesis: verum
end;
set RB = F7(BB,(k + 1),((len f) + 1),(- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))));
take RA = RLine AA,(k + 1),((Line AA,(k + 1)) + ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1)))); :: thesis: ex RB being Matrix of F2(),F4(),F1() ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) & ( for j being Nat st j in (dom A') \ {((len f) + 1)} & j <= k + 1 holds
A' * j,(n + 1) = 0. F1() ) )
take RB = F7(BB,(k + 1),((len f) + 1),(- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " )))); :: thesis: ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) & ( for j being Nat st j in (dom A') \ {((len f) + 1)} & j <= k + 1 holds
A' * j,(n + 1) = 0. F1() ) )
A58: width RA = F3() by A4, MATRIX_1:24;
A59: len AA = F2() by MATRIX_1:def 3;
A60: now
A61: dom AA = Seg (len AA) by FINSEQ_1:def 3;
let j be Nat; :: thesis: ( j in (dom RA) \ {((len f) + 1)} & j <= k + 1 implies RA * j,(n + 1) = 0. F1() )
assume that
A62: j in (dom RA) \ {((len f) + 1)} and
A63: j <= k + 1 ; :: thesis: RA * j,(n + 1) = 0. F1()
j in dom RA by A62, XBOOLE_0:def 5;
then A64: [j,(n + 1)] in Indices AA by A26, A48, A50, A58, ZFMISC_1:106;
A65: ( dom RA = Seg (len RA) & len RA = F2() ) by FINSEQ_1:def 3, MATRIX_1:def 3;
now
per cases ( j <= k or j = k + 1 ) by A63, NAT_1:8;
suppose A66: j <= k ; :: thesis: RA * j,(n + 1) = 0. F1()
then j < k + 1 by NAT_1:13;
hence RA * j,(n + 1) = AA * j,(n + 1) by A46, A47, A64, MATRIX11:def 3
.= 0. F1() by A41, A59, A62, A65, A61, A66 ;
:: thesis: verum
end;
suppose A67: j = k + 1 ; :: thesis: RA * j,(n + 1) = 0. F1()
(Line AA,((len f) + 1)) . (n + 1) = AA * ((len f) + 1),(n + 1) by A26, A46, MATRIX_1:def 8;
then A68: ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1))) . (n + 1) = (- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (AA * ((len f) + 1),(n + 1)) by A26, A46, FVSUM_1:63
.= ((- (AA * (k + 1),(n + 1))) * ((AA * ((len f) + 1),(n + 1)) " )) * (AA * ((len f) + 1),(n + 1)) by VECTSP_1:41
.= (- (AA * (k + 1),(n + 1))) * (((AA * ((len f) + 1),(n + 1)) " ) * (AA * ((len f) + 1),(n + 1))) by GROUP_1:def 4
.= (- (AA * (k + 1),(n + 1))) * (1_ F1()) by A38, VECTSP_1:def 22
.= - (AA * (k + 1),(n + 1)) by VECTSP_1:def 13 ;
(Line AA,(k + 1)) . (n + 1) = AA * (k + 1),(n + 1) by A26, A46, MATRIX_1:def 8;
then ((Line AA,(k + 1)) + ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1)))) . (n + 1) = (AA * (k + 1),(n + 1)) + (- (AA * (k + 1),(n + 1))) by A26, A46, A68, FVSUM_1:22
.= 0. F1() by VECTSP_1:66 ;
hence RA * j,(n + 1) = 0. F1() by A46, A47, A64, A67, MATRIX11:def 3; :: thesis: verum
end;
end;
end;
hence RA * j,(n + 1) = 0. F1() ; :: thesis: verum
end;
A69: dom AA = Seg (len AA) by FINSEQ_1:def 3;
A70: now
let i, j be Nat; :: thesis: ( i in dom f implies ( RA * i,(f /. i) <> 0. F1() & ( j in dom f & i < j implies f /. i < f /. j ) & ( j in (dom f) \ {i} implies RA * j,(f /. i) = 0. F1() ) & ( j in Seg (width RA) & j < f /. i implies RA * i,j = 0. F1() ) ) )
assume A71: i in dom f ; :: thesis: ( RA * i,(f /. i) <> 0. F1() & ( j in dom f & i < j implies f /. i < f /. j ) & ( j in (dom f) \ {i} implies RA * j,(f /. i) = 0. F1() ) & ( j in Seg (width RA) & j < f /. i implies RA * i,j = 0. F1() ) )
set fi = f /. i;
A72: ( f /. i = f . i & f . i in rng f ) by A71, FUNCT_1:def 5, PARTFUN1:def 8;
then A73: f /. i in Seg n by A14;
A74: ( (len f) + 1 > len f & f /. i <= n ) by A14, A72, FINSEQ_1:3, NAT_1:13;
( [((len f) + 1),(f /. i)] in Indices AA & (Line AA,((len f) + 1)) . (f /. i) = AA * ((len f) + 1),(f /. i) ) by A25, A32, A30, A48, A46, A73, MATRIX_1:def 8, ZFMISC_1:106;
then (Line AA,((len f) + 1)) . (f /. i) = 0. F1() by A39, A74;
then A75: ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1))) . (f /. i) = (- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (0. F1()) by A32, A46, A73, FVSUM_1:63
.= 0. F1() by VECTSP_1:44 ;
(Line AA,(k + 1)) . (f /. i) = AA * (k + 1),(f /. i) by A32, A46, A73, MATRIX_1:def 8;
then A76: ((Line AA,(k + 1)) + ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1)))) . (f /. i) = (AA * (k + 1),(f /. i)) + (0. F1()) by A32, A46, A73, A75, FVSUM_1:22
.= AA * (k + 1),(f /. i) by RLVECT_1:def 7 ;
A77: [i,(f /. i)] in Indices AA by A25, A32, A33, A31, A48, A71, A73, ZFMISC_1:106;
now
per cases ( i <> k + 1 or i = k + 1 ) ;
suppose i <> k + 1 ; :: thesis: RA * i,(f /. i) <> 0. F1()
then RA * i,(f /. i) = AA * i,(f /. i) by A46, A47, A77, MATRIX11:def 3;
hence RA * i,(f /. i) <> 0. F1() by A40, A71; :: thesis: verum
end;
suppose i = k + 1 ; :: thesis: RA * i,(f /. i) <> 0. F1()
then RA * i,(f /. i) = AA * i,(f /. i) by A46, A47, A77, A76, MATRIX11:def 3;
hence RA * i,(f /. i) <> 0. F1() by A40, A71; :: thesis: verum
end;
end;
end;
hence ( RA * i,(f /. i) <> 0. F1() & ( j in dom f & i < j implies f /. i < f /. j ) ) by A15, A71; :: thesis: ( ( j in (dom f) \ {i} implies RA * j,(f /. i) = 0. F1() ) & ( j in Seg (width RA) & j < f /. i implies RA * i,j = 0. F1() ) )
thus ( j in (dom f) \ {i} implies RA * j,(f /. i) = 0. F1() ) :: thesis: ( j in Seg (width RA) & j < f /. i implies RA * i,j = 0. F1() )
proof
assume A78: j in (dom f) \ {i} ; :: thesis: RA * j,(f /. i) = 0. F1()
then j in Seg (len f) by A31, XBOOLE_0:def 5;
then A79: [j,(f /. i)] in Indices AA by A25, A32, A33, A48, A73, ZFMISC_1:106;
per cases ( j <> k + 1 or j = k + 1 ) ;
suppose j <> k + 1 ; :: thesis: RA * j,(f /. i) = 0. F1()
hence RA * j,(f /. i) = AA * j,(f /. i) by A46, A47, A79, MATRIX11:def 3
.= 0. F1() by A40, A71, A78 ;
:: thesis: verum
end;
suppose A80: j = k + 1 ; :: thesis: RA * j,(f /. i) = 0. F1()
hence RA * j,(f /. i) = ((Line AA,(k + 1)) + ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1)))) . (f /. i) by A46, A47, A79, MATRIX11:def 3
.= 0. F1() by A40, A71, A76, A78, A80 ;
:: thesis: verum
end;
end;
end;
thus ( j in Seg (width RA) & j < f /. i implies RA * i,j = 0. F1() ) :: thesis: verum
proof
assume that
A81: j in Seg (width RA) and
A82: j < f /. i ; :: thesis: RA * i,j = 0. F1()
A83: [((len f) + 1),j] in Indices AA by A30, A59, A69, A46, A58, A81, ZFMISC_1:106;
A84: [i,j] in Indices AA by A33, A31, A59, A69, A46, A58, A71, A81, ZFMISC_1:106;
per cases ( i <> k + 1 or i = k + 1 ) ;
suppose i <> k + 1 ; :: thesis: RA * i,j = 0. F1()
hence RA * i,j = AA * i,j by A46, A47, A84, MATRIX11:def 3
.= 0. F1() by A40, A46, A58, A71, A81, A82 ;
:: thesis: verum
end;
suppose A85: i = k + 1 ; :: thesis: RA * i,j = 0. F1()
f /. i <= n by A14, A72, FINSEQ_1:3;
then A86: j <= n by A82, XXREAL_0:2;
(len f) + 1 > len f by NAT_1:13;
then 0. F1() = AA * ((len f) + 1),j by A39, A83, A86
.= (Line AA,((len f) + 1)) . j by A46, A58, A81, MATRIX_1:def 8 ;
then A87: ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1))) . j = (- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (0. F1()) by A46, A58, A81, FVSUM_1:63
.= 0. F1() by VECTSP_1:36 ;
(Line AA,(k + 1)) . j = AA * i,j by A46, A58, A81, A85, MATRIX_1:def 8
.= 0. F1() by A40, A46, A58, A71, A81, A82 ;
then ((Line AA,(k + 1)) + ((- ((AA * (k + 1),(n + 1)) * ((AA * ((len f) + 1),(n + 1)) " ))) * (Line AA,((len f) + 1)))) . j = (0. F1()) + (0. F1()) by A46, A58, A81, A87, FVSUM_1:22
.= 0. F1() by RLVECT_1:def 7 ;
hence RA * i,j = 0. F1() by A46, A47, A84, A85, MATRIX11:def 3; :: thesis: verum
end;
end;
end;
end;
A88: (len f) + 1 in Seg (len AA) by A4, A30, MATRIX_1:24;
then A89: the_rank_of F5() = the_rank_of RA by A37, A45, MATRIX13:92;
P1[RA,RB] by A2, A36, A45, A88, A69;
hence ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) & ( for j being Nat st j in (dom A') \ {((len f) + 1)} & j <= k + 1 holds
A' * j,(n + 1) = 0. F1() ) ) by A89, A49, A51, A70, A60; :: thesis: verum
end;
end;
end;
hence ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) & ( for j being Nat st j in (dom A') \ {((len f) + 1)} & j <= k + 1 holds
A' * j,(n + 1) = 0. F1() ) ) ; :: thesis: verum
end;
A90: j0 in Seg F3() by A21, A25, ZFMISC_1:106;
ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) )
proof
per cases ( A' * ((len f) + 1),(n + 1) <> 0. F1() or A' * ((len f) + 1),(n + 1) = 0. F1() ) ;
suppose A' * ((len f) + 1),(n + 1) <> 0. F1() ; :: thesis: ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) )
hence ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) ) by A8, A10, A15; :: thesis: verum
end;
suppose A91: A' * ((len f) + 1),(n + 1) = 0. F1() ; :: thesis: ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) )
set RB = F7(B',((len f) + 1),i0,(1_ F1()));
set LA = Line A',i0;
set LAf = Line A',((len f) + 1);
set RA = RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)));
take RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0))) ; :: thesis: ex B' being Matrix of F2(),F4(),F1() st
( P1[ RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0))),B'] & the_rank_of F5() = the_rank_of (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) & (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * ((len f) + 1),(n + 1) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) & i > len f & j <= n holds
(RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * i,j = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j, RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))] ) )
take F7(B',((len f) + 1),i0,(1_ F1())) ; :: thesis: ( P1[ RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0))),F7(B',((len f) + 1),i0,(1_ F1()))] & the_rank_of F5() = the_rank_of (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) & (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * ((len f) + 1),(n + 1) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) & i > len f & j <= n holds
(RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * i,j = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j, RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))] ) )
( i0 in dom A' & dom A' = Seg (len A') ) by A21, FINSEQ_1:def 3, ZFMISC_1:106;
hence ( P1[ RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0))),F7(B',((len f) + 1),i0,(1_ F1()))] & the_rank_of F5() = the_rank_of (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) ) by A2, A8, A23, A24, A91, MATRIX13:92; :: thesis: ( (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * ((len f) + 1),(n + 1) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) & i > len f & j <= n holds
(RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * i,j = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j, RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))] ) )
A92: ( (1_ F1()) * (Line A',i0) = Line A',i0 & len ((Line A',((len f) + 1)) + (Line A',i0)) = width A' ) by FINSEQ_1:def 18, FVSUM_1:70;
[((len f) + 1),j0] in Indices A' by A25, A30, A90, ZFMISC_1:106;
then A93: (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * ((len f) + 1),(n + 1) = ((Line A',((len f) + 1)) + (Line A',i0)) . (n + 1) by A23, A92, MATRIX11:def 3;
A94: width A' = F3() by A4, MATRIX_1:24;
then A95: (Line A',i0) . (n + 1) = A' * i0,(n + 1) by A23, A90, MATRIX_1:def 8;
(Line A',((len f) + 1)) . (n + 1) = 0. F1() by A23, A90, A91, A94, MATRIX_1:def 8;
then (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * ((len f) + 1),(n + 1) = (0. F1()) + (A' * i0,(n + 1)) by A26, A94, A93, A95, FVSUM_1:22
.= A' * i0,(n + 1) by RLVECT_1:def 7 ;
hence (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * ((len f) + 1),(n + 1) <> 0. F1() by A23, A24; :: thesis: ( ( for i, j being Nat st [i,j] in Indices (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) & i > len f & j <= n holds
(RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * i,j = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j, RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))] ) )
A96: Indices (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) = Indices A' by MATRIX_1:27;
now
let i, j be Nat; :: thesis: ( [i,j] in Indices (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) & i > len f & j <= n implies (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * i,j = 0. F1() )
assume that
A97: [i,j] in Indices (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) and
A98: i > len f and
A99: j <= n ; :: thesis: (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * i,j = 0. F1()
A100: j in Seg F3() by A94, A96, A97, ZFMISC_1:106;
A101: i >= (len f) + 1 by A98, NAT_1:13;
now
per cases ( i > (len f) + 1 or i = (len f) + 1 ) by A101, XXREAL_0:1;
suppose i > (len f) + 1 ; :: thesis: (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * i,j = 0. F1()
hence (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * i,j = A' * i,j by A92, A96, A97, MATRIX11:def 3
.= 0. F1() by A10, A96, A97, A98, A99 ;
:: thesis: verum
end;
suppose A102: i = (len f) + 1 ; :: thesis: (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * i,j = 0. F1()
A103: [i0,j] in Indices A' by A25, A27, A100, ZFMISC_1:106;
A104: ( (Line A',((len f) + 1)) . j = A' * ((len f) + 1),j & (Line A',i0) . j = A' * i0,j ) by A94, A100, MATRIX_1:def 8;
(RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * i,j = ((Line A',((len f) + 1)) + (Line A',i0)) . j by A92, A96, A97, A102, MATRIX11:def 3;
hence (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * i,j = (A' * ((len f) + 1),j) + (A' * i0,j) by A94, A100, A104, FVSUM_1:22
.= (0. F1()) + (A' * i0,j) by A10, A96, A97, A98, A99, A102
.= (0. F1()) + (0. F1()) by A10, A22, A99, A103
.= 0. F1() by RLVECT_1:def 7 ;
:: thesis: verum
end;
end;
end;
hence (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * i,j = 0. F1() ; :: thesis: verum
end;
hence for i, j being Nat st [i,j] in Indices (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) & i > len f & j <= n holds
(RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * i,j = 0. F1() ; :: thesis: for i, j being Nat st i in dom f holds
S1[f,i,j, RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))]
let i, j be Nat; :: thesis: ( i in dom f implies S1[f,i,j, RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))] )
assume A105: i in dom f ; :: thesis: S1[f,i,j, RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))]
i <= len f by A31, A105, FINSEQ_1:3;
then A106: i < (len f) + 1 by NAT_1:13;
( f /. i = f . i & f . i in rng f ) by A105, FUNCT_1:def 5, PARTFUN1:def 8;
then A107: f /. i in Seg n by A14;
then [i,(f /. i)] in Indices A' by A25, A32, A33, A31, A105, ZFMISC_1:106;
then (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * i,(f /. i) = A' * i,(f /. i) by A92, A106, MATRIX11:def 3;
hence ( (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * i,(f /. i) <> 0. F1() & ( j in dom f & i < j implies f /. i < f /. j ) ) by A15, A105; :: thesis: ( ( j in (dom f) \ {i} implies (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * j,(f /. i) = 0. F1() ) & ( j in Seg (width (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0))))) & j < f /. i implies (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * i,j = 0. F1() ) )
thus ( j in (dom f) \ {i} implies (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * j,(f /. i) = 0. F1() ) :: thesis: ( j in Seg (width (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0))))) & j < f /. i implies (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * i,j = 0. F1() )
proof
assume A108: j in (dom f) \ {i} ; :: thesis: (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * j,(f /. i) = 0. F1()
then A109: j in dom f by XBOOLE_0:def 5;
then j <= len f by A31, FINSEQ_1:3;
then A110: j < (len f) + 1 by NAT_1:13;
[j,(f /. i)] in Indices A' by A25, A32, A33, A31, A107, A109, ZFMISC_1:106;
hence (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * j,(f /. i) = A' * j,(f /. i) by A92, A110, MATRIX11:def 3
.= 0. F1() by A15, A105, A108 ;
:: thesis: verum
end;
assume that
A111: j in Seg (width (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0))))) and
A112: j < f /. i ; :: thesis: (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * i,j = 0. F1()
A113: width (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) = width A' by A92, MATRIX11:def 3;
then [i,j] in Indices A' by A25, A33, A31, A94, A105, A111, ZFMISC_1:106;
hence (RLine A',((len f) + 1),((Line A',((len f) + 1)) + ((1_ F1()) * (Line A',i0)))) * i,j = A' * i,j by A92, A106, MATRIX11:def 3
.= 0. F1() by A15, A105, A111, A112, A113 ;
:: thesis: verum
end;
end;
end;
then consider A0 being Matrix of F2(),F3(),F1(), B0 being Matrix of F2(),F4(),F1() such that
A114: ( P1[A0,B0] & the_rank_of F5() = the_rank_of A0 & A0 * ((len f) + 1),(n + 1) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A0 & i > len f & j <= n holds
A0 * i,j = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A0] ) ) ;
A115: S3[ 0 ]
proof
assume 0 <= F2() ; :: thesis: ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & A' * ((len f) + 1),(n + 1) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= n holds
A' * i,j = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) & ( for j being Nat st j in (dom A') \ {((len f) + 1)} & j <= 0 holds
A' * j,(n + 1) = 0. F1() ) )
take A0 ; :: thesis: ex B' being Matrix of F2(),F4(),F1() st
( P1[A0,B'] & the_rank_of F5() = the_rank_of A0 & A0 * ((len f) + 1),(n + 1) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A0 & i > len f & j <= n holds
A0 * i,j = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A0] ) & ( for j being Nat st j in (dom A0) \ {((len f) + 1)} & j <= 0 holds
A0 * j,(n + 1) = 0. F1() ) )
take B0 ; :: thesis: ( P1[A0,B0] & the_rank_of F5() = the_rank_of A0 & A0 * ((len f) + 1),(n + 1) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A0 & i > len f & j <= n holds
A0 * i,j = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A0] ) & ( for j being Nat st j in (dom A0) \ {((len f) + 1)} & j <= 0 holds
A0 * j,(n + 1) = 0. F1() ) )
now
A116: dom A0 = Seg (len A0) by FINSEQ_1:def 3;
let j be Nat; :: thesis: ( j in (dom A0) \ {((len f) + 1)} & j <= 0 implies A0 * j,(n + 1) = 0. F1() )
assume ( j in (dom A0) \ {((len f) + 1)} & j <= 0 ) ; :: thesis: A0 * j,(n + 1) = 0. F1()
hence A0 * j,(n + 1) = 0. F1() by A116; :: thesis: verum
end;
hence ( P1[A0,B0] & the_rank_of F5() = the_rank_of A0 & A0 * ((len f) + 1),(n + 1) <> 0. F1() & ( for i, j being Nat st [i,j] in Indices A0 & i > len f & j <= n holds
A0 * i,j = 0. F1() ) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A0] ) & ( for j being Nat st j in (dom A0) \ {((len f) + 1)} & j <= 0 holds
A0 * j,(n + 1) = 0. F1() ) ) by A114; :: thesis: verum
end;
for k being Nat holds S3[k] from NAT_1:sch 2(A115, A34);
then consider Aa being Matrix of F2(),F3(),F1(), Bb being Matrix of F2(),F4(),F1() such that
A117: ( P1[Aa,Bb] & the_rank_of F5() = the_rank_of Aa ) and
A118: Aa * ((len f) + 1),(n + 1) <> 0. F1() and
A119: for i, j being Nat st [i,j] in Indices Aa & i > len f & j <= n holds
Aa * i,j = 0. F1() and
A120: for i, j being Nat st i in dom f holds
S1[f,i,j,Aa] and
A121: for j being Nat st j in (dom Aa) \ {((len f) + 1)} & j <= F2() holds
Aa * j,(n + 1) = 0. F1() ;
take Aa ; :: thesis: ex B' being Matrix of F2(),F4(),F1() st
( P1[Aa,B'] & the_rank_of F5() = the_rank_of Aa & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices Aa & i > len f & j <= n + 1 holds
Aa * i,j = 0. F1() ) & f is one-to-one & len f <= n + 1 & len f <= F2() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,Aa] ) ) )
take Bb ; :: thesis: ( P1[Aa,Bb] & the_rank_of F5() = the_rank_of Aa & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices Aa & i > len f & j <= n + 1 holds
Aa * i,j = 0. F1() ) & f is one-to-one & len f <= n + 1 & len f <= F2() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,Aa] ) ) )
thus ( P1[Aa,Bb] & the_rank_of F5() = the_rank_of Aa ) by A117; :: thesis: ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices Aa & i > len f & j <= n + 1 holds
Aa * i,j = 0. F1() ) & f is one-to-one & len f <= n + 1 & len f <= F2() & rng f c= Seg (n + 1) & ( for i, j being Nat st i in dom f holds
S1[f,i,j,Aa] ) )
take f' = f ^ <*(n + 1)*>; :: thesis: ( ( for i, j being Nat st [i,j] in Indices Aa & i > len f' & j <= n + 1 holds
Aa * i,j = 0. F1() ) & f' is one-to-one & len f' <= n + 1 & len f' <= F2() & rng f' c= Seg (n + 1) & ( for i, j being Nat st i in dom f' holds
S1[f',i,j,Aa] ) )
A122: len f' = (len f) + 1 by FINSEQ_2:19;
A123: ( len Aa = F2() & dom Aa = Seg (len Aa) ) by A4, FINSEQ_1:def 3, MATRIX_1:24;
A124: now
let i, j be Nat; :: thesis: ( [i,j] in Indices Aa & i > len f' & j <= n + 1 implies Aa * b1,b2 = 0. F1() )
assume that
A125: [i,j] in Indices Aa and
A126: i > len f' and
A127: j <= n + 1 ; :: thesis: Aa * b1,b2 = 0. F1()
per cases ( j <= n or j = n + 1 ) by A127, NAT_1:8;
suppose A128: j <= n ; :: thesis: Aa * b1,b2 = 0. F1()
i > len f by A122, A126, NAT_1:13;
hence Aa * i,j = 0. F1() by A119, A125, A128; :: thesis: verum
end;
suppose A129: j = n + 1 ; :: thesis: Aa * b1,b2 = 0. F1()
i in dom Aa by A125, ZFMISC_1:106;
then ( i in (dom Aa) \ {((len f) + 1)} & i <= F2() ) by A122, A123, A126, FINSEQ_1:3, ZFMISC_1:64;
hence Aa * i,j = 0. F1() by A121, A129; :: thesis: verum
end;
end;
end;
A130: width Aa = F3() by A4, MATRIX_1:24;
A131: len f' <= F2() by A28, A29, A122, XXREAL_0:2;
A132: now
let i, j be Nat; :: thesis: ( i in dom f' implies ( Aa * i,(f' /. i) <> 0. F1() & ( j in dom f' & i < j implies f' /. i < f' /. j ) & ( j in (dom f') \ {i} implies Aa * j,(f' /. i) = 0. F1() ) & ( j in Seg (width Aa) & j < f' /. i implies Aa * i,j = 0. F1() ) ) )
assume A133: i in dom f' ; :: thesis: ( Aa * i,(f' /. i) <> 0. F1() & ( j in dom f' & i < j implies f' /. i < f' /. j ) & ( j in (dom f') \ {i} implies Aa * j,(f' /. i) = 0. F1() ) & ( j in Seg (width Aa) & j < f' /. i implies Aa * i,j = 0. F1() ) )
A134: dom f' = Seg ((len f) + 1) by A122, FINSEQ_1:def 3
.= (dom f) \/ {((len f) + 1)} by A31, FINSEQ_1:11 ;
A135: now
let k be Nat; :: thesis: ( k in dom f implies f /. k = f' /. k )
assume A136: k in dom f ; :: thesis: f /. k = f' /. k
A137: k in dom f' by A134, A136, XBOOLE_0:def 3;
thus f /. k = f . k by A136, PARTFUN1:def 8
.= f' . k by A136, FINSEQ_1:def 7
.= f' /. k by A137, PARTFUN1:def 8 ; :: thesis: verum
end;
now
per cases ( i in dom f or i in {((len f) + 1)} ) by A133, A134, XBOOLE_0:def 3;
suppose A138: i in dom f ; :: thesis: Aa * i,(f' /. i) <> 0. F1()
then f /. i = f' /. i by A135;
hence Aa * i,(f' /. i) <> 0. F1() by A120, A138; :: thesis: verum
end;
suppose A139: i in {((len f) + 1)} ; :: thesis: Aa * i,(f' /. i) <> 0. F1()
A140: f' /. i = f' . i by A133, PARTFUN1:def 8;
i = (len f) + 1 by A139, TARSKI:def 1;
hence Aa * i,(f' /. i) <> 0. F1() by A118, A140, FINSEQ_1:59; :: thesis: verum
end;
end;
end;
hence Aa * i,(f' /. i) <> 0. F1() ; :: thesis: ( ( j in dom f' & i < j implies f' /. i < f' /. j ) & ( j in (dom f') \ {i} implies Aa * j,(f' /. i) = 0. F1() ) & ( j in Seg (width Aa) & j < f' /. i implies Aa * i,j = 0. F1() ) )
thus ( j in dom f' & i < j implies f' /. i < f' /. j ) :: thesis: ( ( j in (dom f') \ {i} implies Aa * j,(f' /. i) = 0. F1() ) & ( j in Seg (width Aa) & j < f' /. i implies Aa * i,j = 0. F1() ) )
proof
assume that
A141: j in dom f' and
A142: i < j ; :: thesis: f' /. i < f' /. j
per cases ( ( j in {((len f) + 1)} & i in {((len f) + 1)} ) or ( j in {((len f) + 1)} & i in dom f ) or ( j in dom f & i in {((len f) + 1)} ) or ( j in dom f & i in dom f ) ) by A133, A134, A141, XBOOLE_0:def 3;
suppose A143: ( j in {((len f) + 1)} & i in {((len f) + 1)} ) ; :: thesis: f' /. i < f' /. j
then i = (len f) + 1 by TARSKI:def 1;
hence f' /. i < f' /. j by A142, A143, TARSKI:def 1; :: thesis: verum
end;
suppose ( j in dom f & i in {((len f) + 1)} ) ; :: thesis: f' /. i < f' /. j
then ( j <= len f & i = (len f) + 1 ) by A31, FINSEQ_1:3, TARSKI:def 1;
hence f' /. i < f' /. j by A142, NAT_1:13; :: thesis: verum
end;
suppose A147: ( j in dom f & i in dom f ) ; :: thesis: f' /. i < f' /. j
then ( f /. i = f' /. i & f /. j = f' /. j ) by A135;
hence f' /. i < f' /. j by A15, A142, A147; :: thesis: verum
end;
end;
end;
dom f' = Seg (len f') by FINSEQ_1:def 3;
then A148: dom f' c= dom Aa by A123, A131, FINSEQ_1:7;
thus ( j in (dom f') \ {i} implies Aa * j,(f' /. i) = 0. F1() ) :: thesis: ( j in Seg (width Aa) & j < f' /. i implies Aa * i,j = 0. F1() )
proof
assume A149: j in (dom f') \ {i} ; :: thesis: Aa * j,(f' /. i) = 0. F1()
per cases ( i = (len f) + 1 or i <> (len f) + 1 ) ;
suppose A150: i = (len f) + 1 ; :: thesis: Aa * j,(f' /. i) = 0. F1()
(len f) + 1 in {((len f) + 1)} by TARSKI:def 1;
then (len f) + 1 in dom f' by A134, XBOOLE_0:def 3;
then A151: f' . ((len f) + 1) = f' /. i by A150, PARTFUN1:def 8;
A152: j in dom f' by A149, ZFMISC_1:64;
j <> i by A149, ZFMISC_1:64;
then A153: j in (dom Aa) \ {i} by A148, A152, ZFMISC_1:64;
j <= F2() by A123, A148, A152, FINSEQ_1:3;
then Aa * j,(n + 1) = 0. F1() by A121, A150, A153;
hence Aa * j,(f' /. i) = 0. F1() by A151, FINSEQ_1:59; :: thesis: verum
end;
suppose A154: i <> (len f) + 1 ; :: thesis: Aa * j,(f' /. i) = 0. F1()
A155: j in dom f' by A149, XBOOLE_0:def 5;
A156: ( i in dom f or i in {((len f) + 1)} ) by A133, A134, XBOOLE_0:def 3;
then A157: f . i in rng f by A154, FUNCT_1:def 5, TARSKI:def 1;
A158: ( f /. i = f' /. i & f . i = f /. i ) by A135, A154, A156, PARTFUN1:def 8, TARSKI:def 1;
then A159: 1 <= f' /. i by A14, A157, FINSEQ_1:3;
A160: f' /. i <= n by A14, A158, A157, FINSEQ_1:3;
n <= F3() by A7, NAT_1:13;
then f' /. i <= F3() by A160, XXREAL_0:2;
then f' /. i in Seg (width Aa) by A130, A159;
then A161: [j,(f' /. i)] in Indices Aa by A148, A155, ZFMISC_1:106;
per cases ( j = (len f) + 1 or j <> (len f) + 1 ) ;
suppose j = (len f) + 1 ; :: thesis: Aa * j,(f' /. i) = 0. F1()
then j > len f by NAT_1:13;
hence Aa * j,(f' /. i) = 0. F1() by A119, A160, A161; :: thesis: verum
end;
end;
end;
end;
end;
thus ( j in Seg (width Aa) & j < f' /. i implies Aa * i,j = 0. F1() ) :: thesis: verum
proof
assume that
A164: j in Seg (width Aa) and
A165: j < f' /. i ; :: thesis: Aa * i,j = 0. F1()
end;
end;
A172: ( rng <*(n + 1)*> = {(n + 1)} & (rng f) \/ {(n + 1)} c= (Seg n) \/ {(n + 1)} ) by A14, FINSEQ_1:55, XBOOLE_1:9;
A173: (Seg n) \/ {(n + 1)} = Seg (n + 1) by FINSEQ_1:11;
( rng f misses {(n + 1)} & <*(n + 1)*> is one-to-one ) by A14, FINSEQ_3:15, FINSEQ_3:102, XBOOLE_1:63;
hence ( ( for i, j being Nat st [i,j] in Indices Aa & i > len f' & j <= n + 1 holds
Aa * i,j = 0. F1() ) & f' is one-to-one & len f' <= n + 1 & len f' <= F2() & rng f' c= Seg (n + 1) & ( for i, j being Nat st i in dom f' holds
S1[f',i,j,Aa] ) ) by A11, A12, A28, A29, A122, A124, A172, A173, A132, FINSEQ_1:44, FINSEQ_3:98, XREAL_1:8, XXREAL_0:2; :: thesis: verum
end;
end;
end;
A174: S2[ 0 ]
proof
assume 0 <= F3() ; :: thesis: ex A' being Matrix of F2(),F3(),F1() ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= 0 holds
A' * i,j = 0. F1() ) & f is one-to-one & len f <= 0 & len f <= F2() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) ) )
take A' = F5(); :: thesis: ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= 0 holds
A' * i,j = 0. F1() ) & f is one-to-one & len f <= 0 & len f <= F2() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) ) )
take B' = F6(); :: thesis: ( P1[A',B'] & the_rank_of F5() = the_rank_of A' & ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= 0 holds
A' * i,j = 0. F1() ) & f is one-to-one & len f <= 0 & len f <= F2() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) ) )
thus ( P1[A',B'] & the_rank_of F5() = the_rank_of A' ) by A1; :: thesis: ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= 0 holds
A' * i,j = 0. F1() ) & f is one-to-one & len f <= 0 & len f <= F2() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) )
take f = <*> NAT ; :: thesis: ( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= 0 holds
A' * i,j = 0. F1() ) & f is one-to-one & len f <= 0 & len f <= F2() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) )
now
let i, j be Nat; :: thesis: ( [i,j] in Indices A' & i > len f & j <= 0 implies A' * i,j = 0. F1() )
assume that
A175: [i,j] in Indices A' and
i > len f and
A176: j <= 0 ; :: thesis: A' * i,j = 0. F1()
j in Seg (width A') by A175, ZFMISC_1:106;
hence A' * i,j = 0. F1() by A176; :: thesis: verum
end;
hence ( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= 0 holds
A' * i,j = 0. F1() ) & f is one-to-one & len f <= 0 & len f <= F2() & rng f c= Seg 0 & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) ) ; :: thesis: verum
end;
for n being Nat holds S2[n] from NAT_1:sch 2(A174, A5);
then consider A' being Matrix of F2(),F3(),F1(), B' being Matrix of F2(),F4(),F1() such that
A177: P1[A',B'] and
A178: the_rank_of F5() = the_rank_of A' and
A179: ex f being FinSequence of NAT st
( ( for i, j being Nat st [i,j] in Indices A' & i > len f & j <= F3() holds
A' * i,j = 0. F1() ) & f is one-to-one & len f <= F3() & len f <= F2() & rng f c= Seg F3() & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) ) ;
consider f being FinSequence of NAT such that
A180: for i, j being Nat st [i,j] in Indices A' & i > len f & j <= F3() holds
A' * i,j = 0. F1() and
A181: f is one-to-one and
len f <= F3() and
A182: len f <= F2() and
A183: rng f c= Seg F3() and
A184: for i, j being Nat st i in dom f holds
S1[f,i,j,A'] by A179;
A185: len A' = F2() by A4, MATRIX_1:24;
take A' ; :: thesis: ex B' being Matrix of F2(),F4(),F1() st
( P1[A',B'] & the_rank_of F5() = the_rank_of A' & ( for i being Nat st i in dom A' & i > the_rank_of F5() holds
Line A',i = F3() |-> (0. F1()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) ) )
take B' ; :: thesis: ( P1[A',B'] & the_rank_of F5() = the_rank_of A' & ( for i being Nat st i in dom A' & i > the_rank_of F5() holds
Line A',i = F3() |-> (0. F1()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) ) )
thus ( P1[A',B'] & the_rank_of F5() = the_rank_of A' ) by A177, A178; :: thesis: ( ( for i being Nat st i in dom A' & i > the_rank_of F5() holds
Line A',i = F3() |-> (0. F1()) ) & ex f being FinSequence of NAT st
( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) ) )
A186: dom A' = Seg (len A') by FINSEQ_1:def 3;
set L = len f;
A187: Seg (len f) c= Seg F2() by A182, FINSEQ_1:7;
( idseq (len f) is FinSequence of NAT & len (idseq (len f)) = len f ) by FINSEQ_1:def 18, FINSEQ_2:52;
then reconsider idL = idseq (len f), F' = f as Element of (len f) -tuples_on NAT by FINSEQ_2:110;
set S = Segm A',idL,F';
A188: dom f = Seg (len f) by FINSEQ_1:def 3;
set D = diagonal_of_Matrix (Segm A',idL,F');
A189: Indices (Segm A',idL,F') = [:(Seg (len f)),(Seg (len f)):] by MATRIX_1:25;
for k being Element of NAT st k in dom (diagonal_of_Matrix (Segm A',idL,F')) holds
(diagonal_of_Matrix (Segm A',idL,F')) . k <> 0. F1()
proof
A190: len (diagonal_of_Matrix (Segm A',idL,F')) = len f by MATRIX_3:def 10;
let k be Element of NAT ; :: thesis: ( k in dom (diagonal_of_Matrix (Segm A',idL,F')) implies (diagonal_of_Matrix (Segm A',idL,F')) . k <> 0. F1() )
assume k in dom (diagonal_of_Matrix (Segm A',idL,F')) ; :: thesis: (diagonal_of_Matrix (Segm A',idL,F')) . k <> 0. F1()
then A191: k in Seg (len f) by A190, FINSEQ_1:def 3;
then [k,k] in Indices (Segm A',idL,F') by A189, ZFMISC_1:106;
then (Segm A',idL,F') * k,k = A' * (idL . k),(f . k) by MATRIX13:def 1
.= A' * k,(f . k) by A191, FINSEQ_2:57
.= A' * k,(f /. k) by A188, A191, PARTFUN1:def 8 ;
then (Segm A',idL,F') * k,k <> 0. F1() by A184, A188, A191;
hence (diagonal_of_Matrix (Segm A',idL,F')) . k <> 0. F1() by A191, MATRIX_3:def 10; :: thesis: verum
end;
then A192: Product (diagonal_of_Matrix (Segm A',idL,F')) <> 0. F1() by FVSUM_1:107;
now
let i, j be Nat; :: thesis: ( [i,j] in Indices (Segm A',idL,F') & i > j implies (Segm A',idL,F') * i,j = 0. F1() )
assume A193: [i,j] in Indices (Segm A',idL,F') ; :: thesis: ( i > j implies (Segm A',idL,F') * i,j = 0. F1() )
A194: i in Seg (len f) by A189, A193, ZFMISC_1:106;
assume i > j ; :: thesis: (Segm A',idL,F') * i,j = 0. F1()
then A195: i in (dom f) \ {j} by A188, A194, ZFMISC_1:64;
reconsider i' = i, j' = j as Element of NAT by ORDINAL1:def 13;
A196: j in Seg (len f) by A189, A193, ZFMISC_1:106;
thus (Segm A',idL,F') * i,j = A' * (idL . i'),(f . j') by A193, MATRIX13:def 1
.= A' * i,(f . j) by A194, FINSEQ_2:57
.= A' * i,(f /. j) by A188, A196, PARTFUN1:def 8
.= 0. F1() by A184, A188, A196, A195 ; :: thesis: verum
end;
then Segm A',idL,F' is Upper_Triangular_Matrix of len f,F1() by MATRIX_2:def 3;
then A197: Det (Segm A',idL,F') <> 0. F1() by A192, MATRIX13:7;
A198: len (Segm A',(Seg (len f)),(Seg (width A'))) = card (Seg (len f)) by MATRIX_1:def 3;
A199: width A' = F3() by A4, MATRIX_1:24;
rng idL = Seg (len f) by RELAT_1:71;
then [:(rng idL),(rng F'):] c= Indices A' by A183, A187, A185, A186, A199, ZFMISC_1:119;
then A200: the_rank_of A' >= len f by A197, MATRIX13:76;
A201: now
set w0 = (width A') |-> (0. F1());
let i be Nat; :: thesis: ( i in (dom A') \ (Seg (len f)) implies Line A',i = (width A') |-> (0. F1()) )
assume A202: i in (dom A') \ (Seg (len f)) ; :: thesis: Line A',i = (width A') |-> (0. F1())
set LA = Line A',i;
A203: now
not i in Seg (len f) by A202, XBOOLE_0:def 5;
then A204: ( i > len f or i < 1 ) by A202;
let j be Nat; :: thesis: ( 1 <= j & j <= width A' implies (Line A',i) . j = ((width A') |-> (0. F1())) . j )
assume that
A205: 1 <= j and
A206: j <= width A' ; :: thesis: (Line A',i) . j = ((width A') |-> (0. F1())) . j
j in NAT by ORDINAL1:def 13;
then A207: j in Seg (width A') by A205, A206;
A208: i in dom A' by A202, XBOOLE_0:def 5;
then A209: [i,j] in Indices A' by A207, ZFMISC_1:106;
thus (Line A',i) . j = A' * i,j by A207, MATRIX_1:def 8
.= 0. F1() by A180, A186, A199, A206, A208, A209, A204, FINSEQ_1:3
.= ((width A') |-> (0. F1())) . j by A207, FINSEQ_2:71 ; :: thesis: verum
end;
( len (Line A',i) = width A' & len ((width A') |-> (0. F1())) = width A' ) by FINSEQ_1:def 18;
hence Line A',i = (width A') |-> (0. F1()) by A203, FINSEQ_1:18; :: thesis: verum
end;
then the_rank_of A' = the_rank_of (Segm A',(Seg (len f)),(Seg (width A'))) by A187, A185, A186, Th11;
then the_rank_of A' <= card (Seg (len f)) by A198, MATRIX13:74;
then A210: the_rank_of A' <= len f by FINSEQ_1:78;
then A211: the_rank_of F5() = len f by A178, A200, XXREAL_0:1;
thus for i being Nat st i in dom A' & i > the_rank_of F5() holds
Line A',i = F3() |-> (0. F1()) :: thesis: ex f being FinSequence of NAT st
( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) )
proof
let i be Nat; :: thesis: ( i in dom A' & i > the_rank_of F5() implies Line A',i = F3() |-> (0. F1()) )
assume that
A212: i in dom A' and
A213: i > the_rank_of F5() ; :: thesis: Line A',i = F3() |-> (0. F1())
not i in Seg (len f) by A211, A213, FINSEQ_1:3;
then i in (dom A') \ (Seg (len f)) by A212, XBOOLE_0:def 5;
hence Line A',i = F3() |-> (0. F1()) by A199, A201; :: thesis: verum
end;
take f ; :: thesis: ( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) )
thus ( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) ) by A4, A181, A183, A184, A200, A210, MATRIX_1:24, XXREAL_0:1; :: thesis: verum
end;
end;
end;
then consider A' being Matrix of F2(),F3(),F1(), B' being Matrix of F2(),F4(),F1() such that
A214: P1[A',B'] and
A215: the_rank_of F5() = the_rank_of A' and
A216: for i being Nat st i in dom A' & i > the_rank_of F5() holds
Line A',i = F3() |-> (0. F1()) and
A217: ex f being FinSequence of NAT st
( len f = the_rank_of A' & f is one-to-one & rng f c= Seg (width A') & ( for i, j being Nat st i in dom f holds
S1[f,i,j,A'] ) ) ;
consider f being FinSequence of NAT such that
A218: len f = the_rank_of A' and
A219: f is one-to-one and
A220: rng f c= Seg (width A') and
A221: for i, j being Nat st i in dom f holds
S1[f,i,j,A'] by A217;
not 0 in rng f by A220;
then reconsider rngf = rng f as finite without_zero Subset of NAT by A220, PSCOMP_1:def 1, XBOOLE_1:1;
A222: ( F2() = 0 or F2() > 0 ) ;
set S = Segm A',(Seg (card rngf)),rngf;
A223: dom f = Seg (the_rank_of F5()) by A215, A218, FINSEQ_1:def 3;
take A' ; :: thesis: ex B' being Matrix of F2(),F4(),F1() ex N being finite without_zero Subset of NAT st
( N c= Seg F3() & the_rank_of F5() = the_rank_of A' & the_rank_of F5() = card N & P1[A',B'] & Segm A',(Seg (card N)),N is diagonal & ( for i being Nat st i in Seg (card N) holds
A' * i,((Sgm N) /. i) <> 0. F1() ) & ( for i being Nat st i in dom A' & i > card N holds
Line A',i = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width A') & j < (Sgm N) . i holds
A' * i,j = 0. F1() ) )
take B' ; :: thesis: ex N being finite without_zero Subset of NAT st
( N c= Seg F3() & the_rank_of F5() = the_rank_of A' & the_rank_of F5() = card N & P1[A',B'] & Segm A',(Seg (card N)),N is diagonal & ( for i being Nat st i in Seg (card N) holds
A' * i,((Sgm N) /. i) <> 0. F1() ) & ( for i being Nat st i in dom A' & i > card N holds
Line A',i = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width A') & j < (Sgm N) . i holds
A' * i,j = 0. F1() ) )
take rngf ; :: thesis: ( rngf c= Seg F3() & the_rank_of F5() = the_rank_of A' & the_rank_of F5() = card rngf & P1[A',B'] & Segm A',(Seg (card rngf)),rngf is diagonal & ( for i being Nat st i in Seg (card rngf) holds
A' * i,((Sgm rngf) /. i) <> 0. F1() ) & ( for i being Nat st i in dom A' & i > card rngf holds
Line A',i = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card rngf) & j in Seg (width A') & j < (Sgm rngf) . i holds
A' * i,j = 0. F1() ) )
len A' = F2() by MATRIX_1:def 3;
then ( width A' = 0 or width A' = F3() ) by A222, MATRIX_1:24, MATRIX_1:def 4;
then Seg (width A') c= Seg F3() by FINSEQ_1:7;
hence ( rngf c= Seg F3() & the_rank_of F5() = the_rank_of A' ) by A215, A220, XBOOLE_1:1; :: thesis: ( the_rank_of F5() = card rngf & P1[A',B'] & Segm A',(Seg (card rngf)),rngf is diagonal & ( for i being Nat st i in Seg (card rngf) holds
A' * i,((Sgm rngf) /. i) <> 0. F1() ) & ( for i being Nat st i in dom A' & i > card rngf holds
Line A',i = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card rngf) & j in Seg (width A') & j < (Sgm rngf) . i holds
A' * i,j = 0. F1() ) )
dom f,rngf are_equipotent by A219, WELLORD2:def 4;
hence A224: card rngf = card (dom f) by CARD_1:21
.= card (Seg (the_rank_of F5())) by A215, A218, FINSEQ_1:def 3
.= the_rank_of F5() by FINSEQ_1:78 ;
:: thesis: ( P1[A',B'] & Segm A',(Seg (card rngf)),rngf is diagonal & ( for i being Nat st i in Seg (card rngf) holds
A' * i,((Sgm rngf) /. i) <> 0. F1() ) & ( for i being Nat st i in dom A' & i > card rngf holds
Line A',i = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card rngf) & j in Seg (width A') & j < (Sgm rngf) . i holds
A' * i,j = 0. F1() ) )
now
let i, j be Nat; :: thesis: ( i in dom f & j in dom f & i < j implies f . i < f . j )
assume that
A225: ( i in dom f & j in dom f ) and
A226: i < j ; :: thesis: f . i < f . j
( f . i = f /. i & f . j = f /. j ) by A225, PARTFUN1:def 8;
hence f . i < f . j by A221, A225, A226; :: thesis: verum
end;
then A227: Sgm rngf = f by A219, A220, Th6;
thus P1[A',B'] by A214; :: thesis: ( Segm A',(Seg (card rngf)),rngf is diagonal & ( for i being Nat st i in Seg (card rngf) holds
A' * i,((Sgm rngf) /. i) <> 0. F1() ) & ( for i being Nat st i in dom A' & i > card rngf holds
Line A',i = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card rngf) & j in Seg (width A') & j < (Sgm rngf) . i holds
A' * i,j = 0. F1() ) )
A228: card (Seg (card rngf)) = card rngf by FINSEQ_1:78;
then A229: Indices (Segm A',(Seg (card rngf)),rngf) = [:(Seg (the_rank_of F5())),(Seg (the_rank_of F5())):] by A224, MATRIX_1:25;
now
let i, j be Element of NAT ; :: thesis: ( i in Seg (the_rank_of F5()) & j in Seg (the_rank_of F5()) & i <> j implies (Segm A',(Seg (card rngf)),rngf) * i,j = 0. F1() )
assume that
A230: i in Seg (the_rank_of F5()) and
A231: j in Seg (the_rank_of F5()) and
A232: i <> j ; :: thesis: (Segm A',(Seg (card rngf)),rngf) * i,j = 0. F1()
A233: i in (dom f) \ {j} by A223, A230, A232, ZFMISC_1:64;
A234: (idseq (the_rank_of F5())) . i = i by A230, FINSEQ_2:57;
[i,j] in Indices (Segm A',(Seg (card rngf)),rngf) by A229, A230, A231, ZFMISC_1:106;
then (Segm A',(Seg (card rngf)),rngf) * i,j = A' * ((Sgm (Seg (the_rank_of F5()))) . i),(f . j) by A224, A227, MATRIX13:def 1
.= A' * i,(f . j) by A234, FINSEQ_3:54
.= A' * i,(f /. j) by A223, A231, PARTFUN1:def 8 ;
hence (Segm A',(Seg (card rngf)),rngf) * i,j = 0. F1() by A221, A223, A231, A233; :: thesis: verum
end;
hence Segm A',(Seg (card rngf)),rngf is diagonal by A224, A228, MATRIX_7:def 2; :: thesis: ( ( for i being Nat st i in Seg (card rngf) holds
A' * i,((Sgm rngf) /. i) <> 0. F1() ) & ( for i being Nat st i in dom A' & i > card rngf holds
Line A',i = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card rngf) & j in Seg (width A') & j < (Sgm rngf) . i holds
A' * i,j = 0. F1() ) )
thus for i being Nat st i in Seg (card rngf) holds
A' * i,((Sgm rngf) /. i) <> 0. F1() by A221, A224, A227, A223; :: thesis: ( ( for i being Nat st i in dom A' & i > card rngf holds
Line A',i = F3() |-> (0. F1()) ) & ( for i, j being Nat st i in Seg (card rngf) & j in Seg (width A') & j < (Sgm rngf) . i holds
A' * i,j = 0. F1() ) )
thus for i being Nat st i in dom A' & i > card rngf holds
Line A',i = F3() |-> (0. F1()) by A216, A224; :: thesis: for i, j being Nat st i in Seg (card rngf) & j in Seg (width A') & j < (Sgm rngf) . i holds
A' * i,j = 0. F1()
let i, j be Nat; :: thesis: ( i in Seg (card rngf) & j in Seg (width A') & j < (Sgm rngf) . i implies A' * i,j = 0. F1() )
assume that
A235: i in Seg (card rngf) and
A236: j in Seg (width A') and
A237: j < (Sgm rngf) . i ; :: thesis: A' * i,j = 0. F1()
j < f /. i by A224, A227, A223, A235, A237, PARTFUN1:def 8;
hence A' * i,j = 0. F1() by A221, A224, A223, A235, A236; :: thesis: verum