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 A1: ( len A = len B & ( 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 L = len A;
set wA = width A;
set wB = width B;
reconsider A' = A as Matrix of len A, width A,K by MATRIX_2:7;
reconsider B' = B as Matrix of len A, width B,K by A1, MATRIX_2:7;
deffunc H₁( 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 S₁[ 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 (A' ^^ B') = the_rank_of (A1 ^^ B1) & Solutions_of A',B' = Solutions_of A1,B1 );
A2: S₁[A',B'] ;
A3: for A1 being Matrix of len A, width A,K
for B1 being Matrix of len A, width B,K st S₁[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
S₁[ RLine A1,i,((Line A1,i) + (a * (Line A1,j))),H₁(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 S₁[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
S₁[ RLine A1,i,((Line A1,i) + (a * (Line A1,j))),H₁(B1,i,j,a)]
let B1 be Matrix of len A, width B,K; :: thesis: ( S₁[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
S₁[ RLine A1,i,((Line A1,i) + (a * (Line A1,j))),H₁(B1,i,j,a)] )
assume A4: S₁[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
S₁[ RLine A1,i,((Line A1,i) + (a * (Line A1,j))),H₁(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
S₁[ RLine A1,i,((Line A1,i) + (a * (Line A1,j))),H₁(B1,i,j,a)]
let i, j be Nat; :: thesis: ( j in dom A1 & ( i = j implies a <> - (1_ K) ) implies S₁[ RLine A1,i,((Line A1,i) + (a * (Line A1,j))),H₁(B1,i,j,a)] )
assume A5: ( j in dom A1 & ( i = j implies a <> - (1_ K) ) ) ; :: thesis: S₁[ RLine A1,i,((Line A1,i) + (a * (Line A1,j))),H₁(B1,i,j,a)]
set LAi = Line A1,i;
set LAj = Line A1,j;
set LBi = Line B1,i;
set LBj = Line B1,j;
set RA = RLine A1,i,((Line A1,i) + (a * (Line A1,j)));
set RB = H₁(B1,i,j,a);
A6: dom A1 = Seg (len A1) by FINSEQ_1:def 3
.= Seg (len A) by MATRIX_1:def 3 ;
A7: ( len (A1 ^^ B1) = len A & len A1 = len A & len B1 = len A ) by MATRIX_1:def 3;
A8: Solutions_of A1,B1 = Solutions_of (RLine A1,i,((Line A1,i) + (a * (Line A1,j)))),H₁(B1,i,j,a) by A5, A6, Th40;

per cases ( not i in Seg (len A) or i in Seg (len A) ) ;

suppose not i in Seg (len A) ; :: thesis: S₁[ RLine A1,i,((Line A1,i) + (a * (Line A1,j))),H₁(B1,i,j,a)]

then ( RLine A1,i,((Line A1,i) + (a * (Line A1,j))) = A1 & H₁(B1,i,j,a) = B1 ) by A7, MATRIX13:40;
hence S₁[ RLine A1,i,((Line A1,i) + (a * (Line A1,j))),H₁(B1,i,j,a)] by A4; :: thesis: verum

end;

suppose A9: i in Seg (len A) ; :: thesis: S₁[ RLine A1,i,((Line A1,i) + (a * (Line A1,j))),H₁(B1,i,j,a)]

A10: len (A1 ^^ B1) = len A by MATRIX_1:def 3;
A11: ( len ((Line A1,i) + (a * (Line A1,j))) = width A1 & len ((Line B1,i) + (a * (Line B1,j))) = width B1 & len (Line A1,i) = width A1 & len (Line B1,i) = width B1 & len (a * (Line A1,j)) = width A1 & len (a * (Line B1,j)) = width B1 ) by FINSEQ_1:def 18;
then (RLine A1,i,((Line A1,i) + (a * (Line A1,j)))) ^^ H₁(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 Th3, A11
.= 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 A9, Th15
.= RLine (A1 ^^ B1),i,((Line (A1 ^^ B1),i) + (a * (Line (A1 ^^ B1),j))) by A5, A6, Th15 ;
then the_rank_of ((RLine A1,i,((Line A1,i) + (a * (Line A1,j)))) ^^ H₁(B1,i,j,a)) = the_rank_of (A1 ^^ B1) by A5, A6, A10, MATRIX13:92;
hence S₁[ RLine A1,i,((Line A1,i) + (a * (Line A1,j))),H₁(B1,i,j,a)] by A8, A4; :: thesis: verum

end;

end;

end;

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
A12: N c= Seg (width A) and
A13: ( the_rank_of A' = the_rank_of A1 & the_rank_of A' = card N ) and
A14: ( S₁[A1,B1] & Segm A1,(Seg (card N)),N = 1. K,(card N) ) and
A15: 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(A2, A3);

per cases ( len A = 0 or len A > 0 ) ;

suppose A16: len A = 0 ; :: thesis: ( the_rank_of A = the_rank_of (A ^^ B) iff not Solutions_of A,B is empty )

then len (A' ^^ B') = 0 by MATRIX_1:def 3;
then ( the_rank_of A <= 0 & the_rank_of (A ^^ B) <= 0 ) by A16, MATRIX13:74;
then ( the_rank_of A = 0 & the_rank_of (A ^^ B) = 0 & Solutions_of A',B' = {{} } ) by A16, Th51;
hence ( the_rank_of A = the_rank_of (A ^^ B) iff not Solutions_of A,B is empty ) ; :: thesis: verum

end;

suppose A17: 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 N <> {} ; :: thesis: ( the_rank_of A = the_rank_of (A ^^ B) iff not Solutions_of A,B is empty )

then card N <> 0 ;
then A18: ( card N > 0 & card N in Seg (card N) ) by FINSEQ_1:5;
card N <= len A by A13, MATRIX13:74;
then A19: ( Seg (card N) c= Seg (len A) & Seg (len A1) = dom A1 & len A1 = len A & Seg (len B1) = dom B1 & len B1 = len A & width A1 = width A & width B1 = width B ) by A17, FINSEQ_1:7, FINSEQ_1:def 3, MATRIX_1:24;
A20: (Seg (len A)) \ (Seg (card N)) c= Seg (len A) by XBOOLE_1:36;
set SN = Seg (card N);
set SS = (Seg (len A)) \ (Seg (card N));

A21: now

let i be Nat; :: thesis: ( i in (Seg (len A)) \ (Seg (card N)) implies Line A1,i = (width A1) |-> (0. K) )
assume A22: i in (Seg (len A)) \ (Seg (card N)) ; :: thesis: Line A1,i = (width A1) |-> (0. K)
( i in Seg (len A) & not i in Seg (card N) ) by A22, XBOOLE_0:def 5;
then ( 1 <= i & ( i < 1 or i > card N ) ) by FINSEQ_1:3;
then ( i > card N & i in dom A1 ) by A22, A19, XBOOLE_0:def 5;
hence Line A1,i = (width A1) |-> (0. K) by A15, A19; :: thesis: verum

end;

A23: 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 A24: P2 = Seg (card N) by A23, RELAT_1:169;
rng (Sgm (Seg (width A))) = Seg (width A) by FINSEQ_1:def 13;
then A25: ( (Sgm (Seg (width A))) .: Q2 = N & Q2 c= dom (Sgm (Seg (width A))) & dom (Sgm (Seg (width A))) = Seg (card (Seg (width A))) & Sgm (Seg (width A)) is one-to-one ) by A12, FINSEQ_3:45, FINSEQ_3:99, FUNCT_1:147, RELAT_1:167;
then N,Q2 are_equipotent by CARD_1:60;
then A26: card N = card Q2 by CARD_1:21;
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 A13, A14;
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 A19, A20, A21, Th24;
then A27: Solutions_of A1,B1 = Solutions_of (Segm A1,(Seg (card N)),(Seg (width A))),(Segm B1,(Seg (card N)),(Seg (width B))) by A18, A19, Th45;
Segm (Segm A1,(Seg (card N)),(Seg (width A))),P2,Q2 = 1. K,(card N) by A14, A12, 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 A25, A18, Th50, A23, A24, A26;
hence not Solutions_of A,B is empty by A14, A27; :: thesis: verum

end;

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 A14;
then consider x being set such that
A28: x in Solutions_of A1,B1 by XBOOLE_0:def 1;
reconsider x = x as Matrix of width A, width B,K by A17, A28, Th53;
set AB = A1 ^^ B1;
A29: ( dom (A1 ^^ B1) = Seg (len (A1 ^^ B1)) & len (A1 ^^ B1) = len A & width (A1 ^^ B1) = (width A1) + (width B1) & Indices (A1 ^^ B1) = [:(Seg (len A)),(Seg ((width A1) + (width B1))):] ) by A17, FINSEQ_1:def 3, 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 A30: i in (Seg (len A)) \ (Seg (card N)) ; :: thesis: Line (A1 ^^ B1),i = (width (A1 ^^ B1)) |-> (0. K)
A31: ( i in dom A1 & Line A1,i = (width A1) |-> (0. K) ) by A19, A20, A30, A21;
A32: ( 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 A20, A30, Th15
.= (width (A1 ^^ B1)) |-> (0. K) by A31, A32, A29, A28, FINSEQ_2:143 ; :: thesis: verum

end;

then A33: the_rank_of (Segm (A1 ^^ B1),(Seg (card N)),(Seg (width (A1 ^^ B1)))) = the_rank_of (A1 ^^ B1) by A19, A29, Th11;
len (Segm (A1 ^^ B1),(Seg (card N)),(Seg (width (A1 ^^ B1)))) = card (Seg (card N)) by MATRIX_1:def 3;
then the_rank_of (A1 ^^ B1) <= card (Seg (card N)) by A33, MATRIX13:74;
then A34: the_rank_of (A1 ^^ B1) <= card N by FINSEQ_1:78;
width A1 <= width (A1 ^^ B1) by A29, NAT_1:11;
then Seg (width A1) c= Seg (width (A1 ^^ B1)) by FINSEQ_1:7;
then A35: [:(Seg (len A)),(Seg (width A1)):] c= Indices (A1 ^^ B1) by A29, ZFMISC_1:118;
the_rank_of (Segm (A1 ^^ B1),(Seg (len A)),(Seg (width A1))) = card N by A13, Th19;
then card N <= the_rank_of (A1 ^^ B1) by A35, MATRIX13:79;
then the_rank_of (A1 ^^ B1) = card N by A34, XXREAL_0:1;
hence the_rank_of A = the_rank_of (A ^^ B) by A13, A14; :: thesis: verum

end;

end;

suppose A36: 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);
A37: ( len (0. K,(len A),(width A)) = len A & len A1 = len A & width A1 = width A & len B' = len A & width B' = width B & Indices (0. K,(len A),(width A)) = [:(Seg (len A)),(Seg (width A)):] & Indices B' = [:(Seg (len A)),(Seg (width B)):] & (width A) + (width B) = width (A' ^^ B') & len A = len (A' ^^ B') & Indices (A' ^^ B') = [:(Seg (len A)),(Seg ((width A) + (width B))):] ) by A17, MATRIX_1:24;

now

let i be Nat; :: thesis: ( 1 <= i & i <= len A implies (0. K,(len A),(width A)) . i = A1 . i )
assume A38: ( 1 <= i & i <= len A ) ; :: thesis: (0. K,(len A),(width A)) . i = A1 . i
i in NAT by ORDINAL1:def 13;
then A39: ( i in Seg (len A) & dom A1 = Seg (len A1) & len A1 = len A ) by A38, FINSEQ_1:def 3, MATRIX_1:def 3;
hence (0. K,(len A),(width A)) . i = (width A) |-> (0. K) by FINSEQ_2:71
.= Line A1,i by A36, A39, A15
.= A1 . i by A39, MATRIX_2:10 ;
:: thesis: verum

end;

then 0. K,(len A),(width A) = A1 by A37, FINSEQ_1:18;
then A40: the_rank_of A = 0 by A13, A37, MATRIX13:95;
then A41: 0. K,(len A),(width A) = A by MATRIX13:95;
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 A42: the_rank_of A = the_rank_of (A ^^ B) ; :: thesis: not Solutions_of A,B is empty
A43: Segm (A' ^^ B'),(Seg (len A)),((Seg ((width A) + (width B))) \ (Seg (width A))) = B by Th19;
(Seg ((width A) + (width B))) \ (Seg (width A)) c= Seg ((width A) + (width B)) by XBOOLE_1:36;
then [:(Seg (len A)),((Seg ((width A) + (width B))) \ (Seg (width A))):] c= Indices (A ^^ B) by A37, ZFMISC_1:118;
then 0 >= the_rank_of B by A40, A43, A42, MATRIX13:79;
then 0 = the_rank_of B ;
then A44: B = 0. K,(len A),(width B) by A1, MATRIX13:95;
consider x being Matrix of width A, width B,K;
( ( width A = 0 & width B = 0 ) or Solutions_of A',B' = { X where X is Matrix of width A, width B,K : verum } ) by A41, A44, A1, A17, Th54;
then ( Solutions_of A',B' = {{} } or x in Solutions_of A',B' ) by Th56, A41, A44;
hence not Solutions_of A,B is empty ; :: thesis: verum

end;

thus ( not Solutions_of A,B is empty implies the_rank_of A = the_rank_of (A ^^ B) ) :: thesis: verum

proof

assume A45: 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 the_rank_of (A' ^^ B') > 0 by A40;
then consider i, j being Nat such that
A46: ( [i,j] in Indices (A' ^^ B') & (A' ^^ B') * i,j <> 0. K ) by MATRIX13:94;
A47: ( i in Seg (len A) & j in Seg ((width A) + (width B)) & len (Line A',i) = width A ) by A37, A46, FINSEQ_1:def 18, ZFMISC_1:106;
then A48: ( dom (Line (A' ^^ B'),i) = Seg ((width A) + (width B)) & dom (Line A',i) = Seg (width A) & dom (Line B',i) = Seg (width B) & Line (A' ^^ B'),i = (Line A',i) ^ (Line B',i) ) by A37, Th15, FINSEQ_2:144;

per cases ( j in dom (Line A',i) or ex n being Nat st
( n in dom (Line B',i) & j = (width A) + n ) ) by A47, A48, FINSEQ_1:38;

suppose A49: j in dom (Line A',i) ; :: thesis: contradiction

then A50: [i,j] in Indices (0. K,(len A),(width A)) by A37, A47, A48, ZFMISC_1:106;
(A' ^^ B') * i,j = (Line (A' ^^ B'),i) . j by A37, A47, MATRIX_1:def 8
.= (Line A',i) . j by A48, A49, FINSEQ_1:def 7
.= A' * i,j by A48, A49, MATRIX_1:def 8
.= 0. K by A50, A41, MATRIX_3:3 ;
hence contradiction by A46; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom (Line B',i) & j = (width A) + n ) ; :: thesis: contradiction

then consider n being Nat such that
A51: ( n in dom (Line B',i) & j = (width A) + n ) ;
A52: ( [i,n] in Indices B & B = 0. K,(len A),(width B) ) by A37, A41, A45, A47, A48, A51, Th52, ZFMISC_1:106;
(A' ^^ B') * i,j = (Line (A' ^^ B'),i) . j by A37, A47, MATRIX_1:def 8
.= (Line B',i) . n by A47, A48, A51, FINSEQ_1:def 7
.= B' * i,n by A48, A51, MATRIX_1:def 8
.= 0. K by A52, MATRIX_3:3 ;
hence contradiction by A46; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;