let n be Nat; :: thesis: for K being Field
for M being diagonal Matrix 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 Matrix of n,K st the_rank_of M = n holds
lines M is Basis of (n -VectSp_over K)
let M be diagonal Matrix 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 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:24;

now :: thesis: for v being Vector of (n -VectSp_over K) holds
( ( v in Lin (lines M) implies v in V9 ) & ( v in V9 implies v in Lin (lines M) ) )

let v be Vector of (n -VectSp_over K); :: thesis: ( ( 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 ) ; :: thesis: ( v in V9 implies v in Lin (lines M) )
thus ( v in V9 implies v in Lin (lines M) ) :: thesis: verum

proof

reconsider t = v as Element of n -tuples_on the carrier of K by Th102;
assume v in V9 ; :: thesis: v in Lin (lines M)
deffunc H₁( 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 = H₁(j) from FINSEQ_2:sch 1();
A4: dom f = Seg n by A2, FINSEQ_1:def 3;
width M = n by MATRIX_0:24;
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 :: thesis: for i being Nat st i in Seg n holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i))

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 A5: 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 A5, MATRIX_0:52
.= H₁(i) by A3, A4, A5 ;
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
A6: L (#) (MX2FinS M) = M1 by A1, Th105, Th108;
set MX = MX2FinS M;
A7: len t = n by CARD_1:def 7;
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 4;

A9: now :: thesis: for i being Nat st 1 <= i & i <= n holds
SumL . i = t . i

set diag = diagonal_of_Matrix M;
let i be Nat; :: thesis: ( 1 <= i & i <= n implies SumL . i = t . i )
assume that
A10: 1 <= i and
A11: i <= n ; :: thesis: SumL . i = t . i
A12: i in Seg n by A10, A11;
then A13: (diagonal_of_Matrix M) . i = M * (i,i) by MATRIX_3:def 10;
len (diagonal_of_Matrix M) = n by MATRIX_3:def 10;
then A14: dom (diagonal_of_Matrix M) = Seg n by FINSEQ_1:def 3;
A15: width M = n by MATRIX_0:24;
then A16: (Line (M,i)) . i = M * (i,i) by A12, MATRIX_0:def 7;
set C = Col (M1,i);
A17: dom t = Seg n by FINSEQ_2:124;
len (Col (M1,i)) = len M1 by MATRIX_0:def 8;
then A18: dom (Col (M1,i)) = Seg (len M1) by FINSEQ_1:def 3;
len M = n by MATRIX_0:24;
then A19: dom M = Seg n by FINSEQ_1:def 3;
A20: Det M <> 0. K by A1, Th83;
A21: len M1 = n by MATRIX_0:24;
then A22: dom M1 = Seg n by FINSEQ_1:def 3;
Det M = Product (diagonal_of_Matrix M) by A10, A11, MATRIX_7:17, NAT_1:14;
then A23: (diagonal_of_Matrix M) . i <> 0. K by A12, A20, A14, FVSUM_1:82;
A24: Line (M1,i) = M1 . i by A12, MATRIX_0:52
.= ((t /. i) * ((M * (i,i)) ")) * (Line (M,i)) by A3, A12, A22 ;
A25: width M1 = n by MATRIX_0:24;

now :: thesis: for k being Nat st k in dom (Col (M1,i)) & k <> i holds
0. K = (Col (M1,i)) . k

let k be Nat; :: thesis: ( k in dom (Col (M1,i)) & k <> i implies 0. K = (Col (M1,i)) . k )
assume that
A26: k in dom (Col (M1,i)) and
A27: k <> i ; :: thesis: 0. K = (Col (M1,i)) . k
A28: [k,i] in Indices M by A21, A15, A12, A18, A19, A26, ZFMISC_1:87;
A29: (Line (M,k)) . i = M * (k,i) by A15, A12, MATRIX_0:def 7
.= 0. K by A27, A28, MATRIX_1:def 6 ;
A30: (MX2FinS M) /. k = M . k by A21, A18, A19, A26, PARTFUN1:def 6
.= Line (M,k) by A21, A18, A26, MATRIX_0:52 ;
Line (M1,k) = M1 . k by A18, A26, MATRIX_0:52
.= (L . ((MX2FinS M) /. k)) * ((MX2FinS M) /. k) by A6, A21, A18, A22, A26, VECTSP_6:def 5
.= (L . ((MX2FinS M) /. k)) * (Line (M,k)) by A15, A30, Th102 ;
then (Line (M1,k)) . i = (L . ((MX2FinS M) /. k)) * (0. K) by A15, A12, A29, FVSUM_1:51
.= 0. K ;
hence 0. K = M1 * (k,i) by A25, A12, MATRIX_0:def 7
.= (Col (M1,i)) . k by A21, A18, A22, A26, MATRIX_0:def 8 ;
:: thesis: verum

end;

then (Col (M1,i)) . i = Sum (Col (M1,i)) by A21, A12, A18, MATRIX_3:12
.= SumL . i by A1, A6, A8, A12, Th105, Th107 ;
hence SumL . i = M1 * (i,i) by A12, A22, MATRIX_0:def 8
.= (Line (M1,i)) . i by A25, A12, MATRIX_0:def 7
.= ((t /. i) * ((M * (i,i)) ")) * (M * (i,i)) by A15, A12, A24, A16, FVSUM_1:51
.= (t /. i) * (((M * (i,i)) ") * (M * (i,i))) by GROUP_1:def 3
.= (t /. i) * (1_ K) by A23, A13, VECTSP_1:def 10
.= t /. i
.= t . i by A12, A17, PARTFUN1:def 6 ;
:: thesis: verum

end;

len SumL = n by CARD_1:def 7;
then SumL = t by A7, A9;
hence v in Lin (lines M) by VECTSP_7:7; :: thesis: verum

end;

end;

then A31: Lin (lines M) = ModuleStr(# 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:30;
lines M is linearly-independent by A1, Th110;
hence lines M is Basis of (n -VectSp_over K) by A31, VECTSP_7:def 3; :: thesis: verum