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 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

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 ) by STRUCT_0:def 5; :: 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_1: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

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_2:8
.= 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

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
i in NAT by ORDINAL1:def 12;
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:24;
then A17: (Line (M,i)) . i = M * (i,i) by A12, MATRIX_1:def 7;
set C = Col (M1,i);
A18: dom t = Seg n by FINSEQ_2:124;
len (Col (M1,i)) = len M1 by MATRIX_1:def 8;
then A19: dom (Col (M1,i)) = Seg (len M1) by FINSEQ_1:def 3;
len M = n by MATRIX_1:24;
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:24;
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:82;
A25: Line (M1,i) = M1 . i by A12, MATRIX_2:8
.= ((t /. i) * ((M * (i,i)) ")) * (Line (M,i)) by A3, A12, A23 ;
A26: width M1 = n by MATRIX_1:24;

now

let k be Nat; :: thesis: ( 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 ; :: thesis: 0. K = (Col (M1,i)) . k
A29: [k,i] in Indices M by A22, A16, A12, A19, A20, A27, ZFMISC_1:87;
A30: (Line (M,k)) . i = M * (k,i) by A16, A12, MATRIX_1:def 7
.= 0. K by A28, A29, MATRIX_1:def 14 ;
A31: (MX2FinS M) /. k = M . k by A22, A19, A20, A27, PARTFUN1:def 6
.= Line (M,k) by A22, A19, A27, MATRIX_2:8 ;
Line (M1,k) = M1 . k by A19, A27, MATRIX_2:8
.= (L . ((MX2FinS M) /. k)) * ((MX2FinS M) /. k) by A6, A22, A19, A23, A27, VECTSP_6:def 5
.= (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:51
.= 0. K by VECTSP_1:7 ;
hence 0. K = M1 * (k,i) by A26, A12, MATRIX_1:def 7
.= (Col (M1,i)) . k by A22, A19, A23, A27, MATRIX_1:def 8 ;
:: thesis: verum

end;

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

end;

len SumL = n by CARD_1:def 7;
then SumL = t by A7, A9, FINSEQ_1:14;
hence v in Lin (lines M) by VECTSP_7:7; :: thesis: 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:30;
lines M is linearly-independent by A1, Th110;
hence lines M is Basis of n -VectSp_over K by A32, VECTSP_7:def 3; :: thesis: verum