let L be positive-definite RATional Z_Lattice; for I being Basis of (EMLat L)
for v being Vector of (DivisibleMod L)
for l being Linear_Combination of DualBasis I st v in I holds
(ScProductDM L) . (v,(Sum l)) = l . ((B2DB I) . v)
let I be Basis of (EMLat L); for v being Vector of (DivisibleMod L)
for l being Linear_Combination of DualBasis I st v in I holds
(ScProductDM L) . (v,(Sum l)) = l . ((B2DB I) . v)
let v be Vector of (DivisibleMod L); for l being Linear_Combination of DualBasis I st v in I holds
(ScProductDM L) . (v,(Sum l)) = l . ((B2DB I) . v)
let l be Linear_Combination of DualBasis I; ( v in I implies (ScProductDM L) . (v,(Sum l)) = l . ((B2DB I) . v) )
assume A1:
v in I
; (ScProductDM L) . (v,(Sum l)) = l . ((B2DB I) . v)
v in dom (B2DB I)
by A1, defB2DB;
then
(B2DB I) . v in rng (B2DB I)
by FUNCT_1:3;
then A2:
(B2DB I) . v in DualBasis I
;
then reconsider bv = (B2DB I) . v as Vector of (DivisibleMod L) ;
per cases
( not (B2DB I) . v in Carrier l or (B2DB I) . v in Carrier l )
;
suppose B1:
not
(B2DB I) . v in Carrier l
;
(ScProductDM L) . (v,(Sum l)) = l . ((B2DB I) . v)consider F being
FinSequence of
(DivisibleMod L) such that B2:
(
F is
one-to-one &
rng F = Carrier l &
SumSc (
v,
l)
= Sum (ScFS (v,l,F)) )
by defSumScDM;
B3:
len F = len (ScFS (v,l,F))
by defScFSDM;
then B4:
dom (ScFS (v,l,F)) = dom F
by FINSEQ_3:29;
for
k being
Nat st
k in dom (ScFS (v,l,F)) holds
(ScFS (v,l,F)) . k = - ((ScFS (v,l,F)) /. k)
proof
let k be
Nat;
( k in dom (ScFS (v,l,F)) implies (ScFS (v,l,F)) . k = - ((ScFS (v,l,F)) /. k) )
assume C1:
k in dom (ScFS (v,l,F))
;
(ScFS (v,l,F)) . k = - ((ScFS (v,l,F)) /. k)
CX2:
(ScFS (v,l,F)) . k = (ScProductDM L) . (
v,
((l . (F /. k)) * (F /. k)))
by C1, defScFSDM;
F . k in Carrier l
by B2, B4, C1, FUNCT_1:3;
then C2:
F /. k in Carrier l
by B4, C1, PARTFUN1:def 6;
then
F /. k in DualBasis I
by TARSKI:def 3, VECTSP_6:def 4;
then C4:
F /. k in rng (B2DB I)
by defB2DB;
then C5:
(B2DB I) . (((B2DB I) ") . (F /. k)) = F /. k
by FUNCT_1:35;
F /. k in dom ((B2DB I) ")
by C4, FUNCT_1:33;
then
((B2DB I) ") . (F /. k) in rng ((B2DB I) ")
by FUNCT_1:3;
then
((B2DB I) ") . (F /. k) in dom (B2DB I)
by FUNCT_1:33;
then
((B2DB I) ") . (F /. k) in I
;
then
(ScProductDM L) . (
v,
(F /. k))
= 0. F_Real
by A1, B1, C2, C5, defB2DB;
then
(l . (F /. k)) * ((ScProductDM L) . (v,(F /. k))) = 0. F_Real
;
then
(ScProductDM L) . (
v,
((l . (F /. k)) * (F /. k)))
= 0. F_Real
by ZMODLAT2:13;
hence (ScFS (v,l,F)) . k =
- ((ScFS (v,l,F)) . k)
by CX2
.=
- ((ScFS (v,l,F)) /. k)
by C1, PARTFUN1:def 6
;
verum
end; then B5:
Sum (ScFS (v,l,F)) = - (Sum (ScFS (v,l,F)))
by B3, RLVECT_2:4;
thus l . ((B2DB I) . v) =
0. INT.Ring
by A2, B1
.=
(ScProductDM L) . (
v,
(Sum l))
by B2, B5, ThSumScDM1
;
verum end; suppose
(B2DB I) . v in Carrier l
;
(ScProductDM L) . (v,(Sum l)) = l . ((B2DB I) . v)then C2:
Carrier l = ((Carrier l) \ {((B2DB I) . v)}) \/ {((B2DB I) . v)}
by XBOOLE_1:45, ZFMISC_1:31;
C3:
((Carrier l) \ {((B2DB I) . v)}) /\ {((B2DB I) . v)} = {}
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) \ {bv},
l2 being
Linear_Combination of
{bv} such that C4:
l = l1 + l2
by C2, C3, ZMODUL04:26;
for
x being
Vector of
(DivisibleMod L) st
x in (Carrier l) \ {bv} holds
x in Carrier l1
then
(Carrier l) \ {bv} c= Carrier l1
;
then C6:
Carrier l1 = (Carrier l) \ {bv}
by VECTSP_6:def 4;
then C7:
not
bv in Carrier l1
by ZFMISC_1:56;
consider F1 being
FinSequence of
(DivisibleMod L) such that C8:
(
F1 is
one-to-one &
rng F1 = Carrier l1 &
SumSc (
v,
l1)
= Sum (ScFS (v,l1,F1)) )
by defSumScDM;
C9:
len F1 = len (ScFS (v,l1,F1))
by defScFSDM;
then C10:
dom (ScFS (v,l1,F1)) = dom F1
by FINSEQ_3:29;
for
k being
Nat st
k in dom (ScFS (v,l1,F1)) holds
(ScFS (v,l1,F1)) . k = - ((ScFS (v,l1,F1)) /. k)
proof
let k be
Nat;
( k in dom (ScFS (v,l1,F1)) implies (ScFS (v,l1,F1)) . k = - ((ScFS (v,l1,F1)) /. k) )
assume D1:
k in dom (ScFS (v,l1,F1))
;
(ScFS (v,l1,F1)) . k = - ((ScFS (v,l1,F1)) /. k)
D2:
(ScFS (v,l1,F1)) . k = (ScProductDM L) . (
v,
((l1 . (F1 /. k)) * (F1 /. k)))
by D1, defScFSDM;
per cases
( F1 /. k <> (B2DB I) . v or F1 /. k = (B2DB I) . v )
;
suppose E1:
F1 /. k <> (B2DB I) . v
;
(ScFS (v,l1,F1)) . k = - ((ScFS (v,l1,F1)) /. k)
F1 . k in Carrier l1
by C8, C10, D1, FUNCT_1:3;
then
F1 /. k in Carrier l1
by C10, D1, PARTFUN1:def 6;
then
F1 /. k in Carrier l
by C6, XBOOLE_0:def 5;
then
F1 /. k in DualBasis I
by TARSKI:def 3, VECTSP_6:def 4;
then E5:
F1 /. k in rng (B2DB I)
by defB2DB;
then
F1 /. k in dom ((B2DB I) ")
by FUNCT_1:33;
then
((B2DB I) ") . (F1 /. k) in rng ((B2DB I) ")
by FUNCT_1:3;
then
((B2DB I) ") . (F1 /. k) in dom (B2DB I)
by FUNCT_1:33;
then E7:
((B2DB I) ") . (F1 /. k) in I
;
E9:
(B2DB I) . (((B2DB I) ") . (F1 /. k)) = F1 /. k
by E5, FUNCT_1:35;
(ScProductDM L) . (
v,
(F1 /. k))
= 0. F_Real
by A1, E1, E7, E9, defB2DB;
then
(l1 . (F1 /. k)) * ((ScProductDM L) . (v,(F1 /. k))) = 0. F_Real
;
then
(ScProductDM L) . (
v,
((l1 . (F1 /. k)) * (F1 /. k)))
= 0. F_Real
by ZMODLAT2:13;
hence (ScFS (v,l1,F1)) . k =
- ((ScFS (v,l1,F1)) . k)
by D2
.=
- ((ScFS (v,l1,F1)) /. k)
by D1, PARTFUN1:def 6
;
verum end; suppose
F1 /. k = (B2DB I) . v
;
(ScFS (v,l1,F1)) . k = - ((ScFS (v,l1,F1)) /. k)then (ScFS (v,l1,F1)) . k =
(ScProductDM L) . (
v,
((0. INT.Ring) * (F1 /. k)))
by C7, D2
.=
(ScProductDM L) . (
v,
(0. (DivisibleMod L)))
by VECTSP_1:14
.=
0. F_Real
by ZMODLAT2:14
;
hence (ScFS (v,l1,F1)) . k =
- ((ScFS (v,l1,F1)) . k)
.=
- ((ScFS (v,l1,F1)) /. k)
by D1, PARTFUN1:def 6
;
verum end;
end; then C11:
Sum (ScFS (v,l1,F1)) = - (Sum (ScFS (v,l1,F1)))
by C9, RLVECT_2:4;
C12:
SumSc (
v,
l2) =
(ScProductDM L) . (
v,
((l2 . bv) * bv))
by LmSumScDM14
.=
(l2 . bv) * ((ScProductDM L) . (v,bv))
by ZMODLAT2:13
.=
(l2 . bv) * 1
by A1, defB2DB
.=
l2 . bv
;
C13:
l . bv =
(l1 . bv) + (l2 . bv)
by C4, VECTSP_6:22
.=
(0. INT.Ring) + (l2 . bv)
by C7
.=
l2 . bv
;
thus (ScProductDM L) . (
v,
(Sum l)) =
SumSc (
v,
l)
by ThSumScDM1
.=
(SumSc (v,l1)) + (SumSc (v,l2))
by C4, LmSumScDM1X
.=
l . ((B2DB I) . v)
by C8, C11, C12, C13
;
verum end;