assume DualBasis I is linearly-dependent ; :: thesis: contradiction
then consider l being Linear_Combination of DualBasis I such that
B1: ( Sum l = 0. () & Carrier l <> {} ) by VECTSP_7:def 1;
consider u being object such that
B2: u in Carrier l by ;
reconsider u = u as Element of () by B2;
B21: Carrier l c= DualBasis I by VECTSP_6:def 4;
then u in DualBasis I by B2;
then B31: u in rng (B2DB I) by defB2DB;
then u in dom ((B2DB I) ") by FUNCT_1:33;
then ((B2DB I) ") . u in rng ((B2DB I) ") by FUNCT_1:3;
then B4: ((B2DB I) ") . u in dom (B2DB I) by FUNCT_1:33;
then ((B2DB I) ") . u in I ;
then reconsider bu = ((B2DB I) ") . u as Vector of () ;
EMLat L is Submodule of DivisibleMod L by ZMODLAT2:20;
then reconsider bu = bu as Vector of () by ZMODUL01:25;
B5: (ScProductDM L) . (bu,(Sum l)) = SumSc (bu,l) by ThSumScDM1;
B6: Carrier l = (() \ {u}) \/ {u} by ;
B7: ((Carrier l) \ {u}) /\ {u} = {} by ;
l is Linear_Combination of Carrier l by VECTSP_6:7;
then consider l1 being Linear_Combination of () \ {u}, l2 being Linear_Combination of {u} such that
B8: l = l1 + l2 by ;
for x being Vector of () st x in () \ {u} holds
x in Carrier l1
proof
let x be Vector of (); :: thesis: ( x in () \ {u} implies x in Carrier l1 )
assume C1: x in () \ {u} ; :: thesis: x in Carrier l1
x in Carrier l by ;
then C2: l . x <> 0. INT.Ring by VECTSP_6:2;
C3: Carrier l2 c= {u} by VECTSP_6:def 4;
C4: l . x = (l1 . x) + (l2 . x) by ;
not x in Carrier l2 by ;
then l1 . x <> 0. INT.Ring by C2, C4;
hence x in Carrier l1 ; :: thesis: verum
end;
then (Carrier l) \ {u} c= Carrier l1 ;
then B10: Carrier l1 = () \ {u} by VECTSP_6:def 4;
then B11: not u in Carrier l1 by ZFMISC_1:56;
B12: (B2DB I) . bu = u by ;
consider F1 being FinSequence of () such that
B13: ( F1 is one-to-one & rng F1 = Carrier l1 & SumSc (bu,l1) = Sum (ScFS (bu,l1,F1)) ) by defSumScDM;
B14: len F1 = len (ScFS (bu,l1,F1)) by defScFSDM;
for k being Nat st k in dom (ScFS (bu,l1,F1)) holds
(ScFS (bu,l1,F1)) . k = - ((ScFS (bu,l1,F1)) /. k)
proof
let k be Nat; :: thesis: ( k in dom (ScFS (bu,l1,F1)) implies (ScFS (bu,l1,F1)) . k = - ((ScFS (bu,l1,F1)) /. k) )
assume C1: k in dom (ScFS (bu,l1,F1)) ; :: thesis: (ScFS (bu,l1,F1)) . k = - ((ScFS (bu,l1,F1)) /. k)
C2: (ScFS (bu,l1,F1)) . k = () . (bu,((l1 . (F1 /. k)) * (F1 /. k))) by ;
C3: dom (ScFS (bu,l1,F1)) = dom F1 by ;
per cases ( F1 /. k <> (B2DB I) . bu or F1 /. k = (B2DB I) . bu ) ;
suppose D1: F1 /. k <> (B2DB I) . bu ; :: thesis: (ScFS (bu,l1,F1)) . k = - ((ScFS (bu,l1,F1)) /. k)
then F1 /. k <> u by ;
then not F1 /. k in {u} by TARSKI:def 1;
then D2: not F1 /. k in Carrier l2 by ;
l . (F1 /. k) = (l1 . (F1 /. k)) + (l2 . (F1 /. k)) by
.= (l1 . (F1 /. k)) + () by D2
.= l1 . (F1 /. k) ;
then D3: (ScFS (bu,l1,F1)) . k = () . (bu,((l . (F1 /. k)) * (F1 /. k))) by
.= () . (((l . (F1 /. k)) * (F1 /. k)),bu) by ZMODLAT2:6
.= (l . (F1 /. k)) * (() . ((F1 /. k),bu)) by ZMODLAT2:6
.= (l . (F1 /. k)) * (() . (bu,(F1 /. k))) by ZMODLAT2:6 ;
F1 . k in Carrier l1 by ;
then F1 . k in Carrier l by ;
then F1 . k in DualBasis I by B21;
then F1 /. k in DualBasis I by ;
then D7: 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 D6: ((B2DB I) ") . (F1 /. k) in I ;
EMLat L is Submodule of DivisibleMod L by ZMODLAT2:20;
then reconsider bf = ((B2DB I) ") . (F1 /. k) as Vector of () by ;
(B2DB I) . bf = F1 /. k by ;
then (ScFS (bu,l1,F1)) . k = (l . (F1 /. k)) * () by B4, D1, D3, D6, defB2DB
.= 0. F_Real ;
hence (ScFS (bu,l1,F1)) . k = - ((ScFS (bu,l1,F1)) . k)
.= - ((ScFS (bu,l1,F1)) /. k) by ;
:: thesis: verum
end;
suppose F1 /. k = (B2DB I) . bu ; :: thesis: (ScFS (bu,l1,F1)) . k = - ((ScFS (bu,l1,F1)) /. k)
then F1 /. k = u by ;
then (ScFS (bu,l1,F1)) . k = () . (bu,(() * (F1 /. k))) by
.= () . (bu,(0. ())) by VECTSP_1:14
.= 0. F_Real by ZMODLAT2:14 ;
hence (ScFS (bu,l1,F1)) . k = - ((ScFS (bu,l1,F1)) . k)
.= - ((ScFS (bu,l1,F1)) /. k) by ;
:: thesis: verum
end;
end;
end;
then B15: Sum (ScFS (bu,l1,F1)) = - (Sum (ScFS (bu,l1,F1))) by ;
B16: SumSc (bu,l2) = () . (bu,((l2 . u) * u)) by LmSumScDM14
.= () . (((l2 . u) * u),bu) by ZMODLAT2:6
.= (l2 . u) * (() . (u,bu)) by ZMODLAT2:6
.= (l2 . u) * (() . (bu,u)) by ZMODLAT2:6
.= (l2 . u) * 1 by
.= l2 . u ;
B17: l . u = (l1 . u) + (l2 . u) by
.= () + (l2 . u) by B11
.= l2 . u ;
SumSc (bu,l) = (SumSc (bu,l1)) + (SumSc (bu,l2)) by
.= l . u by B13, B15, B16, B17 ;
hence contradiction by B1, B2, B5, VECTSP_6:2, ZMODLAT2:14; :: thesis: verum