let L be positive-definite RATional Z_Lattice; :: thesis: for I being Basis of ()
for v being Vector of ()
for l being Linear_Combination of DualBasis I st v in I holds
() . (v,(Sum l)) = l . ((B2DB I) . v)

let I be Basis of (); :: thesis: for v being Vector of ()
for l being Linear_Combination of DualBasis I st v in I holds
() . (v,(Sum l)) = l . ((B2DB I) . v)

let v be Vector of (); :: thesis: for l being Linear_Combination of DualBasis I st v in I holds
() . (v,(Sum l)) = l . ((B2DB I) . v)

let l be Linear_Combination of DualBasis I; :: thesis: ( v in I implies () . (v,(Sum l)) = l . ((B2DB I) . v) )
assume A1: v in I ; :: thesis: () . (v,(Sum l)) = l . ((B2DB I) . v)
v in dom (B2DB I) by ;
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 () ;
per cases ) . v in Carrier l or (B2DB I) . v in Carrier l ) ;
suppose B1: not (B2DB I) . v in Carrier l ; :: thesis: () . (v,(Sum l)) = l . ((B2DB I) . v)
consider F being FinSequence of () 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; :: thesis: ( 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)) ; :: thesis: (ScFS (v,l,F)) . k = - ((ScFS (v,l,F)) /. k)
CX2: (ScFS (v,l,F)) . k = () . (v,((l . (F /. k)) * (F /. k))) by ;
F . k in Carrier l by ;
then C2: F /. k in Carrier l by ;
then F /. k in DualBasis I by ;
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 ;
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)) * (() . (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 ;
:: thesis: verum
end;
then B5: Sum (ScFS (v,l,F)) = - (Sum (ScFS (v,l,F))) by ;
thus l . ((B2DB I) . v) = 0. INT.Ring by A2, B1
.= () . (v,(Sum l)) by ; :: thesis: verum
end;
suppose (B2DB I) . v in Carrier l ; :: thesis: () . (v,(Sum l)) = l . ((B2DB I) . v)
then C2: Carrier l = (() \ {((B2DB I) . v)}) \/ {((B2DB I) . v)} by ;
C3: ((Carrier l) \ {((B2DB I) . v)}) /\ {((B2DB I) . v)} = {} by ;
l is Linear_Combination of Carrier l by VECTSP_6:7;
then consider l1 being Linear_Combination of () \ {bv}, l2 being Linear_Combination of {bv} such that
C4: l = l1 + l2 by ;
for x being Vector of () st x in () \ {bv} holds
x in Carrier l1
proof
let x be Vector of (); :: thesis: ( x in () \ {bv} implies x in Carrier l1 )
assume D1: x in () \ {bv} ; :: thesis: x in Carrier l1
x in Carrier l by ;
then D2: l . x <> 0. INT.Ring by VECTSP_6:2;
D3: Carrier l2 c= {bv} by VECTSP_6:def 4;
D4: l . x = (l1 . x) + (l2 . x) by ;
not x in Carrier l2 by ;
then l1 . x <> 0. INT.Ring by D2, D4;
hence x in Carrier l1 ; :: thesis: verum
end;
then (Carrier l) \ {bv} c= Carrier l1 ;
then C6: Carrier l1 = () \ {bv} by VECTSP_6:def 4;
then C7: not bv in Carrier l1 by ZFMISC_1:56;
consider F1 being FinSequence of () 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; :: thesis: ( 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)) ; :: thesis: (ScFS (v,l1,F1)) . k = - ((ScFS (v,l1,F1)) /. k)
D2: (ScFS (v,l1,F1)) . k = () . (v,((l1 . (F1 /. k)) * (F1 /. k))) by ;
per cases ( F1 /. k <> (B2DB I) . v or F1 /. k = (B2DB I) . v ) ;
suppose E1: F1 /. k <> (B2DB I) . v ; :: thesis: (ScFS (v,l1,F1)) . k = - ((ScFS (v,l1,F1)) /. k)
F1 . k in Carrier l1 by ;
then F1 /. k in Carrier l1 by ;
then F1 /. k in Carrier l by ;
then F1 /. k in DualBasis I by ;
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 ;
(ScProductDM L) . (v,(F1 /. k)) = 0. F_Real by A1, E1, E7, E9, defB2DB;
then (l1 . (F1 /. k)) * (() . (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 ;
:: thesis: verum
end;
suppose F1 /. k = (B2DB I) . v ; :: thesis: (ScFS (v,l1,F1)) . k = - ((ScFS (v,l1,F1)) /. k)
then (ScFS (v,l1,F1)) . k = () . (v,(() * (F1 /. k))) by C7, D2
.= () . (v,(0. ())) 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 ;
:: thesis: verum
end;
end;
end;
then C11: Sum (ScFS (v,l1,F1)) = - (Sum (ScFS (v,l1,F1))) by ;
C12: SumSc (v,l2) = () . (v,((l2 . bv) * bv)) by LmSumScDM14
.= (l2 . bv) * (() . (v,bv)) by ZMODLAT2:13
.= (l2 . bv) * 1 by
.= l2 . bv ;
C13: l . bv = (l1 . bv) + (l2 . bv) by
.= () + (l2 . bv) by C7
.= l2 . bv ;
thus () . (v,(Sum l)) = SumSc (v,l) by ThSumScDM1
.= (SumSc (v,l1)) + (SumSc (v,l2)) by
.= l . ((B2DB I) . v) by C8, C11, C12, C13 ; :: thesis: verum
end;
end;