let L be Z_Lattice; :: thesis: for I being finite Subset of L

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

<;v,u;> in RAT ) holds

for v being Vector of L st v in Lin I holds

<;v,u;> in RAT

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

<;v,u;> in RAT ) holds

for v being Vector of L st v in Lin I holds

<;v,u;> in RAT

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

<;v,u;> in RAT ) implies for v being Vector of L st v in Lin I holds

<;v,u;> in RAT )

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

<;v,u;> in RAT ; :: thesis: for v being Vector of L st v in Lin I holds

<;v,u;> in RAT

defpred S_{1}[ Nat] means for I being finite Subset of L st card I = $1 & ( for v being Vector of L st v in I holds

<;v,u;> in RAT ) holds

for v being Vector of L st v in Lin I holds

<;v,u;> in RAT ;

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

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

card I is Nat ;

hence for v being Vector of L st v in Lin I holds

<;v,u;> in RAT by X1, AS; :: thesis: verum

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

<;v,u;> in RAT ) holds

for v being Vector of L st v in Lin I holds

<;v,u;> in RAT

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

<;v,u;> in RAT ) holds

for v being Vector of L st v in Lin I holds

<;v,u;> in RAT

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

<;v,u;> in RAT ) implies for v being Vector of L st v in Lin I holds

<;v,u;> in RAT )

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

<;v,u;> in RAT ; :: thesis: for v being Vector of L st v in Lin I holds

<;v,u;> in RAT

defpred S

<;v,u;> in RAT ) holds

for v being Vector of L st v in Lin I holds

<;v,u;> in RAT ;

P1: S

proof

P2:
for n being Nat st S
let I be finite Subset of L; :: thesis: ( card I = 0 & ( for v being Vector of L st v in I holds

<;v,u;> in RAT ) implies for v being Vector of L st v in Lin I holds

<;v,u;> in RAT )

assume ( card I = 0 & ( for v being Vector of L st v in I holds

<;v,u;> in RAT ) ) ; :: thesis: for v being Vector of L st v in Lin I holds

<;v,u;> in RAT

then I = {} the carrier of L ;

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

let v be Vector of L; :: thesis: ( v in Lin I implies <;v,u;> in RAT )

assume v in Lin I ; :: thesis: <;v,u;> in RAT

then v in {(0. L)} by A2, VECTSP_4:def 3;

then v = 0. L by TARSKI:def 1;

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

hence <;v,u;> in RAT by RAT_1:def 2; :: thesis: verum

end;<;v,u;> in RAT ) implies for v being Vector of L st v in Lin I holds

<;v,u;> in RAT )

assume ( card I = 0 & ( for v being Vector of L st v in I holds

<;v,u;> in RAT ) ) ; :: thesis: for v being Vector of L st v in Lin I holds

<;v,u;> in RAT

then I = {} the carrier of L ;

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

let v be Vector of L; :: thesis: ( v in Lin I implies <;v,u;> in RAT )

assume v in Lin I ; :: thesis: <;v,u;> in RAT

then v in {(0. L)} by A2, VECTSP_4:def 3;

then v = 0. L by TARSKI:def 1;

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

hence <;v,u;> in RAT by RAT_1:def 2; :: thesis: verum

S

proof

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

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

let I be finite Subset of L; :: thesis: ( card I = n + 1 & ( for v being Vector of L st v in I holds

<;v,u;> in RAT ) implies for v being Vector of L st v in Lin I holds

<;v,u;> in RAT )

assume A1: ( card I = n + 1 & ( for v being Vector of L st v in I holds

<;v,u;> in RAT ) ) ; :: thesis: for v being Vector of L st v in Lin I holds

<;v,u;> in RAT

then I <> {} ;

then consider v being object such that

A3: v in I by XBOOLE_0:def 1;

reconsider v = v as Vector of L by A3;

(I \ {v}) \/ {v} = I \/ {v} by XBOOLE_1:39

.= I by A3, ZFMISC_1:40 ;

then A4: Lin I = (Lin (I \ {v})) + (Lin {v}) by ZMODUL02:72;

A5: card (I \ {v}) = (card I) - (card {v}) by A3, CARD_2:44, ZFMISC_1:31

.= (card I) - 1 by CARD_1:30

.= n by A1 ;

reconsider J = I \ {v} as finite Subset of L ;

B8: for x being Vector of L st x in J holds

<;x,u;> in RAT

<;x,u;> in RAT :: thesis: verum

end;assume A0: S

let I be finite Subset of L; :: thesis: ( card I = n + 1 & ( for v being Vector of L st v in I holds

<;v,u;> in RAT ) implies for v being Vector of L st v in Lin I holds

<;v,u;> in RAT )

assume A1: ( card I = n + 1 & ( for v being Vector of L st v in I holds

<;v,u;> in RAT ) ) ; :: thesis: for v being Vector of L st v in Lin I holds

<;v,u;> in RAT

then I <> {} ;

then consider v being object such that

A3: v in I by XBOOLE_0:def 1;

reconsider v = v as Vector of L by A3;

(I \ {v}) \/ {v} = I \/ {v} by XBOOLE_1:39

.= I by A3, ZFMISC_1:40 ;

then A4: Lin I = (Lin (I \ {v})) + (Lin {v}) by ZMODUL02:72;

A5: card (I \ {v}) = (card I) - (card {v}) by A3, CARD_2:44, ZFMISC_1:31

.= (card I) - 1 by CARD_1:30

.= n by A1 ;

reconsider J = I \ {v} as finite Subset of L ;

B8: for x being Vector of L st x in J holds

<;x,u;> in RAT

proof

thus
for x being Vector of L st x in Lin I holds
let x be Vector of L; :: thesis: ( x in J implies <;x,u;> in RAT )

assume x in J ; :: thesis: <;x,u;> in RAT

then x in I by XBOOLE_1:36, TARSKI:def 3;

hence <;x,u;> in RAT by A1; :: thesis: verum

end;assume x in J ; :: thesis: <;x,u;> in RAT

then x in I by XBOOLE_1:36, TARSKI:def 3;

hence <;x,u;> in RAT by A1; :: thesis: verum

<;x,u;> in RAT :: thesis: verum

proof

let x be Vector of L; :: thesis: ( x in Lin I implies <;x,u;> in RAT )

assume x in Lin I ; :: thesis: <;x,u;> in RAT

then consider xu1, xu2 being Vector of L such that

A10: ( xu1 in Lin (I \ {v}) & xu2 in Lin {v} & x = xu1 + xu2 ) by A4, ZMODUL01:92;

consider ixu2 being Element of INT.Ring such that

A12: xu2 = ixu2 * v by A10, ZMODUL06:19;

B11: x = ((1. INT.Ring) * xu1) + (ixu2 * v) by A10, A12, VECTSP_1:def 17;

set i1 = 1. INT.Ring;

B13: <;x,u;> = ((1. INT.Ring) * <;xu1,u;>) + (ixu2 * <;v,u;>) by B11, ZMODLAT1:10;

B14: <;xu1,u;> in RAT by A0, A5, B8, A10;

<;v,u;> in RAT by A1, A3;

hence <;x,u;> in RAT by B13, B14, RAT_1:def 2; :: thesis: verum

end;assume x in Lin I ; :: thesis: <;x,u;> in RAT

then consider xu1, xu2 being Vector of L such that

A10: ( xu1 in Lin (I \ {v}) & xu2 in Lin {v} & x = xu1 + xu2 ) by A4, ZMODUL01:92;

consider ixu2 being Element of INT.Ring such that

A12: xu2 = ixu2 * v by A10, ZMODUL06:19;

B11: x = ((1. INT.Ring) * xu1) + (ixu2 * v) by A10, A12, VECTSP_1:def 17;

set i1 = 1. INT.Ring;

B13: <;x,u;> = ((1. INT.Ring) * <;xu1,u;>) + (ixu2 * <;v,u;>) by B11, ZMODLAT1:10;

B14: <;xu1,u;> in RAT by A0, A5, B8, A10;

<;v,u;> in RAT by A1, A3;

hence <;x,u;> in RAT by B13, B14, RAT_1:def 2; :: thesis: verum

card I is Nat ;

hence for v being Vector of L st v in Lin I holds

<;v,u;> in RAT by X1, AS; :: thesis: verum