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 ;
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 ;
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
.= 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
.= 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 ;
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 () 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) = () |-> (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
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 ;
hence ( the_rank_of A = the_rank_of (A ^^ B) iff not Solutions_of (A,B) is empty ) by ; :: 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 ())) " 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 ;
then A23: P2 = Seg (card N) by ;
rng (Sgm (Seg ())) = Seg () by FINSEQ_1:def 13;
then A24: (Sgm (Seg ())) .: Q2 = N by ;
( Q2 c= dom (Sgm (Seg ())) & Sgm (Seg ()) is one-to-one ) by ;
then N,Q2 are_equipotent by ;
then A25: ( dom (Sgm (Seg ())) = Seg (card (Seg ())) & card N = card Q2 ) by ;
A26: ( Seg (len A1) = dom A1 & len A1 = len A ) by ;
A27: width A1 = width A by ;
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 ;
then A30: ( i < 1 or i > card N ) ;
i in Seg (len A) by ;
hence Line (A1,i) = (width A1) |-> (0. K) by ; :: thesis: verum
end;
card N <= len A by ;
then A31: Seg (card N) c= Seg (len A) by FINSEQ_1:5;
A32: len B1 = len A by ;
A33: ( Seg (len B1) = dom B1 & width B1 = width B ) by ;
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 ;
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 ;
then A34: Solutions_of (A1,B1) = Solutions_of ((Segm (A1,(Seg (card N)),(Seg ()))),(Segm (B1,(Seg (card N)),(Seg ())))) by A21, A31, A26, A32, A27, A33, Th45;
Segm ((Segm (A1,(Seg (card N)),(Seg ()))),P2,Q2) = 1. (K,(card N)) by ;
then ex X being Matrix of card (Seg ()), card (Seg ()),K st
( Segm (X,((Seg (card (Seg ()))) \ Q2),(Seg (card (Seg ())))) = 0. (K,((card (Seg ())) -' (card (Seg (card N)))),(card (Seg ()))) & Segm (X,Q2,(Seg (card (Seg ())))) = Segm (B1,(Seg (card N)),(Seg ())) & X in Solutions_of ((Segm (A1,(Seg (card N)),(Seg ()))),(Segm (B1,(Seg (card N)),(Seg ())))) ) by ;
hence not Solutions_of (A,B) is empty by ; :: 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 ;
reconsider x = x as Matrix of width A, width B,K by ;
A39: the_rank_of (Segm ((A1 ^^ B1),(Seg (len A)),(Seg (width A1)))) = card N by ;
A40: width (A1 ^^ B1) = (width A1) + (width B1) by ;
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 ;
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
.= (width (A1 ^^ B1)) |-> (0. K) by ; :: thesis: verum
end;
then the_rank_of (Segm ((A1 ^^ B1),(Seg (card N)),(Seg (width (A1 ^^ B1))))) = the_rank_of (A1 ^^ B1) by ;
then the_rank_of (A1 ^^ B1) <= card (Seg (card N)) by ;
then A44: the_rank_of (A1 ^^ B1) <= card N by FINSEQ_1:57;
width A1 <= width (A1 ^^ B1) by ;
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 ;
then card N <= the_rank_of (A1 ^^ B1) by ;
then the_rank_of (A1 ^^ B1) = card N by ;
hence the_rank_of A = the_rank_of (A ^^ B) by ; :: 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),());
A46: now :: thesis: for i being Nat st 1 <= i & i <= len A holds
(0. (K,(len A),())) . i = A1 . i
let i be Nat; :: thesis: ( 1 <= i & i <= len A implies (0. (K,(len A),())) . i = A1 . i )
assume A47: ( 1 <= i & i <= len A ) ; :: thesis: (0. (K,(len A),())) . i = A1 . i
A48: ( dom A1 = Seg (len A1) & len A1 = len A ) by ;
A49: i in Seg (len A) by A47;
hence (0. (K,(len A),())) . i = () |-> (0. K) by FINSEQ_2:57
.= Line (A1,i) by A18, A45, A49, A48
.= A1 . i by ;
:: thesis: verum
end;
A50: len (0. (K,(len A),())) = len A by ;
A51: width A1 = width A by ;
len A1 = len A by ;
then 0. (K,(len A),()) = A1 by ;
then A52: the_rank_of A = 0 by ;
then A53: 0. (K,(len A),()) = A by MATRIX13:95;
A54: Indices (A9 ^^ B9) = [:(Seg (len A)),(Seg (() + ())):] by ;
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 (() + ())) \ (Seg ()) c= Seg (() + ()) by XBOOLE_1:36;
then A56: [:(Seg (len A)),((Seg (() + ())) \ (Seg ())):] c= Indices (A ^^ B) by ;
Segm ((A9 ^^ B9),(Seg (len A)),((Seg (() + ())) \ (Seg ()))) = B by Th19;
then 0 = the_rank_of B by ;
then A57: B = 0. (K,(len A),()) by ;
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 ;
hence not Solutions_of (A,B) is empty ; :: thesis: verum
end;
A58: Indices B9 = [:(Seg (len A)),(Seg ()):] by ;
A59: (width A) + () = width (A9 ^^ B9) by ;
A60: Indices (0. (K,(len A),())) = [:(Seg (len A)),(Seg ()):] by ;
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 ;
A64: j in Seg (() + ()) by ;
A65: dom (Line ((A9 ^^ B9),i)) = Seg (() + ()) by ;
A66: len (Line (A9,i)) = width A by CARD_1:def 7;
A67: dom (Line (B9,i)) = Seg () by FINSEQ_2:124;
A68: dom (Line (A9,i)) = Seg () by FINSEQ_2:124;
A69: i in Seg (len A) by ;
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 = () + n ) )
by ;
suppose A71: j in dom (Line (A9,i)) ; :: thesis: contradiction
then A72: [i,j] in Indices (0. (K,(len A),())) by ;
(A9 ^^ B9) * (i,j) = (Line ((A9 ^^ B9),i)) . j by
.= (Line (A9,i)) . j by
.= A9 * (i,j) by
.= 0. K by ;
hence contradiction by A63; :: thesis: verum
end;
suppose ex n being Nat st
( n in dom (Line (B9,i)) & j = () + n ) ; :: thesis: contradiction
then consider n being Nat such that
A73: n in dom (Line (B9,i)) and
A74: j = () + n ;
A75: [i,n] in Indices B by ;
A76: B = 0. (K,(len A),()) by ;
(A9 ^^ B9) * (i,j) = (Line ((A9 ^^ B9),i)) . j by
.= (Line (B9,i)) . n by
.= B9 * (i,n) by
.= 0. K by ;
hence contradiction by A63; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;