let n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: ( the_rank_of M = n implies lines M is Basis of n -VectSp_over K )
assume A1:
the_rank_of M = n
; :: thesis: lines M is Basis of n -VectSp_over K
set V = n -VectSp_over K;
set lM = lines M;
reconsider V' = 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);
:: thesis: ( ( v in Lin (lines M) implies v in V' ) & ( v in V' implies v in Lin (lines M) ) )thus
(
v in Lin (lines M) implies
v in V' )
by STRUCT_0:def 5;
:: thesis: ( v in V' implies v in Lin (lines M) )thus
(
v in V' implies
v in Lin (lines M) )
:: thesis: verumproof
assume
v in V'
;
:: thesis: v in Lin (lines M)
reconsider t =
v as
Element of
n -tuples_on the
carrier of
K by Th102;
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;
A5:
M is
without_repeated_line
by A1, Th105;
now let i be
Nat;
:: thesis: ( i in Seg n implies ex a being Element of K st Line M1,i = a * (Line M,i) )assume A6:
i in Seg n
;
:: thesis: ex a being Element of K st Line M1,i = a * (Line M,i) Line M1,
i =
M1 . i
by A6, MATRIX_2:10
.=
H1(
i)
by A3, A6, A4
;
hence
ex
a being
Element of
K st
Line M1,
i = a * (Line M,i)
;
:: thesis: verum end;
then consider L being
Linear_Combination of
lines M such that A7:
L (#) (MX2FinS M) = M1
by A5, Th108;
set MX =
MX2FinS M;
A8:
Carrier L c= lines M
by VECTSP_6:def 7;
reconsider SumL =
Sum L as
Element of
n -tuples_on the
carrier of
K by Th102;
A9:
(
len SumL = n &
len t = n )
by FINSEQ_1:def 18;
now let i be
Nat;
:: thesis: ( 1 <= i & i <= n implies SumL . i = t . i )assume A10:
( 1
<= i &
i <= n )
;
:: thesis: SumL . i = t . iset C =
Col M1,
i;
A11:
i in NAT
by ORDINAL1:def 13;
A12:
(
len (Col M1,i) = len M1 &
len M1 = n &
len M = n &
width M1 = n &
width M = n )
by MATRIX_1:25, MATRIX_1:def 9;
then A13:
(
i in Seg n &
dom (Col M1,i) = Seg (len M1) &
dom M1 = Seg n &
dom M = Seg n )
by A10, A11, FINSEQ_1:def 3;
now let k be
Nat;
:: thesis: ( k in dom (Col M1,i) & k <> i implies 0. K = (Col M1,i) . k )assume A14:
(
k in dom (Col M1,i) &
k <> i )
;
:: thesis: 0. K = (Col M1,i) . kA15:
[k,i] in Indices M
by A12, A13, A14, ZFMISC_1:106;
A16:
(MX2FinS M) /. k =
M . k
by A12, A13, A14, PARTFUN1:def 8
.=
Line M,
k
by A12, A13, A14, MATRIX_2:10
;
A17:
(Line M,k) . i =
M * k,
i
by A12, A13, MATRIX_1:def 8
.=
0. K
by A14, A15, MATRIX_1:def 15
;
Line M1,
k =
M1 . k
by A13, A14, MATRIX_2:10
.=
(L . ((MX2FinS M) /. k)) * ((MX2FinS M) /. k)
by A7, A12, A13, A14, VECTSP_6:def 8
.=
(L . ((MX2FinS M) /. k)) * (Line M,k)
by A12, A16, Th102
;
then (Line M1,k) . i =
(L . ((MX2FinS M) /. k)) * (0. K)
by A12, A13, A17, FVSUM_1:63
.=
0. K
by VECTSP_1:39
;
hence 0. K =
M1 * k,
i
by A12, A13, MATRIX_1:def 8
.=
(Col M1,i) . k
by A12, A13, A14, MATRIX_1:def 9
;
:: thesis: verum end; then A18:
(Col M1,i) . i =
Sum (Col M1,i)
by A12, A13, MATRIX_3:14
.=
SumL . i
by A1, A7, A8, A13, Th105, Th107
;
set diag =
diagonal_of_Matrix M;
(
n >= 1 &
len (diagonal_of_Matrix M) = n )
by A10, MATRIX_3:def 10, NAT_1:14;
then
(
Det M = Product (diagonal_of_Matrix M) &
Det M <> 0. K &
dom (diagonal_of_Matrix M) = Seg n )
by A1, Th83, FINSEQ_1:def 3, MATRIX_7:17;
then A19:
(
(diagonal_of_Matrix M) . i <> 0. K &
(diagonal_of_Matrix M) . i = M * i,
i )
by A13, FVSUM_1:107, MATRIX_3:def 10;
A20:
Line M1,
i =
M1 . i
by A13, MATRIX_2:10
.=
((t /. i) * ((M * i,i) " )) * (Line M,i)
by A3, A13
;
A21:
(Line M,i) . i = M * i,
i
by A12, A13, MATRIX_1:def 8;
A22:
dom t = Seg n
by FINSEQ_2:144;
thus SumL . i =
M1 * i,
i
by A13, A18, MATRIX_1:def 9
.=
(Line M1,i) . i
by A12, A13, MATRIX_1:def 8
.=
((t /. i) * ((M * i,i) " )) * (M * i,i)
by A12, A13, A20, A21, FVSUM_1:63
.=
(t /. i) * (((M * i,i) " ) * (M * i,i))
by GROUP_1:def 4
.=
(t /. i) * (1_ K)
by A19, VECTSP_1:def 22
.=
t /. i
by VECTSP_1:def 13
.=
t . i
by A13, A22, PARTFUN1:def 8
;
:: thesis: verum end;
then
SumL = t
by A9, FINSEQ_1:18;
hence
v in Lin (lines M)
by VECTSP_7:12;
:: thesis: verum
end; end;
then
( Lin (lines M) = VectSpStr(# the carrier of (n -VectSp_over K),the addF of (n -VectSp_over K),the U2 of (n -VectSp_over K),the lmult of (n -VectSp_over K) #) & lines M is linearly-independent )
by A1, Th110, VECTSP_4:38;
hence
lines M is Basis of n -VectSp_over K
by VECTSP_7:def 3; :: thesis: verum