let L be positive-definite Z_Lattice; for b being OrdBasis of EMLat L
for v, w being Vector of (DivisibleMod L) st ( for n being Nat st n in dom b holds
(ScProductDM L) . ((b /. n),v) = (ScProductDM L) . ((b /. n),w) ) holds
v = w
let b be OrdBasis of EMLat L; for v, w being Vector of (DivisibleMod L) st ( for n being Nat st n in dom b holds
(ScProductDM L) . ((b /. n),v) = (ScProductDM L) . ((b /. n),w) ) holds
v = w
let v, w be Vector of (DivisibleMod L); ( ( for n being Nat st n in dom b holds
(ScProductDM L) . ((b /. n),v) = (ScProductDM L) . ((b /. n),w) ) implies v = w )
assume A1:
for n being Nat st n in dom b holds
(ScProductDM L) . ((b /. n),v) = (ScProductDM L) . ((b /. n),w)
; v = w
consider i being Element of INT.Ring such that
A2:
( i <> 0 & i * v in EMbedding L )
by ZMODUL08:29;
consider j being Element of INT.Ring such that
A3:
( j <> 0 & j * w in EMbedding L )
by ZMODUL08:29;
i * v in rng (MorphsZQ L)
by A2, ZMODUL08:def 3;
then reconsider iv = i * v as Vector of (EMLat L) by defEMLat;
j * w in rng (MorphsZQ L)
by A3, ZMODUL08:def 3;
then reconsider jw = j * w as Vector of (EMLat L) by defEMLat;
A4:
EMLat L is Submodule of DivisibleMod L
by ThDivisibleL1;
for n being Nat st n in dom b holds
<;(b /. n),(j * iv);> = <;(b /. n),(i * jw);>
proof
let n be
Nat;
( n in dom b implies <;(b /. n),(j * iv);> = <;(b /. n),(i * jw);> )
assume B1:
n in dom b
;
<;(b /. n),(j * iv);> = <;(b /. n),(i * jw);>
b /. n in EMLat L
;
then
b /. n in DivisibleMod L
by A4, ZMODUL01:24;
then reconsider bn =
b /. n as
Vector of
(DivisibleMod L) ;
b /. n in EMLat L
;
then
b /. n in rng (MorphsZQ L)
by defEMLat;
then B2:
b /. n in EMbedding L
by ZMODUL08:def 3;
B3:
(i * j) * ((ScProductDM L) . ((b /. n),v)) =
j * (i * ((ScProductDM L) . (bn,v)))
.=
j * (i * ((ScProductDM L) . (v,bn)))
by ThSPDM1
.=
j * ((ScProductDM L) . ((i * v),bn))
by ThSPDM1
.=
j * ((ScProductEM L) . (iv,(b /. n)))
by A2, B2, ThSPEM3
.=
j * <;iv,(b /. n);>
by defEMLat
.=
<;(j * iv),(b /. n);>
by ZMODLAT1:def 3
.=
<;(b /. n),(j * iv);>
by ZMODLAT1:def 3
;
(i * j) * ((ScProductDM L) . ((b /. n),w)) =
i * (j * ((ScProductDM L) . (bn,w)))
.=
i * (j * ((ScProductDM L) . (w,bn)))
by ThSPDM1
.=
i * ((ScProductDM L) . ((j * w),bn))
by ThSPDM1
.=
i * ((ScProductEM L) . (jw,(b /. n)))
by A3, B2, ThSPEM3
.=
i * <;jw,(b /. n);>
by defEMLat
.=
<;(i * jw),(b /. n);>
by ZMODLAT1:def 3
.=
<;(b /. n),(i * jw);>
by ZMODLAT1:def 3
;
hence
<;(b /. n),(j * iv);> = <;(b /. n),(i * jw);>
by A1, B1, B3;
verum
end;
then j * iv =
i * jw
by ZL2ThSc1
.=
i * (j * w)
by A4, ZMODUL01:29
;
then j * (i * v) =
i * (j * w)
by A4, ZMODUL01:29
.=
(i * j) * w
by VECTSP_1:def 16
;
then
(i * j) * v = (i * j) * w
by VECTSP_1:def 16;
hence
v = w
by A2, A3, ZMODUL01:10; verum