let K be Field; :: thesis: for A, B being Matrix of K st the_rank_of A = the_rank_of (A ^^ B) & len A = len B holds
for N being finite without_zero Subset of NAT st N c= dom A & ( for i being Nat st i in N holds
Line (A,i) = (width A) |-> (0. K) ) holds
for i being Nat st i in N holds
Line (B,i) = (width B) |-> (0. K)
let A, B be Matrix of K; :: thesis: ( the_rank_of A = the_rank_of (A ^^ B) & len A = len B implies for N being finite without_zero Subset of NAT st N c= dom A & ( for i being Nat st i in N holds
Line (A,i) = (width A) |-> (0. K) ) holds
for i being Nat st i in N holds
Line (B,i) = (width B) |-> (0. K) )
assume that
A1: the_rank_of A = the_rank_of (A ^^ B) and
A2: len A = len B ; :: thesis: for N being finite without_zero Subset of NAT st N c= dom A & ( for i being Nat st i in N holds
Line (A,i) = (width A) |-> (0. K) ) holds
for i being Nat st i in N holds
Line (B,i) = (width B) |-> (0. K)
reconsider B9 = B as Matrix of len A, width B,K by A2, MATRIX_0:51;
reconsider A9 = A as Matrix of len A, width A,K by MATRIX_0:51;
set AB = A9 ^^ B9;
let N be finite without_zero Subset of NAT; :: thesis: ( N c= dom A & ( for i being Nat st i in N holds
Line (A,i) = (width A) |-> (0. K) ) implies for i being Nat st i in N holds
Line (B,i) = (width B) |-> (0. K) )
assume that
A3: N c= dom A and
A4: for i being Nat st i in N holds
Line (A,i) = (width A) |-> (0. K) ; :: thesis: for i being Nat st i in N holds
Line (B,i) = (width B) |-> (0. K)
let i be Nat; :: thesis: ( i in N implies Line (B,i) = (width B) |-> (0. K) )
assume A5: i in N ; :: thesis: Line (B,i) = (width B) |-> (0. K)
dom A <> {} by A3, A5;
then Seg (len A) <> {} by FINSEQ_1:def 3;
then A6: len A <> 0 ;
then A7: width (A9 ^^ B9) = (width A) + (width B) by MATRIX_0:23;
then width A <= width (A9 ^^ B9) by NAT_1:11;
then A8: Seg (width A) c= Seg (width (A9 ^^ B9)) by FINSEQ_1:5;
A9: card (Seg (len A)) = len A by FINSEQ_1:57;
A10: Segm ((A9 ^^ B9),(Seg (len A)),(Seg (width A))) = A by Th19;
A11: dom A = Seg (len A) by FINSEQ_1:def 3;
A12: (Sgm (Seg (len A))) . i = (idseq (len A)) . i by FINSEQ_3:48
.= i by A3, A5, A11, FINSEQ_2:49 ;
card (Seg (width A)) = width A by FINSEQ_1:57;
then A13: (card (Seg (width A))) |-> (0. K) = Line (A,i) by A4, A5
.= (Line ((A9 ^^ B9),i)) * (Sgm (Seg (width A))) by A3, A5, A11, A10, A8, A9, A12, MATRIX13:47 ;
assume Line (B,i) <> (width B) |-> (0. K) ; :: thesis: contradiction
then consider j being Nat such that
A14: j in Seg (width B) and
A15: (Line (B,i)) . j <> ((width B) |-> (0. K)) . j by FINSEQ_2:119;
A16: ( len (Line (A9,i)) = width A9 & 1 <= j ) by A14, FINSEQ_1:1, MATRIX_0:def 7;
len (Line (B9,i)) = width B9 by MATRIX_0:def 7;
then A17: j <= len (Line (B9,i)) by A14, FINSEQ_1:1;
A18: j + (width A) in Seg (width (A9 ^^ B9)) by A14, A7, FINSEQ_1:60;
then (A9 ^^ B9) * (i,(j + (width A))) = (Line ((A9 ^^ B9),i)) . (j + (width A)) by MATRIX_0:def 7
.= ((Line (A9,i)) ^ (Line (B9,i))) . (j + (width A)) by A3, A5, A11, Th15
.= (Line (B9,i)) . j by A16, A17, FINSEQ_1:65 ;
then A19: (A9 ^^ B9) * (i,(j + (width A))) <> 0. K by A14, A15, FINSEQ_2:57;
consider P, Q being finite without_zero Subset of NAT such that
A20: [:P,Q:] c= Indices A9 and
A21: card P = card Q and
A22: card P = the_rank_of A9 and
A23: Det (EqSegm (A9,P,Q)) <> 0. K by MATRIX13:def 4;
( P = {} iff Q = {} ) by A21;
then consider P2, Q2 being finite without_zero Subset of NAT such that
A24: P2 c= Seg (len A) and
A25: Q2 c= Seg (width A) and
A26: P2 = (Sgm (Seg (len A))) .: P and
Q2 = (Sgm (Seg (width A))) .: Q and
card P2 = card P and
card Q2 = card Q and
A27: Segm (A,P,Q) = Segm ((A9 ^^ B9),P2,Q2) by A20, A10, MATRIX13:57;
A28: Segm ((A9 ^^ B9),P2,Q2) = EqSegm (A,P,Q) by A21, A27, MATRIX13:def 3;
A29: ( dom (A9 ^^ B9) = Seg (len (A9 ^^ B9)) & len (A9 ^^ B9) = len A ) by A6, FINSEQ_1:def 3, MATRIX_0:23;
then A30: [:P2,(Seg (width A)):] c= Indices (A9 ^^ B9) by A24, A8, ZFMISC_1:96;
j >= 1 by A14, FINSEQ_1:1;
then j + (width A) >= 1 + (width A) by XREAL_1:6;
then j + (width A) > width A by NAT_1:13;
then not j + (width A) in Q2 by A25, FINSEQ_1:1;
then A31: j + (width A) in (Seg (width (A9 ^^ B9))) \ Q2 by A18, XBOOLE_0:def 5;
not i in P2

proof

A32: Line (A,i) = (width A) |-> (0. K) by A4, A5
.= (0. K) * (Line (A,i)) by FVSUM_1:58 ;
A33: Sgm (Seg (len A)) = idseq (len A) by FINSEQ_3:48
.= id (Seg (len A)) ;
A34: P c= Seg (len A) by A20, A21, MATRIX13:67;
A35: rng (Sgm P) = P by FINSEQ_1:def 14;
assume i in P2 ; :: thesis: contradiction
then i in P by A26, A33, A34, FUNCT_1:92;
then consider x being object such that
A36: x in dom (Sgm P) and
A37: (Sgm P) . x = i by A35, FUNCT_1:def 3;
reconsider x = x as Element of NAT by A36;
A38: Segm (A,P,Q) = EqSegm (A,P,Q) by A21, MATRIX13:def 3;
A39: Q c= Seg (width A) by A20, A21, MATRIX13:67;
A40: rng (Sgm Q) = Q by FINSEQ_1:def 14;
A41: dom (Sgm P) = Seg (card P) by FINSEQ_3:40;
then ( dom (Line (A,i)) = Seg (width A) & Line ((Segm (A,P,Q)),x) = (Line (A,i)) * (Sgm Q) ) by A39, A36, A37, FINSEQ_2:124, MATRIX13:47;
then Line ((Segm (A,P,Q)),x) = (0. K) * (Line ((Segm (A,P,Q)),x)) by A39, A40, A32, MATRIX13:87;
then (0. K) * (Det (EqSegm (A,P,Q))) = Det (RLine ((EqSegm (A,P,Q)),x,(Line ((EqSegm (A,P,Q)),x)))) by A41, A36, A38, MATRIX11:35
.= Det (EqSegm (A,P,Q)) by MATRIX11:30 ;
hence contradiction by A23; :: thesis: verum

end;

then i in (dom (A9 ^^ B9)) \ P2 by A3, A5, A11, A29, XBOOLE_0:def 5;
then card P > the_rank_of (Segm ((A9 ^^ B9),P2,Q2)) by A1, A19, A22, A25, A30, A31, A13, Th10;
hence contradiction by A23, A28, MATRIX13:83; :: thesis: verum