let L be positive-definite Z_Lattice; :: thesis: 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; :: thesis: 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); :: thesis: ( ( 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) ; :: thesis: 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);>

.= 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; :: thesis: verum

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; :: thesis: 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); :: thesis: ( ( 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) ; :: thesis: 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

then j * iv =
i * jw
by ZL2ThSc1
let n be Nat; :: thesis: ( n in dom b implies <;(b /. n),(j * iv);> = <;(b /. n),(i * jw);> )

assume B1: n in dom b ; :: thesis: <;(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; :: thesis: verum

end;assume B1: n in dom b ; :: thesis: <;(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; :: thesis: verum

.= 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; :: thesis: verum