let K be Field; for A being Matrix of K
for P, Q, Q9 being finite without_zero Subset of NAT st [:P,Q9:] c= Indices A holds
for i, j being Nat st i in (dom A) \ P & j in (Seg (width A)) \ Q & A * (i,j) <> 0. K & Q c= Q9 & (Line (A,i)) * (Sgm Q9) = (card Q9) |-> (0. K) holds
the_rank_of A > the_rank_of (Segm (A,P,Q))
let A be Matrix of K; for P, Q, Q9 being finite without_zero Subset of NAT st [:P,Q9:] c= Indices A holds
for i, j being Nat st i in (dom A) \ P & j in (Seg (width A)) \ Q & A * (i,j) <> 0. K & Q c= Q9 & (Line (A,i)) * (Sgm Q9) = (card Q9) |-> (0. K) holds
the_rank_of A > the_rank_of (Segm (A,P,Q))
let P, Q, R be finite without_zero Subset of NAT; ( [:P,R:] c= Indices A implies for i, j being Nat st i in (dom A) \ P & j in (Seg (width A)) \ Q & A * (i,j) <> 0. K & Q c= R & (Line (A,i)) * (Sgm R) = (card R) |-> (0. K) holds
the_rank_of A > the_rank_of (Segm (A,P,Q)) )
assume A1:
[:P,R:] c= Indices A
; for i, j being Nat st i in (dom A) \ P & j in (Seg (width A)) \ Q & A * (i,j) <> 0. K & Q c= R & (Line (A,i)) * (Sgm R) = (card R) |-> (0. K) holds
the_rank_of A > the_rank_of (Segm (A,P,Q))
let i, j be Nat; ( i in (dom A) \ P & j in (Seg (width A)) \ Q & A * (i,j) <> 0. K & Q c= R & (Line (A,i)) * (Sgm R) = (card R) |-> (0. K) implies the_rank_of A > the_rank_of (Segm (A,P,Q)) )
assume that
A2:
i in (dom A) \ P
and
A3:
j in (Seg (width A)) \ Q
and
A4:
A * (i,j) <> 0. K
and
A5:
Q c= R
and
A6:
(Line (A,i)) * (Sgm R) = (card R) |-> (0. K)
; the_rank_of A > the_rank_of (Segm (A,P,Q))
A7:
dom A = Seg (len A)
by FINSEQ_1:def 3;
then A8:
i in Seg (len A)
by A2, XBOOLE_0:def 5;
A9:
[:P,Q:] c= [:P,R:]
by A5, ZFMISC_1:95;
then A10:
[:P,Q:] c= Indices A
by A1;
reconsider i0 = i, j0 = j as non zero Element of NAT by A2, A3, A7;
A11:
j in Seg (width A)
by A3, XBOOLE_0:def 5;
set S = Segm (A,P,Q);
consider P9, Q9 being finite without_zero Subset of NAT such that
A12:
[:P9,Q9:] c= Indices (Segm (A,P,Q))
and
A13:
card P9 = card Q9
and
A14:
card P9 = the_rank_of (Segm (A,P,Q))
and
A15:
Det (EqSegm ((Segm (A,P,Q)),P9,Q9)) <> 0. K
by MATRIX13:def 4;
( P9 = {} iff Q9 = {} )
by A13;
then consider P2, Q2 being finite without_zero Subset of NAT such that
A16:
P2 c= P
and
A17:
Q2 c= Q
and
P2 = (Sgm P) .: P9
and
Q2 = (Sgm Q) .: Q9
and
A18:
card P2 = card P9
and
A19:
card Q2 = card Q9
and
A20:
Segm ((Segm (A,P,Q)),P9,Q9) = Segm (A,P2,Q2)
by A12, MATRIX13:57;
set Q2j = Q2 \/ {j0};
set P2i = P2 \/ {i0};
set ESS = EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}));
set SS = Segm (A,(P2 \/ {i0}),(Q2 \/ {j0}));
per cases
( [:P,Q:] = {} or [:P,Q:] <> {} )
;
suppose
[:P,Q:] = {}
;
the_rank_of A > the_rank_of (Segm (A,P,Q))then
(
card P = 0 or
card Q = 0 )
by CARD_1:27, ZFMISC_1:90;
then A21:
the_rank_of (Segm (A,P,Q)) = 0
by MATRIX13:77;
[i,j] in Indices A
by A7, A8, A11, ZFMISC_1:87;
hence
the_rank_of A > the_rank_of (Segm (A,P,Q))
by A4, A21, MATRIX13:94;
verum end; suppose A22:
[:P,Q:] <> {}
;
the_rank_of A > the_rank_of (Segm (A,P,Q))then
P c= dom A
by A10, ZFMISC_1:114;
then A23:
P2 c= dom A
by A16;
[:P,R:] <> {}
by A9, A22, XBOOLE_1:3;
then A24:
R c= Seg (width A)
by A1, ZFMISC_1:114;
then A25:
dom (Sgm R) = Seg (card R)
by FINSEQ_3:40;
Q c= Seg (width A)
by A10, A22, ZFMISC_1:114;
then A26:
Q2 c= Seg (width A)
by A17;
A27:
{j0} c= Seg (width A)
by A11, ZFMISC_1:31;
then A28:
Sgm (Q2 \/ {j0}) is
one-to-one
by A26, FINSEQ_3:92, XBOOLE_1:8;
A29:
Q2 \/ {j0} c= Seg (width A)
by A26, A27, XBOOLE_1:8;
then A30:
rng (Sgm (Q2 \/ {j0})) = Q2 \/ {j0}
by FINSEQ_1:def 13;
A31:
{i0} c= dom A
by A7, A8, ZFMISC_1:31;
then A32:
P2 \/ {i0} c= dom A
by A23, XBOOLE_1:8;
then A33:
[:(P2 \/ {i0}),(Q2 \/ {j0}):] c= Indices A
by A29, ZFMISC_1:96;
A34:
dom (Sgm (P2 \/ {i0})) = Seg (card (P2 \/ {i0}))
by A7, A23, A31, FINSEQ_3:40, XBOOLE_1:8;
i in {i}
by TARSKI:def 1;
then A35:
i in P2 \/ {i0}
by XBOOLE_0:def 3;
A36:
not
i in P2
by A2, A16, XBOOLE_0:def 5;
then A37:
card (P2 \/ {i0}) = (card P2) + 1
by CARD_2:41;
then A38:
(card (P2 \/ {i0})) -' 1
= card P9
by A18, NAT_D:34;
A39:
not
j in Q2
by A3, A17, XBOOLE_0:def 5;
then A40:
card (Q2 \/ {j0}) = (card Q2) + 1
by CARD_2:41;
then A41:
EqSegm (
A,
(P2 \/ {i0}),
(Q2 \/ {j0}))
= Segm (
A,
(P2 \/ {i0}),
(Q2 \/ {j0}))
by A13, A18, A19, A36, CARD_2:41, MATRIX13:def 3;
j in {j}
by TARSKI:def 1;
then
j in Q2 \/ {j0}
by XBOOLE_0:def 3;
then consider y being
object such that A42:
y in dom (Sgm (Q2 \/ {j0}))
and A43:
(Sgm (Q2 \/ {j0})) . y = j
by A30, FUNCT_1:def 3;
rng (Sgm (P2 \/ {i0})) = P2 \/ {i0}
by A7, A32, FINSEQ_1:def 13;
then consider x being
object such that A44:
x in dom (Sgm (P2 \/ {i0}))
and A45:
(Sgm (P2 \/ {i0})) . x = i
by A35, FUNCT_1:def 3;
reconsider x =
x,
y =
y as
Element of
NAT by A44, A42;
- (1_ K) <> 0. K
by VECTSP_1:28;
then A46:
(power K) . (
(- (1_ K)),
(x + y))
<> 0. K
by Lm2;
set L =
LaplaceExpL (
(EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),
x);
A47:
dom (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) =
Seg (len (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)))
by FINSEQ_1:def 3
.=
Seg (card (P2 \/ {i0}))
by LAPLACE:def 7
;
then A48:
y in dom (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x))
by A13, A18, A19, A26, A27, A37, A40, A42, FINSEQ_3:40, XBOOLE_1:8;
A49:
dom (Sgm (Q2 \/ {j0})) = Seg (card (Q2 \/ {j0}))
by A26, A27, FINSEQ_3:40, XBOOLE_1:8;
then Delete (
(EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),
x,
y) =
EqSegm (
A,
((P2 \/ {i0}) \ {i}),
((Q2 \/ {j0}) \ {j}))
by A13, A18, A19, A37, A40, A34, A44, A45, A42, A43, MATRIX13:64
.=
EqSegm (
A,
P2,
((Q2 \/ {j0}) \ {j}))
by A36, ZFMISC_1:117
.=
EqSegm (
A,
P2,
Q2)
by A39, ZFMISC_1:117
.=
Segm (
A,
P2,
Q2)
by A13, A18, A19, MATRIX13:def 3
.=
EqSegm (
(Segm (A,P,Q)),
P9,
Q9)
by A13, A20, MATRIX13:def 3
;
then A50:
((power K) . ((- (1_ K)),(x + y))) * (Det (Delete ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x,y))) <> 0. K
by A15, A38, A46, VECTSP_1:12;
A51:
Indices (EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))) = [:(Seg (card (P2 \/ {i0}))),(Seg (card (P2 \/ {i0}))):]
by MATRIX_0:24;
then A52:
[x,y] in Indices (EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0})))
by A13, A18, A19, A37, A40, A34, A49, A44, A42, ZFMISC_1:87;
A53:
rng (Sgm R) = R
by A24, FINSEQ_1:def 13;
now for k being Nat st k in dom (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) & k <> y holds
(LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) . k = 0. Klet k be
Nat;
( k in dom (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) & k <> y implies (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) . k = 0. K )assume that A54:
k in dom (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x))
and A55:
k <> y
;
(LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) . k = 0. K
(Sgm (Q2 \/ {j0})) . k <> j
by A13, A18, A19, A37, A40, A49, A28, A42, A43, A47, A54, A55, FUNCT_1:def 4;
then A56:
not
(Sgm (Q2 \/ {j0})) . k in {j}
by TARSKI:def 1;
(Sgm (Q2 \/ {j0})) . k in Q2 \/ {j0}
by A13, A18, A19, A37, A40, A30, A49, A47, A54, FUNCT_1:def 3;
then
(Sgm (Q2 \/ {j0})) . k in Q2
by A56, XBOOLE_0:def 3;
then A57:
(Sgm (Q2 \/ {j0})) . k in Q
by A17;
then A58:
(Sgm (Q2 \/ {j0})) . k in R
by A5;
consider z being
object such that A59:
z in dom (Sgm R)
and A60:
(Sgm R) . z = (Sgm (Q2 \/ {j0})) . k
by A5, A53, A57, FUNCT_1:def 3;
reconsider z =
z as
Element of
NAT by A59;
[x,k] in Indices (EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0})))
by A34, A44, A47, A51, A54, ZFMISC_1:87;
then (EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))) * (
x,
k) =
A * (
i,
((Sgm (Q2 \/ {j0})) . k))
by A45, A41, MATRIX13:def 1
.=
(Line (A,i)) . ((Sgm R) . z)
by A24, A60, A58, MATRIX_0:def 7
.=
((card R) |-> (0. K)) . z
by A6, A59, FUNCT_1:13
.=
0. K
by A25, A59, FINSEQ_2:57
;
hence (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) . k =
(0. K) * (Cofactor ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x,k))
by A54, LAPLACE:def 7
.=
0. K
;
verum end; then A61:
(LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) . y =
Sum (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x))
by A48, MATRIX_3:12
.=
Det (EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0})))
by A34, A44, LAPLACE:25
;
(LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) . y =
((Segm (A,(P2 \/ {i0}),(Q2 \/ {j0}))) * (x,y)) * (Cofactor ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x,y))
by A48, A41, LAPLACE:def 7
.=
(A * (i,j)) * (((power K) . ((- (1_ K)),(x + y))) * (Det (Delete ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x,y))))
by A45, A43, A41, A52, MATRIX13:def 1
;
then
Det (EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))) <> 0. K
by A4, A61, A50, VECTSP_1:12;
then
the_rank_of A >= card (P2 \/ {i0})
by A13, A18, A19, A37, A40, A33, MATRIX13:def 4;
hence
the_rank_of A > the_rank_of (Segm (A,P,Q))
by A14, A18, A37, NAT_1:13;
verum end;