let K be Field; for M being diagonal Matrix of K
for NonZero1 being set st NonZero1 = { i where i is Element of NAT : ( [i,i] in Indices M & M * (i,i) <> 0. K ) } holds
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K holds
( P c= NonZero1 & Q c= NonZero1 )
let M be diagonal Matrix of K; for NonZero1 being set st NonZero1 = { i where i is Element of NAT : ( [i,i] in Indices M & M * (i,i) <> 0. K ) } holds
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K holds
( P c= NonZero1 & Q c= NonZero1 )
let NonZero1 be set ; ( NonZero1 = { i where i is Element of NAT : ( [i,i] in Indices M & M * (i,i) <> 0. K ) } implies for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K holds
( P c= NonZero1 & Q c= NonZero1 ) )
assume A1:
NonZero1 = { i where i is Element of NAT : ( [i,i] in Indices M & M * (i,i) <> 0. K ) }
; for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K holds
( P c= NonZero1 & Q c= NonZero1 )
let P, Q be finite without_zero Subset of NAT; ( [:P,Q:] c= Indices M & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K implies ( P c= NonZero1 & Q c= NonZero1 ) )
assume that
A2:
[:P,Q:] c= Indices M
and
A3:
card P = card Q
and
A4:
Det (EqSegm (M,P,Q)) <> 0. K
; ( P c= NonZero1 & Q c= NonZero1 )
set S = Segm (M,P,Q);
set SQ = Sgm Q;
set SP = Sgm P;
set ES = EqSegm (M,P,Q);
A5:
Indices (Segm (M,P,Q)) = [:(Seg (len (Segm (M,P,Q)))),(Seg (width (Segm (M,P,Q)))):]
by FINSEQ_1:def 3;
A6:
EqSegm (M,P,Q) = Segm (M,P,Q)
by A3, Def3;
thus
P c= NonZero1
Q c= NonZero1proof
assume
not
P c= NonZero1
;
contradiction
then consider x being
object such that A7:
x in P
and A8:
not
x in NonZero1
;
A9:
P c= Seg (len M)
by A2, A3, Th67;
then A10:
rng (Sgm P) = P
by FINSEQ_1:def 13;
then consider y being
object such that A11:
y in dom (Sgm P)
and A12:
(Sgm P) . y = x
by A7, FUNCT_1:def 3;
reconsider x =
x,
y =
y as
Element of
NAT by A7, A11;
set L =
Line (
(Segm (M,P,Q)),
y);
A13:
dom (Sgm P) = Seg (card P)
by A9, FINSEQ_3:40;
Q c= Seg (width M)
by A2, A3, Th67;
then A14:
rng (Sgm Q) = Q
by FINSEQ_1:def 13;
A15:
now for i being Nat st 1 <= i & i <= width (Segm (M,P,Q)) holds
(Line ((Segm (M,P,Q)),y)) . i = ((0. K) * (Line ((Segm (M,P,Q)),y))) . ilet i be
Nat;
( 1 <= i & i <= width (Segm (M,P,Q)) implies (Line ((Segm (M,P,Q)),y)) . i = ((0. K) * (Line ((Segm (M,P,Q)),y))) . i )assume that A16:
1
<= i
and A17:
i <= width (Segm (M,P,Q))
;
(Line ((Segm (M,P,Q)),y)) . i = ((0. K) * (Line ((Segm (M,P,Q)),y))) . iA18:
i in Seg (width (Segm (M,P,Q)))
by A16, A17;
then A19:
(Line ((Segm (M,P,Q)),y)) . i = (Segm (M,P,Q)) * (
y,
i)
by MATRIX_0:def 7;
y in Seg (len (Segm (M,P,Q)))
by A3, A13, A11, MATRIX_0:24;
then A20:
[y,i] in Indices (Segm (M,P,Q))
by A5, A18, ZFMISC_1:87;
then A21:
(Segm (M,P,Q)) * (
y,
i)
= M * (
x,
((Sgm Q) . i))
by A12, Def1;
A22:
(0. K) * (0. K) = 0. K
;
A23:
(
(Sgm Q) . i <> x or
(Sgm Q) . i = x )
;
[x,((Sgm Q) . i)] in Indices M
by A2, A10, A14, A12, A20, Th17;
then
(Line ((Segm (M,P,Q)),y)) . i = 0. K
by A1, A8, A21, A19, A23, MATRIX_1:def 6;
hence
(Line ((Segm (M,P,Q)),y)) . i = ((0. K) * (Line ((Segm (M,P,Q)),y))) . i
by A18, A22, FVSUM_1:51;
verum end;
A24:
len (Line ((Segm (M,P,Q)),y)) = width (Segm (M,P,Q))
by MATRIX_0:def 7;
len (Line ((Segm (M,P,Q)),y)) = len ((0. K) * (Line ((Segm (M,P,Q)),y)))
by MATRIXR1:16;
then
Line (
(Segm (M,P,Q)),
y)
= (0. K) * (Line ((Segm (M,P,Q)),y))
by A24, A15;
then A25:
Det (RLine ((EqSegm (M,P,Q)),y,(Line ((EqSegm (M,P,Q)),y)))) = (0. K) * (Det (EqSegm (M,P,Q)))
by A6, A13, A11, MATRIX11:35;
RLine (
(EqSegm (M,P,Q)),
y,
(Line ((EqSegm (M,P,Q)),y)))
= EqSegm (
M,
P,
Q)
by MATRIX11:30;
hence
contradiction
by A4, A25;
verum
end;
A26:
dom (Segm (M,P,Q)) = Seg (len (Segm (M,P,Q)))
by FINSEQ_1:def 3;
A27:
len (Segm (M,P,Q)) = card P
by A3, MATRIX_0:24;
A28:
width (Segm (M,P,Q)) = card P
by A3, MATRIX_0:24;
thus
Q c= NonZero1
verumproof
A29:
Q c= Seg (width M)
by A2, A3, Th67;
then A30:
dom (Sgm Q) = Seg (card Q)
by FINSEQ_3:40;
assume
not
Q c= NonZero1
;
contradiction
then consider x being
object such that A31:
x in Q
and A32:
not
x in NonZero1
;
A33:
rng (Sgm Q) = Q
by A29, FINSEQ_1:def 13;
then consider y being
object such that A34:
y in dom (Sgm Q)
and A35:
(Sgm Q) . y = x
by A31, FUNCT_1:def 3;
reconsider x =
x,
y =
y as
Element of
NAT by A31, A34;
set C =
Col (
(EqSegm (M,P,Q)),
y);
P c= Seg (len M)
by A2, A3, Th67;
then A36:
rng (Sgm P) = P
by FINSEQ_1:def 13;
now for k being Element of NAT st k in Seg (card P) holds
(Col ((EqSegm (M,P,Q)),y)) . k = 0. Klet k be
Element of
NAT ;
( k in Seg (card P) implies (Col ((EqSegm (M,P,Q)),y)) . k = 0. K )assume A37:
k in Seg (card P)
;
(Col ((EqSegm (M,P,Q)),y)) . k = 0. KA38:
(Segm (M,P,Q)) * (
k,
y)
= (Col ((EqSegm (M,P,Q)),y)) . k
by A6, A27, A26, A37, MATRIX_0:def 8;
A39:
[k,y] in Indices (Segm (M,P,Q))
by A3, A5, A27, A28, A30, A34, A37, ZFMISC_1:87;
then A40:
(Segm (M,P,Q)) * (
k,
y)
= M * (
((Sgm P) . k),
x)
by A35, Def1;
A41:
(
(Sgm P) . k <> x or
(Sgm P) . k = x )
;
[((Sgm P) . k),x] in Indices M
by A2, A36, A33, A35, A39, Th17;
hence
(Col ((EqSegm (M,P,Q)),y)) . k = 0. K
by A1, A32, A40, A38, A41, MATRIX_1:def 6;
verum end;
hence
contradiction
by A3, A4, A30, A34, MATRIX_9:53;
verum
end;