let L be Z_Lattice; 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 S1[ 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:
S1[ 0 ]
proof
let I be
finite Subset of
L;
( 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 ) )
;
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;
( v in Lin I & u in Lin I implies <;v,u;> in RAT )
assume
(
v in Lin I &
u in Lin I )
;
<;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;
verum
end;
P2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A0:
S1[
n]
;
S1[n + 1]
let I be
finite Subset of
L;
( 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 ) )
;
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
A6X:
for
x being
Vector of
L st
x in J holds
<;x,v;> in RAT
thus
for
x,
y being
Vector of
L st
x in Lin I &
y in Lin I holds
<;x,y;> in RAT
verumproof
let x,
y be
Vector of
L;
( x in Lin I & y in Lin I implies <;x,y;> in RAT )
assume A9:
(
x in Lin I &
y in Lin I )
;
<;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;
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;
verum
end;
end;
X1:
for n being Nat holds S1[n]
from NAT_1:sch 2(P1, P2);
let I be Basis of L; ( ( 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
; 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; <;v,u;> in RAT
( v in Lin I & u in Lin I )
by X3;
hence
<;v,u;> in RAT
by X1, X2, X4; verum