let L be Z_Lattice; for v being Vector of (DivisibleMod L)
for I being Basis of (EMbedding L) st ( for u being Vector of (DivisibleMod L) st u in I holds
(ScProductDM L) . (v,u) in INT.Ring ) holds
v is Dual of L
let v be Vector of (DivisibleMod L); for I being Basis of (EMbedding L) st ( for u being Vector of (DivisibleMod L) st u in I holds
(ScProductDM L) . (v,u) in INT.Ring ) holds
v is Dual of L
let I be Basis of (EMbedding L); ( ( for u being Vector of (DivisibleMod L) st u in I holds
(ScProductDM L) . (v,u) in INT.Ring ) implies v is Dual of L )
assume A1:
for u being Vector of (DivisibleMod L) st u in I holds
(ScProductDM L) . (v,u) in INT.Ring
; v is Dual of L
defpred S1[ Nat] means for I being finite Subset of (EMbedding L) st card I = $1 & I is linearly-independent & ( for u being Vector of (DivisibleMod L) st u in I holds
(ScProductDM L) . (v,u) in INT.Ring ) holds
for w being Vector of (DivisibleMod L) st w in Lin I holds
(ScProductDM L) . (v,w) in INT.Ring ;
P1:
S1[ 0 ]
P2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume B1:
S1[
n]
;
S1[n + 1]
let I be
finite Subset of
(EMbedding L);
( card I = n + 1 & I is linearly-independent & ( for u being Vector of (DivisibleMod L) st u in I holds
(ScProductDM L) . (v,u) in INT.Ring ) implies for w being Vector of (DivisibleMod L) st w in Lin I holds
(ScProductDM L) . (v,w) in INT.Ring )
assume B2:
(
card I = n + 1 &
I is
linearly-independent & ( for
u being
Vector of
(DivisibleMod L) st
u in I holds
(ScProductDM L) . (
v,
u)
in INT.Ring ) )
;
for w being Vector of (DivisibleMod L) st w in Lin I holds
(ScProductDM L) . (v,w) in INT.Ring
not
I is
empty
by B2;
then consider u being
object such that B3:
u in I
;
reconsider u =
u as
Vector of
(EMbedding L) by B3;
set Iu =
I \ {u};
{u} is
Subset of
I
by B3, SUBSET_1:41;
then B4:
card (I \ {u}) =
(n + 1) - (card {u})
by B2, CARD_2:44
.=
(n + 1) - 1
by CARD_1:30
.=
n
;
reconsider Iu =
I \ {u} as
finite Subset of
(EMbedding L) ;
I = Iu \/ {u}
by B3, XBOOLE_1:45, ZFMISC_1:31;
then B5:
Lin I = (Lin Iu) + (Lin {u})
by ZMODUL02:72;
B7:
Iu c= I
by XBOOLE_1:36;
B6:
Iu is
linearly-independent
by B2, XBOOLE_1:36, ZMODUL02:56;
B8:
for
w being
Vector of
(DivisibleMod L) st
w in Iu holds
(ScProductDM L) . (
v,
w)
in INT.Ring
by B2, B7;
let w be
Vector of
(DivisibleMod L);
( w in Lin I implies (ScProductDM L) . (v,w) in INT.Ring )
assume C1:
w in Lin I
;
(ScProductDM L) . (v,w) in INT.Ring
consider w1,
w2 being
Vector of
(EMbedding L) such that C2:
(
w1 in Lin Iu &
w2 in Lin {u} &
w = w1 + w2 )
by B5, C1, ZMODUL01:92;
CX:
EMbedding L is
Submodule of
DivisibleMod L
by ZMODUL08:24;
then C9:
w1 is
Vector of
(DivisibleMod L)
by ZMODUL01:25;
reconsider ww1 =
w1 as
Vector of
(DivisibleMod L) by CX, ZMODUL01:25;
C3:
(ScProductDM L) . (
v,
w1)
in INT.Ring
by B1, B4, B6, B8, C2, C9;
consider i being
Element of
INT.Ring such that C4:
w2 = i * u
by C2, ZMODUL06:19;
u is
Element of
(DivisibleMod L)
by CX, ZMODUL01:25;
then C6:
(ScProductDM L) . (
v,
u)
in INT.Ring
by B2, B3;
reconsider uu =
u as
Element of
(DivisibleMod L) by CX, ZMODUL01:25;
i * uu in DivisibleMod L
;
then reconsider ww2 =
w2 as
Vector of
(DivisibleMod L) by C4, CX, ZMODUL01:29;
C11:
(ScProductDM L) . (
v,
(i * u)) =
(ScProductDM L) . (
v,
(i * uu))
by CX, ZMODUL01:29
.=
(ScProductDM L) . (
(i * uu),
v)
by ZMODLAT2:6
.=
i * ((ScProductDM L) . (uu,v))
by ZMODLAT2:6
.=
i * ((ScProductDM L) . (v,u))
by ZMODLAT2:6
;
C10:
w = ww1 + ww2
by C2, CX, ZMODUL01:28;
(ScProductDM L) . (
v,
w) =
(ScProductDM L) . (
w,
v)
by ZMODLAT2:6
.=
((ScProductDM L) . (ww1,v)) + ((ScProductDM L) . (ww2,v))
by C10, ZMODLAT2:6
.=
((ScProductDM L) . (v,w1)) + ((ScProductDM L) . (ww2,v))
by ZMODLAT2:6
.=
((ScProductDM L) . (v,w1)) + ((ScProductDM L) . (v,w2))
by ZMODLAT2:6
;
hence
(ScProductDM L) . (
v,
w)
in INT.Ring
by C3, C4, C6, C11, INT_1:def 2;
verum
end;
P3:
for n being Nat holds S1[n]
from NAT_1:sch 2(P1, P2);
P4:
card I is Nat
;
( I is linearly-independent & EMbedding L = Lin I )
by VECTSP_7:def 3;
then
for w being Vector of (DivisibleMod L) st w in EMbedding L holds
(ScProductDM L) . (v,w) in INT.Ring
by A1, P3, P4;
hence
v is Dual of L
by defDualElement; verum