let L be positive-definite RATional Z_Lattice; :: thesis: for I being Basis of ()
for v being Vector of () st v is Dual of L holds
v in Lin ()

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

let v be Vector of (); :: thesis: ( v is Dual of L implies v in Lin () )
assume A1: v is Dual of L ; :: thesis: v in Lin ()
set f = (B2DB I) " ;
defpred S1[ object , object ] means ( ( \$1 in DualBasis I implies \$2 = () . ((((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 () holds
ex y being object st
( y in the carrier of INT.Ring & S1[x,y] )
proof
let x be object ; :: thesis: ( x in the carrier of () implies ex y being object st
( y in the carrier of INT.Ring & S1[x,y] ) )

assume x in the carrier of () ; :: thesis: ex y being object st
( y in the carrier of INT.Ring & S1[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 & S1[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 () 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 () by ;
then B5: (ScProductDM L) . (v,(((B2DB I) ") . x)) in INT.Ring by ;
take () . ((((B2DB I) ") . x),v) ; :: thesis: ( () . ((((B2DB I) ") . x),v) in the carrier of INT.Ring & S1[x,() . ((((B2DB I) ") . x),v)] )
thus ( (ScProductDM L) . ((((B2DB I) ") . x),v) in the carrier of INT.Ring & S1[x,() . ((((B2DB I) ") . x),v)] ) by ; :: thesis: verum
end;
suppose not x in DualBasis I ; :: thesis: ex y being object st
( y in the carrier of INT.Ring & S1[x,y] )

hence ex y being object st
( y in the carrier of INT.Ring & S1[x,y] ) ; :: thesis: verum
end;
end;
end;
consider l being Function of (), the carrier of INT.Ring such that
A3: for x being object st x in the carrier of () holds
S1[x,l . x] from reconsider l = l as Element of Funcs ( the carrier of (), the carrier of INT.Ring) by FUNCT_2:8;
for v being Vector of () 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 () st not x in DualBasis I holds
not x in Carrier l
proof
let x be Vector of (); :: 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 () by ;
then reconsider b = b as OrdBasis of EMLat L by ;
for n being Nat st n in dom b holds
() . ((b /. n),v) = () . ((b /. n),(Sum l))
proof
let n be Nat; :: thesis: ( n in dom b implies () . ((b /. n),v) = () . ((b /. n),(Sum l)) )
assume B1: n in dom b ; :: thesis: () . ((b /. n),v) = () . ((b /. n),(Sum l))
EMLat L is Submodule of DivisibleMod L by ZMODLAT2:20;
then reconsider bn = b /. n as Vector of () by ZMODUL01:25;
(ScProductDM L) . (bn,v) = SumSc (bn,l)
proof
b . n in rng b by ;
then B2: bn in I by ;
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 () st v <> (B2DB I) . bn holds
() . (bn,((l . v) * v)) = 0. F_Real
proof
let v be Vector of (); :: thesis: ( v <> (B2DB I) . bn implies () . (bn,((l . v) * v)) = 0. F_Real )
assume C1: v <> (B2DB I) . bn ; :: thesis: () . (bn,((l . v) * v)) = 0. F_Real
per cases ;
suppose not v in DualBasis I ; :: thesis: () . (bn,((l . v) * v)) = 0. F_Real
then l . v = 0. INT.Ring by A3;
then (l . v) * v = 0. () 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: () . (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 ;
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 ;
then (l . v) * (() . (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 () by B31;
per cases ) . bn in Carrier l or (B2DB I) . bn in Carrier l ) ;
suppose C1: not (B2DB I) . bn in Carrier l ; :: thesis: () . (bn,v) = SumSc (bn,l)
consider F being FinSequence of () 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 = () . (bn,((l . (F /. k)) * (F /. k))) by ;
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 ;
:: 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 = () . (bn,(() * (F /. k))) by C1, D2
.= () . (bn,(0. ())) 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 ;
:: thesis: verum
end;
end;
end;
then C4: Sum (ScFS (bn,l,F)) = - (Sum (ScFS (bn,l,F))) by ;
l . ((B2DB I) . bn) = () . ((((B2DB I) ") . ((B2DB I) . bn)),v) by ;
then (ScProductDM L) . ((((B2DB I) ") . bbn),v) = 0. INT.Ring by C1;
hence (ScProductDM L) . (bn,v) = SumSc (bn,l) by ; :: thesis: verum
end;
suppose (B2DB I) . bn in Carrier l ; :: thesis: () . (bn,v) = SumSc (bn,l)
then C2: Carrier l = (() \ {((B2DB I) . bn)}) \/ {((B2DB I) . bn)} by ;
C3: ((Carrier l) \ {((B2DB I) . bn)}) /\ {((B2DB I) . bn)} = {} by ;
l is Linear_Combination of Carrier l by VECTSP_6:7;
then consider l1 being Linear_Combination of () \ {bbn}, l2 being Linear_Combination of {bbn} such that
C4: l = l1 + l2 by ;
for x being Vector of () st x in () \ {bbn} holds
x in Carrier l1
proof
let x be Vector of (); :: thesis: ( x in () \ {bbn} implies x in Carrier l1 )
assume D1: x in () \ {bbn} ; :: 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= {bbn} 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) \ {bbn} c= Carrier l1 ;
then Carrier l1 = () \ {bbn} by VECTSP_6:def 4;
then C12: not bbn in Carrier l1 by ZFMISC_1:56;
consider F1 being FinSequence of () 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 ;
l . (F1 /. k) = (l1 . (F1 /. k)) + (l2 . (F1 /. k)) by
.= (l1 . (F1 /. k)) + () by E2
.= l1 . (F1 /. k) ;
then (ScFS (bn,l1,F1)) . k = () . (bn,((l . (F1 /. k)) * (F1 /. k))) by
.= 0. F_Real by B4, E1 ;
hence (ScFS (bn,l1,F1)) . k = - ((ScFS (bn,l1,F1)) . k)
.= - ((ScFS (bn,l1,F1)) /. k) by ;
:: 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 = () . (bn,(() * (F1 /. k))) by
.= () . (bn,(0. ())) 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 ;
:: thesis: verum
end;
end;
end;
then C9: Sum (ScFS (bn,l1,F1)) = - (Sum (ScFS (bn,l1,F1))) by ;
C10: SumSc (bn,l2) = () . (bn,((l2 . bbn) * bbn)) by LmSumScDM14
.= (l2 . bbn) * (() . (bn,bbn)) by ZMODLAT2:13
.= (l2 . bbn) * 1 by
.= l2 . bbn ;
l . bbn = (l1 . bbn) + (l2 . bbn) by
.= () + (l2 . bbn) by C12
.= l2 . bbn ;
then C11: SumSc (bn,l2) = () . ((((B2DB I) ") . bbn),v) by A3, B3, C10
.= () . (bn,v) by ;
thus SumSc (bn,l) = (SumSc (bn,l1)) + (SumSc (bn,l2)) by
.= () . (bn,v) by C7, C9, C11 ; :: thesis: verum
end;
end;
end;
hence (ScProductDM L) . ((b /. n),v) = () . ((b /. n),(Sum l)) by ThSumScDM1; :: thesis: verum
end;
hence v in Lin () by ; :: thesis: verum