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) . (v,(b /. n)) = (ScProductDM L) . (w,(b /. n)) ) 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) . (v,(b /. n)) = (ScProductDM L) . (w,(b /. n)) ) holds
v = w
let v, w be Vector of (DivisibleMod L); ( ( for n being Nat st n in dom b holds
(ScProductDM L) . (v,(b /. n)) = (ScProductDM L) . (w,(b /. n)) ) implies v = w )
assume A1:
for n being Nat st n in dom b holds
(ScProductDM L) . (v,(b /. n)) = (ScProductDM L) . (w,(b /. n))
; v = w
for n being Nat st n in dom b holds
(ScProductDM L) . ((b /. n),v) = (ScProductDM L) . ((b /. n),w)
proof
let n be
Nat;
( n in dom b implies (ScProductDM L) . ((b /. n),v) = (ScProductDM L) . ((b /. n),w) )
assume B1:
n in dom b
;
(ScProductDM L) . ((b /. n),v) = (ScProductDM L) . ((b /. n),w)
B2:
EMLat L is
Submodule of
DivisibleMod L
by ThDivisibleL1;
b /. n in EMLat L
;
then
b /. n in DivisibleMod L
by B2, ZMODUL01:24;
then reconsider bn =
b /. n as
Vector of
(DivisibleMod L) ;
thus (ScProductDM L) . (
(b /. n),
v) =
(ScProductDM L) . (
v,
bn)
by ThSPDM1
.=
(ScProductDM L) . (
w,
(b /. n))
by A1, B1
.=
(ScProductDM L) . (
bn,
w)
by ThSPDM1
.=
(ScProductDM L) . (
(b /. n),
w)
;
verum
end;
hence
v = w
by ZL2ThSc1D; verum