let L be positive-definite RATional Z_Lattice; :: thesis: 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); :: thesis: 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); :: thesis: 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; :: thesis: ( v in I implies (ScProductDM L) . (v,(Sum l)) = l . ((B2DB I) . v) )

assume A1: v in I ; :: thesis: (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) ;

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); :: thesis: 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); :: thesis: 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; :: thesis: ( v in I implies (ScProductDM L) . (v,(Sum l)) = l . ((B2DB I) . v) )

assume A1: v in I ; :: thesis: (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 )
;

end;

suppose B1:
not (B2DB I) . v in Carrier l
; :: thesis: (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)

thus l . ((B2DB I) . v) = 0. INT.Ring by A2, B1

.= (ScProductDM L) . (v,(Sum l)) by B2, B5, ThSumScDM1 ; :: thesis: verum

end;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

then B5:
Sum (ScFS (v,l,F)) = - (Sum (ScFS (v,l,F)))
by B3, RLVECT_2:4;
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 = (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 ;

:: thesis: verum

end;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 = (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 ;

:: thesis: verum

thus l . ((B2DB I) . v) = 0. INT.Ring by A2, B1

.= (ScProductDM L) . (v,(Sum l)) by B2, B5, ThSumScDM1 ; :: thesis: verum

suppose
(B2DB I) . v in Carrier l
; :: thesis: (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 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)

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 ; :: thesis: verum

end;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

proof

then
(Carrier l) \ {bv} c= Carrier l1
;
let x be Vector of (DivisibleMod L); :: thesis: ( x in (Carrier l) \ {bv} implies x in Carrier l1 )

assume D1: x in (Carrier l) \ {bv} ; :: thesis: x in Carrier l1

x in Carrier l by D1, XBOOLE_0:def 5;

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 C4, VECTSP_6:22;

not x in Carrier l2 by D1, D3, XBOOLE_0:def 5;

then l1 . x <> 0. INT.Ring by D2, D4;

hence x in Carrier l1 ; :: thesis: verum

end;assume D1: x in (Carrier l) \ {bv} ; :: thesis: x in Carrier l1

x in Carrier l by D1, XBOOLE_0:def 5;

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 C4, VECTSP_6:22;

not x in Carrier l2 by D1, D3, XBOOLE_0:def 5;

then l1 . x <> 0. INT.Ring by D2, D4;

hence x in Carrier l1 ; :: thesis: verum

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

then C11:
Sum (ScFS (v,l1,F1)) = - (Sum (ScFS (v,l1,F1)))
by C9, RLVECT_2:4;
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 = (ScProductDM L) . (v,((l1 . (F1 /. k)) * (F1 /. k))) by D1, defScFSDM;

end;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 = (ScProductDM L) . (v,((l1 . (F1 /. k)) * (F1 /. k))) by D1, defScFSDM;

per cases
( F1 /. k <> (B2DB I) . v or F1 /. k = (B2DB I) . v )
;

end;

suppose E1:
F1 /. k <> (B2DB I) . v
; :: thesis: (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 ;

:: thesis: verum

end;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 ;

:: thesis: verum

suppose
F1 /. k = (B2DB I) . v
; :: thesis: (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 ;

:: thesis: verum

end;.= (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 ;

:: thesis: verum

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 ; :: thesis: verum