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
proof
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);>
proof
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;
b . m1 = b /. m1 by B1, B4, PARTFUN1:def 6
.= 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 AA1: lines M is linearly-dependent by A2, MATRIX13:121;
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 S1[ 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 S1[k,x]
proof
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 S1[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 S1[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 S1[k,x] ; :: thesis: verum
end;
consider KrM1 being FinSequence of the carrier of ((rank L) -VectSp_over F_Rat) such that
KRM11: ( dom KrM1 = Seg (rank L) & ( for k being Nat st k in Seg (rank L) holds
S1[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 )
proof
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;
for k being Nat
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
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;
then Z4A: Sum KrM1 = K1 * (Sum rM1) by KRM1, Z1, RLVECT_2:66
.= 0. ((rank L) -VectSp_over F_Rat) by Z1, VECTSP_1:15 ;
Z4B: Kr <> (Seg (len Kr)) --> (0. INT.Ring)
proof
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 SKrM1 = Sum KrM1;
Z5: for n being Nat st n in dom b holds
(Sum KrM1) . n = 0. INT.Ring
proof
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;
defpred S2[ 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 S2[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
S2[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);>
proof
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);>
proof
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;
hence (Sum KrM1) . n = <;(Sum Krb),(b /. n);> by Z62, Z63, LMThGM21; :: thesis: verum
end;
for n being Nat st n in dom b holds
<;(0. L),(b /. n);> = <;(Sum Krb),(b /. n);>
proof
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;
then Z8: Sum Krb = 0. L by ZL2ThSc1X;
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