let L be positive-definite RATional Z_Lattice; :: thesis: for I being Basis of (EMLat L)

for v being Vector of (DivisibleMod L) st v is Dual of L holds

v in Lin (DualBasis I)

let I be Basis of (EMLat L); :: thesis: for v being Vector of (DivisibleMod L) st v is Dual of L holds

v in Lin (DualBasis I)

let v be Vector of (DivisibleMod L); :: thesis: ( v is Dual of L implies v in Lin (DualBasis I) )

assume A1: v is Dual of L ; :: thesis: v in Lin (DualBasis I)

set f = (B2DB I) " ;

defpred S_{1}[ object , object ] means ( ( $1 in DualBasis I implies $2 = (ScProductDM L) . ((((B2DB I) ") . $1),v) ) & ( not $1 in DualBasis I implies $2 = 0. INT.Ring ) );

A2: for x being object st x in the carrier of (DivisibleMod L) holds

ex y being object st

( y in the carrier of INT.Ring & S_{1}[x,y] )

A3: for x being object st x in the carrier of (DivisibleMod L) holds

S_{1}[x,l . x]
from FUNCT_2:sch 1(A2);

reconsider l = l as Element of Funcs ( the carrier of (DivisibleMod L), the carrier of INT.Ring) by FUNCT_2:8;

for v being Vector of (DivisibleMod L) st not v in DualBasis I holds

l . v = 0. INT.Ring by A3;

then reconsider l = l as Linear_Combination of DivisibleMod L by VECTSP_6:def 1;

Carrier l c= DualBasis I

consider b being FinSequence such that

A6: ( rng b = I & b is one-to-one ) by FINSEQ_4:58;

b is FinSequence of (EMLat L) by A6, FINSEQ_1:def 4;

then reconsider b = b as OrdBasis of EMLat L by A6, ZMATRLIN:def 5;

for n being Nat st n in dom b holds

(ScProductDM L) . ((b /. n),v) = (ScProductDM L) . ((b /. n),(Sum l))

for v being Vector of (DivisibleMod L) st v is Dual of L holds

v in Lin (DualBasis I)

let I be Basis of (EMLat L); :: thesis: for v being Vector of (DivisibleMod L) st v is Dual of L holds

v in Lin (DualBasis I)

let v be Vector of (DivisibleMod L); :: thesis: ( v is Dual of L implies v in Lin (DualBasis I) )

assume A1: v is Dual of L ; :: thesis: v in Lin (DualBasis I)

set f = (B2DB I) " ;

defpred S

A2: for x being object st x in the carrier of (DivisibleMod L) holds

ex y being object st

( y in the carrier of INT.Ring & S

proof

consider l being Function of (DivisibleMod L), the carrier of INT.Ring such that
let x be object ; :: thesis: ( x in the carrier of (DivisibleMod L) implies ex y being object st

( y in the carrier of INT.Ring & S_{1}[x,y] ) )

assume x in the carrier of (DivisibleMod L) ; :: thesis: ex y being object st

( y in the carrier of INT.Ring & S_{1}[x,y] )

end;( y in the carrier of INT.Ring & S

assume x in the carrier of (DivisibleMod L) ; :: thesis: ex y being object st

( y in the carrier of INT.Ring & S

per cases
( x in DualBasis I or not x in DualBasis I )
;

end;

suppose B2:
x in DualBasis I
; :: thesis: ex y being object st

( y in the carrier of INT.Ring & S_{1}[x,y] )

( y in the carrier of INT.Ring & S

then
x in rng (B2DB I)
by defB2DB;

then x in dom ((B2DB I) ") by FUNCT_1:33;

then ((B2DB I) ") . x in rng ((B2DB I) ") by FUNCT_1:3;

then ((B2DB I) ") . x in dom (B2DB I) by FUNCT_1:33;

then ((B2DB I) ") . x in I ;

then ((B2DB I) ") . x in EMLat L ;

then ((B2DB I) ") . x in rng (MorphsZQ L) by ZMODLAT2:def 4;

then B3: ((B2DB I) ") . x in EMbedding L by ZMODUL08:def 3;

EMbedding L is Submodule of DivisibleMod L by ZMODUL08:24;

then B4: ((B2DB I) ") . x is Vector of (DivisibleMod L) by B3, ZMODUL01:25;

then B5: (ScProductDM L) . (v,(((B2DB I) ") . x)) in INT.Ring by A1, B3, defDualElement;

take (ScProductDM L) . ((((B2DB I) ") . x),v) ; :: thesis: ( (ScProductDM L) . ((((B2DB I) ") . x),v) in the carrier of INT.Ring & S_{1}[x,(ScProductDM L) . ((((B2DB I) ") . x),v)] )

thus ( (ScProductDM L) . ((((B2DB I) ") . x),v) in the carrier of INT.Ring & S_{1}[x,(ScProductDM L) . ((((B2DB I) ") . x),v)] )
by B2, B4, B5, ZMODLAT2:6; :: thesis: verum

end;then x in dom ((B2DB I) ") by FUNCT_1:33;

then ((B2DB I) ") . x in rng ((B2DB I) ") by FUNCT_1:3;

then ((B2DB I) ") . x in dom (B2DB I) by FUNCT_1:33;

then ((B2DB I) ") . x in I ;

then ((B2DB I) ") . x in EMLat L ;

then ((B2DB I) ") . x in rng (MorphsZQ L) by ZMODLAT2:def 4;

then B3: ((B2DB I) ") . x in EMbedding L by ZMODUL08:def 3;

EMbedding L is Submodule of DivisibleMod L by ZMODUL08:24;

then B4: ((B2DB I) ") . x is Vector of (DivisibleMod L) by B3, ZMODUL01:25;

then B5: (ScProductDM L) . (v,(((B2DB I) ") . x)) in INT.Ring by A1, B3, defDualElement;

take (ScProductDM L) . ((((B2DB I) ") . x),v) ; :: thesis: ( (ScProductDM L) . ((((B2DB I) ") . x),v) in the carrier of INT.Ring & S

thus ( (ScProductDM L) . ((((B2DB I) ") . x),v) in the carrier of INT.Ring & S

A3: for x being object st x in the carrier of (DivisibleMod L) holds

S

reconsider l = l as Element of Funcs ( the carrier of (DivisibleMod L), the carrier of INT.Ring) by FUNCT_2:8;

for v being Vector of (DivisibleMod L) st not v in DualBasis I holds

l . v = 0. INT.Ring by A3;

then reconsider l = l as Linear_Combination of DivisibleMod L by VECTSP_6:def 1;

Carrier l c= DualBasis I

proof

then A5:
l is Linear_Combination of DualBasis I
by VECTSP_6:def 4;
for x being Vector of (DivisibleMod L) st not x in DualBasis I holds

not x in Carrier l

end;not x in Carrier l

proof

hence
Carrier l c= DualBasis I
; :: thesis: verum
let x be Vector of (DivisibleMod L); :: thesis: ( not x in DualBasis I implies not x in Carrier l )

assume B1: not x in DualBasis I ; :: thesis: not x in Carrier l

l . x = 0. INT.Ring by A3, B1;

hence not x in Carrier l by VECTSP_6:2; :: thesis: verum

end;assume B1: not x in DualBasis I ; :: thesis: not x in Carrier l

l . x = 0. INT.Ring by A3, B1;

hence not x in Carrier l by VECTSP_6:2; :: thesis: verum

consider b being FinSequence such that

A6: ( rng b = I & b is one-to-one ) by FINSEQ_4:58;

b is FinSequence of (EMLat L) by A6, FINSEQ_1:def 4;

then reconsider b = b as OrdBasis of EMLat L by A6, ZMATRLIN:def 5;

for n being Nat st n in dom b holds

(ScProductDM L) . ((b /. n),v) = (ScProductDM L) . ((b /. n),(Sum l))

proof

hence
v in Lin (DualBasis I)
by A5, ZMODLAT2:63, ZMODUL02:64; :: thesis: verum
let n be Nat; :: thesis: ( n in dom b implies (ScProductDM L) . ((b /. n),v) = (ScProductDM L) . ((b /. n),(Sum l)) )

assume B1: n in dom b ; :: thesis: (ScProductDM L) . ((b /. n),v) = (ScProductDM L) . ((b /. n),(Sum l))

EMLat L is Submodule of DivisibleMod L by ZMODLAT2:20;

then reconsider bn = b /. n as Vector of (DivisibleMod L) by ZMODUL01:25;

(ScProductDM L) . (bn,v) = SumSc (bn,l)

end;assume B1: n in dom b ; :: thesis: (ScProductDM L) . ((b /. n),v) = (ScProductDM L) . ((b /. n),(Sum l))

EMLat L is Submodule of DivisibleMod L by ZMODLAT2:20;

then reconsider bn = b /. n as Vector of (DivisibleMod L) by ZMODUL01:25;

(ScProductDM L) . (bn,v) = SumSc (bn,l)

proof

hence
(ScProductDM L) . ((b /. n),v) = (ScProductDM L) . ((b /. n),(Sum l))
by ThSumScDM1; :: thesis: verum
b . n in rng b
by B1, FUNCT_1:3;

then B2: bn in I by A6, B1, PARTFUN1:def 6;

then B5: bn in dom (B2DB I) by defB2DB;

then B3: (B2DB I) . bn in rng (B2DB I) by FUNCT_1:3;

then B31: (B2DB I) . bn in DualBasis I ;

B4: for v being Vector of (DivisibleMod L) st v <> (B2DB I) . bn holds

(ScProductDM L) . (bn,((l . v) * v)) = 0. F_Real

end;then B2: bn in I by A6, B1, PARTFUN1:def 6;

then B5: bn in dom (B2DB I) by defB2DB;

then B3: (B2DB I) . bn in rng (B2DB I) by FUNCT_1:3;

then B31: (B2DB I) . bn in DualBasis I ;

B4: for v being Vector of (DivisibleMod L) st v <> (B2DB I) . bn holds

(ScProductDM L) . (bn,((l . v) * v)) = 0. F_Real

proof

reconsider bbn = (B2DB I) . bn as Vector of (DivisibleMod L) by B31;
let v be Vector of (DivisibleMod L); :: thesis: ( v <> (B2DB I) . bn implies (ScProductDM L) . (bn,((l . v) * v)) = 0. F_Real )

assume C1: v <> (B2DB I) . bn ; :: thesis: (ScProductDM L) . (bn,((l . v) * v)) = 0. F_Real

end;assume C1: v <> (B2DB I) . bn ; :: thesis: (ScProductDM L) . (bn,((l . v) * v)) = 0. F_Real

per cases
( not v in DualBasis I or v in DualBasis I )
;

end;

suppose
not v in DualBasis I
; :: thesis: (ScProductDM L) . (bn,((l . v) * v)) = 0. F_Real

then
l . v = 0. INT.Ring
by A3;

then (l . v) * v = 0. (DivisibleMod L) by VECTSP_1:14;

hence (ScProductDM L) . (bn,((l . v) * v)) = 0. F_Real by ZMODLAT2:14; :: thesis: verum

end;then (l . v) * v = 0. (DivisibleMod L) by VECTSP_1:14;

hence (ScProductDM L) . (bn,((l . v) * v)) = 0. F_Real by ZMODLAT2:14; :: thesis: verum

suppose
v in DualBasis I
; :: thesis: (ScProductDM L) . (bn,((l . v) * v)) = 0. F_Real

then C21:
v in rng (B2DB I)
by defB2DB;

then C0: (B2DB I) . (((B2DB I) ") . v) = v by FUNCT_1:35;

v in dom ((B2DB I) ") by C21, FUNCT_1:33;

then ((B2DB I) ") . v in rng ((B2DB I) ") by FUNCT_1:3;

then ((B2DB I) ") . v in dom (B2DB I) by FUNCT_1:33;

then ((B2DB I) ") . v in I ;

then (ScProductDM L) . (bn,v) = 0. F_Real by B2, C0, C1, defB2DB;

then (l . v) * ((ScProductDM L) . (bn,v)) = 0. F_Real ;

hence (ScProductDM L) . (bn,((l . v) * v)) = 0. F_Real by ZMODLAT2:13; :: thesis: verum

end;then C0: (B2DB I) . (((B2DB I) ") . v) = v by FUNCT_1:35;

v in dom ((B2DB I) ") by C21, FUNCT_1:33;

then ((B2DB I) ") . v in rng ((B2DB I) ") by FUNCT_1:3;

then ((B2DB I) ") . v in dom (B2DB I) by FUNCT_1:33;

then ((B2DB I) ") . v in I ;

then (ScProductDM L) . (bn,v) = 0. F_Real by B2, C0, C1, defB2DB;

then (l . v) * ((ScProductDM L) . (bn,v)) = 0. F_Real ;

hence (ScProductDM L) . (bn,((l . v) * v)) = 0. F_Real by ZMODLAT2:13; :: thesis: verum

per cases
( not (B2DB I) . bn in Carrier l or (B2DB I) . bn in Carrier l )
;

end;

suppose C1:
not (B2DB I) . bn in Carrier l
; :: thesis: (ScProductDM L) . (bn,v) = SumSc (bn,l)

consider F being FinSequence of (DivisibleMod L) such that

C2: ( F is one-to-one & rng F = Carrier l & SumSc (bn,l) = Sum (ScFS (bn,l,F)) ) by defSumScDM;

C3: len F = len (ScFS (bn,l,F)) by defScFSDM;

for k being Nat st k in dom (ScFS (bn,l,F)) holds

(ScFS (bn,l,F)) . k = - ((ScFS (bn,l,F)) /. k)

l . ((B2DB I) . bn) = (ScProductDM L) . ((((B2DB I) ") . ((B2DB I) . bn)),v) by A3, B31;

then (ScProductDM L) . ((((B2DB I) ") . bbn),v) = 0. INT.Ring by C1;

hence (ScProductDM L) . (bn,v) = SumSc (bn,l) by B5, C2, C4, FUNCT_1:34; :: thesis: verum

end;C2: ( F is one-to-one & rng F = Carrier l & SumSc (bn,l) = Sum (ScFS (bn,l,F)) ) by defSumScDM;

C3: len F = len (ScFS (bn,l,F)) by defScFSDM;

for k being Nat st k in dom (ScFS (bn,l,F)) holds

(ScFS (bn,l,F)) . k = - ((ScFS (bn,l,F)) /. k)

proof

then C4:
Sum (ScFS (bn,l,F)) = - (Sum (ScFS (bn,l,F)))
by C3, RLVECT_2:4;
let k be Nat; :: thesis: ( k in dom (ScFS (bn,l,F)) implies (ScFS (bn,l,F)) . k = - ((ScFS (bn,l,F)) /. k) )

assume D1: k in dom (ScFS (bn,l,F)) ; :: thesis: (ScFS (bn,l,F)) . k = - ((ScFS (bn,l,F)) /. k)

D2: (ScFS (bn,l,F)) . k = (ScProductDM L) . (bn,((l . (F /. k)) * (F /. k))) by D1, defScFSDM;

end;assume D1: k in dom (ScFS (bn,l,F)) ; :: thesis: (ScFS (bn,l,F)) . k = - ((ScFS (bn,l,F)) /. k)

D2: (ScFS (bn,l,F)) . k = (ScProductDM L) . (bn,((l . (F /. k)) * (F /. k))) by D1, defScFSDM;

per cases
( F /. k <> (B2DB I) . bn or F /. k = (B2DB I) . bn )
;

end;

suppose
F /. k <> (B2DB I) . bn
; :: thesis: (ScFS (bn,l,F)) . k = - ((ScFS (bn,l,F)) /. k)

then
(ScFS (bn,l,F)) . k = 0. F_Real
by B4, D2;

hence (ScFS (bn,l,F)) . k = - ((ScFS (bn,l,F)) . k)

.= - ((ScFS (bn,l,F)) /. k) by D1, PARTFUN1:def 6 ;

:: thesis: verum

end;hence (ScFS (bn,l,F)) . k = - ((ScFS (bn,l,F)) . k)

.= - ((ScFS (bn,l,F)) /. k) by D1, PARTFUN1:def 6 ;

:: thesis: verum

suppose
F /. k = (B2DB I) . bn
; :: thesis: (ScFS (bn,l,F)) . k = - ((ScFS (bn,l,F)) /. k)

then (ScFS (bn,l,F)) . k =
(ScProductDM L) . (bn,((0. INT.Ring) * (F /. k)))
by C1, D2

.= (ScProductDM L) . (bn,(0. (DivisibleMod L))) by VECTSP_1:14

.= 0. F_Real by ZMODLAT2:14 ;

hence (ScFS (bn,l,F)) . k = - ((ScFS (bn,l,F)) . k)

.= - ((ScFS (bn,l,F)) /. k) by D1, PARTFUN1:def 6 ;

:: thesis: verum

end;.= (ScProductDM L) . (bn,(0. (DivisibleMod L))) by VECTSP_1:14

.= 0. F_Real by ZMODLAT2:14 ;

hence (ScFS (bn,l,F)) . k = - ((ScFS (bn,l,F)) . k)

.= - ((ScFS (bn,l,F)) /. k) by D1, PARTFUN1:def 6 ;

:: thesis: verum

l . ((B2DB I) . bn) = (ScProductDM L) . ((((B2DB I) ") . ((B2DB I) . bn)),v) by A3, B31;

then (ScProductDM L) . ((((B2DB I) ") . bbn),v) = 0. INT.Ring by C1;

hence (ScProductDM L) . (bn,v) = SumSc (bn,l) by B5, C2, C4, FUNCT_1:34; :: thesis: verum

suppose
(B2DB I) . bn in Carrier l
; :: thesis: (ScProductDM L) . (bn,v) = SumSc (bn,l)

then C2:
Carrier l = ((Carrier l) \ {((B2DB I) . bn)}) \/ {((B2DB I) . bn)}
by XBOOLE_1:45, ZFMISC_1:31;

C3: ((Carrier l) \ {((B2DB I) . bn)}) /\ {((B2DB I) . bn)} = {} 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) \ {bbn}, l2 being Linear_Combination of {bbn} such that

C4: l = l1 + l2 by C2, C3, ZMODUL04:26;

for x being Vector of (DivisibleMod L) st x in (Carrier l) \ {bbn} holds

x in Carrier l1

then Carrier l1 = (Carrier l) \ {bbn} by VECTSP_6:def 4;

then C12: not bbn in Carrier l1 by ZFMISC_1:56;

consider F1 being FinSequence of (DivisibleMod L) such that

C7: ( F1 is one-to-one & rng F1 = Carrier l1 & SumSc (bn,l1) = Sum (ScFS (bn,l1,F1)) ) by defSumScDM;

C8: len F1 = len (ScFS (bn,l1,F1)) by defScFSDM;

for k being Nat st k in dom (ScFS (bn,l1,F1)) holds

(ScFS (bn,l1,F1)) . k = - ((ScFS (bn,l1,F1)) /. k)

C10: SumSc (bn,l2) = (ScProductDM L) . (bn,((l2 . bbn) * bbn)) by LmSumScDM14

.= (l2 . bbn) * ((ScProductDM L) . (bn,bbn)) by ZMODLAT2:13

.= (l2 . bbn) * 1 by B2, defB2DB

.= l2 . bbn ;

l . bbn = (l1 . bbn) + (l2 . bbn) by C4, VECTSP_6:22

.= (0. INT.Ring) + (l2 . bbn) by C12

.= l2 . bbn ;

then C11: SumSc (bn,l2) = (ScProductDM L) . ((((B2DB I) ") . bbn),v) by A3, B3, C10

.= (ScProductDM L) . (bn,v) by B5, FUNCT_1:34 ;

thus SumSc (bn,l) = (SumSc (bn,l1)) + (SumSc (bn,l2)) by C4, LmSumScDM1X

.= (ScProductDM L) . (bn,v) by C7, C9, C11 ; :: thesis: verum

end;C3: ((Carrier l) \ {((B2DB I) . bn)}) /\ {((B2DB I) . bn)} = {} 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) \ {bbn}, l2 being Linear_Combination of {bbn} such that

C4: l = l1 + l2 by C2, C3, ZMODUL04:26;

for x being Vector of (DivisibleMod L) st x in (Carrier l) \ {bbn} holds

x in Carrier l1

proof

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

assume D1: x in (Carrier l) \ {bbn} ; :: 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= {bbn} 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) \ {bbn} ; :: 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= {bbn} 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 Carrier l1 = (Carrier l) \ {bbn} by VECTSP_6:def 4;

then C12: not bbn in Carrier l1 by ZFMISC_1:56;

consider F1 being FinSequence of (DivisibleMod L) such that

C7: ( F1 is one-to-one & rng F1 = Carrier l1 & SumSc (bn,l1) = Sum (ScFS (bn,l1,F1)) ) by defSumScDM;

C8: len F1 = len (ScFS (bn,l1,F1)) by defScFSDM;

for k being Nat st k in dom (ScFS (bn,l1,F1)) holds

(ScFS (bn,l1,F1)) . k = - ((ScFS (bn,l1,F1)) /. k)

proof

then C9:
Sum (ScFS (bn,l1,F1)) = - (Sum (ScFS (bn,l1,F1)))
by C8, RLVECT_2:4;
let k be Nat; :: thesis: ( k in dom (ScFS (bn,l1,F1)) implies (ScFS (bn,l1,F1)) . k = - ((ScFS (bn,l1,F1)) /. k) )

assume D1: k in dom (ScFS (bn,l1,F1)) ; :: thesis: (ScFS (bn,l1,F1)) . k = - ((ScFS (bn,l1,F1)) /. k)

end;assume D1: k in dom (ScFS (bn,l1,F1)) ; :: thesis: (ScFS (bn,l1,F1)) . k = - ((ScFS (bn,l1,F1)) /. k)

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

end;

suppose E1:
F1 /. k <> (B2DB I) . bn
; :: thesis: (ScFS (bn,l1,F1)) . k = - ((ScFS (bn,l1,F1)) /. k)

then
not F1 /. k in {bbn}
by TARSKI:def 1;

then E2: not F1 /. k in Carrier l2 by TARSKI:def 3, VECTSP_6:def 4;

l . (F1 /. k) = (l1 . (F1 /. k)) + (l2 . (F1 /. k)) by C4, VECTSP_6:22

.= (l1 . (F1 /. k)) + (0. INT.Ring) by E2

.= l1 . (F1 /. k) ;

then (ScFS (bn,l1,F1)) . k = (ScProductDM L) . (bn,((l . (F1 /. k)) * (F1 /. k))) by D1, defScFSDM

.= 0. F_Real by B4, E1 ;

hence (ScFS (bn,l1,F1)) . k = - ((ScFS (bn,l1,F1)) . k)

.= - ((ScFS (bn,l1,F1)) /. k) by D1, PARTFUN1:def 6 ;

:: thesis: verum

end;then E2: not F1 /. k in Carrier l2 by TARSKI:def 3, VECTSP_6:def 4;

l . (F1 /. k) = (l1 . (F1 /. k)) + (l2 . (F1 /. k)) by C4, VECTSP_6:22

.= (l1 . (F1 /. k)) + (0. INT.Ring) by E2

.= l1 . (F1 /. k) ;

then (ScFS (bn,l1,F1)) . k = (ScProductDM L) . (bn,((l . (F1 /. k)) * (F1 /. k))) by D1, defScFSDM

.= 0. F_Real by B4, E1 ;

hence (ScFS (bn,l1,F1)) . k = - ((ScFS (bn,l1,F1)) . k)

.= - ((ScFS (bn,l1,F1)) /. k) by D1, PARTFUN1:def 6 ;

:: thesis: verum

suppose
F1 /. k = (B2DB I) . bn
; :: thesis: (ScFS (bn,l1,F1)) . k = - ((ScFS (bn,l1,F1)) /. k)

then
l1 . (F1 /. k) = 0. INT.Ring
by C12;

then (ScFS (bn,l1,F1)) . k = (ScProductDM L) . (bn,((0. INT.Ring) * (F1 /. k))) by D1, defScFSDM

.= (ScProductDM L) . (bn,(0. (DivisibleMod L))) by VECTSP_1:14

.= 0. F_Real by ZMODLAT2:14 ;

hence (ScFS (bn,l1,F1)) . k = - ((ScFS (bn,l1,F1)) . k)

.= - ((ScFS (bn,l1,F1)) /. k) by D1, PARTFUN1:def 6 ;

:: thesis: verum

end;then (ScFS (bn,l1,F1)) . k = (ScProductDM L) . (bn,((0. INT.Ring) * (F1 /. k))) by D1, defScFSDM

.= (ScProductDM L) . (bn,(0. (DivisibleMod L))) by VECTSP_1:14

.= 0. F_Real by ZMODLAT2:14 ;

hence (ScFS (bn,l1,F1)) . k = - ((ScFS (bn,l1,F1)) . k)

.= - ((ScFS (bn,l1,F1)) /. k) by D1, PARTFUN1:def 6 ;

:: thesis: verum

C10: SumSc (bn,l2) = (ScProductDM L) . (bn,((l2 . bbn) * bbn)) by LmSumScDM14

.= (l2 . bbn) * ((ScProductDM L) . (bn,bbn)) by ZMODLAT2:13

.= (l2 . bbn) * 1 by B2, defB2DB

.= l2 . bbn ;

l . bbn = (l1 . bbn) + (l2 . bbn) by C4, VECTSP_6:22

.= (0. INT.Ring) + (l2 . bbn) by C12

.= l2 . bbn ;

then C11: SumSc (bn,l2) = (ScProductDM L) . ((((B2DB I) ") . bbn),v) by A3, B3, C10

.= (ScProductDM L) . (bn,v) by B5, FUNCT_1:34 ;

thus SumSc (bn,l) = (SumSc (bn,l1)) + (SumSc (bn,l2)) by C4, LmSumScDM1X

.= (ScProductDM L) . (bn,v) by C7, C9, C11 ; :: thesis: verum