let n', m', j, i be Nat; :: thesis: for K being Field
for a being Element of K
for M' being Matrix of n',m',K st j in Seg (len M') & ( i = j implies a <> - (1_ K) ) holds
the_rank_of M' = the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j))))
let K be Field; :: thesis: for a being Element of K
for M' being Matrix of n',m',K st j in Seg (len M') & ( i = j implies a <> - (1_ K) ) holds
the_rank_of M' = the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j))))
let a be Element of K; :: thesis: for M' being Matrix of n',m',K st j in Seg (len M') & ( i = j implies a <> - (1_ K) ) holds
the_rank_of M' = the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j))))
let M' be Matrix of n',m',K; :: thesis: ( j in Seg (len M') & ( i = j implies a <> - (1_ K) ) implies the_rank_of M' = the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j)))) )
assume that
A1:
j in Seg (len M')
and
A2:
( i = j implies a <> - (1_ K) )
; :: thesis: the_rank_of M' = the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j))))
per cases
( not i in Seg (len M') or i in Seg (len M') )
;
suppose A3:
i in Seg (len M')
;
:: thesis: the_rank_of M' = the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j))))set Li =
Line M',
i;
set Lj =
Line M',
j;
set R =
RLine M',
i,
((Line M',i) + (a * (Line M',j)));
set W =
width M';
set KK = the
carrier of
K;
A4:
(
len ((Line M',i) + (a * (Line M',j))) = width M' &
len M' = n' &
len (Line M',i) = width M' &
len (Line M',j) = width M' &
len (a * (Line M',j)) = width M' )
by FINSEQ_1:def 18, MATRIX_1:def 3;
then A5:
(
Line (RLine M',i,((Line M',i) + (a * (Line M',j)))),
i = (Line M',i) + (a * (Line M',j)) &
dom (Line M',i) = Seg (width M') &
dom (Line M',j) = Seg (width M') &
dom (a * (Line M',j)) = Seg (width M') &
width M' = width (RLine M',i,((Line M',i) + (a * (Line M',j)))) )
by A3, FINSEQ_1:def 3, MATRIX11:28, MATRIX11:def 3;
reconsider Li' =
Line M',
i,
Lj' =
Line M',
j,
LL =
(Line M',i) + (a * (Line M',j)) as
Element of the
carrier of
K * by FINSEQ_1:def 11;
A6:
RLine (RLine M',i,((Line M',i) + (a * (Line M',j)))),
i,
(Line M',i) =
Replace (RLine M',i,((Line M',i) + (a * (Line M',j)))),
i,
Li'
by A4, A5, MATRIX11:29
.=
Replace (Replace M',i,LL),
i,
Li'
by A4, MATRIX11:29
.=
Replace M',
i,
Li'
by FUNCT_7:36
.=
RLine M',
i,
(Line M',i)
by A4, MATRIX11:29
.=
M'
by MATRIX11:30
;
A7:
RLine (RLine M',i,((Line M',i) + (a * (Line M',j)))),
i,
(Line M',j) =
Replace (RLine M',i,((Line M',i) + (a * (Line M',j)))),
i,
Lj'
by A4, A5, MATRIX11:29
.=
Replace (Replace M',i,LL),
i,
Lj'
by A4, MATRIX11:29
.=
Replace M',
i,
Lj'
by FUNCT_7:36
.=
RLine M',
i,
(Line M',j)
by A4, MATRIX11:29
;
consider P,
Q being
finite without_zero Subset of
NAT such that A8:
(
[:P,Q:] c= Indices (RLine M',i,((Line M',i) + (a * (Line M',j)))) &
card P = card Q )
and A9:
(
card P = the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j)))) &
Det (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P,Q) <> 0. K )
by Def4;
A10:
(
EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),
P,
Q = Segm (RLine M',i,((Line M',i) + (a * (Line M',j)))),
P,
Q &
EqSegm M',
P,
Q = Segm M',
P,
Q )
by A8, Def3;
A11:
Indices (RLine M',i,((Line M',i) + (a * (Line M',j)))) = Indices M'
by MATRIX_1:27;
A12:
now per cases
( not i in P or i in P )
;
suppose
not
i in P
;
:: thesis: the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j)))) <= the_rank_of M'then
Segm M',
P,
Q = Segm (RLine M',i,((Line M',i) + (a * (Line M',j)))),
P,
Q
by A8, A11, Th60;
hence
the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j)))) <= the_rank_of M'
by A8, A9, A10, A11, Def4;
:: thesis: verum end; suppose A13:
i in P
;
:: thesis: the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j)))) <= the_rank_of M'consider k being
Nat such that A14:
P c= Seg k
by Th43;
rng (Sgm P) = P
by A14, FINSEQ_1:def 13;
then consider m being
set such that A15:
(
m in dom (Sgm P) &
(Sgm P) . m = i )
by A13, FUNCT_1:def 5;
A16:
dom (Sgm P) = Seg (card P)
by A14, FINSEQ_3:45;
reconsider m =
m as
Element of
NAT by A15;
A17:
(
Q c= Seg (width M') &
Q c= Seg (width (RLine M',i,((Line M',i) + (a * (Line M',j))))) )
by A8, A11, Th67;
then A18:
rng (Sgm Q) c= Seg (width M')
by FINSEQ_1:def 13;
then A19:
(
dom ((Line M',j) * (Sgm Q)) = dom (Sgm Q) &
dom (Sgm Q) = Seg (card Q) )
by A5, A17, FINSEQ_3:45, RELAT_1:46;
then reconsider LjQ =
(Line M',j) * (Sgm Q) as
FinSequence by FINSEQ_1:def 2;
(
rng LjQ c= rng (Line M',j) &
rng (Line M',j) c= the
carrier of
K )
by FINSEQ_1:def 4, RELAT_1:45;
then
rng LjQ c= the
carrier of
K
by XBOOLE_1:1;
then reconsider LjQ =
LjQ as
FinSequence of
K by FINSEQ_1:def 4;
set SR =
EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),
P,
Q;
set SM =
EqSegm M',
P,
Q;
A20:
(
len LjQ = card P &
len (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P,Q) = card P &
len LjQ = len (a * LjQ) )
by A8, A19, FINSEQ_1:def 3, MATRIXR1:16, MATRIX_1:def 3;
A21:
(
len (Line (EqSegm M',P,Q),m) = width (EqSegm M',P,Q) &
width (EqSegm M',P,Q) = card P &
card P = len (EqSegm M',P,Q) )
by MATRIX_1:25, MATRIX_1:def 8;
A22:
(
Line (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P,Q),
m = (Line (RLine M',i,((Line M',i) + (a * (Line M',j)))),i) * (Sgm Q) &
Line (EqSegm M',P,Q),
m = (Line M',i) * (Sgm Q) )
by A10, A15, A16, A17, Th47;
A23:
a * LjQ = (a * (Line M',j)) * (Sgm Q)
by A5, A18, Th87;
A24:
(
RLine (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P,Q),
m,
(Line (EqSegm M',P,Q),m) = Segm M',
P,
Q &
RLine (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P,Q),
m,
LjQ = Segm (RLine M',i,(Line M',j)),
P,
Q &
Segm (RLine M',i,(Line M',j)),
P,
Q = EqSegm (RLine M',i,(Line M',j)),
P,
Q )
by A4, A5, A6, A7, A8, A10, A15, A22, Def3, Th59;
EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),
P,
Q =
RLine (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P,Q),
m,
(Line (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P,Q),m)
by MATRIX11:30
.=
RLine (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P,Q),
m,
((Line (EqSegm M',P,Q),m) + (a * LjQ))
by A5, A18, A22, A23, Th88
;
then A25:
Det (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P,Q) =
(Det (RLine (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P,Q),m,(Line (EqSegm M',P,Q),m))) + (Det (RLine (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P,Q),m,(a * LjQ)))
by A15, A16, A20, A21, MATRIX11:36
.=
(Det (RLine (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P,Q),m,(Line (EqSegm M',P,Q),m))) + (a * (Det (RLine (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P,Q),m,LjQ)))
by A15, A16, A20, MATRIX11:34
.=
(Det (EqSegm M',P,Q)) + (a * (Det (EqSegm (RLine M',i,(Line M',j)),P,Q)))
by A8, A24, Def3
;
per cases
( Det (EqSegm M',P,Q) <> 0. K or Det (EqSegm M',P,Q) = 0. K )
;
suppose A26:
Det (EqSegm M',P,Q) = 0. K
;
:: thesis: the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j)))) <= the_rank_of M'reconsider j0 =
j as non
zero Element of
NAT by A1;
per cases
( i = j or ( i <> j & j in P ) or ( i <> j & not j in P ) )
;
suppose
i = j
;
:: thesis: the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j)))) <= the_rank_of M'then Det (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P,Q) =
(Det (EqSegm M',P,Q)) + (a * (Det (EqSegm M',P,Q)))
by A25, MATRIX11:30
.=
((1_ K) * (Det (EqSegm M',P,Q))) + (a * (Det (EqSegm M',P,Q)))
by VECTSP_1:def 13
.=
((1_ K) + a) * (Det (EqSegm M',P,Q))
by VECTSP_1:def 18
;
hence
the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j)))) <= the_rank_of M'
by A9, A26, VECTSP_1:44;
:: thesis: verum end; suppose A27:
(
i <> j &
j in P )
;
:: thesis: the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j)))) <= the_rank_of M'
rng (Sgm P) = P
by A14, FINSEQ_1:def 13;
then consider l being
set such that A28:
(
l in dom (Sgm P) &
(Sgm P) . l = j0 )
by A27, FUNCT_1:def 5;
reconsider l =
l as
Element of
NAT by A28;
A29:
RLine (EqSegm M',P,Q),
m,
(Line (EqSegm M',P,Q),l) = EqSegm (RLine M',i,(Line M',j)),
P,
Q
by A4, A8, A10, A11, A15, A16, A17, A24, A28, Th47, Th59;
0. K = Det (RLine (EqSegm M',P,Q),m,(Line (EqSegm M',P,Q),l))
by A15, A16, A27, A28, MATRIX11:51;
then 0. K =
a * (Det (RLine (EqSegm M',P,Q),m,(Line (EqSegm M',P,Q),l)))
by VECTSP_1:44
.=
(Det (EqSegm M',P,Q)) + (a * (Det (EqSegm (RLine M',i,(Line M',j)),P,Q)))
by A26, A29, RLVECT_1:def 7
;
hence
the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j)))) <= the_rank_of M'
by A9, A25;
:: thesis: verum end; suppose A30:
(
i <> j & not
j in P )
;
:: thesis: the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j)))) <= the_rank_of M'set Pij =
(P \ {i}) \/ {j0};
a * (Det (EqSegm (RLine M',i,(Line M',j)),P,Q)) <> 0. K
by A9, A25, A26, RLVECT_1:def 7;
then A31:
Det (EqSegm (RLine M',i,(Line M',j)),P,Q) <> 0. K
by VECTSP_1:44;
(
Det (EqSegm (RLine M',i,(Line M',j)),P,Q) = Det (EqSegm M',((P \ {i}) \/ {j0}),Q) or
Det (EqSegm (RLine M',i,(Line M',j)),P,Q) = - (Det (EqSegm M',((P \ {i}) \/ {j0}),Q)) )
by A1, A3, A4, A8, A11, A13, A30, Th68;
then
(
Det (EqSegm M',((P \ {i}) \/ {j0}),Q) <> 0. K &
card P = card ((P \ {i}) \/ {j0}) &
[:((P \ {i}) \/ {j0}),Q:] c= Indices M' )
by A1, A3, A4, A8, A11, A13, A30, A31, Th68, VECTSP_2:34;
hence
the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j)))) <= the_rank_of M'
by A8, A9, Def4;
:: thesis: verum end; end; end; consider P1,
Q1 being
finite without_zero Subset of
NAT such that A32:
(
[:P1,Q1:] c= Indices M' &
card P1 = card Q1 )
and A33:
(
card P1 = the_rank_of M' &
Det (EqSegm M',P1,Q1) <> 0. K )
by Def4;
A34:
(
EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),
P1,
Q1 = Segm (RLine M',i,((Line M',i) + (a * (Line M',j)))),
P1,
Q1 &
EqSegm M',
P1,
Q1 = Segm M',
P1,
Q1 )
by A32, Def3;
now per cases
( not i in P1 or i in P1 )
;
suppose
not
i in P1
;
:: thesis: the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j)))) >= the_rank_of M'then
Segm M',
P1,
Q1 = Segm (RLine M',i,((Line M',i) + (a * (Line M',j)))),
P1,
Q1
by A32, Th60;
hence
the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j)))) >= the_rank_of M'
by A11, A32, A33, A34, Def4;
:: thesis: verum end; suppose A35:
i in P1
;
:: thesis: the_rank_of M' <= the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j))))consider k being
Nat such that A36:
P1 c= Seg k
by Th43;
rng (Sgm P1) = P1
by A36, FINSEQ_1:def 13;
then consider m being
set such that A37:
(
m in dom (Sgm P1) &
(Sgm P1) . m = i )
by A35, FUNCT_1:def 5;
A38:
dom (Sgm P1) = Seg (card P1)
by A36, FINSEQ_3:45;
reconsider m =
m as
Element of
NAT by A37;
A39:
(
Q1 c= Seg (width M') &
Q1 c= Seg (width (RLine M',i,((Line M',i) + (a * (Line M',j))))) )
by A11, A32, Th67;
then A40:
rng (Sgm Q1) c= Seg (width M')
by FINSEQ_1:def 13;
then A41:
(
dom ((Line M',j) * (Sgm Q1)) = dom (Sgm Q1) &
dom (Sgm Q1) = Seg (card Q1) )
by A5, A39, FINSEQ_3:45, RELAT_1:46;
then reconsider LjQ =
(Line M',j) * (Sgm Q1) as
FinSequence by FINSEQ_1:def 2;
(
rng LjQ c= rng (Line M',j) &
rng (Line M',j) c= the
carrier of
K )
by FINSEQ_1:def 4, RELAT_1:45;
then
rng LjQ c= the
carrier of
K
by XBOOLE_1:1;
then reconsider LjQ =
LjQ as
FinSequence of
K by FINSEQ_1:def 4;
set SR =
EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),
P1,
Q1;
set SM =
EqSegm M',
P1,
Q1;
A42:
(
len LjQ = card P1 &
len (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P1,Q1) = card P1 &
len LjQ = len (a * LjQ) )
by A32, A41, FINSEQ_1:def 3, MATRIXR1:16, MATRIX_1:def 3;
A43:
(
len (Line (EqSegm M',P1,Q1),m) = width (EqSegm M',P1,Q1) &
width (EqSegm M',P1,Q1) = card P1 &
card P1 = len (EqSegm M',P1,Q1) )
by MATRIX_1:25, MATRIX_1:def 8;
A44:
(
Line (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P1,Q1),
m = (Line (RLine M',i,((Line M',i) + (a * (Line M',j)))),i) * (Sgm Q1) &
Line (EqSegm M',P1,Q1),
m = (Line M',i) * (Sgm Q1) )
by A34, A37, A38, A39, Th47;
A45:
a * LjQ = (a * (Line M',j)) * (Sgm Q1)
by A5, A40, Th87;
A46:
(
RLine (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P1,Q1),
m,
(Line (EqSegm M',P1,Q1),m) = Segm M',
P1,
Q1 &
RLine (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P1,Q1),
m,
LjQ = Segm (RLine M',i,(Line M',j)),
P1,
Q1 &
Segm (RLine M',i,(Line M',j)),
P1,
Q1 = EqSegm (RLine M',i,(Line M',j)),
P1,
Q1 )
by A4, A5, A6, A7, A11, A32, A34, A37, A44, Def3, Th59;
EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),
P1,
Q1 =
RLine (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P1,Q1),
m,
(Line (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P1,Q1),m)
by MATRIX11:30
.=
RLine (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P1,Q1),
m,
((Line (EqSegm M',P1,Q1),m) + (a * LjQ))
by A5, A40, A44, A45, Th88
;
then A47:
Det (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P1,Q1) =
(Det (RLine (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P1,Q1),m,(Line (EqSegm M',P1,Q1),m))) + (Det (RLine (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P1,Q1),m,(a * LjQ)))
by A37, A38, A42, A43, MATRIX11:36
.=
(Det (RLine (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P1,Q1),m,(Line (EqSegm M',P1,Q1),m))) + (a * (Det (RLine (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P1,Q1),m,LjQ)))
by A37, A38, A42, MATRIX11:34
.=
(Det (EqSegm M',P1,Q1)) + (a * (Det (EqSegm (RLine M',i,(Line M',j)),P1,Q1)))
by A32, A46, Def3
;
per cases
( Det (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P1,Q1) <> 0. K or Det (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P1,Q1) = 0. K )
;
suppose
Det (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P1,Q1) <> 0. K
;
:: thesis: the_rank_of M' <= the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j))))end; suppose A48:
Det (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P1,Q1) = 0. K
;
:: thesis: the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j)))) >= the_rank_of M'reconsider j0 =
j as non
zero Element of
NAT by A1;
per cases
( i = j or ( i <> j & j in P1 ) or ( i <> j & not j in P1 ) )
;
suppose A49:
i = j
;
:: thesis: the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j)))) >= the_rank_of M'then Det (EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),P1,Q1) =
(Det (EqSegm M',P1,Q1)) + (a * (Det (EqSegm M',P1,Q1)))
by A47, MATRIX11:30
.=
((1_ K) * (Det (EqSegm M',P1,Q1))) + (a * (Det (EqSegm M',P1,Q1)))
by VECTSP_1:def 13
.=
((1_ K) + a) * (Det (EqSegm M',P1,Q1))
by VECTSP_1:def 18
;
then
(1_ K) + a = 0. K
by A33, A48, VECTSP_1:44;
then a =
(0. K) - (1_ K)
by VECTSP_2:22
.=
(0. K) + (- (1_ K))
.=
- (1_ K)
by RLVECT_1:def 7
;
hence
the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j)))) >= the_rank_of M'
by A2, A49;
:: thesis: verum end; suppose A50:
(
i <> j &
j in P1 )
;
:: thesis: the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j)))) >= the_rank_of M'
rng (Sgm P1) = P1
by A36, FINSEQ_1:def 13;
then consider l being
set such that A51:
(
l in dom (Sgm P1) &
(Sgm P1) . l = j0 )
by A50, FUNCT_1:def 5;
reconsider l =
l as
Element of
NAT by A51;
A52:
RLine (EqSegm M',P1,Q1),
m,
(Line (EqSegm M',P1,Q1),l) = EqSegm (RLine M',i,(Line M',j)),
P1,
Q1
by A4, A32, A34, A37, A38, A39, A46, A51, Th47, Th59;
0. K = Det (RLine (EqSegm M',P1,Q1),m,(Line (EqSegm M',P1,Q1),l))
by A37, A38, A50, A51, MATRIX11:51;
then
0. K = a * (Det (RLine (EqSegm M',P1,Q1),m,(Line (EqSegm M',P1,Q1),l)))
by VECTSP_1:44;
hence
the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j)))) >= the_rank_of M'
by A33, A47, A48, A52, RLVECT_1:def 7;
:: thesis: verum end; suppose A53:
(
i <> j & not
j in P1 )
;
:: thesis: the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j)))) >= the_rank_of M'set Pij =
(P1 \ {i}) \/ {j0};
a * (Det (EqSegm (RLine M',i,(Line M',j)),P1,Q1)) <> 0. K
by A33, A47, A48, RLVECT_1:def 7;
then A54:
Det (EqSegm (RLine M',i,(Line M',j)),P1,Q1) <> 0. K
by VECTSP_1:44;
(
Det (EqSegm (RLine M',i,(Line M',j)),P1,Q1) = Det (EqSegm M',((P1 \ {i}) \/ {j0}),Q1) or
Det (EqSegm (RLine M',i,(Line M',j)),P1,Q1) = - (Det (EqSegm M',((P1 \ {i}) \/ {j0}),Q1)) )
by A1, A3, A4, A32, A35, A53, Th68;
then A55:
(
Det (EqSegm M',((P1 \ {i}) \/ {j0}),Q1) <> 0. K &
card P1 = card ((P1 \ {i}) \/ {j0}) &
[:((P1 \ {i}) \/ {j0}),Q1:] c= Indices (RLine M',i,((Line M',i) + (a * (Line M',j)))) )
by A1, A3, A4, A11, A32, A35, A53, A54, Th68, VECTSP_2:34;
( not
i in P1 \ {i} & not
i in {j} )
by A53, TARSKI:def 1, ZFMISC_1:64;
then A56:
not
i in (P1 \ {i}) \/ {j0}
by XBOOLE_0:def 3;
EqSegm M',
((P1 \ {i}) \/ {j0}),
Q1 =
Segm M',
((P1 \ {i}) \/ {j0}),
Q1
by A32, A55, Def3
.=
Segm (RLine M',i,((Line M',i) + (a * (Line M',j)))),
((P1 \ {i}) \/ {j0}),
Q1
by A11, A55, A56, Th60
.=
EqSegm (RLine M',i,((Line M',i) + (a * (Line M',j)))),
((P1 \ {i}) \/ {j0}),
Q1
by A32, A55, Def3
;
hence
the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j)))) >= the_rank_of M'
by A32, A33, A55, Def4;
:: thesis: verum end; end; end; hence
the_rank_of M' = the_rank_of (RLine M',i,((Line M',i) + (a * (Line M',j))))
by A12, XXREAL_0:1;
:: thesis: verum end;