let L be non trivial positive-definite RATional Z_Lattice; 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; 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;
( [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) ~)
;
((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;
verum
end;
deffunc H1( Nat, Nat) -> Element of the carrier of F_Real = ((GramMatrix b) ~) * ($1,$2);
set Dn = { H1(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:
{ H1(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= { H1(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 ;
TARSKI:def 3 ( not x in { (((GramMatrix b) ~) * (i,j)) where i, j is Nat : [i,j] in Indices ((GramMatrix b) ~) } or x in { H1(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) ~) }
;
x in { H1(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 { H1(u,v) where u, v is Element of NAT : ( u in Seg (len ((GramMatrix b) ~)) & v in Seg (width ((GramMatrix b) ~)) ) }
by F40;
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 ;
TARSKI:def 3 ( 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) ~) }
;
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;
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
; ( 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; 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;
( [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) ~))
;
(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;
verum
end;
hence
a * ((GramMatrix b) ~) is Matrix of dim L,INT.Ring
by A6, MATRIX_0:20, ZMATRLIN:5; verum