let L be non trivial positive-definite RATional Z_Lattice; :: thesis: for b being OrdBasis of L holds Det (GramMatrix b) <> 0. F_Real

let b be OrdBasis of L; :: thesis: Det (GramMatrix b) <> 0. F_Real

reconsider M = GramMatrix b as Matrix of rank L,F_Rat by ThGM1;

assume Det (GramMatrix b) = 0. F_Real ; :: thesis: contradiction

then AS: Det M = 0. F_Rat by LmSign1A;

A1: len M = rank L by MATRIX_0:def 2;

A2: the_rank_of M <> rank L by AS, MATRIX13:83;

B3: dom M = Seg (len M) by FINSEQ_1:def 3

.= Seg (rank L) by MATRIX_0:def 2 ;

B4: dom M = Seg (len b) by B3, ZMATRLIN:49

.= dom b by FINSEQ_1:def 3 ;

( dom b = Seg (rank L) & rank L is Element of NAT ) by B3, B4, ORDINAL1:def 12;

then len b = rank L by FINSEQ_1:def 3;

then C4: Indices (BilinearM ((InnerProduct L),b,b)) = [:(Seg (rank L)),(Seg (rank L)):] by MATRIX_0:24;

OTO2: M is one-to-one

lines M c= the carrier of ((rank L) -VectSp_over F_Rat) ;

then reconsider M1 = M as FinSequence of ((rank L) -VectSp_over F_Rat) by FINSEQ_1:def 4;

consider r being FinSequence of F_Rat, rM1 being FinSequence of ((rank L) -VectSp_over F_Rat) such that

Z1: ( len r = rank L & len rM1 = rank L & ( for i being Nat st i in dom rM1 holds

rM1 . i = (r /. i) * (M1 /. i) ) & Sum rM1 = 0. ((rank L) -VectSp_over F_Rat) & r <> (Seg (len r)) --> (0. F_Rat) ) by A1, AA1, OTO2, LMBASE2;

consider K being Integer, Kr being FinSequence of INT.Ring such that

Z2: ( K <> 0 & len Kr = rank L & ( for i being Nat st i in dom Kr holds

Kr . i = K * (r /. i) ) ) by Z1, LMThGM23;

reconsider K1 = K as Element of F_Rat by INT_1:def 2, NUMBERS:14;

defpred S_{1}[ Nat, object ] means ex rM1i being Element of ((rank L) -VectSp_over F_Rat) st

( rM1i = rM1 . $1 & $2 = K1 * rM1i );

KRM10: for k being Nat st k in Seg (rank L) holds

ex x being Element of the carrier of ((rank L) -VectSp_over F_Rat) st S_{1}[k,x]

KRM11: ( dom KrM1 = Seg (rank L) & ( for k being Nat st k in Seg (rank L) holds

S_{1}[k,KrM1 . k] ) )
from FINSEQ_1:sch 5(KRM10);

KRM1Z: rank L is Element of NAT by ORDINAL1:def 12;

then KRM1: len KrM1 = rank L by FINSEQ_1:def 3, KRM11;

Z3: for i being Nat st i in dom KrM1 holds

ex M1i being Element of ((rank L) -VectSp_over F_Rat) ex Kri being Element of F_Rat st

( M1i = M1 . i & Kri = Kr . i & KrM1 . i = Kri * M1i )

for v being Element of ((rank L) -VectSp_over F_Rat) st k in dom KrM1 & v = rM1 . k holds

KrM1 . k = K1 * v

.= 0. ((rank L) -VectSp_over F_Rat) by Z1, VECTSP_1:15 ;

Z4B: Kr <> (Seg (len Kr)) --> (0. INT.Ring)

Z5: for n being Nat st n in dom b holds

(Sum KrM1) . n = 0. INT.Ring_{2}[ Nat, object ] means $2 = (Kr /. $1) * (b /. $1);

Z510: for k being Nat st k in Seg (rank L) holds

ex x being Element of the carrier of L st S_{2}[k,x]
;

consider Krb being FinSequence of the carrier of L such that

Z511: ( dom Krb = Seg (rank L) & ( for k being Nat st k in Seg (rank L) holds

S_{2}[k,Krb . k] ) )
from FINSEQ_1:sch 5(Z510);

Z51Z: rank L is Element of NAT by ORDINAL1:def 12;

then Z51: len Krb = rank L by FINSEQ_1:def 3, Z511;

Z6: for n being Nat st n in dom b holds

(Sum KrM1) . n = <;(Sum Krb),(b /. n);>

<;(0. L),(b /. n);> = <;(Sum Krb),(b /. n);>

Z9: b is one-to-one by ZMATRLIN:def 5;

len Kr = len b by B3, B4, Z2, FINSEQ_1:def 3;

then rng b is linearly-dependent by Z51, Z511, Z4B, Z2, Z8, Z9, LMBASE2;

then not rng b is base by VECTSP_7:def 3;

hence contradiction by ZMATRLIN:def 5; :: thesis: verum

let b be OrdBasis of L; :: thesis: Det (GramMatrix b) <> 0. F_Real

reconsider M = GramMatrix b as Matrix of rank L,F_Rat by ThGM1;

assume Det (GramMatrix b) = 0. F_Real ; :: thesis: contradiction

then AS: Det M = 0. F_Rat by LmSign1A;

A1: len M = rank L by MATRIX_0:def 2;

A2: the_rank_of M <> rank L by AS, MATRIX13:83;

B3: dom M = Seg (len M) by FINSEQ_1:def 3

.= Seg (rank L) by MATRIX_0:def 2 ;

B4: dom M = Seg (len b) by B3, ZMATRLIN:49

.= dom b by FINSEQ_1:def 3 ;

( dom b = Seg (rank L) & rank L is Element of NAT ) by B3, B4, ORDINAL1:def 12;

then len b = rank L by FINSEQ_1:def 3;

then C4: Indices (BilinearM ((InnerProduct L),b,b)) = [:(Seg (rank L)),(Seg (rank L)):] by MATRIX_0:24;

OTO2: M is one-to-one

proof

then AA1:
lines M is linearly-dependent
by A2, MATRIX13:121;
assume
not M is one-to-one
; :: thesis: contradiction

then consider m1, m2 being object such that

B1: ( m1 in dom M & m2 in dom M & M . m1 = M . m2 & m1 <> m2 ) ;

B3: dom M = Seg (len (GramMatrix b)) by FINSEQ_1:def 3

.= Seg (rank L) by MATRIX_0:def 2 ;

B4: dom M = Seg (len b) by B3, ZMATRLIN:49

.= dom b by FINSEQ_1:def 3 ;

reconsider m1 = m1, m2 = m2 as Nat by B1;

B5: for n being Nat st n in dom b holds

<;(b /. n),(b /. m1);> = <;(b /. n),(b /. m2);>

.= b /. m2 by B5, ZL2ThSc1

.= b . m2 by B1, B4, PARTFUN1:def 6 ;

then not b is one-to-one by B1, B4;

hence contradiction by ZMATRLIN:def 5; :: thesis: verum

end;then consider m1, m2 being object such that

B1: ( m1 in dom M & m2 in dom M & M . m1 = M . m2 & m1 <> m2 ) ;

B3: dom M = Seg (len (GramMatrix b)) by FINSEQ_1:def 3

.= Seg (rank L) by MATRIX_0:def 2 ;

B4: dom M = Seg (len b) by B3, ZMATRLIN:49

.= dom b by FINSEQ_1:def 3 ;

reconsider m1 = m1, m2 = m2 as Nat by B1;

B5: for n being Nat st n in dom b holds

<;(b /. n),(b /. m1);> = <;(b /. n),(b /. m2);>

proof

b . m1 =
b /. m1
by B1, B4, PARTFUN1:def 6
let n be Nat; :: thesis: ( n in dom b implies <;(b /. n),(b /. m1);> = <;(b /. n),(b /. m2);> )

assume C1: n in dom b ; :: thesis: <;(b /. n),(b /. m1);> = <;(b /. n),(b /. m2);>

C3: [m1,n] in Indices (BilinearM ((InnerProduct L),b,b)) by C1, B1, B3, B4, C4, ZFMISC_1:87;

C6: [m2,n] in Indices (BilinearM ((InnerProduct L),b,b)) by C4, C1, B1, B3, B4, ZFMISC_1:87;

X1: ex p being FinSequence of F_Real st

( p = (BilinearM ((InnerProduct L),b,b)) . m1 & (BilinearM ((InnerProduct L),b,b)) * (m1,n) = p . n ) by MATRIX_0:def 5, C3;

thus <;(b /. n),(b /. m1);> = <;(b /. m1),(b /. n);> by ZMODLAT1:def 3

.= (InnerProduct L) . ((b /. m1),(b /. n))

.= (BilinearM ((InnerProduct L),b,b)) * (m1,n) by B1, B4, C1, ZMODLAT1:def 32

.= (BilinearM ((InnerProduct L),b,b)) * (m2,n) by B1, C6, X1, MATRIX_0:def 5

.= (InnerProduct L) . ((b /. m2),(b /. n)) by B1, B4, C1, ZMODLAT1:def 32

.= <;(b /. m2),(b /. n);>

.= <;(b /. n),(b /. m2);> by ZMODLAT1:def 3 ; :: thesis: verum

end;assume C1: n in dom b ; :: thesis: <;(b /. n),(b /. m1);> = <;(b /. n),(b /. m2);>

C3: [m1,n] in Indices (BilinearM ((InnerProduct L),b,b)) by C1, B1, B3, B4, C4, ZFMISC_1:87;

C6: [m2,n] in Indices (BilinearM ((InnerProduct L),b,b)) by C4, C1, B1, B3, B4, ZFMISC_1:87;

X1: ex p being FinSequence of F_Real st

( p = (BilinearM ((InnerProduct L),b,b)) . m1 & (BilinearM ((InnerProduct L),b,b)) * (m1,n) = p . n ) by MATRIX_0:def 5, C3;

thus <;(b /. n),(b /. m1);> = <;(b /. m1),(b /. n);> by ZMODLAT1:def 3

.= (InnerProduct L) . ((b /. m1),(b /. n))

.= (BilinearM ((InnerProduct L),b,b)) * (m1,n) by B1, B4, C1, ZMODLAT1:def 32

.= (BilinearM ((InnerProduct L),b,b)) * (m2,n) by B1, C6, X1, MATRIX_0:def 5

.= (InnerProduct L) . ((b /. m2),(b /. n)) by B1, B4, C1, ZMODLAT1:def 32

.= <;(b /. m2),(b /. n);>

.= <;(b /. n),(b /. m2);> by ZMODLAT1:def 3 ; :: thesis: verum

.= b /. m2 by B5, ZL2ThSc1

.= b . m2 by B1, B4, PARTFUN1:def 6 ;

then not b is one-to-one by B1, B4;

hence contradiction by ZMATRLIN:def 5; :: thesis: verum

lines M c= the carrier of ((rank L) -VectSp_over F_Rat) ;

then reconsider M1 = M as FinSequence of ((rank L) -VectSp_over F_Rat) by FINSEQ_1:def 4;

consider r being FinSequence of F_Rat, rM1 being FinSequence of ((rank L) -VectSp_over F_Rat) such that

Z1: ( len r = rank L & len rM1 = rank L & ( for i being Nat st i in dom rM1 holds

rM1 . i = (r /. i) * (M1 /. i) ) & Sum rM1 = 0. ((rank L) -VectSp_over F_Rat) & r <> (Seg (len r)) --> (0. F_Rat) ) by A1, AA1, OTO2, LMBASE2;

consider K being Integer, Kr being FinSequence of INT.Ring such that

Z2: ( K <> 0 & len Kr = rank L & ( for i being Nat st i in dom Kr holds

Kr . i = K * (r /. i) ) ) by Z1, LMThGM23;

reconsider K1 = K as Element of F_Rat by INT_1:def 2, NUMBERS:14;

defpred S

( rM1i = rM1 . $1 & $2 = K1 * rM1i );

KRM10: for k being Nat st k in Seg (rank L) holds

ex x being Element of the carrier of ((rank L) -VectSp_over F_Rat) st S

proof

consider KrM1 being FinSequence of the carrier of ((rank L) -VectSp_over F_Rat) such that
let k be Nat; :: thesis: ( k in Seg (rank L) implies ex x being Element of the carrier of ((rank L) -VectSp_over F_Rat) st S_{1}[k,x] )

assume KRM12: k in Seg (rank L) ; :: thesis: ex x being Element of the carrier of ((rank L) -VectSp_over F_Rat) st S_{1}[k,x]

dom rM1 = Seg (rank L) by Z1, FINSEQ_1:def 3;

then rM1 . k = rM1 /. k by KRM12, PARTFUN1:def 6;

then reconsider rM1i = rM1 . k as Element of ((rank L) -VectSp_over F_Rat) ;

K1 * rM1i is Element of the carrier of ((rank L) -VectSp_over F_Rat) ;

hence ex x being Element of the carrier of ((rank L) -VectSp_over F_Rat) st S_{1}[k,x]
; :: thesis: verum

end;assume KRM12: k in Seg (rank L) ; :: thesis: ex x being Element of the carrier of ((rank L) -VectSp_over F_Rat) st S

dom rM1 = Seg (rank L) by Z1, FINSEQ_1:def 3;

then rM1 . k = rM1 /. k by KRM12, PARTFUN1:def 6;

then reconsider rM1i = rM1 . k as Element of ((rank L) -VectSp_over F_Rat) ;

K1 * rM1i is Element of the carrier of ((rank L) -VectSp_over F_Rat) ;

hence ex x being Element of the carrier of ((rank L) -VectSp_over F_Rat) st S

KRM11: ( dom KrM1 = Seg (rank L) & ( for k being Nat st k in Seg (rank L) holds

S

KRM1Z: rank L is Element of NAT by ORDINAL1:def 12;

then KRM1: len KrM1 = rank L by FINSEQ_1:def 3, KRM11;

Z3: for i being Nat st i in dom KrM1 holds

ex M1i being Element of ((rank L) -VectSp_over F_Rat) ex Kri being Element of F_Rat st

( M1i = M1 . i & Kri = Kr . i & KrM1 . i = Kri * M1i )

proof

for k being Nat
let i be Nat; :: thesis: ( i in dom KrM1 implies ex M1i being Element of ((rank L) -VectSp_over F_Rat) ex Kri being Element of F_Rat st

( M1i = M1 . i & Kri = Kr . i & KrM1 . i = Kri * M1i ) )

assume Z300: i in dom KrM1 ; :: thesis: ex M1i being Element of ((rank L) -VectSp_over F_Rat) ex Kri being Element of F_Rat st

( M1i = M1 . i & Kri = Kr . i & KrM1 . i = Kri * M1i )

then consider rM1i being Element of ((rank L) -VectSp_over F_Rat) such that

Z301: ( rM1i = rM1 . i & KrM1 . i = K1 * rM1i ) by KRM11;

Z303: i in dom rM1 by Z1, Z300, KRM11, FINSEQ_1:def 3;

Z305: i in dom Kr by Z2, Z300, KRM11, FINSEQ_1:def 3;

Z307: dom M1 = Seg (rank L) by A1, FINSEQ_1:def 3;

then M1 /. i = M1 . i by KRM11, Z300, PARTFUN1:def 6;

then reconsider M1i = M1 . i as Element of ((rank L) -VectSp_over F_Rat) ;

Kr . i = Kr /. i by PARTFUN1:def 6, Z305;

then reconsider Kri = Kr . i as Element of F_Rat by NUMBERS:14;

take M1i ; :: thesis: ex Kri being Element of F_Rat st

( M1i = M1 . i & Kri = Kr . i & KrM1 . i = Kri * M1i )

take Kri ; :: thesis: ( M1i = M1 . i & Kri = Kr . i & KrM1 . i = Kri * M1i )

thus ( M1i = M1 . i & Kri = Kr . i ) ; :: thesis: KrM1 . i = Kri * M1i

thus KrM1 . i = K1 * ((r /. i) * (M1 /. i)) by Z1, Z301, Z303

.= K1 * ((r /. i) * M1i) by Z300, Z307, KRM11, PARTFUN1:def 6

.= (K1 * (r /. i)) * M1i by VECTSP_1:def 16

.= Kri * M1i by Z2, Z305 ; :: thesis: verum

end;( M1i = M1 . i & Kri = Kr . i & KrM1 . i = Kri * M1i ) )

assume Z300: i in dom KrM1 ; :: thesis: ex M1i being Element of ((rank L) -VectSp_over F_Rat) ex Kri being Element of F_Rat st

( M1i = M1 . i & Kri = Kr . i & KrM1 . i = Kri * M1i )

then consider rM1i being Element of ((rank L) -VectSp_over F_Rat) such that

Z301: ( rM1i = rM1 . i & KrM1 . i = K1 * rM1i ) by KRM11;

Z303: i in dom rM1 by Z1, Z300, KRM11, FINSEQ_1:def 3;

Z305: i in dom Kr by Z2, Z300, KRM11, FINSEQ_1:def 3;

Z307: dom M1 = Seg (rank L) by A1, FINSEQ_1:def 3;

then M1 /. i = M1 . i by KRM11, Z300, PARTFUN1:def 6;

then reconsider M1i = M1 . i as Element of ((rank L) -VectSp_over F_Rat) ;

Kr . i = Kr /. i by PARTFUN1:def 6, Z305;

then reconsider Kri = Kr . i as Element of F_Rat by NUMBERS:14;

take M1i ; :: thesis: ex Kri being Element of F_Rat st

( M1i = M1 . i & Kri = Kr . i & KrM1 . i = Kri * M1i )

take Kri ; :: thesis: ( M1i = M1 . i & Kri = Kr . i & KrM1 . i = Kri * M1i )

thus ( M1i = M1 . i & Kri = Kr . i ) ; :: thesis: KrM1 . i = Kri * M1i

thus KrM1 . i = K1 * ((r /. i) * (M1 /. i)) by Z1, Z301, Z303

.= K1 * ((r /. i) * M1i) by Z300, Z307, KRM11, PARTFUN1:def 6

.= (K1 * (r /. i)) * M1i by VECTSP_1:def 16

.= Kri * M1i by Z2, Z305 ; :: thesis: verum

for v being Element of ((rank L) -VectSp_over F_Rat) st k in dom KrM1 & v = rM1 . k holds

KrM1 . k = K1 * v

proof

then Z4A: Sum KrM1 =
K1 * (Sum rM1)
by KRM1, Z1, RLVECT_2:66
let k be Nat; :: thesis: for v being Element of ((rank L) -VectSp_over F_Rat) st k in dom KrM1 & v = rM1 . k holds

KrM1 . k = K1 * v

let v be Element of ((rank L) -VectSp_over F_Rat); :: thesis: ( k in dom KrM1 & v = rM1 . k implies KrM1 . k = K1 * v )

assume Z41: ( k in dom KrM1 & v = rM1 . k ) ; :: thesis: KrM1 . k = K1 * v

then consider rM1i being Element of ((rank L) -VectSp_over F_Rat) such that

Z42: ( rM1i = rM1 . k & KrM1 . k = K1 * rM1i ) by KRM11;

thus KrM1 . k = K1 * v by Z42, Z41; :: thesis: verum

end;KrM1 . k = K1 * v

let v be Element of ((rank L) -VectSp_over F_Rat); :: thesis: ( k in dom KrM1 & v = rM1 . k implies KrM1 . k = K1 * v )

assume Z41: ( k in dom KrM1 & v = rM1 . k ) ; :: thesis: KrM1 . k = K1 * v

then consider rM1i being Element of ((rank L) -VectSp_over F_Rat) such that

Z42: ( rM1i = rM1 . k & KrM1 . k = K1 * rM1i ) by KRM11;

thus KrM1 . k = K1 * v by Z42, Z41; :: thesis: verum

.= 0. ((rank L) -VectSp_over F_Rat) by Z1, VECTSP_1:15 ;

Z4B: Kr <> (Seg (len Kr)) --> (0. INT.Ring)

proof

set SKrM1 = Sum KrM1;
set f = (Seg (len Kr)) --> (0. INT.Ring);

set g = (Seg (len r)) --> (0. F_Rat);

dom r = Seg (len r) by FINSEQ_1:def 3

.= dom ((Seg (len r)) --> (0. F_Rat)) by FUNCT_2:def 1 ;

then consider i being object such that

R1: ( i in dom r & r . i <> ((Seg (len r)) --> (0. F_Rat)) . i ) by Z1;

R2: i in Seg (len r) by FINSEQ_1:def 3, R1;

reconsider i = i as Nat by R1;

r . i <> 0. F_Rat by R1, R2, FUNCOP_1:7;

then R3: r /. i <> 0. INT.Ring by R1, PARTFUN1:def 6;

R9: i in Seg (len Kr) by R1, Z1, Z2, FINSEQ_1:def 3;

then i in dom Kr by FINSEQ_1:def 3;

then Kr . i = K1 * (r /. i) by Z2;

hence Kr <> (Seg (len Kr)) --> (0. INT.Ring) by R3, R9, Z2, FUNCOP_1:7; :: thesis: verum

end;set g = (Seg (len r)) --> (0. F_Rat);

dom r = Seg (len r) by FINSEQ_1:def 3

.= dom ((Seg (len r)) --> (0. F_Rat)) by FUNCT_2:def 1 ;

then consider i being object such that

R1: ( i in dom r & r . i <> ((Seg (len r)) --> (0. F_Rat)) . i ) by Z1;

R2: i in Seg (len r) by FINSEQ_1:def 3, R1;

reconsider i = i as Nat by R1;

r . i <> 0. F_Rat by R1, R2, FUNCOP_1:7;

then R3: r /. i <> 0. INT.Ring by R1, PARTFUN1:def 6;

R9: i in Seg (len Kr) by R1, Z1, Z2, FINSEQ_1:def 3;

then i in dom Kr by FINSEQ_1:def 3;

then Kr . i = K1 * (r /. i) by Z2;

hence Kr <> (Seg (len Kr)) --> (0. INT.Ring) by R3, R9, Z2, FUNCOP_1:7; :: thesis: verum

Z5: for n being Nat st n in dom b holds

(Sum KrM1) . n = 0. INT.Ring

proof

defpred S
let n be Nat; :: thesis: ( n in dom b implies (Sum KrM1) . n = 0. INT.Ring )

assume Z55: n in dom b ; :: thesis: (Sum KrM1) . n = 0. INT.Ring

Z51: addLoopStr(# the carrier of ((rank L) -VectSp_over F_Rat), the addF of ((rank L) -VectSp_over F_Rat), the ZeroF of ((rank L) -VectSp_over F_Rat) #) = (rank L) -Group_over F_Rat by PRVECT_1:def 5;

(rank L) -Group_over F_Rat = addLoopStr(# ((rank L) -tuples_on the carrier of F_Rat),(product ( the addF of F_Rat,(rank L))),((rank L) |-> (0. F_Rat)) #) by PRVECT_1:def 3;

hence (Sum KrM1) . n = 0. INT.Ring by B3, B4, Z4A, Z51, Z55, FUNCOP_1:7; :: thesis: verum

end;assume Z55: n in dom b ; :: thesis: (Sum KrM1) . n = 0. INT.Ring

Z51: addLoopStr(# the carrier of ((rank L) -VectSp_over F_Rat), the addF of ((rank L) -VectSp_over F_Rat), the ZeroF of ((rank L) -VectSp_over F_Rat) #) = (rank L) -Group_over F_Rat by PRVECT_1:def 5;

(rank L) -Group_over F_Rat = addLoopStr(# ((rank L) -tuples_on the carrier of F_Rat),(product ( the addF of F_Rat,(rank L))),((rank L) |-> (0. F_Rat)) #) by PRVECT_1:def 3;

hence (Sum KrM1) . n = 0. INT.Ring by B3, B4, Z4A, Z51, Z55, FUNCOP_1:7; :: thesis: verum

Z510: for k being Nat st k in Seg (rank L) holds

ex x being Element of the carrier of L st S

consider Krb being FinSequence of the carrier of L such that

Z511: ( dom Krb = Seg (rank L) & ( for k being Nat st k in Seg (rank L) holds

S

Z51Z: rank L is Element of NAT by ORDINAL1:def 12;

then Z51: len Krb = rank L by FINSEQ_1:def 3, Z511;

Z6: for n being Nat st n in dom b holds

(Sum KrM1) . n = <;(Sum Krb),(b /. n);>

proof

for n being Nat st n in dom b holds
let n be Nat; :: thesis: ( n in dom b implies (Sum KrM1) . n = <;(Sum Krb),(b /. n);> )

assume Z61: n in dom b ; :: thesis: (Sum KrM1) . n = <;(Sum Krb),(b /. n);>

then consider SKrM1n being FinSequence of F_Rat such that

Z62: ( len SKrM1n = len KrM1 & (Sum KrM1) . n = Sum SKrM1n & ( for k being Nat st k in dom SKrM1n holds

SKrM1n . k = (KrM1 /. k) . n ) ) by B3, B4, LMSUM1;

Z63: len Krb = rank L by Z511, Z51Z, FINSEQ_1:def 3

.= len SKrM1n by Z62, KRM11, KRM1Z, FINSEQ_1:def 3 ;

for k being Nat st k in dom SKrM1n holds

SKrM1n . k = <;(Krb /. k),(b /. n);>

end;assume Z61: n in dom b ; :: thesis: (Sum KrM1) . n = <;(Sum Krb),(b /. n);>

then consider SKrM1n being FinSequence of F_Rat such that

Z62: ( len SKrM1n = len KrM1 & (Sum KrM1) . n = Sum SKrM1n & ( for k being Nat st k in dom SKrM1n holds

SKrM1n . k = (KrM1 /. k) . n ) ) by B3, B4, LMSUM1;

Z63: len Krb = rank L by Z511, Z51Z, FINSEQ_1:def 3

.= len SKrM1n by Z62, KRM11, KRM1Z, FINSEQ_1:def 3 ;

for k being Nat st k in dom SKrM1n holds

SKrM1n . k = <;(Krb /. k),(b /. n);>

proof

hence
(Sum KrM1) . n = <;(Sum Krb),(b /. n);>
by Z62, Z63, LMThGM21; :: thesis: verum
let k be Nat; :: thesis: ( k in dom SKrM1n implies SKrM1n . k = <;(Krb /. k),(b /. n);> )

assume X0: k in dom SKrM1n ; :: thesis: SKrM1n . k = <;(Krb /. k),(b /. n);>

then XX11: k in Seg (len Krb) by Z63, FINSEQ_1:def 3;

then XX1: k in dom Krb by FINSEQ_1:def 3;

then Z65: Krb /. k = Krb . k by PARTFUN1:def 6

.= (Kr /. k) * (b /. k) by Z511, XX1 ;

KrM1 /. k in the carrier of ((rank L) -VectSp_over F_Rat) ;

then KrM1 /. k in (rank L) -tuples_on the carrier of F_Rat by MATRIX13:102;

then consider KrM1k being Element of the carrier of F_Rat * such that

T660: ( KrM1 /. k = KrM1k & len KrM1k = rank L ) ;

T66: ( KrM1k = KrM1 . k & SKrM1n . k = KrM1k . n ) by KRM11, XX1, Z511, T660, Z62, X0, PARTFUN1:def 6;

Z70: k in dom b by XX11, Z511, B3, B4, FINSEQ_1:def 3;

k in dom KrM1 by KRM1, KRM11, X0, Z62, FINSEQ_1:def 3;

then consider M1k being Element of ((rank L) -VectSp_over F_Rat), Krk being Element of F_Rat such that

Z31: ( M1k = M1 . k & Krk = Kr . k & KrM1 . k = Krk * M1k ) by Z3;

E10: [k,n] in Indices M by Z70, Z61, B3, B4, C4, ZFMISC_1:87;

then consider p being FinSequence of F_Rat such that

W34: ( p = M . k & M * (k,n) = p . n ) by MATRIX_0:def 5;

reconsider MMkn = M * (k,n) as Element of F_Rat ;

E3: k in dom Kr by Z2, Z70, B3, B4, FINSEQ_1:def 3;

Z90: KrM1k . n = Krk * (M * (k,n)) by T66, W34, Z31, Z61, B3, B4, LMThGM24

.= (Kr /. k) * (M * (k,n)) by Z31, E3, PARTFUN1:def 6 ;

<;(Krb /. k),(b /. n);> = <;(b /. n),((Kr /. k) * (b /. k));> by Z65, ZMODLAT1:def 3

.= (Kr /. k) * <;(b /. n),(b /. k);> by ZMODLAT1:9

.= (Kr /. k) * <;(b /. k),(b /. n);> by ZMODLAT1:def 3

.= (Kr /. k) * ((InnerProduct L) . ((b /. k),(b /. n)))

.= (Kr /. k) * ((BilinearM ((InnerProduct L),b,b)) * (k,n)) by ZMODLAT1:def 32, Z61, Z70

.= (Kr /. k) * (M * (k,n)) by E10, ZMATRLIN:1

.= SKrM1n . k by T660, Z62, X0, Z90 ;

hence SKrM1n . k = <;(Krb /. k),(b /. n);> ; :: thesis: verum

end;assume X0: k in dom SKrM1n ; :: thesis: SKrM1n . k = <;(Krb /. k),(b /. n);>

then XX11: k in Seg (len Krb) by Z63, FINSEQ_1:def 3;

then XX1: k in dom Krb by FINSEQ_1:def 3;

then Z65: Krb /. k = Krb . k by PARTFUN1:def 6

.= (Kr /. k) * (b /. k) by Z511, XX1 ;

KrM1 /. k in the carrier of ((rank L) -VectSp_over F_Rat) ;

then KrM1 /. k in (rank L) -tuples_on the carrier of F_Rat by MATRIX13:102;

then consider KrM1k being Element of the carrier of F_Rat * such that

T660: ( KrM1 /. k = KrM1k & len KrM1k = rank L ) ;

T66: ( KrM1k = KrM1 . k & SKrM1n . k = KrM1k . n ) by KRM11, XX1, Z511, T660, Z62, X0, PARTFUN1:def 6;

Z70: k in dom b by XX11, Z511, B3, B4, FINSEQ_1:def 3;

k in dom KrM1 by KRM1, KRM11, X0, Z62, FINSEQ_1:def 3;

then consider M1k being Element of ((rank L) -VectSp_over F_Rat), Krk being Element of F_Rat such that

Z31: ( M1k = M1 . k & Krk = Kr . k & KrM1 . k = Krk * M1k ) by Z3;

E10: [k,n] in Indices M by Z70, Z61, B3, B4, C4, ZFMISC_1:87;

then consider p being FinSequence of F_Rat such that

W34: ( p = M . k & M * (k,n) = p . n ) by MATRIX_0:def 5;

reconsider MMkn = M * (k,n) as Element of F_Rat ;

E3: k in dom Kr by Z2, Z70, B3, B4, FINSEQ_1:def 3;

Z90: KrM1k . n = Krk * (M * (k,n)) by T66, W34, Z31, Z61, B3, B4, LMThGM24

.= (Kr /. k) * (M * (k,n)) by Z31, E3, PARTFUN1:def 6 ;

<;(Krb /. k),(b /. n);> = <;(b /. n),((Kr /. k) * (b /. k));> by Z65, ZMODLAT1:def 3

.= (Kr /. k) * <;(b /. n),(b /. k);> by ZMODLAT1:9

.= (Kr /. k) * <;(b /. k),(b /. n);> by ZMODLAT1:def 3

.= (Kr /. k) * ((InnerProduct L) . ((b /. k),(b /. n)))

.= (Kr /. k) * ((BilinearM ((InnerProduct L),b,b)) * (k,n)) by ZMODLAT1:def 32, Z61, Z70

.= (Kr /. k) * (M * (k,n)) by E10, ZMATRLIN:1

.= SKrM1n . k by T660, Z62, X0, Z90 ;

hence SKrM1n . k = <;(Krb /. k),(b /. n);> ; :: thesis: verum

<;(0. L),(b /. n);> = <;(Sum Krb),(b /. n);>

proof

then Z8:
Sum Krb = 0. L
by ZL2ThSc1X;
let n be Nat; :: thesis: ( n in dom b implies <;(0. L),(b /. n);> = <;(Sum Krb),(b /. n);> )

assume Z71: n in dom b ; :: thesis: <;(0. L),(b /. n);> = <;(Sum Krb),(b /. n);>

thus <;(0. L),(b /. n);> = 0. INT.Ring by ZMODLAT1:12

.= (Sum KrM1) . n by Z5, Z71

.= <;(Sum Krb),(b /. n);> by Z6, Z71 ; :: thesis: verum

end;assume Z71: n in dom b ; :: thesis: <;(0. L),(b /. n);> = <;(Sum Krb),(b /. n);>

thus <;(0. L),(b /. n);> = 0. INT.Ring by ZMODLAT1:12

.= (Sum KrM1) . n by Z5, Z71

.= <;(Sum Krb),(b /. n);> by Z6, Z71 ; :: thesis: verum

Z9: b is one-to-one by ZMATRLIN:def 5;

len Kr = len b by B3, B4, Z2, FINSEQ_1:def 3;

then rng b is linearly-dependent by Z51, Z511, Z4B, Z2, Z8, Z9, LMBASE2;

then not rng b is base by VECTSP_7:def 3;

hence contradiction by ZMATRLIN:def 5; :: thesis: verum