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

proof

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;

deffunc H₁( Nat, Nat) -> Element of the carrier of F_Real = ((GramMatrix b) ~) * ($1,$2);
set Dn = { H₁(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₁(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₁(u,v) where u, v is Element of NAT : ( u in Seg (len ((GramMatrix b) ~)) & v in Seg (width ((GramMatrix b) ~)) ) }

proof

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₁(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₁(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₁(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;

{ (((GramMatrix b) ~) * (i,j)) where i, j is Nat : [i,j] in Indices ((GramMatrix b) ~) } c= the carrier of F_Rat

proof

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;

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;
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

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;

hence a * ((GramMatrix b) ~) is Matrix of dim L,INT.Ring by A6, MATRIX_0:20, ZMATRLIN:5; :: thesis: verum