let L be Z_Lattice; :: thesis: for v being Vector of ()
for I being Basis of () st ( for u being Vector of () st u in I holds
() . (v,u) in INT.Ring ) holds
v is Dual of L

let v be Vector of (); :: thesis: for I being Basis of () st ( for u being Vector of () st u in I holds
() . (v,u) in INT.Ring ) holds
v is Dual of L

let I be Basis of (); :: thesis: ( ( for u being Vector of () st u in I holds
() . (v,u) in INT.Ring ) implies v is Dual of L )

assume A1: for u being Vector of () st u in I holds
() . (v,u) in INT.Ring ; :: thesis: v is Dual of L
defpred S1[ Nat] means for I being finite Subset of () st card I = \$1 & I is linearly-independent & ( for u being Vector of () st u in I holds
() . (v,u) in INT.Ring ) holds
for w being Vector of () st w in Lin I holds
() . (v,w) in INT.Ring ;
P1: S1[ 0 ]
proof
let I be finite Subset of (); :: thesis: ( card I = 0 & I is linearly-independent & ( for u being Vector of () st u in I holds
() . (v,u) in INT.Ring ) implies for w being Vector of () st w in Lin I holds
() . (v,w) in INT.Ring )

assume B1: ( card I = 0 & I is linearly-independent & ( for u being Vector of () st u in I holds
() . (v,u) in INT.Ring ) ) ; :: thesis: for w being Vector of () st w in Lin I holds
() . (v,w) in INT.Ring

I = {} the carrier of () by B1;
then B2: Lin I = (0). () by ZMODUL02:67;
for w being Vector of () st w in Lin I holds
() . (v,w) in INT.Ring
proof
let w be Vector of (); :: thesis: ( w in Lin I implies () . (v,w) in INT.Ring )
assume C1: w in Lin I ; :: thesis: () . (v,w) in INT.Ring
w = 0. () by
.= zeroCoset L by ZMODUL08:def 3
.= 0. () by ZMODUL08:def 4 ;
then (ScProductDM L) . (w,v) in INT.Ring by LmDE00;
hence (ScProductDM L) . (v,w) in INT.Ring by ZMODLAT2:6; :: thesis: verum
end;
hence for w being Vector of () st w in Lin I holds
() . (v,w) in INT.Ring ; :: thesis: verum
end;
P2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume B1: S1[n] ; :: thesis: S1[n + 1]
let I be finite Subset of (); :: thesis: ( card I = n + 1 & I is linearly-independent & ( for u being Vector of () st u in I holds
() . (v,u) in INT.Ring ) implies for w being Vector of () st w in Lin I holds
() . (v,w) in INT.Ring )

assume B2: ( card I = n + 1 & I is linearly-independent & ( for u being Vector of () st u in I holds
() . (v,u) in INT.Ring ) ) ; :: thesis: for w being Vector of () st w in Lin I holds
() . (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 () by B3;
set Iu = I \ {u};
{u} is Subset of I by ;
then B4: card (I \ {u}) = (n + 1) - () by
.= (n + 1) - 1 by CARD_1:30
.= n ;
reconsider Iu = I \ {u} as finite Subset of () ;
I = Iu \/ {u} by ;
then B5: Lin I = (Lin Iu) + () by ZMODUL02:72;
B7: Iu c= I by XBOOLE_1:36;
B6: Iu is linearly-independent by ;
B8: for w being Vector of () st w in Iu holds
() . (v,w) in INT.Ring by B2, B7;
let w be Vector of (); :: thesis: ( w in Lin I implies () . (v,w) in INT.Ring )
assume C1: w in Lin I ; :: thesis: () . (v,w) in INT.Ring
consider w1, w2 being Vector of () such that
C2: ( w1 in Lin Iu & w2 in Lin {u} & w = w1 + w2 ) by ;
CX: EMbedding L is Submodule of DivisibleMod L by ZMODUL08:24;
then C9: w1 is Vector of () by ZMODUL01:25;
reconsider ww1 = w1 as Vector of () by ;
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 ;
u is Element of () by ;
then C6: (ScProductDM L) . (v,u) in INT.Ring by B2, B3;
reconsider uu = u as Element of () by ;
i * uu in DivisibleMod L ;
then reconsider ww2 = w2 as Vector of () by ;
C11: () . (v,(i * u)) = () . (v,(i * uu)) by
.= () . ((i * uu),v) by ZMODLAT2:6
.= i * (() . (uu,v)) by ZMODLAT2:6
.= i * (() . (v,u)) by ZMODLAT2:6 ;
C10: w = ww1 + ww2 by ;
() . (v,w) = () . (w,v) by ZMODLAT2:6
.= (() . (ww1,v)) + (() . (ww2,v)) by
.= (() . (v,w1)) + (() . (ww2,v)) by ZMODLAT2:6
.= (() . (v,w1)) + (() . (v,w2)) by ZMODLAT2:6 ;
hence (ScProductDM L) . (v,w) in INT.Ring by ; :: thesis: 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 () st w in EMbedding L holds
() . (v,w) in INT.Ring by A1, P3, P4;
hence v is Dual of L by defDualElement; :: thesis: verum