assume
DualBasis I is linearly-dependent
; :: thesis: contradiction

then consider l being Linear_Combination of DualBasis I such that

B1: ( Sum l = 0. (DivisibleMod L) & Carrier l <> {} ) by VECTSP_7:def 1;

consider u being object such that

B2: u in Carrier l by B1, XBOOLE_0:def 1;

reconsider u = u as Element of (DivisibleMod L) 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) ;

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

then reconsider bu = bu as Vector of (DivisibleMod L) by ZMODUL01:25;

B5: (ScProductDM L) . (bu,(Sum l)) = SumSc (bu,l) by ThSumScDM1;

B6: Carrier l = ((Carrier l) \ {u}) \/ {u} by B2, XBOOLE_1:45, ZFMISC_1:31;

B7: ((Carrier l) \ {u}) /\ {u} = {} 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) \ {u}, l2 being Linear_Combination of {u} such that

B8: l = l1 + l2 by B6, B7, ZMODUL04:26;

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

x in Carrier l1

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

then B11: not u in Carrier l1 by ZFMISC_1:56;

B12: (B2DB I) . bu = u by B31, FUNCT_1:35;

consider F1 being FinSequence of (DivisibleMod L) 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)

B16: SumSc (bu,l2) = (ScProductDM L) . (bu,((l2 . u) * u)) by LmSumScDM14

.= (ScProductDM L) . (((l2 . u) * u),bu) by ZMODLAT2:6

.= (l2 . u) * ((ScProductDM L) . (u,bu)) by ZMODLAT2:6

.= (l2 . u) * ((ScProductDM L) . (bu,u)) by ZMODLAT2:6

.= (l2 . u) * 1 by B4, B12, defB2DB

.= l2 . u ;

B17: l . u = (l1 . u) + (l2 . u) by B8, VECTSP_6:22

.= (0. INT.Ring) + (l2 . u) by B11

.= l2 . u ;

SumSc (bu,l) = (SumSc (bu,l1)) + (SumSc (bu,l2)) by B8, LmSumScDM1X

.= l . u by B13, B15, B16, B17 ;

hence contradiction by B1, B2, B5, VECTSP_6:2, ZMODLAT2:14; :: thesis: verum

then consider l being Linear_Combination of DualBasis I such that

B1: ( Sum l = 0. (DivisibleMod L) & Carrier l <> {} ) by VECTSP_7:def 1;

consider u being object such that

B2: u in Carrier l by B1, XBOOLE_0:def 1;

reconsider u = u as Element of (DivisibleMod L) 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) ;

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

then reconsider bu = bu as Vector of (DivisibleMod L) by ZMODUL01:25;

B5: (ScProductDM L) . (bu,(Sum l)) = SumSc (bu,l) by ThSumScDM1;

B6: Carrier l = ((Carrier l) \ {u}) \/ {u} by B2, XBOOLE_1:45, ZFMISC_1:31;

B7: ((Carrier l) \ {u}) /\ {u} = {} 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) \ {u}, l2 being Linear_Combination of {u} such that

B8: l = l1 + l2 by B6, B7, ZMODUL04:26;

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

x in Carrier l1

proof

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

assume C1: x in (Carrier l) \ {u} ; :: thesis: x in Carrier l1

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

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

not x in Carrier l2 by C1, C3, XBOOLE_0:def 5;

then l1 . x <> 0. INT.Ring by C2, C4;

hence x in Carrier l1 ; :: thesis: verum

end;assume C1: x in (Carrier l) \ {u} ; :: thesis: x in Carrier l1

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

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

not x in Carrier l2 by C1, C3, XBOOLE_0:def 5;

then l1 . x <> 0. INT.Ring by C2, C4;

hence x in Carrier l1 ; :: thesis: verum

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

then B11: not u in Carrier l1 by ZFMISC_1:56;

B12: (B2DB I) . bu = u by B31, FUNCT_1:35;

consider F1 being FinSequence of (DivisibleMod L) 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

then B15:
Sum (ScFS (bu,l1,F1)) = - (Sum (ScFS (bu,l1,F1)))
by B14, RLVECT_2:4;
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 = (ScProductDM L) . (bu,((l1 . (F1 /. k)) * (F1 /. k))) by C1, defScFSDM;

C3: dom (ScFS (bu,l1,F1)) = dom F1 by B14, FINSEQ_3:29;

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

C3: dom (ScFS (bu,l1,F1)) = dom F1 by B14, FINSEQ_3:29;

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

end;

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

then
F1 /. k <> u
by B31, FUNCT_1:35;

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

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

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

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

.= l1 . (F1 /. k) ;

then D3: (ScFS (bu,l1,F1)) . k = (ScProductDM L) . (bu,((l . (F1 /. k)) * (F1 /. k))) by C1, defScFSDM

.= (ScProductDM L) . (((l . (F1 /. k)) * (F1 /. k)),bu) by ZMODLAT2:6

.= (l . (F1 /. k)) * ((ScProductDM L) . ((F1 /. k),bu)) by ZMODLAT2:6

.= (l . (F1 /. k)) * ((ScProductDM L) . (bu,(F1 /. k))) by ZMODLAT2:6 ;

F1 . k in Carrier l1 by B13, C1, C3, FUNCT_1:3;

then F1 . k in Carrier l by B10, XBOOLE_0:def 5;

then F1 . k in DualBasis I by B21;

then F1 /. k in DualBasis I by C1, C3, PARTFUN1:def 6;

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 (DivisibleMod L) by D6, ZMODUL01:25;

(B2DB I) . bf = F1 /. k by D7, FUNCT_1:35;

then (ScFS (bu,l1,F1)) . k = (l . (F1 /. k)) * (0. F_Real) 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 C1, PARTFUN1:def 6 ;

:: thesis: verum

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

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

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

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

.= l1 . (F1 /. k) ;

then D3: (ScFS (bu,l1,F1)) . k = (ScProductDM L) . (bu,((l . (F1 /. k)) * (F1 /. k))) by C1, defScFSDM

.= (ScProductDM L) . (((l . (F1 /. k)) * (F1 /. k)),bu) by ZMODLAT2:6

.= (l . (F1 /. k)) * ((ScProductDM L) . ((F1 /. k),bu)) by ZMODLAT2:6

.= (l . (F1 /. k)) * ((ScProductDM L) . (bu,(F1 /. k))) by ZMODLAT2:6 ;

F1 . k in Carrier l1 by B13, C1, C3, FUNCT_1:3;

then F1 . k in Carrier l by B10, XBOOLE_0:def 5;

then F1 . k in DualBasis I by B21;

then F1 /. k in DualBasis I by C1, C3, PARTFUN1:def 6;

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 (DivisibleMod L) by D6, ZMODUL01:25;

(B2DB I) . bf = F1 /. k by D7, FUNCT_1:35;

then (ScFS (bu,l1,F1)) . k = (l . (F1 /. k)) * (0. F_Real) 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 C1, PARTFUN1:def 6 ;

:: thesis: verum

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

then
F1 /. k = u
by B31, FUNCT_1:35;

then (ScFS (bu,l1,F1)) . k = (ScProductDM L) . (bu,((0. INT.Ring) * (F1 /. k))) by B11, C2

.= (ScProductDM L) . (bu,(0. (DivisibleMod L))) 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 C1, PARTFUN1:def 6 ;

:: thesis: verum

end;then (ScFS (bu,l1,F1)) . k = (ScProductDM L) . (bu,((0. INT.Ring) * (F1 /. k))) by B11, C2

.= (ScProductDM L) . (bu,(0. (DivisibleMod L))) 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 C1, PARTFUN1:def 6 ;

:: thesis: verum

B16: SumSc (bu,l2) = (ScProductDM L) . (bu,((l2 . u) * u)) by LmSumScDM14

.= (ScProductDM L) . (((l2 . u) * u),bu) by ZMODLAT2:6

.= (l2 . u) * ((ScProductDM L) . (u,bu)) by ZMODLAT2:6

.= (l2 . u) * ((ScProductDM L) . (bu,u)) by ZMODLAT2:6

.= (l2 . u) * 1 by B4, B12, defB2DB

.= l2 . u ;

B17: l . u = (l1 . u) + (l2 . u) by B8, VECTSP_6:22

.= (0. INT.Ring) + (l2 . u) by B11

.= l2 . u ;

SumSc (bu,l) = (SumSc (bu,l1)) + (SumSc (bu,l2)) by B8, LmSumScDM1X

.= l . u by B13, B15, B16, B17 ;

hence contradiction by B1, B2, B5, VECTSP_6:2, ZMODLAT2:14; :: thesis: verum