let L be non trivial positive-definite RATional Z_Lattice; :: thesis: for b being OrdBasis of L holds Det () <> 0. F_Real
let b be OrdBasis of L; :: thesis:
reconsider M = GramMatrix b as Matrix of rank L,F_Rat by ThGM1;
assume Det () = 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 ;
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
.= dom b by FINSEQ_1:def 3 ;
( dom b = Seg (rank L) & rank L is Element of NAT ) by ;
then len b = rank L by FINSEQ_1:def 3;
then C4: Indices (BilinearM ((),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 ()) by FINSEQ_1:def 3
.= Seg (rank L) by MATRIX_0:def 2 ;
B4: dom M = Seg (len b) by
.= 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 ((),b,b)) by ;
C6: [m2,n] in Indices (BilinearM ((),b,b)) by ;
X1: ex p being FinSequence of F_Real st
( p = (BilinearM ((),b,b)) . m1 & (BilinearM ((),b,b)) * (m1,n) = p . n ) by ;
thus <;(b /. n),(b /. m1);> = <;(b /. m1),(b /. n);> by ZMODLAT1:def 3
.= () . ((b /. m1),(b /. n))
.= (BilinearM ((),b,b)) * (m1,n) by
.= (BilinearM ((),b,b)) * (m2,n) by
.= () . ((b /. m2),(b /. n)) by
.= <;(b /. m2),(b /. n);>
.= <;(b /. n),(b /. m2);> by ZMODLAT1:def 3 ; :: thesis: verum
end;
b . m1 = b /. m1 by
.= b /. m2 by
.= b . m2 by ;
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 ;
lines M c= the carrier of () ;
then reconsider M1 = M as FinSequence of () by FINSEQ_1:def 4;
consider r being FinSequence of F_Rat, rM1 being FinSequence of () 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. () & r <> (Seg (len r)) --> () ) by ;
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 ;
reconsider K1 = K as Element of F_Rat by ;
defpred S1[ Nat, object ] means ex rM1i being Element of () 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 () st S1[k,x]
proof
let k be Nat; :: thesis: ( k in Seg (rank L) implies ex x being Element of the carrier of () st S1[k,x] )
assume KRM12: k in Seg (rank L) ; :: thesis: ex x being Element of the carrier of () st S1[k,x]
dom rM1 = Seg (rank L) by ;
then rM1 . k = rM1 /. k by ;
then reconsider rM1i = rM1 . k as Element of () ;
K1 * rM1i is Element of the carrier of () ;
hence ex x being Element of the carrier of () st S1[k,x] ; :: thesis: verum
end;
consider KrM1 being FinSequence of the carrier of () such that
KRM11: ( dom KrM1 = Seg (rank L) & ( for k being Nat st k in Seg (rank L) holds
S1[k,KrM1 . k] ) ) from KRM1Z: rank L is Element of NAT by ORDINAL1:def 12;
then KRM1: len KrM1 = rank L by ;
Z3: for i being Nat st i in dom KrM1 holds
ex M1i being Element of () 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 () 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 () ex Kri being Element of F_Rat st
( M1i = M1 . i & Kri = Kr . i & KrM1 . i = Kri * M1i )

then consider rM1i being Element of () such that
Z301: ( rM1i = rM1 . i & KrM1 . i = K1 * rM1i ) by KRM11;
Z303: i in dom rM1 by ;
Z305: i in dom Kr by ;
Z307: dom M1 = Seg (rank L) by ;
then M1 /. i = M1 . i by ;
then reconsider M1i = M1 . i as Element of () ;
Kr . i = Kr /. i by ;
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
.= K1 * ((r /. i) * M1i) by
.= (K1 * (r /. i)) * M1i by VECTSP_1:def 16
.= Kri * M1i by ; :: thesis: verum
end;
for k being Nat
for v being Element of () st k in dom KrM1 & v = rM1 . k holds
KrM1 . k = K1 * v
proof
let k be Nat; :: thesis: for v being Element of () st k in dom KrM1 & v = rM1 . k holds
KrM1 . k = K1 * v

let v be Element of (); :: 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 () such that
Z42: ( rM1i = rM1 . k & KrM1 . k = K1 * rM1i ) by KRM11;
thus KrM1 . k = K1 * v by ; :: thesis: verum
end;
then Z4A: Sum KrM1 = K1 * (Sum rM1) by
.= 0. () by ;
Z4B: Kr <> (Seg (len Kr)) --> ()
proof
set f = (Seg (len Kr)) --> ();
set g = (Seg (len r)) --> ();
dom r = Seg (len r) by FINSEQ_1:def 3
.= dom ((Seg (len r)) --> ()) by FUNCT_2:def 1 ;
then consider i being object such that
R1: ( i in dom r & r . i <> ((Seg (len r)) --> ()) . i ) by Z1;
R2: i in Seg (len r) by ;
reconsider i = i as Nat by R1;
r . i <> 0. F_Rat by ;
then R3: r /. i <> 0. INT.Ring by ;
R9: i in Seg (len Kr) by ;
then i in dom Kr by FINSEQ_1:def 3;
then Kr . i = K1 * (r /. i) by Z2;
hence Kr <> (Seg (len Kr)) --> () by ; :: 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 (), the addF of (), the ZeroF of () #) = (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) |-> ()) #) by PRVECT_1:def 3;
hence (Sum KrM1) . n = 0. INT.Ring by ; :: 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 Z51Z: rank L is Element of NAT by ORDINAL1:def 12;
then Z51: len Krb = rank L by ;
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 ;
Z63: len Krb = rank L by
.= len SKrM1n by ;
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 ;
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 ;
KrM1 /. k in the carrier of () ;
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 ;
Z70: k in dom b by ;
k in dom KrM1 by ;
then consider M1k being Element of (), 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 ;
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 ;
Z90: KrM1k . n = Krk * (M * (k,n)) by T66, W34, Z31, Z61, B3, B4, LMThGM24
.= (Kr /. k) * (M * (k,n)) by ;
<;(Krb /. k),(b /. n);> = <;(b /. n),((Kr /. k) * (b /. k));> by
.= (Kr /. k) * <;(b /. n),(b /. k);> by ZMODLAT1:9
.= (Kr /. k) * <;(b /. k),(b /. n);> by ZMODLAT1:def 3
.= (Kr /. k) * (() . ((b /. k),(b /. n)))
.= (Kr /. k) * ((BilinearM ((),b,b)) * (k,n)) by
.= (Kr /. k) * (M * (k,n)) by
.= 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 ; :: 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
.= <;(Sum Krb),(b /. n);> by ; :: 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 ;
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