defpred S1[ Nat] means for L being Z_Lattice
for l being Linear_Combination of DivisibleMod L
for v being Vector of (DivisibleMod L) st card (Carrier l) = $1 holds
(ScProductDM L) . (v,(Sum l)) = SumSc (v,l);
A1:
S1[ 0 ]
proof
let L be
Z_Lattice;
for l being Linear_Combination of DivisibleMod L
for v being Vector of (DivisibleMod L) st card (Carrier l) = 0 holds
(ScProductDM L) . (v,(Sum l)) = SumSc (v,l)let l be
Linear_Combination of
DivisibleMod L;
for v being Vector of (DivisibleMod L) st card (Carrier l) = 0 holds
(ScProductDM L) . (v,(Sum l)) = SumSc (v,l)let v be
Vector of
(DivisibleMod L);
( card (Carrier l) = 0 implies (ScProductDM L) . (v,(Sum l)) = SumSc (v,l) )
assume B1:
card (Carrier l) = 0
;
(ScProductDM L) . (v,(Sum l)) = SumSc (v,l)
B2:
Carrier l = {}
by B1;
then
Sum l = 0. (DivisibleMod L)
by VECTSP_6:19;
then
(ScProductDM L) . (
v,
(Sum l))
= 0. F_Real
by ZMODLAT2:14;
hence
(ScProductDM L) . (
v,
(Sum l))
= SumSc (
v,
l)
by B2, LmSumScDM13;
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 L be
Z_Lattice;
for l being Linear_Combination of DivisibleMod L
for v being Vector of (DivisibleMod L) st card (Carrier l) = n + 1 holds
(ScProductDM L) . (v,(Sum l)) = SumSc (v,l)let l be
Linear_Combination of
DivisibleMod L;
for v being Vector of (DivisibleMod L) st card (Carrier l) = n + 1 holds
(ScProductDM L) . (v,(Sum l)) = SumSc (v,l)let v be
Vector of
(DivisibleMod L);
( card (Carrier l) = n + 1 implies (ScProductDM L) . (v,(Sum l)) = SumSc (v,l) )
assume B2:
card (Carrier l) = n + 1
;
(ScProductDM L) . (v,(Sum l)) = SumSc (v,l)
Carrier l <> {}
by B2;
then consider u being
object such that B3:
u in Carrier l
by XBOOLE_0:def 1;
reconsider u =
u as
Element of
(DivisibleMod L) by B3;
B4:
card ((Carrier l) \ {u}) =
(card (Carrier l)) - (card {u})
by B3, CARD_2:44, ZFMISC_1:31
.=
(n + 1) - 1
by B2, CARD_2:42
.=
n
;
B5:
Carrier l = ((Carrier l) \ {u}) \/ {u}
by B3, XBOOLE_1:45, ZFMISC_1:31;
B6:
((Carrier l) \ {u}) /\ {u} = {}
by XBOOLE_0:def 7, XBOOLE_1:79;
l is
Linear_Combination of
Carrier l
by VECTSP_6:7;
then consider l1 being
Linear_Combination of
(Carrier l) \ {u},
l2 being
Linear_Combination of
{u} such that B7:
l = l1 + l2
by B5, B6, ZMODUL04:26;
Sum l = (Sum l1) + (Sum l2)
by B7, ZMODUL02:52;
then B8:
(ScProductDM L) . (
v,
(Sum l))
= ((ScProductDM L) . (v,(Sum l1))) + ((ScProductDM L) . (v,(Sum l2)))
by ZMODLAT2:12;
for
x being
Vector of
(DivisibleMod L) st
x in (Carrier l) \ {u} holds
x in Carrier l1
then
(Carrier l) \ {u} c= Carrier l1
;
then
Carrier l1 = (Carrier l) \ {u}
by VECTSP_6:def 4;
then B10:
(ScProductDM L) . (
v,
(Sum l1))
= SumSc (
v,
l1)
by B1, B4;
SumSc (
v,
l2) =
(ScProductDM L) . (
v,
((l2 . u) * u))
by LmSumScDM14
.=
(ScProductDM L) . (
v,
(Sum l2))
by VECTSP_6:17
;
hence
(ScProductDM L) . (
v,
(Sum l))
= SumSc (
v,
l)
by B7, B8, B10, LmSumScDM1X;
verum
end;
A3:
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A2);
let L be Z_Lattice; for l being Linear_Combination of DivisibleMod L
for v being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,(Sum l)) = SumSc (v,l)
let l be Linear_Combination of DivisibleMod L; for v being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,(Sum l)) = SumSc (v,l)
let v be Vector of (DivisibleMod L); (ScProductDM L) . (v,(Sum l)) = SumSc (v,l)
reconsider n = card (Carrier l) as Nat ;
S1[n]
by A3;
hence
(ScProductDM L) . (v,(Sum l)) = SumSc (v,l)
; verum