let K be Field; :: thesis: for A, B being Matrix of K st len A = len B & ( width A = 0 implies width B = 0 ) holds
( the_rank_of A = the_rank_of (A ^^ B) iff not Solutions_of (A,B) is empty )
let A, B be Matrix of K; :: thesis: ( len A = len B & ( width A = 0 implies width B = 0 ) implies ( the_rank_of A = the_rank_of (A ^^ B) iff not Solutions_of (A,B) is empty ) )
assume that
A1: len A = len B and
A2: ( width A = 0 implies width B = 0 ) ; :: thesis: ( the_rank_of A = the_rank_of (A ^^ B) iff not Solutions_of (A,B) is empty )
set wB = width B;
set L = len A;
reconsider B9 = B as Matrix of len A, width B,K by A1, MATRIX_0:51;
set wA = width A;
reconsider A9 = A as Matrix of len A, width A,K by MATRIX_0:51;
deffunc H1( Matrix of len A, width B,K, Nat, Nat, Element of K) -> FinSequence of the carrier of K * = RLine ($1,$2,((Line ($1,$2)) + ($4 * (Line ($1,$3)))));
defpred S1[ set , set ] means for A1 being Matrix of len A, width A,K
for B1 being Matrix of len A, width B,K st A1 = $1 & B1 = $2 holds
( the_rank_of (A9 ^^ B9) = the_rank_of (A1 ^^ B1) & Solutions_of (A9,B9) = Solutions_of (A1,B1) );
A3: for A1 being Matrix of len A, width A,K
for B1 being Matrix of len A, width B,K st S1[A1,B1] holds
for a being Element of K
for i, j being Nat st j in dom A1 & ( i = j implies a <> - (1_ K) ) holds
S1[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H1(B1,i,j,a)]
proof
let A1 be Matrix of len A, width A,K; :: thesis: for B1 being Matrix of len A, width B,K st S1[A1,B1] holds
for a being Element of K
for i, j being Nat st j in dom A1 & ( i = j implies a <> - (1_ K) ) holds
S1[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H1(B1,i,j,a)]
let B1 be Matrix of len A, width B,K; :: thesis: ( S1[A1,B1] implies for a being Element of K
for i, j being Nat st j in dom A1 & ( i = j implies a <> - (1_ K) ) holds
S1[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H1(B1,i,j,a)] )
assume A4: S1[A1,B1] ; :: thesis: for a being Element of K
for i, j being Nat st j in dom A1 & ( i = j implies a <> - (1_ K) ) holds
S1[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H1(B1,i,j,a)]
let a be Element of K; :: thesis: for i, j being Nat st j in dom A1 & ( i = j implies a <> - (1_ K) ) holds
S1[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H1(B1,i,j,a)]
let i, j be Nat; :: thesis: ( j in dom A1 & ( i = j implies a <> - (1_ K) ) implies S1[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H1(B1,i,j,a)] )
assume that
A5: j in dom A1 and
A6: ( i = j implies a <> - (1_ K) ) ; :: thesis: S1[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H1(B1,i,j,a)]
set LAj = Line (A1,j);
set LAi = Line (A1,i);
set RA = RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j)))));
A7: dom A1 = Seg (len A1) by FINSEQ_1:def 3
.= Seg (len A) by MATRIX_0:def 2 ;
then A8: Solutions_of (A1,B1) = Solutions_of ((RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j)))))),H1(B1,i,j,a)) by A5, A6, Th40;
set RB = H1(B1,i,j,a);
set LBj = Line (B1,j);
set LBi = Line (B1,i);
A9: ( len A1 = len A & len B1 = len A ) by MATRIX_0:def 2;
per cases ( not i in Seg (len A) or i in Seg (len A) ) ;
suppose not i in Seg (len A) ; :: thesis: S1[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H1(B1,i,j,a)]
then ( RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))) = A1 & H1(B1,i,j,a) = B1 ) by A9, MATRIX13:40;
hence S1[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H1(B1,i,j,a)] by A4; :: thesis: verum
end;
suppose A10: i in Seg (len A) ; :: thesis: S1[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H1(B1,i,j,a)]
A11: len (A1 ^^ B1) = len A by MATRIX_0:def 2;
A12: ( len (a * (Line (A1,j))) = width A1 & len (a * (Line (B1,j))) = width B1 ) by CARD_1:def 7;
A13: ( len (Line (A1,i)) = width A1 & len (Line (B1,i)) = width B1 ) by CARD_1:def 7;
( len ((Line (A1,i)) + (a * (Line (A1,j)))) = width A1 & len ((Line (B1,i)) + (a * (Line (B1,j)))) = width B1 ) by CARD_1:def 7;
then (RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j)))))) ^^ H1(B1,i,j,a) = RLine ((A1 ^^ B1),i,(((Line (A1,i)) + (a * (Line (A1,j)))) ^ ((Line (B1,i)) + (a * (Line (B1,j)))))) by Th18
.= RLine ((A1 ^^ B1),i,(((Line (A1,i)) ^ (Line (B1,i))) + ((a * (Line (A1,j))) ^ (a * (Line (B1,j)))))) by A13, A12, Th3
.= RLine ((A1 ^^ B1),i,(((Line (A1,i)) ^ (Line (B1,i))) + (a * ((Line (A1,j)) ^ (Line (B1,j)))))) by Th4
.= RLine ((A1 ^^ B1),i,((Line ((A1 ^^ B1),i)) + (a * ((Line (A1,j)) ^ (Line (B1,j)))))) by A10, Th15
.= RLine ((A1 ^^ B1),i,((Line ((A1 ^^ B1),i)) + (a * (Line ((A1 ^^ B1),j))))) by A5, A7, Th15 ;
then the_rank_of ((RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j)))))) ^^ H1(B1,i,j,a)) = the_rank_of (A1 ^^ B1) by A5, A6, A7, A11, MATRIX13:92;
hence S1[ RLine (A1,i,((Line (A1,i)) + (a * (Line (A1,j))))),H1(B1,i,j,a)] by A4, A8; :: thesis: verum
end;
end;
end;
A14: S1[A9,B9] ;
consider A1 being Matrix of len A, width A,K, B1 being Matrix of len A, width B,K, N being finite without_zero Subset of NAT such that
A15: N c= Seg (width A) and
A16: ( the_rank_of A9 = the_rank_of A1 & the_rank_of A9 = card N ) and
A17: ( S1[A1,B1] & Segm (A1,(Seg (card N)),N) = 1. (K,(card N)) ) and
A18: for i being Nat st i in dom A1 & i > card N holds
Line (A1,i) = (width A) |-> (0. K) and
for i, j being Nat st i in Seg (card N) & j in Seg (width A1) & j < (Sgm N) . i holds
A1 * (i,j) = 0. K from MATRIX15:sch 2(A14, A3);
per cases ( len A = 0 or len A > 0 ) ;
suppose A19: len A = 0 ; :: thesis: ( the_rank_of A = the_rank_of (A ^^ B) iff not Solutions_of (A,B) is empty )
then ( len (A9 ^^ B9) = 0 & the_rank_of A = 0 ) by MATRIX13:74, MATRIX_0:def 2;
hence ( the_rank_of A = the_rank_of (A ^^ B) iff not Solutions_of (A,B) is empty ) by A19, Th51, MATRIX13:74; :: thesis: verum
end;
suppose A20: len A > 0 ; :: thesis: ( the_rank_of A = the_rank_of (A ^^ B) iff not Solutions_of (A,B) is empty )
per cases ( N <> {} or N = {} ) ;
suppose A21: N <> {} ; :: thesis: ( the_rank_of A = the_rank_of (A ^^ B) iff not Solutions_of (A,B) is empty )
set SN = Seg (card N);
set SS = (Seg (len A)) \ (Seg (card N));
A22: card (Seg (card N)) = card N by FINSEQ_1:57;
reconsider P2 = (Sgm (Seg (card N))) " (Seg (card N)), Q2 = (Sgm (Seg (width A))) " N as finite without_zero Subset of NAT by MATRIX13:53;
( dom (Sgm (Seg (card N))) = Seg (card (Seg (card N))) & rng (Sgm (Seg (card N))) = Seg (card N) ) by FINSEQ_1:def 14, FINSEQ_3:40;
then A23: P2 = Seg (card N) by A22, RELAT_1:134;
rng (Sgm (Seg (width A))) = Seg (width A) by FINSEQ_1:def 14;
then A24: (Sgm (Seg (width A))) .: Q2 = N by A15, FUNCT_1:77;
( Q2 c= dom (Sgm (Seg (width A))) & Sgm (Seg (width A)) is one-to-one ) by FINSEQ_3:92, RELAT_1:132;
then N,Q2 are_equipotent by A24, CARD_1:33;
then A25: ( dom (Sgm (Seg (width A))) = Seg (card (Seg (width A))) & card N = card Q2 ) by CARD_1:5, FINSEQ_3:40;
A26: ( Seg (len A1) = dom A1 & len A1 = len A ) by A20, FINSEQ_1:def 3, MATRIX_0:23;
A27: width A1 = width A by A20, MATRIX_0:23;
A28: now :: thesis: for i being Nat st i in (Seg (len A)) \ (Seg (card N)) holds
Line (A1,i) = (width A1) |-> (0. K)
let i be Nat; :: thesis: ( i in (Seg (len A)) \ (Seg (card N)) implies Line (A1,i) = (width A1) |-> (0. K) )
assume A29: i in (Seg (len A)) \ (Seg (card N)) ; :: thesis: Line (A1,i) = (width A1) |-> (0. K)
not i in Seg (card N) by A29, XBOOLE_0:def 5;
then A30: ( i < 1 or i > card N ) ;
i in Seg (len A) by A29, XBOOLE_0:def 5;
hence Line (A1,i) = (width A1) |-> (0. K) by A18, A26, A27, A30, FINSEQ_1:1; :: thesis: verum
end;
card N <= len A by A16, MATRIX13:74;
then A31: Seg (card N) c= Seg (len A) by FINSEQ_1:5;
A32: len B1 = len A by A20, MATRIX_0:23;
A33: ( Seg (len B1) = dom B1 & width B1 = width B ) by A20, FINSEQ_1:def 3, MATRIX_0:23;
thus ( the_rank_of A = the_rank_of (A ^^ B) implies not Solutions_of (A,B) is empty ) :: thesis: ( not Solutions_of (A,B) is empty implies the_rank_of A = the_rank_of (A ^^ B) )
proof
assume the_rank_of A = the_rank_of (A ^^ B) ; :: thesis: not Solutions_of (A,B) is empty
then the_rank_of A1 = the_rank_of (A1 ^^ B1) by A16, A17;
then for i being Nat st i in (dom A1) \ (Seg (card N)) holds
( Line (A1,i) = (width A1) |-> (0. K) & Line (B1,i) = (width B1) |-> (0. K) ) by A26, A32, A28, Th24, XBOOLE_1:36;
then A34: Solutions_of (A1,B1) = Solutions_of ((Segm (A1,(Seg (card N)),(Seg (width A)))),(Segm (B1,(Seg (card N)),(Seg (width B))))) by A21, A31, A26, A32, A27, A33, Th45;
Segm ((Segm (A1,(Seg (card N)),(Seg (width A)))),P2,Q2) = 1. (K,(card N)) by A15, A17, MATRIX13:56;
then ex X being Matrix of card (Seg (width A)), card (Seg (width B)),K st
( Segm (X,((Seg (card (Seg (width A)))) \ Q2),(Seg (card (Seg (width B))))) = 0. (K,((card (Seg (width A))) -' (card (Seg (card N)))),(card (Seg (width B)))) & Segm (X,Q2,(Seg (card (Seg (width B))))) = Segm (B1,(Seg (card N)),(Seg (width B))) & X in Solutions_of ((Segm (A1,(Seg (card N)),(Seg (width A)))),(Segm (B1,(Seg (card N)),(Seg (width B))))) ) by A21, A22, A23, A25, Th50, RELAT_1:132;
hence not Solutions_of (A,B) is empty by A17, A34; :: thesis: verum
end;
A35: (Seg (len A)) \ (Seg (card N)) c= Seg (len A) by XBOOLE_1:36;
thus ( not Solutions_of (A,B) is empty implies the_rank_of A = the_rank_of (A ^^ B) ) :: thesis: verum
proof
assume not Solutions_of (A,B) is empty ; :: thesis: the_rank_of A = the_rank_of (A ^^ B)
then not Solutions_of (A1,B1) is empty by A17;
then consider x being object such that
A36: x in Solutions_of (A1,B1) ;
set AB = A1 ^^ B1;
A37: len (Segm ((A1 ^^ B1),(Seg (card N)),(Seg (width (A1 ^^ B1))))) = card (Seg (card N)) by MATRIX_0:def 2;
A38: ( dom (A1 ^^ B1) = Seg (len (A1 ^^ B1)) & len (A1 ^^ B1) = len A ) by A20, FINSEQ_1:def 3, MATRIX_0:23;
reconsider x = x as Matrix of width A, width B,K by A20, A36, Th53;
A39: the_rank_of (Segm ((A1 ^^ B1),(Seg (len A)),(Seg (width A1)))) = card N by A16, Th19;
A40: width (A1 ^^ B1) = (width A1) + (width B1) by A20, MATRIX_0:23;
now :: thesis: for i being Nat st i in (Seg (len A)) \ (Seg (card N)) holds
Line ((A1 ^^ B1),i) = (width (A1 ^^ B1)) |-> (0. K)
let i be Nat; :: thesis: ( i in (Seg (len A)) \ (Seg (card N)) implies Line ((A1 ^^ B1),i) = (width (A1 ^^ B1)) |-> (0. K) )
assume A41: i in (Seg (len A)) \ (Seg (card N)) ; :: thesis: Line ((A1 ^^ B1),i) = (width (A1 ^^ B1)) |-> (0. K)
A42: Line (A1,i) = (width A1) |-> (0. K) by A28, A41;
A43: ( x in Solutions_of (A1,B1) & i in dom A1 & Line (A1,i) = (width A1) |-> (0. K) implies Line (B1,i) = (width B1) |-> (0. K) ) by Th41;
thus Line ((A1 ^^ B1),i) = (Line (A1,i)) ^ (Line (B1,i)) by A35, A41, Th15
.= (width (A1 ^^ B1)) |-> (0. K) by A26, A35, A36, A40, A41, A42, A43, FINSEQ_2:123 ; :: thesis: verum
end;
then the_rank_of (Segm ((A1 ^^ B1),(Seg (card N)),(Seg (width (A1 ^^ B1))))) = the_rank_of (A1 ^^ B1) by A31, A38, Th11;
then the_rank_of (A1 ^^ B1) <= card (Seg (card N)) by A37, MATRIX13:74;
then A44: the_rank_of (A1 ^^ B1) <= card N by FINSEQ_1:57;
width A1 <= width (A1 ^^ B1) by A40, NAT_1:11;
then Seg (width A1) c= Seg (width (A1 ^^ B1)) by FINSEQ_1:5;
then [:(Seg (len A)),(Seg (width A1)):] c= Indices (A1 ^^ B1) by A38, ZFMISC_1:95;
then card N <= the_rank_of (A1 ^^ B1) by A39, MATRIX13:79;
then the_rank_of (A1 ^^ B1) = card N by A44, XXREAL_0:1;
hence the_rank_of A = the_rank_of (A ^^ B) by A16, A17; :: thesis: verum
end;
end;
suppose A45: N = {} ; :: thesis: ( the_rank_of A = the_rank_of (A ^^ B) iff not Solutions_of (A,B) is empty )
set ZERO = 0. (K,(len A),(width A));
A46: now :: thesis: for i being Nat st 1 <= i & i <= len A holds
(0. (K,(len A),(width A))) . i = A1 . i
let i be Nat; :: thesis: ( 1 <= i & i <= len A implies (0. (K,(len A),(width A))) . i = A1 . i )
assume A47: ( 1 <= i & i <= len A ) ; :: thesis: (0. (K,(len A),(width A))) . i = A1 . i
A48: ( dom A1 = Seg (len A1) & len A1 = len A ) by FINSEQ_1:def 3, MATRIX_0:def 2;
A49: i in Seg (len A) by A47;
hence (0. (K,(len A),(width A))) . i = (width A) |-> (0. K) by FINSEQ_2:57
.= Line (A1,i) by A18, A45, A49, A48
.= A1 . i by A49, MATRIX_0:52 ;
:: thesis: verum
end;
A50: len (0. (K,(len A),(width A))) = len A by A20, MATRIX_0:23;
A51: width A1 = width A by A20, MATRIX_0:23;
len A1 = len A by A20, MATRIX_0:23;
then 0. (K,(len A),(width A)) = A1 by A50, A46;
then A52: the_rank_of A = 0 by A16, A50, A51, MATRIX13:95;
then A53: 0. (K,(len A),(width A)) = A by MATRIX13:95;
A54: Indices (A9 ^^ B9) = [:(Seg (len A)),(Seg ((width A) + (width B))):] by A20, MATRIX_0:23;
thus ( the_rank_of A = the_rank_of (A ^^ B) implies not Solutions_of (A,B) is empty ) :: thesis: ( not Solutions_of (A,B) is empty implies the_rank_of A = the_rank_of (A ^^ B) )
proof
set x = the Matrix of width A, width B,K;
assume A55: the_rank_of A = the_rank_of (A ^^ B) ; :: thesis: not Solutions_of (A,B) is empty
(Seg ((width A) + (width B))) \ (Seg (width A)) c= Seg ((width A) + (width B)) by XBOOLE_1:36;
then A56: [:(Seg (len A)),((Seg ((width A) + (width B))) \ (Seg (width A))):] c= Indices (A ^^ B) by A54, ZFMISC_1:95;
Segm ((A9 ^^ B9),(Seg (len A)),((Seg ((width A) + (width B))) \ (Seg (width A)))) = B by Th19;
then 0 = the_rank_of B by A52, A55, A56, MATRIX13:79;
then A57: B = 0. (K,(len A),(width B)) by A1, MATRIX13:95;
then ( ( width A = 0 & width B = 0 ) or Solutions_of (A9,B9) = { X where X is Matrix of width A, width B,K : verum } ) by A2, A20, A53, Th54;
then ( Solutions_of (A9,B9) = {{}} or the Matrix of width A, width B,K in Solutions_of (A9,B9) ) by A53, A57, Th56;
hence not Solutions_of (A,B) is empty ; :: thesis: verum
end;
A58: Indices B9 = [:(Seg (len A)),(Seg (width B)):] by A20, MATRIX_0:23;
A59: (width A) + (width B) = width (A9 ^^ B9) by A20, MATRIX_0:23;
A60: Indices (0. (K,(len A),(width A))) = [:(Seg (len A)),(Seg (width A)):] by A20, MATRIX_0:23;
thus ( not Solutions_of (A,B) is empty implies the_rank_of A = the_rank_of (A ^^ B) ) :: thesis: verum
proof
assume A61: not Solutions_of (A,B) is empty ; :: thesis: the_rank_of A = the_rank_of (A ^^ B)
assume the_rank_of A <> the_rank_of (A ^^ B) ; :: thesis: contradiction
then consider i, j being Nat such that
A62: [i,j] in Indices (A9 ^^ B9) and
A63: (A9 ^^ B9) * (i,j) <> 0. K by A52, MATRIX13:94;
A64: j in Seg ((width A) + (width B)) by A59, A62, ZFMISC_1:87;
A65: dom (Line ((A9 ^^ B9),i)) = Seg ((width A) + (width B)) by A59, FINSEQ_2:124;
A66: len (Line (A9,i)) = width A by CARD_1:def 7;
A67: dom (Line (B9,i)) = Seg (width B) by FINSEQ_2:124;
A68: dom (Line (A9,i)) = Seg (width A) by FINSEQ_2:124;
A69: i in Seg (len A) by A54, A62, ZFMISC_1:87;
then A70: Line ((A9 ^^ B9),i) = (Line (A9,i)) ^ (Line (B9,i)) by Th15;
per cases ( j in dom (Line (A9,i)) or ex n being Nat st
( n in dom (Line (B9,i)) & j = (width A) + n ) ) by A64, A66, A65, A70, FINSEQ_1:25;
suppose A71: j in dom (Line (A9,i)) ; :: thesis: contradiction
then A72: [i,j] in Indices (0. (K,(len A),(width A))) by A60, A69, A68, ZFMISC_1:87;
(A9 ^^ B9) * (i,j) = (Line ((A9 ^^ B9),i)) . j by A59, A64, MATRIX_0:def 7
.= (Line (A9,i)) . j by A70, A71, FINSEQ_1:def 7
.= A9 * (i,j) by A68, A71, MATRIX_0:def 7
.= 0. K by A53, A72, MATRIX_3:1 ;
hence contradiction by A63; :: thesis: verum
end;
suppose ex n being Nat st
( n in dom (Line (B9,i)) & j = (width A) + n ) ; :: thesis: contradiction
then consider n being Nat such that
A73: n in dom (Line (B9,i)) and
A74: j = (width A) + n ;
A75: [i,n] in Indices B by A58, A69, A67, A73, ZFMISC_1:87;
A76: B = 0. (K,(len A),(width B)) by A53, A61, Th52;
(A9 ^^ B9) * (i,j) = (Line ((A9 ^^ B9),i)) . j by A59, A64, MATRIX_0:def 7
.= (Line (B9,i)) . n by A66, A70, A73, A74, FINSEQ_1:def 7
.= B9 * (i,n) by A67, A73, MATRIX_0:def 7
.= 0. K by A75, A76, MATRIX_3:1 ;
hence contradiction by A63; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;