let n be Nat; for K being Field
for M being Diagonal of n,K st the_rank_of M = n holds
lines M is Basis of n -VectSp_over K
let K be Field; for M being Diagonal of n,K st the_rank_of M = n holds
lines M is Basis of n -VectSp_over K
let M be Diagonal of n,K; ( the_rank_of M = n implies lines M is Basis of n -VectSp_over K )
assume A1:
the_rank_of M = n
; lines M is Basis of n -VectSp_over K
set lM = lines M;
set V = n -VectSp_over K;
reconsider V9 = n -VectSp_over K as Subspace of n -VectSp_over K by VECTSP_4:32;
now let v be
Vector of
(n -VectSp_over K);
( ( v in Lin (lines M) implies v in V9 ) & ( v in V9 implies v in Lin (lines M) ) )thus
(
v in Lin (lines M) implies
v in V9 )
by STRUCT_0:def 5;
( v in V9 implies v in Lin (lines M) )thus
(
v in V9 implies
v in Lin (lines M) )
verumproof
reconsider t =
v as
Element of
n -tuples_on the
carrier of
K by Th102;
assume
v in V9
;
v in Lin (lines M)
deffunc H1(
Nat)
-> Element of
(width M) -tuples_on the
carrier of
K =
((t /. $1) * ((M * $1,$1) " )) * (Line M,$1);
consider f being
FinSequence of
(width M) -tuples_on the
carrier of
K such that A2:
len f = n
and A3:
for
j being
Nat st
j in dom f holds
f . j = H1(
j)
from FINSEQ_2:sch 1();
A4:
dom f = Seg n
by A2, FINSEQ_1:def 3;
width M = n
by MATRIX_1:25;
then reconsider f =
f as
FinSequence of the
carrier of
(n -VectSp_over K) by Th102;
reconsider M1 =
FinS2MX f as
Matrix of
n,
K by A2;
now let i be
Nat;
( i in Seg n implies ex a being Element of K st Line M1,i = a * (Line M,i) )assume A5:
i in Seg n
;
ex a being Element of K st Line M1,i = a * (Line M,i) Line M1,
i =
M1 . i
by A5, MATRIX_2:10
.=
H1(
i)
by A3, A4, A5
;
hence
ex
a being
Element of
K st
Line M1,
i = a * (Line M,i)
;
verum end;
then consider L being
Linear_Combination of
lines M such that A6:
L (#) (MX2FinS M) = M1
by A1, Th105, Th108;
set MX =
MX2FinS M;
A7:
len t = n
by FINSEQ_1:def 18;
reconsider SumL =
Sum L as
Element of
n -tuples_on the
carrier of
K by Th102;
A8:
Carrier L c= lines M
by VECTSP_6:def 7;
A9:
now set diag =
diagonal_of_Matrix M;
let i be
Nat;
( 1 <= i & i <= n implies SumL . i = t . i )assume that A10:
1
<= i
and A11:
i <= n
;
SumL . i = t . i
i in NAT
by ORDINAL1:def 13;
then A12:
i in Seg n
by A10, A11;
then A13:
(diagonal_of_Matrix M) . i = M * i,
i
by MATRIX_3:def 10;
A14:
len (diagonal_of_Matrix M) = n
by MATRIX_3:def 10;
then A15:
dom (diagonal_of_Matrix M) = Seg n
by FINSEQ_1:def 3;
A16:
width M = n
by MATRIX_1:25;
then A17:
(Line M,i) . i = M * i,
i
by A12, MATRIX_1:def 8;
set C =
Col M1,
i;
A18:
dom t = Seg n
by FINSEQ_2:144;
len (Col M1,i) = len M1
by MATRIX_1:def 9;
then A19:
dom (Col M1,i) = Seg (len M1)
by FINSEQ_1:def 3;
len M = n
by MATRIX_1:25;
then A20:
dom M = Seg n
by FINSEQ_1:def 3;
A21:
Det M <> 0. K
by A1, Th83;
A22:
len M1 = n
by MATRIX_1:25;
then A23:
dom M1 = Seg n
by FINSEQ_1:def 3;
Det M = Product (diagonal_of_Matrix M)
by A10, A11, A14, MATRIX_7:17, NAT_1:14;
then A24:
(diagonal_of_Matrix M) . i <> 0. K
by A12, A21, A15, FVSUM_1:107;
A25:
Line M1,
i =
M1 . i
by A12, MATRIX_2:10
.=
((t /. i) * ((M * i,i) " )) * (Line M,i)
by A3, A12, A23
;
A26:
width M1 = n
by MATRIX_1:25;
now let k be
Nat;
( k in dom (Col M1,i) & k <> i implies 0. K = (Col M1,i) . k )assume that A27:
k in dom (Col M1,i)
and A28:
k <> i
;
0. K = (Col M1,i) . kA29:
[k,i] in Indices M
by A22, A16, A12, A19, A20, A27, ZFMISC_1:106;
A30:
(Line M,k) . i =
M * k,
i
by A16, A12, MATRIX_1:def 8
.=
0. K
by A28, A29, MATRIX_1:def 15
;
A31:
(MX2FinS M) /. k =
M . k
by A22, A19, A20, A27, PARTFUN1:def 8
.=
Line M,
k
by A22, A19, A27, MATRIX_2:10
;
Line M1,
k =
M1 . k
by A19, A27, MATRIX_2:10
.=
(L . ((MX2FinS M) /. k)) * ((MX2FinS M) /. k)
by A6, A22, A19, A23, A27, VECTSP_6:def 8
.=
(L . ((MX2FinS M) /. k)) * (Line M,k)
by A16, A31, Th102
;
then (Line M1,k) . i =
(L . ((MX2FinS M) /. k)) * (0. K)
by A16, A12, A30, FVSUM_1:63
.=
0. K
by VECTSP_1:39
;
hence 0. K =
M1 * k,
i
by A26, A12, MATRIX_1:def 8
.=
(Col M1,i) . k
by A22, A19, A23, A27, MATRIX_1:def 9
;
verum end; then (Col M1,i) . i =
Sum (Col M1,i)
by A22, A12, A19, MATRIX_3:14
.=
SumL . i
by A1, A6, A8, A12, Th105, Th107
;
hence SumL . i =
M1 * i,
i
by A12, A23, MATRIX_1:def 9
.=
(Line M1,i) . i
by A26, A12, MATRIX_1:def 8
.=
((t /. i) * ((M * i,i) " )) * (M * i,i)
by A16, A12, A25, A17, FVSUM_1:63
.=
(t /. i) * (((M * i,i) " ) * (M * i,i))
by GROUP_1:def 4
.=
(t /. i) * (1_ K)
by A24, A13, VECTSP_1:def 22
.=
t /. i
by VECTSP_1:def 13
.=
t . i
by A12, A18, PARTFUN1:def 8
;
verum end;
len SumL = n
by FINSEQ_1:def 18;
then
SumL = t
by A7, A9, FINSEQ_1:18;
hence
v in Lin (lines M)
by VECTSP_7:12;
verum
end; end;
then A32:
Lin (lines M) = VectSpStr(# the carrier of (n -VectSp_over K),the addF of (n -VectSp_over K),the ZeroF of (n -VectSp_over K),the lmult of (n -VectSp_over K) #)
by VECTSP_4:38;
lines M is linearly-independent
by A1, Th110;
hence
lines M is Basis of n -VectSp_over K
by A32, VECTSP_7:def 3; verum