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) = 0 ) holds

for u being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,u) = 0

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) = 0 ) holds

for u being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,u) = 0

let I be Basis of (EMbedding L); :: thesis: ( ( for u being Vector of (DivisibleMod L) st u in I holds

(ScProductDM L) . (v,u) = 0 ) implies for u being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,u) = 0 )

assume A1: for u being Vector of (DivisibleMod L) st u in I holds

(ScProductDM L) . (v,u) = 0 ; :: thesis: for u being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,u) = 0

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) = 0 ) holds

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

(ScProductDM L) . (v,w) = 0 ;

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 ;

P5: ( I is linearly-independent & EMbedding L = Lin I ) by VECTSP_7:def 3;

thus for w being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,w) = 0 :: 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) = 0 ) holds

for u being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,u) = 0

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) = 0 ) holds

for u being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,u) = 0

let I be Basis of (EMbedding L); :: thesis: ( ( for u being Vector of (DivisibleMod L) st u in I holds

(ScProductDM L) . (v,u) = 0 ) implies for u being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,u) = 0 )

assume A1: for u being Vector of (DivisibleMod L) st u in I holds

(ScProductDM L) . (v,u) = 0 ; :: thesis: for u being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,u) = 0

defpred S

(ScProductDM L) . (v,u) = 0 ) holds

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

(ScProductDM L) . (v,w) = 0 ;

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) = 0 ) implies for w being Vector of (DivisibleMod L) st w in Lin I holds

(ScProductDM L) . (v,w) = 0 )

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) = 0 ) ) ; :: thesis: for w being Vector of (DivisibleMod L) st w in Lin I holds

(ScProductDM L) . (v,w) = 0

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

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

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

(ScProductDM L) . (v,w) = 0 :: thesis: verum

end;(ScProductDM L) . (v,u) = 0 ) implies for w being Vector of (DivisibleMod L) st w in Lin I holds

(ScProductDM L) . (v,w) = 0 )

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) = 0 ) ) ; :: thesis: for w being Vector of (DivisibleMod L) st w in Lin I holds

(ScProductDM L) . (v,w) = 0

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

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

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

(ScProductDM L) . (v,w) = 0 :: thesis: verum

proof

let w be Vector of (DivisibleMod L); :: thesis: ( w in Lin I implies (ScProductDM L) . (v,w) = 0 )

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

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

.= zeroCoset L by ZMODUL08:def 3

.= 0. (DivisibleMod L) by ZMODUL08:def 4 ;

hence (ScProductDM L) . (v,w) = 0 by ThScDM6; :: thesis: verum

end;assume C1: w in Lin I ; :: thesis: (ScProductDM L) . (v,w) = 0

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

.= zeroCoset L by ZMODUL08:def 3

.= 0. (DivisibleMod L) by ZMODUL08:def 4 ;

hence (ScProductDM L) . (v,w) = 0 by ThScDM6; :: 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) = 0 ) implies for w being Vector of (DivisibleMod L) st w in Lin I holds

(ScProductDM L) . (v,w) = 0 )

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) = 0 ) ) ; :: thesis: for w being Vector of (DivisibleMod L) st w in Lin I holds

(ScProductDM L) . (v,w) = 0

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) = 0 by B2, B7;

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

(ScProductDM L) . (v,w) = 0 :: 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) = 0 ) implies for w being Vector of (DivisibleMod L) st w in Lin I holds

(ScProductDM L) . (v,w) = 0 )

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) = 0 ) ) ; :: thesis: for w being Vector of (DivisibleMod L) st w in Lin I holds

(ScProductDM L) . (v,w) = 0

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) = 0 by B2, B7;

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

(ScProductDM L) . (v,w) = 0 :: thesis: verum

proof

let w be Vector of (DivisibleMod L); :: thesis: ( w in Lin I implies (ScProductDM L) . (v,w) = 0 )

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

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;

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) = 0 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;

C8: (ScProductDM L) . (v,(i * u)) = (ScProductDM L) . (v,(i * uu)) by CX, ZMODUL01:29

.= (ScProductDM L) . ((i * uu),v) by ThSPDM1

.= i * ((ScProductDM L) . (uu,v)) by ThSPDM1

.= i * ((ScProductDM L) . (v,u)) by ThSPDM1 ;

C10: w = ww1 + ww2 by C2, CX, ZMODUL01:28;

(ScProductDM L) . (v,w) = (ScProductDM L) . (w,v) by ThSPDM1

.= ((ScProductDM L) . (ww1,v)) + ((ScProductDM L) . (ww2,v)) by C10, ThSPDM1

.= ((ScProductDM L) . (v,w1)) + ((ScProductDM L) . (ww2,v)) by ThSPDM1

.= ((ScProductDM L) . (v,w1)) + ((ScProductDM L) . (v,w2)) by ThSPDM1 ;

hence (ScProductDM L) . (v,w) = 0 by B1, B4, B6, B8, C2, C4, C6, C8, C9; :: thesis: verum

end;assume C1: w in Lin I ; :: thesis: (ScProductDM L) . (v,w) = 0

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;

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) = 0 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;

C8: (ScProductDM L) . (v,(i * u)) = (ScProductDM L) . (v,(i * uu)) by CX, ZMODUL01:29

.= (ScProductDM L) . ((i * uu),v) by ThSPDM1

.= i * ((ScProductDM L) . (uu,v)) by ThSPDM1

.= i * ((ScProductDM L) . (v,u)) by ThSPDM1 ;

C10: w = ww1 + ww2 by C2, CX, ZMODUL01:28;

(ScProductDM L) . (v,w) = (ScProductDM L) . (w,v) by ThSPDM1

.= ((ScProductDM L) . (ww1,v)) + ((ScProductDM L) . (ww2,v)) by C10, ThSPDM1

.= ((ScProductDM L) . (v,w1)) + ((ScProductDM L) . (ww2,v)) by ThSPDM1

.= ((ScProductDM L) . (v,w1)) + ((ScProductDM L) . (v,w2)) by ThSPDM1 ;

hence (ScProductDM L) . (v,w) = 0 by B1, B4, B6, B8, C2, C4, C6, C8, C9; :: thesis: verum

P4: card I is Nat ;

P5: ( I is linearly-independent & EMbedding L = Lin I ) by VECTSP_7:def 3;

thus for w being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,w) = 0 :: thesis: verum

proof

let w be Vector of (DivisibleMod L); :: thesis: (ScProductDM L) . (v,w) = 0

consider a being Element of INT.Ring such that

B1: ( a <> 0. INT.Ring & a * w in EMbedding L ) by ZMODUL08:29;

(ScProductDM L) . (v,(a * w)) = (ScProductDM L) . ((a * w),v) by ThSPDM1

.= a * ((ScProductDM L) . (w,v)) by ThSPDM1

.= a * ((ScProductDM L) . (v,w)) by ThSPDM1 ;

hence (ScProductDM L) . (v,w) = 0 by A1, B1, P3, P4, P5; :: thesis: verum

end;consider a being Element of INT.Ring such that

B1: ( a <> 0. INT.Ring & a * w in EMbedding L ) by ZMODUL08:29;

(ScProductDM L) . (v,(a * w)) = (ScProductDM L) . ((a * w),v) by ThSPDM1

.= a * ((ScProductDM L) . (w,v)) by ThSPDM1

.= a * ((ScProductDM L) . (v,w)) by ThSPDM1 ;

hence (ScProductDM L) . (v,w) = 0 by A1, B1, P3, P4, P5; :: thesis: verum