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

<;v,u;> in RAT ) holds

for v, u being Vector of L holds <;v,u;> in RAT

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

<;v,u;> in RAT ) holds

for v, u being Vector of L st v in Lin I & u 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);

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

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

assume X2: for v, u being Vector of L st v in I & u in I holds

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

X3: ( I is linearly-independent & Lin I = ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) ) by VECTSP_7:def 3;

X4: card I is Nat ;

let v, u be Vector of L; :: thesis: <;v,u;> in RAT

( v in Lin I & u in Lin I ) by X3;

hence <;v,u;> in RAT by X1, X2, X4; :: thesis: verum

<;v,u;> in RAT ) holds

for v, u being Vector of L holds <;v,u;> in RAT

defpred S

<;v,u;> in RAT ) holds

for v, u being Vector of L st v in Lin I & u 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, u being Vector of L st v in I & u in I holds

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

<;v,u;> in RAT )

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

<;v,u;> in RAT ) ) ; :: thesis: for v, u being Vector of L st v in Lin I & u 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, u be Vector of L; :: thesis: ( v in Lin I & u in Lin I implies <;v,u;> in RAT )

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

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

then ( v = 0. L & u = 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, u being Vector of L st v in Lin I & u in Lin I holds

<;v,u;> in RAT )

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

<;v,u;> in RAT ) ) ; :: thesis: for v, u being Vector of L st v in Lin I & u 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, u be Vector of L; :: thesis: ( v in Lin I & u in Lin I implies <;v,u;> in RAT )

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

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

then ( v = 0. L & u = 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, u being Vector of L st v in I & u in I holds

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

<;v,u;> in RAT )

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

<;v,u;> in RAT ) ) ; :: thesis: for v, u being Vector of L st v in Lin I & u 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, y being Vector of L st x in J & y in J holds

<;x,y;> in RAT

<;x,v;> in RAT

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

end;assume A0: S

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

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

<;v,u;> in RAT )

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

<;v,u;> in RAT ) ) ; :: thesis: for v, u being Vector of L st v in Lin I & u 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, y being Vector of L st x in J & y in J holds

<;x,y;> in RAT

proof

A6X:
for x being Vector of L st x in J holds
let x, y be Vector of L; :: thesis: ( x in J & y in J implies <;x,y;> in RAT )

assume ( x in J & y in J ) ; :: thesis: <;x,y;> in RAT

then ( x in I & y in I ) by XBOOLE_1:36, TARSKI:def 3;

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

end;assume ( x in J & y in J ) ; :: thesis: <;x,y;> in RAT

then ( x in I & y in I ) by XBOOLE_1:36, TARSKI:def 3;

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

<;x,v;> in RAT

proof

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

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

then ( x in I & v in I ) by A3, XBOOLE_1:36, TARSKI:def 3;

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

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

then ( x in I & v in I ) by A3, XBOOLE_1:36, TARSKI:def 3;

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

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

proof

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

assume A9: ( x in Lin I & y in Lin I ) ; :: thesis: <;x,y;> 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 yu1, yu2 being Vector of L such that

A11: ( yu1 in Lin (I \ {v}) & yu2 in Lin {v} & y = yu1 + yu2 ) by A9, A4, ZMODUL01:92;

consider ixu2 being Element of INT.Ring such that

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

consider iyu2 being Element of INT.Ring such that

A13: yu2 = iyu2 * v by A11, ZMODUL06:19;

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

set i1 = 1. INT.Ring;

B13: <;x,y;> = <;(((1. INT.Ring) * xu1) + (ixu2 * v)),yu1;> + <;(((1. INT.Ring) * xu1) + (ixu2 * v)),(iyu2 * v);> by A11, A13, B11, ZMODLAT1:8

.= (((1. INT.Ring) * <;xu1,yu1;>) + (ixu2 * <;v,yu1;>)) + <;(((1. INT.Ring) * xu1) + (ixu2 * v)),(iyu2 * v);> by ZMODLAT1:10

.= (((1. INT.Ring) * <;xu1,yu1;>) + (ixu2 * <;v,yu1;>)) + (((1. INT.Ring) * <;xu1,(iyu2 * v);>) + (ixu2 * <;v,(iyu2 * v);>)) by ZMODLAT1:10

.= ((<;xu1,yu1;> + (ixu2 * <;v,yu1;>)) + <;xu1,(iyu2 * v);>) + (ixu2 * <;v,(iyu2 * v);>)

.= ((<;xu1,yu1;> + (ixu2 * <;v,yu1;>)) + <;xu1,(iyu2 * v);>) + (ixu2 * (iyu2 * <;v,v;>)) by ZMODLAT1:9

.= ((<;xu1,yu1;> + (ixu2 * <;v,yu1;>)) + (iyu2 * <;xu1,v;>)) + ((ixu2 * iyu2) * <;v,v;>) by ZMODLAT1:9 ;

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

<;yu1,v;> in RAT by A11, A6X, ThRatLat1B;

then B15: <;v,yu1;> in RAT by ZMODLAT1:def 3;

B16: <;xu1,v;> in RAT by A10, A6X, ThRatLat1B;

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

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

end;assume A9: ( x in Lin I & y in Lin I ) ; :: thesis: <;x,y;> 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 yu1, yu2 being Vector of L such that

A11: ( yu1 in Lin (I \ {v}) & yu2 in Lin {v} & y = yu1 + yu2 ) by A9, A4, ZMODUL01:92;

consider ixu2 being Element of INT.Ring such that

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

consider iyu2 being Element of INT.Ring such that

A13: yu2 = iyu2 * v by A11, ZMODUL06:19;

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

set i1 = 1. INT.Ring;

B13: <;x,y;> = <;(((1. INT.Ring) * xu1) + (ixu2 * v)),yu1;> + <;(((1. INT.Ring) * xu1) + (ixu2 * v)),(iyu2 * v);> by A11, A13, B11, ZMODLAT1:8

.= (((1. INT.Ring) * <;xu1,yu1;>) + (ixu2 * <;v,yu1;>)) + <;(((1. INT.Ring) * xu1) + (ixu2 * v)),(iyu2 * v);> by ZMODLAT1:10

.= (((1. INT.Ring) * <;xu1,yu1;>) + (ixu2 * <;v,yu1;>)) + (((1. INT.Ring) * <;xu1,(iyu2 * v);>) + (ixu2 * <;v,(iyu2 * v);>)) by ZMODLAT1:10

.= ((<;xu1,yu1;> + (ixu2 * <;v,yu1;>)) + <;xu1,(iyu2 * v);>) + (ixu2 * <;v,(iyu2 * v);>)

.= ((<;xu1,yu1;> + (ixu2 * <;v,yu1;>)) + <;xu1,(iyu2 * v);>) + (ixu2 * (iyu2 * <;v,v;>)) by ZMODLAT1:9

.= ((<;xu1,yu1;> + (ixu2 * <;v,yu1;>)) + (iyu2 * <;xu1,v;>)) + ((ixu2 * iyu2) * <;v,v;>) by ZMODLAT1:9 ;

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

<;yu1,v;> in RAT by A11, A6X, ThRatLat1B;

then B15: <;v,yu1;> in RAT by ZMODLAT1:def 3;

B16: <;xu1,v;> in RAT by A10, A6X, ThRatLat1B;

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

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

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

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

assume X2: for v, u being Vector of L st v in I & u in I holds

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

X3: ( I is linearly-independent & Lin I = ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) ) by VECTSP_7:def 3;

X4: card I is Nat ;

let v, u be Vector of L; :: thesis: <;v,u;> in RAT

( v in Lin I & u in Lin I ) by X3;

hence <;v,u;> in RAT by X1, X2, X4; :: thesis: verum