let L be positive-definite Z_Lattice; 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; 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; ( ( 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;>
; for u being Vector of L holds <;u,v;> = <;u,w;>
defpred S1[ 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:
S1[ 0 ]
proof
let u be
Vector of
L;
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;
( 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 )
;
<;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;
verum
end;
A2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume B1:
S1[
n]
;
S1[n + 1]
let u be
Vector of
L;
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;
( 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 )
;
<;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
;
verum
end;
A3:
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A2);
let u be Vector of L; <;u,v;> = <;u,w;>
A4:
u in Lin I
by ZMODUL03:14;
reconsider n = card I as Nat ;
S1[n]
by A3;
hence
<;u,v;> = <;u,w;>
by A4; verum