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

for A being Subset of V

for l being Linear_Combination of A

for x being Element of V

for a being Element of R holds l +* (x,a) is Linear_Combination of A \/ {x}

let V be LeftMod of R; :: thesis: for A being Subset of V

for l being Linear_Combination of A

for x being Element of V

for a being Element of R holds l +* (x,a) is Linear_Combination of A \/ {x}

let A be Subset of V; :: thesis: for l being Linear_Combination of A

for x being Element of V

for a being Element of R holds l +* (x,a) is Linear_Combination of A \/ {x}

let l be Linear_Combination of A; :: thesis: for x being Element of V

for a being Element of R holds l +* (x,a) is Linear_Combination of A \/ {x}

let x be Element of V; :: thesis: for a being Element of R holds l +* (x,a) is Linear_Combination of A \/ {x}

let a be Element of R; :: thesis: l +* (x,a) is Linear_Combination of A \/ {x}

set m = l +* (x,a);

A1: dom (l +* (x,a)) = dom l by FUNCT_7:30

.= [#] V by FUNCT_2:def 1 ;

rng (l +* (x,a)) c= the carrier of R ;

then reconsider m = l +* (x,a) as Element of Funcs (([#] V), the carrier of R) by A1, FUNCT_2:def 2;

set T = (Carrier l) \/ {x};

for v being Element of V st not v in (Carrier l) \/ {x} holds

m . v = 0. R

A9: Carrier m c= (Carrier l) \/ {x}

then Carrier m c= A \/ {x} by A9;

hence l +* (x,a) is Linear_Combination of A \/ {x} by VECTSP_6:def 4; :: thesis: verum

for A being Subset of V

for l being Linear_Combination of A

for x being Element of V

for a being Element of R holds l +* (x,a) is Linear_Combination of A \/ {x}

let V be LeftMod of R; :: thesis: for A being Subset of V

for l being Linear_Combination of A

for x being Element of V

for a being Element of R holds l +* (x,a) is Linear_Combination of A \/ {x}

let A be Subset of V; :: thesis: for l being Linear_Combination of A

for x being Element of V

for a being Element of R holds l +* (x,a) is Linear_Combination of A \/ {x}

let l be Linear_Combination of A; :: thesis: for x being Element of V

for a being Element of R holds l +* (x,a) is Linear_Combination of A \/ {x}

let x be Element of V; :: thesis: for a being Element of R holds l +* (x,a) is Linear_Combination of A \/ {x}

let a be Element of R; :: thesis: l +* (x,a) is Linear_Combination of A \/ {x}

set m = l +* (x,a);

A1: dom (l +* (x,a)) = dom l by FUNCT_7:30

.= [#] V by FUNCT_2:def 1 ;

rng (l +* (x,a)) c= the carrier of R ;

then reconsider m = l +* (x,a) as Element of Funcs (([#] V), the carrier of R) by A1, FUNCT_2:def 2;

set T = (Carrier l) \/ {x};

for v being Element of V st not v in (Carrier l) \/ {x} holds

m . v = 0. R

proof

then reconsider m = m as Linear_Combination of V by VECTSP_6:def 1;
let v be Element of V; :: thesis: ( not v in (Carrier l) \/ {x} implies m . v = 0. R )

assume A7: not v in (Carrier l) \/ {x} ; :: thesis: m . v = 0. R

not v in {x} by A7, XBOOLE_0:def 3;

then v <> x by TARSKI:def 1;

then A8: m . v = l . v by FUNCT_7:32;

not v in Carrier l by A7, XBOOLE_0:def 3;

hence m . v = 0. R by A8; :: thesis: verum

end;assume A7: not v in (Carrier l) \/ {x} ; :: thesis: m . v = 0. R

not v in {x} by A7, XBOOLE_0:def 3;

then v <> x by TARSKI:def 1;

then A8: m . v = l . v by FUNCT_7:32;

not v in Carrier l by A7, XBOOLE_0:def 3;

hence m . v = 0. R by A8; :: thesis: verum

A9: Carrier m c= (Carrier l) \/ {x}

proof

(Carrier l) \/ {x} c= A \/ {x}
by XBOOLE_1:9, VECTSP_6:def 4;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Carrier m or y in (Carrier l) \/ {x} )

assume y in Carrier m ; :: thesis: y in (Carrier l) \/ {x}

then consider z being Element of V such that

A10: y = z and

A11: m . z <> 0. R ;

end;assume y in Carrier m ; :: thesis: y in (Carrier l) \/ {x}

then consider z being Element of V such that

A10: y = z and

A11: m . z <> 0. R ;

then Carrier m c= A \/ {x} by A9;

hence l +* (x,a) is Linear_Combination of A \/ {x} by VECTSP_6:def 4; :: thesis: verum