let GF be Field; :: thesis: for V being VectSp of GF

for a being Element of GF

for L being Linear_Combination of V st a <> 0. GF holds

Carrier (a * L) = Carrier L

let V be VectSp of GF; :: thesis: for a being Element of GF

for L being Linear_Combination of V st a <> 0. GF holds

Carrier (a * L) = Carrier L

let a be Element of GF; :: thesis: for L being Linear_Combination of V st a <> 0. GF holds

Carrier (a * L) = Carrier L

let L be Linear_Combination of V; :: thesis: ( a <> 0. GF implies Carrier (a * L) = Carrier L )

set T = { u where u is Vector of V : (a * L) . u <> 0. GF } ;

set S = { v where v is Vector of V : L . v <> 0. GF } ;

assume A1: a <> 0. GF ; :: thesis: Carrier (a * L) = Carrier L

{ u where u is Vector of V : (a * L) . u <> 0. GF } = { v where v is Vector of V : L . v <> 0. GF }

for a being Element of GF

for L being Linear_Combination of V st a <> 0. GF holds

Carrier (a * L) = Carrier L

let V be VectSp of GF; :: thesis: for a being Element of GF

for L being Linear_Combination of V st a <> 0. GF holds

Carrier (a * L) = Carrier L

let a be Element of GF; :: thesis: for L being Linear_Combination of V st a <> 0. GF holds

Carrier (a * L) = Carrier L

let L be Linear_Combination of V; :: thesis: ( a <> 0. GF implies Carrier (a * L) = Carrier L )

set T = { u where u is Vector of V : (a * L) . u <> 0. GF } ;

set S = { v where v is Vector of V : L . v <> 0. GF } ;

assume A1: a <> 0. GF ; :: thesis: Carrier (a * L) = Carrier L

{ u where u is Vector of V : (a * L) . u <> 0. GF } = { v where v is Vector of V : L . v <> 0. GF }

proof

hence
Carrier (a * L) = Carrier L
; :: thesis: verum
thus
{ u where u is Vector of V : (a * L) . u <> 0. GF } c= { v where v is Vector of V : L . v <> 0. GF }
:: according to XBOOLE_0:def 10 :: thesis: { v where v is Vector of V : L . v <> 0. GF } c= { u where u is Vector of V : (a * L) . u <> 0. GF }

assume x in { v where v is Vector of V : L . v <> 0. GF } ; :: thesis: x in { u where u is Vector of V : (a * L) . u <> 0. GF }

then consider v being Vector of V such that

A4: x = v and

A5: L . v <> 0. GF ;

(a * L) . v = a * (L . v) by Def9;

then (a * L) . v <> 0. GF by A1, A5, VECTSP_1:12;

hence x in { u where u is Vector of V : (a * L) . u <> 0. GF } by A4; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Vector of V : L . v <> 0. GF } or x in { u where u is Vector of V : (a * L) . u <> 0. GF } )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { u where u is Vector of V : (a * L) . u <> 0. GF } or x in { v where v is Vector of V : L . v <> 0. GF } )

assume x in { u where u is Vector of V : (a * L) . u <> 0. GF } ; :: thesis: x in { v where v is Vector of V : L . v <> 0. GF }

then consider u being Vector of V such that

A2: x = u and

A3: (a * L) . u <> 0. GF ;

(a * L) . u = a * (L . u) by Def9;

then L . u <> 0. GF by A3;

hence x in { v where v is Vector of V : L . v <> 0. GF } by A2; :: thesis: verum

end;assume x in { u where u is Vector of V : (a * L) . u <> 0. GF } ; :: thesis: x in { v where v is Vector of V : L . v <> 0. GF }

then consider u being Vector of V such that

A2: x = u and

A3: (a * L) . u <> 0. GF ;

(a * L) . u = a * (L . u) by Def9;

then L . u <> 0. GF by A3;

hence x in { v where v is Vector of V : L . v <> 0. GF } by A2; :: thesis: verum

assume x in { v where v is Vector of V : L . v <> 0. GF } ; :: thesis: x in { u where u is Vector of V : (a * L) . u <> 0. GF }

then consider v being Vector of V such that

A4: x = v and

A5: L . v <> 0. GF ;

(a * L) . v = a * (L . v) by Def9;

then (a * L) . v <> 0. GF by A1, A5, VECTSP_1:12;

hence x in { u where u is Vector of V : (a * L) . u <> 0. GF } by A4; :: thesis: verum