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

L is INTegral

let b be OrdBasis of L; :: thesis: ( GramMatrix ((InnerProduct L),b) is Matrix of dim L,INT.Ring implies L is INTegral )

assume A1: GramMatrix ((InnerProduct L),b) is Matrix of dim L,INT.Ring ; :: thesis: L is INTegral

set I = rng b;

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

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

reconsider GMI = GramMatrix ((InnerProduct L),b) as Matrix of dim L,INT.Ring by A1;

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

<;v,u;> in INT

L is INTegral

let b be OrdBasis of L; :: thesis: ( GramMatrix ((InnerProduct L),b) is Matrix of dim L,INT.Ring implies L is INTegral )

assume A1: GramMatrix ((InnerProduct L),b) is Matrix of dim L,INT.Ring ; :: thesis: L is INTegral

set I = rng b;

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

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

reconsider GMI = GramMatrix ((InnerProduct L),b) as Matrix of dim L,INT.Ring by A1;

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

<;v,u;> in INT

proof

hence
L is INTegral
by ZMODLAT1:15; :: thesis: verum
let v, u be Vector of L; :: thesis: ( v in I & u in I implies <;v,u;> in INT )

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

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) = GMI * (i,j) by ZMATRLIN:1;

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

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

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) = GMI * (i,j) by ZMATRLIN:1;

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