let K be Field; 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; ( 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
; 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; ( 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)
; for i being Nat st i in N holds
Line (B,i) = (width B) |-> (0. K)
let i be Nat; ( i in N implies Line (B,i) = (width B) |-> (0. K) )
assume A5:
i in N
; 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)
; 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;
then A35:
rng (Sgm P) = P
by FINSEQ_1:def 13;
assume
i in P2
;
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;
then A40:
rng (Sgm Q) = Q
by FINSEQ_1:def 13;
A41:
dom (Sgm P) = Seg (card P)
by A34, 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;
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; verum