let L be Z_Lattice; :: thesis: for b being OrdBasis of L st GramMatrix ((InnerProduct L),b) is Matrix of dim L,F_Rat holds

L is RATional

let b be OrdBasis of L; :: thesis: ( GramMatrix ((InnerProduct L),b) is Matrix of dim L,F_Rat implies L is RATional )

assume A1: GramMatrix ((InnerProduct L),b) is Matrix of dim L,F_Rat ; :: thesis: L is RATional

set I = rng b;

reconsider I = rng b as Basis of L by ZMATRLIN:def 5;

set GM = GramMatrix ((InnerProduct L),b);

reconsider GMR = GramMatrix ((InnerProduct L),b) as Matrix of dim L,F_Rat by A1;

for v, u being Vector of L st v in I & u in I holds

<;v,u;> in RAT

L is RATional

let b be OrdBasis of L; :: thesis: ( GramMatrix ((InnerProduct L),b) is Matrix of dim L,F_Rat implies L is RATional )

assume A1: GramMatrix ((InnerProduct L),b) is Matrix of dim L,F_Rat ; :: thesis: L is RATional

set I = rng b;

reconsider I = rng b as Basis of L by ZMATRLIN:def 5;

set GM = GramMatrix ((InnerProduct L),b);

reconsider GMR = GramMatrix ((InnerProduct L),b) as Matrix of dim L,F_Rat by A1;

for v, u being Vector of L st v in I & u in I holds

<;v,u;> in RAT

proof

hence
L is RATional
by ThRatLat1; :: thesis: verum
let v, u be Vector of L; :: thesis: ( v in I & u in I implies <;v,u;> in RAT )

assume B1: ( v in I & u in I ) ; :: thesis: <;v,u;> in RAT

consider i being Nat such that

B2: ( i in dom b & b . i = v ) by B1, FINSEQ_2:10;

consider j being Nat such that

B3: ( j in dom b & b . j = u ) by B1, FINSEQ_2:10;

B4: b /. i = v by B2, PARTFUN1:def 6;

B6: (GramMatrix ((InnerProduct L),b)) * (i,j) = (InnerProduct L) . ((b /. i),(b /. j)) by B2, B3, ZMODLAT1:def 32

.= <;v,u;> by B3, B4, PARTFUN1:def 6 ;

B7: dom b = Seg (len b) by FINSEQ_1:def 3

.= Seg (dim L) by ZMATRLIN:49 ;

Indices (GramMatrix ((InnerProduct L),b)) = [:(Seg (dim L)),(Seg (dim L)):] by MATRIX_0:24;

then [i,j] in Indices (GramMatrix ((InnerProduct L),b)) by B2, B3, B7, ZFMISC_1:87;

then (GramMatrix ((InnerProduct L),b)) * (i,j) = GMR * (i,j) by ZMATRLIN:1;

hence <;v,u;> in RAT by B6; :: thesis: verum

end;assume B1: ( v in I & u in I ) ; :: thesis: <;v,u;> in RAT

consider i being Nat such that

B2: ( i in dom b & b . i = v ) by B1, FINSEQ_2:10;

consider j being Nat such that

B3: ( j in dom b & b . j = u ) by B1, FINSEQ_2:10;

B4: b /. i = v by B2, PARTFUN1:def 6;

B6: (GramMatrix ((InnerProduct L),b)) * (i,j) = (InnerProduct L) . ((b /. i),(b /. j)) by B2, B3, ZMODLAT1:def 32

.= <;v,u;> by B3, B4, PARTFUN1:def 6 ;

B7: dom b = Seg (len b) by FINSEQ_1:def 3

.= Seg (dim L) by ZMATRLIN:49 ;

Indices (GramMatrix ((InnerProduct L),b)) = [:(Seg (dim L)),(Seg (dim L)):] by MATRIX_0:24;

then [i,j] in Indices (GramMatrix ((InnerProduct L),b)) by B2, B3, B7, ZFMISC_1:87;

then (GramMatrix ((InnerProduct L),b)) * (i,j) = GMR * (i,j) by ZMATRLIN:1;

hence <;v,u;> in RAT by B6; :: thesis: verum