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_2:7;
set wA = width A;
reconsider A9 = A as Matrix of len A, width A,K by MATRIX_2:7;
deffunc H1( Matrix of len A, width B,K, Nat, Nat, Element of K) -> Matrix of len A, width B,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_1:def 3 ;
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_1:def 3;
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_1:def 3;
A12: ( len (a * (Line A1,j)) = width A1 & len (a * (Line B1,j)) = width B1 ) by FINSEQ_1:def 18;
A13: ( len (Line A1,i) = width A1 & len (Line B1,i) = width B1 ) by FINSEQ_1:def 18;
( len ((Line A1,i) + (a * (Line A1,j))) = width A1 & len ((Line B1,i) + (a * (Line B1,j))) = width B1 ) by FINSEQ_1:def 18;
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_1:def 3;
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:78;
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 13, FINSEQ_3:45;
then A23: P2 = Seg (card N) by A22, RELAT_1:169;
rng (Sgm (Seg (width A))) = Seg (width A) by FINSEQ_1:def 13;
then A24: (Sgm (Seg (width A))) .: Q2 = N by A15, FUNCT_1:147;
( Q2 c= dom (Sgm (Seg (width A))) & Sgm (Seg (width A)) is one-to-one ) by FINSEQ_3:99, RELAT_1:167;
then N,Q2 are_equipotent by A24, CARD_1:60;
then A25: ( dom (Sgm (Seg (width A))) = Seg (card (Seg (width A))) & card N = card Q2 ) by CARD_1:21, FINSEQ_3:45;
A26: ( Seg (len A1) = dom A1 & len A1 = len A ) by A20, FINSEQ_1:def 3, MATRIX_1:24;
A27: width A1 = width A by A20, MATRIX_1:24;
A28: now
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 ) by A29;
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:3; :: thesis: verum
end;
card N <= len A by A16, MATRIX13:74;
then A31: Seg (card N) c= Seg (len A) by FINSEQ_1:7;
A32: len B1 = len A by A20, MATRIX_1:24;
A33: ( Seg (len B1) = dom B1 & width B1 = width B ) by A20, FINSEQ_1:def 3, MATRIX_1:24;
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:167;
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 set such that
A36: x in Solutions_of A1,B1 by XBOOLE_0:def 1;
set AB = A1 ^^ B1;
A37: len (Segm (A1 ^^ B1),(Seg (card N)),(Seg (width (A1 ^^ B1)))) = card (Seg (card N)) by MATRIX_1:def 3;
A38: ( dom (A1 ^^ B1) = Seg (len (A1 ^^ B1)) & len (A1 ^^ B1) = len A ) by A20, FINSEQ_1:def 3, MATRIX_1:24;
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_1:24;
now
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:143 ; :: 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:78;
width A1 <= width (A1 ^^ B1) by A40, NAT_1:11;
then Seg (width A1) c= Seg (width (A1 ^^ B1)) by FINSEQ_1:7;
then [:(Seg (len A)),(Seg (width A1)):] c= Indices (A1 ^^ B1) by A38, ZFMISC_1:118;
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
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_1:def 3;
i in NAT by ORDINAL1:def 13;
then A49: i in Seg (len A) by A47;
hence (0. K,(len A),(width A)) . i = (width A) |-> (0. K) by FINSEQ_2:71
.= Line A1,i by A18, A45, A49, A48
.= A1 . i by A49, MATRIX_2:10 ;
:: thesis: verum
end;
A50: len (0. K,(len A),(width A)) = len A by A20, MATRIX_1:24;
A51: width A1 = width A by A20, MATRIX_1:24;
len A1 = len A by A20, MATRIX_1:24;
then 0. K,(len A),(width A) = A1 by A50, A46, FINSEQ_1:18;
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_1:24;
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
consider x being 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:118;
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 x 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_1:24;
A59: (width A) + (width B) = width (A9 ^^ B9) by A20, MATRIX_1:24;
A60: Indices (0. K,(len A),(width A)) = [:(Seg (len A)),(Seg (width A)):] by A20, MATRIX_1:24;
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:106;
A65: dom (Line (A9 ^^ B9),i) = Seg ((width A) + (width B)) by A59, FINSEQ_2:144;
A66: len (Line A9,i) = width A by FINSEQ_1:def 18;
A67: dom (Line B9,i) = Seg (width B) by FINSEQ_2:144;
A68: dom (Line A9,i) = Seg (width A) by FINSEQ_2:144;
A69: i in Seg (len A) by A54, A62, ZFMISC_1:106;
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:38;
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:106;
(A9 ^^ B9) * i,j = (Line (A9 ^^ B9),i) . j by A59, A64, MATRIX_1:def 8
.= (Line A9,i) . j by A70, A71, FINSEQ_1:def 7
.= A9 * i,j by A68, A71, MATRIX_1:def 8
.= 0. K by A53, A72, MATRIX_3:3 ;
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:106;
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_1:def 8
.= (Line B9,i) . n by A66, A70, A73, A74, FINSEQ_1:def 7
.= B9 * i,n by A67, A73, MATRIX_1:def 8
.= 0. K by A75, A76, MATRIX_3:3 ;
hence contradiction by A63; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;