let L be non trivial positive-definite RATional Z_Lattice; for b being OrdBasis of EMLat L
for i being Nat st i in dom b holds
ex v being Vector of (DivisibleMod L) st
( (ScProductDM L) . ((b /. i),v) = 1 & ( for j being Nat st i <> j & j in dom b holds
(ScProductDM L) . ((b /. j),v) = 0 ) )
let b be OrdBasis of EMLat L; for i being Nat st i in dom b holds
ex v being Vector of (DivisibleMod L) st
( (ScProductDM L) . ((b /. i),v) = 1 & ( for j being Nat st i <> j & j in dom b holds
(ScProductDM L) . ((b /. j),v) = 0 ) )
let i be Nat; ( i in dom b implies ex v being Vector of (DivisibleMod L) st
( (ScProductDM L) . ((b /. i),v) = 1 & ( for j being Nat st i <> j & j in dom b holds
(ScProductDM L) . ((b /. j),v) = 0 ) ) )
assume A1:
i in dom b
; ex v being Vector of (DivisibleMod L) st
( (ScProductDM L) . ((b /. i),v) = 1 & ( for j being Nat st i <> j & j in dom b holds
(ScProductDM L) . ((b /. j),v) = 0 ) )
A2:
dim L = dim (EMLat L)
by ZMODLAT2:42;
consider a being Element of F_Real such that
A3:
( a is Element of INT.Ring & a <> 0 & a * ((GramMatrix b) ~) is Matrix of dim L,INT.Ring )
by A2, LmDE311;
(GramMatrix b) ~ is_reverse_of GramMatrix b
by MATRIX_6:def 4;
then A5: ((GramMatrix b) ~) * (GramMatrix b) =
1. (F_Real,(dim (EMLat L)))
by MATRIX_6:def 2
.=
1. (F_Real,(dim L))
by ZMODLAT2:42
;
len ((GramMatrix b) ~) = dim (EMLat L)
by MATRIX_0:def 2;
then width ((GramMatrix b) ~) =
dim (EMLat L)
by MATRIX_0:20
.=
len (GramMatrix b)
by MATRIX_0:def 2
;
then A8:
(a * ((GramMatrix b) ~)) * (GramMatrix b) = a * (1. (F_Real,(dim L)))
by A5, MATRIX15:1;
AX1:
len b = dim (EMLat L)
by ZMATRLIN:49;
then A9:
i in Seg (dim L)
by A1, A2, FINSEQ_1:def 3;
A10:
Indices (1. (F_Real,(dim L))) = [:(Seg (dim L)),(Seg (dim L)):]
by MATRIX_0:24;
then A11:
[i,i] in Indices (1. (F_Real,(dim L)))
by A9, ZFMISC_1:87;
A12:
Indices (a * (1. (F_Real,(dim L)))) = [:(Seg (dim L)),(Seg (dim L)):]
by MATRIX_0:24;
then A14:
[i,i] in Indices ((a * ((GramMatrix b) ~)) * (GramMatrix b))
by A8, A9, ZFMISC_1:87;
AX3: width (a * ((GramMatrix b) ~)) =
dim (EMLat L)
by MATRIX_0:23
.=
len (GramMatrix b)
by MATRIX_0:def 2
;
A15: (Line ((a * ((GramMatrix b) ~)),i)) "*" (Col ((GramMatrix b),i)) =
((a * ((GramMatrix b) ~)) * (GramMatrix b)) * (i,i)
by A14, AX3, MATRIX_3:def 4
.=
a * ((1. (F_Real,(dim L))) * (i,i))
by A8, A11, MATRIX_3:def 5
.=
a * (1. F_Real)
by A11, MATRIX_1:def 3
.=
a
;
A16:
for j being Nat st i <> j & j in dom b holds
(Line ((a * ((GramMatrix b) ~)),i)) "*" (Col ((GramMatrix b),j)) = 0
proof
let j be
Nat;
( i <> j & j in dom b implies (Line ((a * ((GramMatrix b) ~)),i)) "*" (Col ((GramMatrix b),j)) = 0 )
assume B1:
(
i <> j &
j in dom b )
;
(Line ((a * ((GramMatrix b) ~)),i)) "*" (Col ((GramMatrix b),j)) = 0
B2:
j in Seg (dim L)
by A2, AX1, B1, FINSEQ_1:def 3;
then B3:
[i,j] in Indices (1. (F_Real,(dim L)))
by A9, A10, ZFMISC_1:87;
[i,j] in Indices ((a * ((GramMatrix b) ~)) * (GramMatrix b))
by A8, A9, A12, B2, ZFMISC_1:87;
hence (Line ((a * ((GramMatrix b) ~)),i)) "*" (Col ((GramMatrix b),j)) =
((a * ((GramMatrix b) ~)) * (GramMatrix b)) * (
i,
j)
by AX3, MATRIX_3:def 4
.=
a * ((1. (F_Real,(dim L))) * (i,j))
by A8, B3, MATRIX_3:def 5
.=
a * (0. F_Real)
by B1, B3, MATRIX_1:def 3
.=
0
;
verum
end;
reconsider I = rng b as Basis of (EMLat L) by ZMATRLIN:def 5;
defpred S1[ object , object ] means ( ( $1 in I implies for n being Nat st n = (b ") . $1 & n in dom b holds
$2 = (a * ((GramMatrix b) ~)) * (i,n) ) & ( not $1 in I implies $2 = 0. INT.Ring ) );
A17:
for x being Element of (EMLat L) ex y being Element of INT.Ring st S1[x,y]
proof
let x be
Element of
(EMLat L);
ex y being Element of INT.Ring st S1[x,y]
per cases
( x in I or not x in I )
;
suppose B1:
x in I
;
ex y being Element of INT.Ring st S1[x,y]
b is
one-to-one
by ZMATRLIN:def 5;
then B3:
(b ") . x in dom b
by B1, FUNCT_1:32;
then reconsider n =
(b ") . x as
Nat ;
reconsider aG =
a * ((GramMatrix b) ~) as
Matrix of
dim L,
INT.Ring by A3;
B4:
Indices aG = [:(Seg (dim L)),(Seg (dim L)):]
by MATRIX_0:24;
n in Seg (dim L)
by A2, AX1, B3, FINSEQ_1:def 3;
then B5:
[i,n] in Indices aG
by A9, B4, ZFMISC_1:87;
aG * (
i,
n) is
Element of
INT.Ring
;
then reconsider y =
(a * ((GramMatrix b) ~)) * (
i,
n) as
Element of
INT.Ring by B5, ZMATRLIN:1;
take
y
;
S1[x,y]thus
S1[
x,
y]
by B1;
verum end;
end;
consider l being Function of (EMLat L),INT.Ring such that
A18:
for x being Element of (EMLat L) holds S1[x,l . x]
from FUNCT_2:sch 3(A17);
l is Element of Funcs ( the carrier of (EMLat L), the carrier of INT.Ring)
by FUNCT_2:8;
then reconsider l = l as Linear_Combination of EMLat L by A18, VECTSP_6:def 1;
reconsider ai = a as Element of INT.Ring by A3;
L1:
len (GramMatrix b) = len b
by MATRIX_0:24;
L2: width (a * ((GramMatrix b) ~)) =
dim (EMLat L)
by MATRIX_0:23
.=
len b
by ZMATRLIN:49
;
Q7:
len (Line ((a * ((GramMatrix b) ~)),i)) = len b
by L2, MATRIX_0:def 7;
Q8:
len (Col ((GramMatrix b),i)) = len b
by L1, MATRIX_0:def 8;
A31: len (ScFS ((b /. i),l,b)) =
len b
by defScFS
.=
len (mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),i))))
by Q7, Q8, FINSEQ_2:72
;
for k being Nat st 1 <= k & k <= len (ScFS ((b /. i),l,b)) holds
(mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),i)))) . k = (ScFS ((b /. i),l,b)) . k
proof
let k be
Nat;
( 1 <= k & k <= len (ScFS ((b /. i),l,b)) implies (mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),i)))) . k = (ScFS ((b /. i),l,b)) . k )
assume AS1:
( 1
<= k &
k <= len (ScFS ((b /. i),l,b)) )
;
(mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),i)))) . k = (ScFS ((b /. i),l,b)) . k
then Q0:
k in dom (ScFS ((b /. i),l,b))
by FINSEQ_3:25;
D0:
( 1
<= k &
k <= len b )
by AS1, defScFS;
then D1:
k in dom b
by FINSEQ_3:25;
then
b . k in rng b
by FUNCT_1:3;
then Q1:
b /. k in I
by PARTFUN1:def 6, D1;
b is
one-to-one
by ZMATRLIN:def 5;
then Q2:
k =
(b ") . (b . k)
by FUNCT_1:34, D1
.=
(b ") . (b /. k)
by PARTFUN1:def 6, D1
;
Q3:
l . (b /. k) = (a * ((GramMatrix b) ~)) * (
i,
k)
by Q1, Q2, D0, A18, FINSEQ_3:25;
k in Seg (width (a * ((GramMatrix b) ~)))
by D0, L2;
then Q4:
(Line ((a * ((GramMatrix b) ~)),i)) . k = (a * ((GramMatrix b) ~)) * (
i,
k)
by MATRIX_0:def 7;
k in Seg (len (GramMatrix b))
by D0, L1;
then
k in dom (GramMatrix b)
by FINSEQ_1:def 3;
then Q5:
(Col ((GramMatrix b),i)) . k =
(GramMatrix b) * (
k,
i)
by MATRIX_0:def 8
.=
(InnerProduct (EMLat L)) . (
(b /. k),
(b /. i))
by D1, A1, ZMODLAT1:def 32
.=
<;(b /. k),(b /. i);>
.=
<;(b /. i),(b /. k);>
by ZMODLAT1:def 3
.=
(InnerProduct (EMLat L)) . (
(b /. i),
(b /. k))
.=
(GramMatrix b) * (
i,
k)
by D1, A1, ZMODLAT1:def 32
;
Seg (len (mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),i))))) =
Seg (len b)
by Q7, Q8, FINSEQ_2:72
.=
dom b
by FINSEQ_1:def 3
;
then Q6:
k in dom (mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),i))))
by D1, FINSEQ_1:def 3;
<;(b /. i),((l . (b /. k)) * (b /. k));> =
((a * ((GramMatrix b) ~)) * (i,k)) * <;(b /. i),(b /. k);>
by Q3, ZMODLAT1:9
.=
((a * ((GramMatrix b) ~)) * (i,k)) * ((InnerProduct (EMLat L)) . ((b /. i),(b /. k)))
.=
((a * ((GramMatrix b) ~)) * (i,k)) * ((GramMatrix b) * (i,k))
by D1, A1, ZMODLAT1:def 32
.=
(mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),i)))) . k
by Q4, Q5, Q6, FVSUM_1:60
;
hence
(mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),i)))) . k = (ScFS ((b /. i),l,b)) . k
by Q0, defScFS;
verum
end;
then A32:
mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),i))) = ScFS ((b /. i),l,b)
by A31;
set F = canFS (Carrier l);
A303:
( canFS (Carrier l) is one-to-one & rng (canFS (Carrier l)) = Carrier l )
by FUNCT_2:def 3;
then reconsider F = canFS (Carrier l) as FinSequence of (EMLat L) by FINSEQ_1:def 4;
A30:
SumSc ((b /. i),l) = Sum (ScFS ((b /. i),l,F))
by A303, defSumSc;
A302:
Carrier l c= rng b
b is one-to-one
by ZMATRLIN:def 5;
then A20:
SumSc ((b /. i),l) = a
by A15, A30, A32, A302, LM1;
A21:
for j being Nat st i <> j & j in dom b holds
<;(b /. j),(Sum l);> = 0
proof
let j be
Nat;
( i <> j & j in dom b implies <;(b /. j),(Sum l);> = 0 )
assume BJ1:
(
i <> j &
j in dom b )
;
<;(b /. j),(Sum l);> = 0
Q7:
len (Line ((a * ((GramMatrix b) ~)),i)) = len b
by L2, MATRIX_0:def 7;
Q8:
len (Col ((GramMatrix b),j)) = len b
by L1, MATRIX_0:def 8;
A31:
len (ScFS ((b /. j),l,b)) =
len b
by defScFS
.=
len (mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),j))))
by Q7, Q8, FINSEQ_2:72
;
for
k being
Nat st 1
<= k &
k <= len (ScFS ((b /. j),l,b)) holds
(mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),j)))) . k = (ScFS ((b /. j),l,b)) . k
proof
let k be
Nat;
( 1 <= k & k <= len (ScFS ((b /. j),l,b)) implies (mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),j)))) . k = (ScFS ((b /. j),l,b)) . k )
assume AS1:
( 1
<= k &
k <= len (ScFS ((b /. j),l,b)) )
;
(mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),j)))) . k = (ScFS ((b /. j),l,b)) . k
then Q0:
k in dom (ScFS ((b /. j),l,b))
by FINSEQ_3:25;
D0:
( 1
<= k &
k <= len b )
by AS1, defScFS;
then D1:
k in dom b
by FINSEQ_3:25;
then
b . k in rng b
by FUNCT_1:3;
then Q1:
b /. k in I
by PARTFUN1:def 6, D1;
b is
one-to-one
by ZMATRLIN:def 5;
then k =
(b ") . (b . k)
by FUNCT_1:34, D1
.=
(b ") . (b /. k)
by PARTFUN1:def 6, D1
;
then Q3:
l . (b /. k) = (a * ((GramMatrix b) ~)) * (
i,
k)
by Q1, D0, A18, FINSEQ_3:25;
k in Seg (width (a * ((GramMatrix b) ~)))
by D0, L2;
then Q4:
(Line ((a * ((GramMatrix b) ~)),i)) . k = (a * ((GramMatrix b) ~)) * (
i,
k)
by MATRIX_0:def 7;
k in Seg (len (GramMatrix b))
by D0, L1;
then
k in dom (GramMatrix b)
by FINSEQ_1:def 3;
then Q5:
(Col ((GramMatrix b),j)) . k =
(GramMatrix b) * (
k,
j)
by MATRIX_0:def 8
.=
(InnerProduct (EMLat L)) . (
(b /. k),
(b /. j))
by D1, BJ1, ZMODLAT1:def 32
.=
<;(b /. k),(b /. j);>
.=
<;(b /. j),(b /. k);>
by ZMODLAT1:def 3
.=
(InnerProduct (EMLat L)) . (
(b /. j),
(b /. k))
.=
(GramMatrix b) * (
j,
k)
by D1, BJ1, ZMODLAT1:def 32
;
Seg (len (mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),j))))) =
Seg (len b)
by Q7, Q8, FINSEQ_2:72
.=
dom b
by FINSEQ_1:def 3
;
then Q6:
k in dom (mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),j))))
by D1, FINSEQ_1:def 3;
<;(b /. j),((l . (b /. k)) * (b /. k));> =
((a * ((GramMatrix b) ~)) * (i,k)) * <;(b /. j),(b /. k);>
by Q3, ZMODLAT1:9
.=
((a * ((GramMatrix b) ~)) * (i,k)) * ((InnerProduct (EMLat L)) . ((b /. j),(b /. k)))
.=
((a * ((GramMatrix b) ~)) * (i,k)) * ((GramMatrix b) * (j,k))
by D1, BJ1, ZMODLAT1:def 32
.=
(mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),j)))) . k
by Q4, Q5, Q6, FVSUM_1:60
;
hence
(mlt ((Line ((a * ((GramMatrix b) ~)),i)),(Col ((GramMatrix b),j)))) . k = (ScFS ((b /. j),l,b)) . k
by Q0, defScFS;
verum
end;
then
mlt (
(Line ((a * ((GramMatrix b) ~)),i)),
(Col ((GramMatrix b),j)))
= ScFS (
(b /. j),
l,
b)
by A31;
then A32:
Sum (ScFS ((b /. j),l,b)) =
(Line ((a * ((GramMatrix b) ~)),i)) "*" (Col ((GramMatrix b),j))
.=
0
by A16, BJ1
;
A30:
SumSc (
(b /. j),
l)
= Sum (ScFS ((b /. j),l,F))
by A303, defSumSc;
b is
one-to-one
by ZMATRLIN:def 5;
then
Sum (ScFS ((b /. j),l,F)) = Sum (ScFS ((b /. j),l,b))
by LM1, A302;
hence
<;(b /. j),(Sum l);> = 0
by A30, A32, ThSumSc1;
verum
end;
reconsider EL = EMLat L as Submodule of DivisibleMod L by ZMODLAT2:20;
Sum l in EL
;
then
Sum l in DivisibleMod L
by ZMODUL01:24;
then consider u being Vector of (DivisibleMod L) such that
A22:
ai * u = Sum l
by A3, ZMODUL08:23;
take
u
; ( (ScProductDM L) . ((b /. i),u) = 1 & ( for j being Nat st i <> j & j in dom b holds
(ScProductDM L) . ((b /. j),u) = 0 ) )
b /. i in EMLat L
;
then
b /. i in rng (MorphsZQ L)
by ZMODLAT2:def 4;
then A24:
b /. i in EMbedding L
by ZMODUL08:def 3;
Sum l in EMLat L
;
then
Sum l in rng (MorphsZQ L)
by ZMODLAT2:def 4;
then A25:
Sum l in EMbedding L
by ZMODUL08:def 3;
b /. i in EL
;
then
b /. i in DivisibleMod L
by ZMODUL01:24;
then reconsider bi = b /. i as Element of (DivisibleMod L) ;
A28:
a <> 0. F_Real
by A3;
A29: a * ((ScProductDM L) . (bi,u)) =
(ScProductDM L) . (bi,(ai * u))
by ZMODLAT2:13
.=
(ScProductEM L) . ((b /. i),(Sum l))
by A22, A24, A25, ZMODLAT2:8
.=
<;(b /. i),(Sum l);>
by ZMODLAT2:def 4
.=
a * (1. F_Real)
by A20, ThSumSc1
;
for j being Nat st i <> j & j in dom b holds
(ScProductDM L) . ((b /. j),u) = 0
proof
let j be
Nat;
( i <> j & j in dom b implies (ScProductDM L) . ((b /. j),u) = 0 )
assume B1:
(
i <> j &
j in dom b )
;
(ScProductDM L) . ((b /. j),u) = 0
b /. j in EMLat L
;
then
b /. j in rng (MorphsZQ L)
by ZMODLAT2:def 4;
then B2:
b /. j in EMbedding L
by ZMODUL08:def 3;
b /. j in EL
;
then
b /. j in DivisibleMod L
by ZMODUL01:24;
then reconsider bj =
b /. j as
Element of
(DivisibleMod L) ;
a * ((ScProductDM L) . (bj,u)) =
(ScProductDM L) . (
bj,
(ai * u))
by ZMODLAT2:13
.=
(ScProductEM L) . (
(b /. j),
(Sum l))
by A22, A25, B2, ZMODLAT2:8
.=
<;(b /. j),(Sum l);>
by ZMODLAT2:def 4
.=
a * (0. F_Real)
by A21, B1
;
hence
(ScProductDM L) . (
(b /. j),
u)
= 0
by A3;
verum
end;
hence
( (ScProductDM L) . ((b /. i),u) = 1 & ( for j being Nat st i <> j & j in dom b holds
(ScProductDM L) . ((b /. j),u) = 0 ) )
by A28, A29, VECTSP_1:5; verum