let L be positive-definite Z_Lattice; :: thesis: for I being Basis of L

for v, w being Vector of L st ( for u being Vector of L st u in I holds

<;u,v;> = <;u,w;> ) holds

for u being Vector of L holds <;u,v;> = <;u,w;>

let I be Basis of L; :: thesis: for v, w being Vector of L st ( for u being Vector of L st u in I holds

<;u,v;> = <;u,w;> ) holds

for u being Vector of L holds <;u,v;> = <;u,w;>

let v, w be Vector of L; :: thesis: ( ( for u being Vector of L st u in I holds

<;u,v;> = <;u,w;> ) implies for u being Vector of L holds <;u,v;> = <;u,w;> )

assume AS: for u being Vector of L st u in I holds

<;u,v;> = <;u,w;> ; :: thesis: for u being Vector of L holds <;u,v;> = <;u,w;>

defpred S_{1}[ Nat] means for u being Vector of L

for J being finite Subset of L st J c= I & card J = $1 & u in Lin J holds

<;u,v;> = <;u,w;>;

A1: S_{1}[ 0 ]
_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A1, A2);

let u be Vector of L; :: thesis: <;u,v;> = <;u,w;>

A4: u in Lin I by ZMODUL03:14;

reconsider n = card I as Nat ;

S_{1}[n]
by A3;

hence <;u,v;> = <;u,w;> by A4; :: thesis: verum

for v, w being Vector of L st ( for u being Vector of L st u in I holds

<;u,v;> = <;u,w;> ) holds

for u being Vector of L holds <;u,v;> = <;u,w;>

let I be Basis of L; :: thesis: for v, w being Vector of L st ( for u being Vector of L st u in I holds

<;u,v;> = <;u,w;> ) holds

for u being Vector of L holds <;u,v;> = <;u,w;>

let v, w be Vector of L; :: thesis: ( ( for u being Vector of L st u in I holds

<;u,v;> = <;u,w;> ) implies for u being Vector of L holds <;u,v;> = <;u,w;> )

assume AS: for u being Vector of L st u in I holds

<;u,v;> = <;u,w;> ; :: thesis: for u being Vector of L holds <;u,v;> = <;u,w;>

defpred S

for J being finite Subset of L st J c= I & card J = $1 & u in Lin J holds

<;u,v;> = <;u,w;>;

A1: S

proof

A2:
for n being Nat st S
let u be Vector of L; :: thesis: for J being finite Subset of L st J c= I & card J = 0 & u in Lin J holds

<;u,v;> = <;u,w;>

let J be finite Subset of L; :: thesis: ( J c= I & card J = 0 & u in Lin J implies <;u,v;> = <;u,w;> )

assume B1: ( J c= I & card J = 0 & u in Lin J ) ; :: thesis: <;u,v;> = <;u,w;>

J = {} the carrier of L by B1;

then Lin J = (0). L by VECTSP_7:9;

then B2: u = 0. L by B1, VECTSP_4:35;

then <;u,v;> = 0 by ZMODLAT1:12;

hence <;u,v;> = <;u,w;> by B2, ZMODLAT1:12; :: thesis: verum

end;<;u,v;> = <;u,w;>

let J be finite Subset of L; :: thesis: ( J c= I & card J = 0 & u in Lin J implies <;u,v;> = <;u,w;> )

assume B1: ( J c= I & card J = 0 & u in Lin J ) ; :: thesis: <;u,v;> = <;u,w;>

J = {} the carrier of L by B1;

then Lin J = (0). L by VECTSP_7:9;

then B2: u = 0. L by B1, VECTSP_4:35;

then <;u,v;> = 0 by ZMODLAT1:12;

hence <;u,v;> = <;u,w;> by B2, ZMODLAT1:12; :: thesis: verum

S

proof

A3:
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 u be Vector of L; :: thesis: for J being finite Subset of L st J c= I & card J = n + 1 & u in Lin J holds

<;u,v;> = <;u,w;>

let J be finite Subset of L; :: thesis: ( J c= I & card J = n + 1 & u in Lin J implies <;u,v;> = <;u,w;> )

assume B2: ( J c= I & card J = n + 1 & u in Lin J ) ; :: thesis: <;u,v;> = <;u,w;>

not J is empty by B2;

then consider s being object such that

B3: s in J ;

reconsider s = s as Vector of L by B3;

set Js = J \ {s};

{s} is Subset of J by B3, SUBSET_1:41;

then B4: card (J \ {s}) = (n + 1) - (card {s}) by B2, CARD_2:44

.= (n + 1) - 1 by CARD_1:30

.= n ;

reconsider Js = J \ {s} as finite Subset of L ;

reconsider S = {s} as finite Subset of L ;

B6: Js /\ S = {} by XBOOLE_0:def 7, XBOOLE_1:79;

consider l being Linear_Combination of J such that

B7: u = Sum l by B2, VECTSP_7:7;

reconsider lx = l as Linear_Combination of Js \/ S by B3, XBOOLE_1:45, ZFMISC_1:31;

consider lx1 being Linear_Combination of Js, lx2 being Linear_Combination of S such that

B8: lx = lx1 + lx2 by B6, ZMODUL04:26;

B9: u = (Sum lx1) + (Sum lx2) by B7, B8, VECTSP_6:44;

B10: Sum lx1 in Lin Js by VECTSP_7:7;

Js c= J by XBOOLE_1:36;

then B11: Js c= I by B2;

B12: Sum lx2 = (lx2 . s) * s by VECTSP_6:17;

B14: <;(Sum lx2),v;> = (lx2 . s) * <;s,v;> by B12, ZMODLAT1:def 3

.= (lx2 . s) * <;s,w;> by AS, B2, B3

.= <;(Sum lx2),w;> by B12, ZMODLAT1:def 3 ;

thus <;u,v;> = <;(Sum lx1),v;> + <;(Sum lx2),v;> by B9, ZMODLAT1:def 3

.= <;(Sum lx1),w;> + <;(Sum lx2),w;> by B1, B4, B10, B11, B14

.= <;u,w;> by B9, ZMODLAT1:def 3 ; :: thesis: verum

end;assume B1: S

let u be Vector of L; :: thesis: for J being finite Subset of L st J c= I & card J = n + 1 & u in Lin J holds

<;u,v;> = <;u,w;>

let J be finite Subset of L; :: thesis: ( J c= I & card J = n + 1 & u in Lin J implies <;u,v;> = <;u,w;> )

assume B2: ( J c= I & card J = n + 1 & u in Lin J ) ; :: thesis: <;u,v;> = <;u,w;>

not J is empty by B2;

then consider s being object such that

B3: s in J ;

reconsider s = s as Vector of L by B3;

set Js = J \ {s};

{s} is Subset of J by B3, SUBSET_1:41;

then B4: card (J \ {s}) = (n + 1) - (card {s}) by B2, CARD_2:44

.= (n + 1) - 1 by CARD_1:30

.= n ;

reconsider Js = J \ {s} as finite Subset of L ;

reconsider S = {s} as finite Subset of L ;

B6: Js /\ S = {} by XBOOLE_0:def 7, XBOOLE_1:79;

consider l being Linear_Combination of J such that

B7: u = Sum l by B2, VECTSP_7:7;

reconsider lx = l as Linear_Combination of Js \/ S by B3, XBOOLE_1:45, ZFMISC_1:31;

consider lx1 being Linear_Combination of Js, lx2 being Linear_Combination of S such that

B8: lx = lx1 + lx2 by B6, ZMODUL04:26;

B9: u = (Sum lx1) + (Sum lx2) by B7, B8, VECTSP_6:44;

B10: Sum lx1 in Lin Js by VECTSP_7:7;

Js c= J by XBOOLE_1:36;

then B11: Js c= I by B2;

B12: Sum lx2 = (lx2 . s) * s by VECTSP_6:17;

B14: <;(Sum lx2),v;> = (lx2 . s) * <;s,v;> by B12, ZMODLAT1:def 3

.= (lx2 . s) * <;s,w;> by AS, B2, B3

.= <;(Sum lx2),w;> by B12, ZMODLAT1:def 3 ;

thus <;u,v;> = <;(Sum lx1),v;> + <;(Sum lx2),v;> by B9, ZMODLAT1:def 3

.= <;(Sum lx1),w;> + <;(Sum lx2),w;> by B1, B4, B10, B11, B14

.= <;u,w;> by B9, ZMODLAT1:def 3 ; :: thesis: verum

let u be Vector of L; :: thesis: <;u,v;> = <;u,w;>

A4: u in Lin I by ZMODUL03:14;

reconsider n = card I as Nat ;

S

hence <;u,v;> = <;u,w;> by A4; :: thesis: verum