let L be Z_Lattice; :: thesis: 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); :: thesis: 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); :: thesis: ( ( 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 ; :: thesis: v is Dual of L

defpred S_{1}[ 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: S_{1}[ 0 ]
_{1}[n] holds

S_{1}[n + 1]
_{1}[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; :: thesis: verum

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); :: thesis: 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); :: thesis: ( ( 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 ; :: thesis: v is Dual of L

defpred S

(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: S

proof

P2:
for n being Nat st S
let I be finite Subset of (EMbedding L); :: thesis: ( card I = 0 & 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 B1: ( card I = 0 & I is linearly-independent & ( for u being Vector of (DivisibleMod L) st u in I holds

(ScProductDM L) . (v,u) in INT.Ring ) ) ; :: thesis: for w being Vector of (DivisibleMod L) st w in Lin I holds

(ScProductDM L) . (v,w) in INT.Ring

I = {} the carrier of (EMbedding L) by B1;

then B2: Lin I = (0). (EMbedding L) by ZMODUL02:67;

for w being Vector of (DivisibleMod L) st w in Lin I holds

(ScProductDM L) . (v,w) in INT.Ring

(ScProductDM L) . (v,w) in INT.Ring ; :: thesis: verum

end;(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 B1: ( card I = 0 & I is linearly-independent & ( for u being Vector of (DivisibleMod L) st u in I holds

(ScProductDM L) . (v,u) in INT.Ring ) ) ; :: thesis: for w being Vector of (DivisibleMod L) st w in Lin I holds

(ScProductDM L) . (v,w) in INT.Ring

I = {} the carrier of (EMbedding L) by B1;

then B2: Lin I = (0). (EMbedding L) by ZMODUL02:67;

for w being Vector of (DivisibleMod L) st w in Lin I holds

(ScProductDM L) . (v,w) in INT.Ring

proof

hence
for w being Vector of (DivisibleMod L) st w in Lin I holds
let w be Vector of (DivisibleMod L); :: thesis: ( w in Lin I implies (ScProductDM L) . (v,w) in INT.Ring )

assume C1: w in Lin I ; :: thesis: (ScProductDM L) . (v,w) in INT.Ring

w = 0. (EMbedding L) by B2, C1, ZMODUL02:66

.= zeroCoset L by ZMODUL08:def 3

.= 0. (DivisibleMod L) 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;assume C1: w in Lin I ; :: thesis: (ScProductDM L) . (v,w) in INT.Ring

w = 0. (EMbedding L) by B2, C1, ZMODUL02:66

.= zeroCoset L by ZMODUL08:def 3

.= 0. (DivisibleMod L) 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

(ScProductDM L) . (v,w) in INT.Ring ; :: thesis: verum

S

proof

P3:
for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume B1: S_{1}[n]
; :: thesis: S_{1}[n + 1]

let I be finite Subset of (EMbedding L); :: thesis: ( 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 ) ) ; :: thesis: 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); :: thesis: ( w in Lin I implies (ScProductDM L) . (v,w) in INT.Ring )

assume C1: w in Lin I ; :: thesis: (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; :: thesis: verum

end;assume B1: S

let I be finite Subset of (EMbedding L); :: thesis: ( 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 ) ) ; :: thesis: 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); :: thesis: ( w in Lin I implies (ScProductDM L) . (v,w) in INT.Ring )

assume C1: w in Lin I ; :: thesis: (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; :: thesis: verum

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