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₁[ 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₁[x,y] )

proof

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₁[x,y] ) )
assume x in the carrier of (DivisibleMod L) ; :: thesis: ex y being object st
( y in the carrier of INT.Ring & S₁[x,y] )

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

suppose B2: x in DualBasis I ; :: thesis: ex y being object st
( y in the carrier of INT.Ring & S₁[x,y] )

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₁[x,(ScProductDM L) . ((((B2DB I) ") . x),v)] )
thus ( (ScProductDM L) . ((((B2DB I) ") . x),v) in the carrier of INT.Ring & S₁[x,(ScProductDM L) . ((((B2DB I) ") . x),v)] ) by B2, B4, B5, ZMODLAT2:6; :: thesis: verum

end;

suppose not x in DualBasis I ; :: thesis: ex y being object st
( y in the carrier of INT.Ring & S₁[x,y] )

hence ex y being object st
( y in the carrier of INT.Ring & S₁[x,y] ) ; :: thesis: verum

end;

end;

end;

consider l being Function of (DivisibleMod L), the carrier of INT.Ring such that
A3: for x being object st x in the carrier of (DivisibleMod L) holds
S₁[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

proof

for x being Vector of (DivisibleMod L) st not x in DualBasis I holds
not x in Carrier l

proof

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;

hence Carrier l c= DualBasis I ; :: thesis: verum

end;

then A5: l is Linear_Combination of DualBasis I by VECTSP_6:def 4;
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

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)

proof

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

proof

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

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

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;

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;

end;

end;

reconsider bbn = (B2DB I) . bn as Vector of (DivisibleMod L) by B31;

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

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)

proof

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;

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

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;

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;

end;

end;

then C4: Sum (ScFS (bn,l,F)) = - (Sum (ScFS (bn,l,F))) by C3, RLVECT_2:4;
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;

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

proof

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;

then (Carrier l) \ {bbn} c= 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)

proof

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)

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

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;

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;

end;

end;

then C9: Sum (ScFS (bn,l1,F1)) = - (Sum (ScFS (bn,l1,F1))) by C8, RLVECT_2:4;
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;

end;

end;

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

end;

hence v in Lin (DualBasis I) by A5, ZMODLAT2:63, ZMODUL02:64; :: thesis: verum