let K be Ring; :: thesis: for V being LeftMod of K

for A being Subset of V st K is trivial holds

( ( for l being Linear_Combination of A holds Carrier l = {} ) & Lin A is trivial )

let V be LeftMod of K; :: thesis: for A being Subset of V st K is trivial holds

( ( for l being Linear_Combination of A holds Carrier l = {} ) & Lin A is trivial )

let A be Subset of V; :: thesis: ( K is trivial implies ( ( for l being Linear_Combination of A holds Carrier l = {} ) & Lin A is trivial ) )

assume A1: K is trivial ; :: thesis: ( ( for l being Linear_Combination of A holds Carrier l = {} ) & Lin A is trivial )

thus A2: for l being Linear_Combination of A holds Carrier l = {} :: thesis: Lin A is trivial

for A being Subset of V st K is trivial holds

( ( for l being Linear_Combination of A holds Carrier l = {} ) & Lin A is trivial )

let V be LeftMod of K; :: thesis: for A being Subset of V st K is trivial holds

( ( for l being Linear_Combination of A holds Carrier l = {} ) & Lin A is trivial )

let A be Subset of V; :: thesis: ( K is trivial implies ( ( for l being Linear_Combination of A holds Carrier l = {} ) & Lin A is trivial ) )

assume A1: K is trivial ; :: thesis: ( ( for l being Linear_Combination of A holds Carrier l = {} ) & Lin A is trivial )

thus A2: for l being Linear_Combination of A holds Carrier l = {} :: thesis: Lin A is trivial

proof

let l be Linear_Combination of A; :: thesis: Carrier l = {}

assume A3: Carrier l <> {} ; :: thesis: contradiction

set x = the Element of Carrier l;

ex a being Vector of V st

( the Element of Carrier l = a & l . a <> 0. K ) by A3, VECTSP_6:1;

hence contradiction by A1; :: thesis: verum

end;assume A3: Carrier l <> {} ; :: thesis: contradiction

set x = the Element of Carrier l;

ex a being Vector of V st

( the Element of Carrier l = a & l . a <> 0. K ) by A3, VECTSP_6:1;

hence contradiction by A1; :: thesis: verum

now :: thesis: for a being Vector of (Lin A) holds a = 0. (Lin A)

hence
Lin A is trivial
; :: thesis: verumlet a be Vector of (Lin A); :: thesis: a = 0. (Lin A)

a in Lin A ;

then consider l being Linear_Combination of A such that

A4: a = Sum l by MOD_3:4;

Carrier l = {} by A2;

then a = 0. V by A4, VECTSP_6:19;

hence a = 0. (Lin A) by VECTSP_4:11; :: thesis: verum

end;a in Lin A ;

then consider l being Linear_Combination of A such that

A4: a = Sum l by MOD_3:4;

Carrier l = {} by A2;

then a = 0. V by A4, VECTSP_6:19;

hence a = 0. (Lin A) by VECTSP_4:11; :: thesis: verum