let L be non trivial positive-definite RATional Z_Lattice; :: thesis: for b being OrdBasis of L ex a being Element of F_Real st

( a is Element of INT.Ring & a <> 0 & a * ((GramMatrix b) ~) is Matrix of dim L,INT.Ring )

let b be OrdBasis of L; :: thesis: ex a being Element of F_Real st

( a is Element of INT.Ring & a <> 0 & a * ((GramMatrix b) ~) is Matrix of dim L,INT.Ring )

set G = (GramMatrix b) ~ ;

reconsider M = (GramMatrix b) ~ as Matrix of dim L,F_Rat by ThGM3;

A2: rng M c= the carrier of F_Rat * ;

A5: ( len M = dim L & width M = dim L ) by MATRIX_0:24;

B1: for i, j being Nat st [i,j] in Indices ((GramMatrix b) ~) holds

((GramMatrix b) ~) * (i,j) in the carrier of F_Rat_{1}( Nat, Nat) -> Element of the carrier of F_Real = ((GramMatrix b) ~) * ($1,$2);

set Dn = { H_{1}(u,v) where u, v is Element of NAT : ( u in Seg (len ((GramMatrix b) ~)) & v in Seg (width ((GramMatrix b) ~)) ) } ;

F1: Seg (len ((GramMatrix b) ~)) is finite ;

F2: Seg (width ((GramMatrix b) ~)) is finite ;

F3: { H_{1}(u,v) where u, v is Element of NAT : ( u in Seg (len ((GramMatrix b) ~)) & v in Seg (width ((GramMatrix b) ~)) ) } is finite
from FRAENKEL:sch 22(F1, F2);

D2: { (((GramMatrix b) ~) * (i,j)) where i, j is Nat : [i,j] in Indices ((GramMatrix b) ~) } c= { H_{1}(u,v) where u, v is Element of NAT : ( u in Seg (len ((GramMatrix b) ~)) & v in Seg (width ((GramMatrix b) ~)) ) }

consider a being Element of INT such that

A10: ( a <> 0 & ( for r being Element of RAT st r in X holds

a * r in INT ) ) by LmDE311A;

reconsider a = a as Element of F_Real by NUMBERS:15;

A6: ( len (a * ((GramMatrix b) ~)) = dim L & width (a * ((GramMatrix b) ~)) = dim L ) by MATRIX_0:24;

take a ; :: thesis: ( a is Element of INT.Ring & a <> 0 & a * ((GramMatrix b) ~) is Matrix of dim L,INT.Ring )

thus ( a is Element of INT.Ring & a <> 0 ) by A10; :: thesis: a * ((GramMatrix b) ~) is Matrix of dim L,INT.Ring

for i, j being Nat st [i,j] in Indices (a * ((GramMatrix b) ~)) holds

(a * ((GramMatrix b) ~)) * (i,j) in the carrier of INT.Ring

( a is Element of INT.Ring & a <> 0 & a * ((GramMatrix b) ~) is Matrix of dim L,INT.Ring )

let b be OrdBasis of L; :: thesis: ex a being Element of F_Real st

( a is Element of INT.Ring & a <> 0 & a * ((GramMatrix b) ~) is Matrix of dim L,INT.Ring )

set G = (GramMatrix b) ~ ;

reconsider M = (GramMatrix b) ~ as Matrix of dim L,F_Rat by ThGM3;

A2: rng M c= the carrier of F_Rat * ;

A5: ( len M = dim L & width M = dim L ) by MATRIX_0:24;

B1: for i, j being Nat st [i,j] in Indices ((GramMatrix b) ~) holds

((GramMatrix b) ~) * (i,j) in the carrier of F_Rat

proof

deffunc H
let i, j be Nat; :: thesis: ( [i,j] in Indices ((GramMatrix b) ~) implies ((GramMatrix b) ~) * (i,j) in the carrier of F_Rat )

assume B10: [i,j] in Indices ((GramMatrix b) ~) ; :: thesis: ((GramMatrix b) ~) * (i,j) in the carrier of F_Rat

then consider p being FinSequence of F_Real such that

B11: ( p = ((GramMatrix b) ~) . i & ((GramMatrix b) ~) * (i,j) = p . j ) by MATRIX_0:def 5;

B12: ( i in dom ((GramMatrix b) ~) & j in Seg (width ((GramMatrix b) ~)) ) by ZFMISC_1:87, B10;

then p in rng ((GramMatrix b) ~) by B11, FUNCT_1:3;

then B14: len p = width ((GramMatrix b) ~) by A5, MATRIX_0:def 3;

p in the carrier of F_Rat * by A2, B11, B12, FUNCT_1:3;

then p is FinSequence of F_Rat by FINSEQ_1:def 11;

then B15: rng p c= the carrier of F_Rat by FINSEQ_1:def 4;

j in dom p by B12, B14, FINSEQ_1:def 3;

hence ((GramMatrix b) ~) * (i,j) in the carrier of F_Rat by B11, B15, FUNCT_1:3; :: thesis: verum

end;assume B10: [i,j] in Indices ((GramMatrix b) ~) ; :: thesis: ((GramMatrix b) ~) * (i,j) in the carrier of F_Rat

then consider p being FinSequence of F_Real such that

B11: ( p = ((GramMatrix b) ~) . i & ((GramMatrix b) ~) * (i,j) = p . j ) by MATRIX_0:def 5;

B12: ( i in dom ((GramMatrix b) ~) & j in Seg (width ((GramMatrix b) ~)) ) by ZFMISC_1:87, B10;

then p in rng ((GramMatrix b) ~) by B11, FUNCT_1:3;

then B14: len p = width ((GramMatrix b) ~) by A5, MATRIX_0:def 3;

p in the carrier of F_Rat * by A2, B11, B12, FUNCT_1:3;

then p is FinSequence of F_Rat by FINSEQ_1:def 11;

then B15: rng p c= the carrier of F_Rat by FINSEQ_1:def 4;

j in dom p by B12, B14, FINSEQ_1:def 3;

hence ((GramMatrix b) ~) * (i,j) in the carrier of F_Rat by B11, B15, FUNCT_1:3; :: thesis: verum

set Dn = { H

F1: Seg (len ((GramMatrix b) ~)) is finite ;

F2: Seg (width ((GramMatrix b) ~)) is finite ;

F3: { H

D2: { (((GramMatrix b) ~) * (i,j)) where i, j is Nat : [i,j] in Indices ((GramMatrix b) ~) } c= { H

proof

{ (((GramMatrix b) ~) * (i,j)) where i, j is Nat : [i,j] in Indices ((GramMatrix b) ~) } c= the carrier of F_Rat
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (((GramMatrix b) ~) * (i,j)) where i, j is Nat : [i,j] in Indices ((GramMatrix b) ~) } or x in { H_{1}(u,v) where u, v is Element of NAT : ( u in Seg (len ((GramMatrix b) ~)) & v in Seg (width ((GramMatrix b) ~)) ) } )

assume x in { (((GramMatrix b) ~) * (i,j)) where i, j is Nat : [i,j] in Indices ((GramMatrix b) ~) } ; :: thesis: x in { H_{1}(u,v) where u, v is Element of NAT : ( u in Seg (len ((GramMatrix b) ~)) & v in Seg (width ((GramMatrix b) ~)) ) }

then consider i, j being Nat such that

F40: ( x = ((GramMatrix b) ~) * (i,j) & [i,j] in Indices ((GramMatrix b) ~) ) ;

( i in dom ((GramMatrix b) ~) & j in Seg (width ((GramMatrix b) ~)) ) by ZFMISC_1:87, F40;

then ( i in Seg (len ((GramMatrix b) ~)) & j in Seg (width ((GramMatrix b) ~)) ) by FINSEQ_1:def 3;

hence x in { H_{1}(u,v) where u, v is Element of NAT : ( u in Seg (len ((GramMatrix b) ~)) & v in Seg (width ((GramMatrix b) ~)) ) }
by F40; :: thesis: verum

end;assume x in { (((GramMatrix b) ~) * (i,j)) where i, j is Nat : [i,j] in Indices ((GramMatrix b) ~) } ; :: thesis: x in { H

then consider i, j being Nat such that

F40: ( x = ((GramMatrix b) ~) * (i,j) & [i,j] in Indices ((GramMatrix b) ~) ) ;

( i in dom ((GramMatrix b) ~) & j in Seg (width ((GramMatrix b) ~)) ) by ZFMISC_1:87, F40;

then ( i in Seg (len ((GramMatrix b) ~)) & j in Seg (width ((GramMatrix b) ~)) ) by FINSEQ_1:def 3;

hence x in { H

proof

then reconsider X = { (((GramMatrix b) ~) * (i,j)) where i, j is Nat : [i,j] in Indices ((GramMatrix b) ~) } as finite Subset of F_Rat by D2, F3;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (((GramMatrix b) ~) * (i,j)) where i, j is Nat : [i,j] in Indices ((GramMatrix b) ~) } or x in the carrier of F_Rat )

assume x in { (((GramMatrix b) ~) * (i,j)) where i, j is Nat : [i,j] in Indices ((GramMatrix b) ~) } ; :: thesis: x in the carrier of F_Rat

then consider i, j being Nat such that

D1: ( x = ((GramMatrix b) ~) * (i,j) & [i,j] in Indices ((GramMatrix b) ~) ) ;

thus x in the carrier of F_Rat by B1, D1; :: thesis: verum

end;assume x in { (((GramMatrix b) ~) * (i,j)) where i, j is Nat : [i,j] in Indices ((GramMatrix b) ~) } ; :: thesis: x in the carrier of F_Rat

then consider i, j being Nat such that

D1: ( x = ((GramMatrix b) ~) * (i,j) & [i,j] in Indices ((GramMatrix b) ~) ) ;

thus x in the carrier of F_Rat by B1, D1; :: thesis: verum

consider a being Element of INT such that

A10: ( a <> 0 & ( for r being Element of RAT st r in X holds

a * r in INT ) ) by LmDE311A;

reconsider a = a as Element of F_Real by NUMBERS:15;

A6: ( len (a * ((GramMatrix b) ~)) = dim L & width (a * ((GramMatrix b) ~)) = dim L ) by MATRIX_0:24;

take a ; :: thesis: ( a is Element of INT.Ring & a <> 0 & a * ((GramMatrix b) ~) is Matrix of dim L,INT.Ring )

thus ( a is Element of INT.Ring & a <> 0 ) by A10; :: thesis: a * ((GramMatrix b) ~) is Matrix of dim L,INT.Ring

for i, j being Nat st [i,j] in Indices (a * ((GramMatrix b) ~)) holds

(a * ((GramMatrix b) ~)) * (i,j) in the carrier of INT.Ring

proof

hence
a * ((GramMatrix b) ~) is Matrix of dim L,INT.Ring
by A6, MATRIX_0:20, ZMATRLIN:5; :: thesis: verum
let i, j be Nat; :: thesis: ( [i,j] in Indices (a * ((GramMatrix b) ~)) implies (a * ((GramMatrix b) ~)) * (i,j) in the carrier of INT.Ring )

assume B1: [i,j] in Indices (a * ((GramMatrix b) ~)) ; :: thesis: (a * ((GramMatrix b) ~)) * (i,j) in the carrier of INT.Ring

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

.= Indices (a * ((GramMatrix b) ~)) by MATRIX_0:24 ;

then B3: (a * ((GramMatrix b) ~)) * (i,j) = a * (((GramMatrix b) ~) * (i,j)) by B1, MATRIX_3:def 5;

((GramMatrix b) ~) * (i,j) in X by B1, B2;

hence (a * ((GramMatrix b) ~)) * (i,j) in the carrier of INT.Ring by A10, B3; :: thesis: verum

end;assume B1: [i,j] in Indices (a * ((GramMatrix b) ~)) ; :: thesis: (a * ((GramMatrix b) ~)) * (i,j) in the carrier of INT.Ring

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

.= Indices (a * ((GramMatrix b) ~)) by MATRIX_0:24 ;

then B3: (a * ((GramMatrix b) ~)) * (i,j) = a * (((GramMatrix b) ~) * (i,j)) by B1, MATRIX_3:def 5;

((GramMatrix b) ~) * (i,j) in X by B1, B2;

hence (a * ((GramMatrix b) ~)) * (i,j) in the carrier of INT.Ring by A10, B3; :: thesis: verum