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_2:7;
reconsider A9 = A as Matrix of len A, width A,K by MATRIX_2:7;
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 by A3, A5, FINSEQ_1:4, FINSEQ_1:def 3;
then A7: width (A9 ^^ B9) = (width A) + (width B) by MATRIX_1:24;
then width A <= width (A9 ^^ B9) by NAT_1:11;
then A8: Seg (width A) c= Seg (width (A9 ^^ B9)) by FINSEQ_1:7;
A9: card (Seg (len A)) = len A by FINSEQ_1:78;
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:54
.= i by A3, A5, A11, FINSEQ_2:57 ;
card (Seg (width A)) = width A by FINSEQ_1:78;
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:139;
A16: ( len (Line A9,i) = width A9 & 1 <= j ) by A14, FINSEQ_1:3, MATRIX_1:def 8;
len (Line B9,i) = width B9 by MATRIX_1:def 8;
then A17: j <= len (Line B9,i) by A14, FINSEQ_1:3;
A18: j + (width A) in Seg (width (A9 ^^ B9)) by A14, A7, FINSEQ_1:81;
then (A9 ^^ B9) * i,(j + (width A)) = (Line (A9 ^^ B9),i) . (j + (width A)) by MATRIX_1:def 8
.= ((Line A9,i) ^ (Line B9,i)) . (j + (width A)) by A3, A5, A11, Th15
.= (Line B9,i) . j by A16, A17, FINSEQ_1:86 ;
then A19: (A9 ^^ B9) * i,(j + (width A)) <> 0. K by A14, A15, FINSEQ_2:71;
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_1:24;
then A30: [:P2,(Seg (width A)):] c= Indices (A9 ^^ B9) by A24, A8, ZFMISC_1:119;
j >= 1 by A14, FINSEQ_1:3;
then j + (width A) >= 1 + (width A) by XREAL_1:8;
then j + (width A) > width A by NAT_1:13;
then not j + (width A) in Q2 by A25, FINSEQ_1:3;
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:71 ;
A33: Sgm (Seg (len A)) = idseq (len A) by FINSEQ_3:54
.= id (Seg (len A)) ;
A34: P c= Seg (len A) by A20, A21, MATRIX13:67;
then A35: rng (Sgm P) = P by FINSEQ_1:def 13;
assume i in P2 ; :: thesis: contradiction
then i in P by A26, A33, A34, FUNCT_1:162;
then consider x being set such that
A36: x in dom (Sgm P) and
A37: (Sgm P) . x = i by A35, FUNCT_1:def 5;
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;
then A40: rng (Sgm Q) = Q by FINSEQ_1:def 13;
A41: dom (Sgm P) = Seg (card P) by A34, FINSEQ_3:45;
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:144, 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, VECTSP_1:36; :: 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