let F be Field; :: thesis: for x being Element of F

for V being VectSp of F

for v being Element of V holds

( x * v = 0. V iff ( x = 0. F or v = 0. V ) )

let x be Element of F; :: thesis: for V being VectSp of F

for v being Element of V holds

( x * v = 0. V iff ( x = 0. F or v = 0. V ) )

let V be VectSp of F; :: thesis: for v being Element of V holds

( x * v = 0. V iff ( x = 0. F or v = 0. V ) )

let v be Element of V; :: thesis: ( x * v = 0. V iff ( x = 0. F or v = 0. V ) )

( not x * v = 0. V or x = 0. F or v = 0. V )

for V being VectSp of F

for v being Element of V holds

( x * v = 0. V iff ( x = 0. F or v = 0. V ) )

let x be Element of F; :: thesis: for V being VectSp of F

for v being Element of V holds

( x * v = 0. V iff ( x = 0. F or v = 0. V ) )

let V be VectSp of F; :: thesis: for v being Element of V holds

( x * v = 0. V iff ( x = 0. F or v = 0. V ) )

let v be Element of V; :: thesis: ( x * v = 0. V iff ( x = 0. F or v = 0. V ) )

( not x * v = 0. V or x = 0. F or v = 0. V )

proof

hence
( x * v = 0. V iff ( x = 0. F or v = 0. V ) )
by Th10; :: thesis: verum
assume
x * v = 0. V
; :: thesis: ( x = 0. F or v = 0. V )

then A1: ((x ") * x) * v = (x ") * (0. V) by Def15

.= 0. V by Th10 ;

assume x <> 0. F ; :: thesis: v = 0. V

then 0. V = (1. F) * v by A1, Def10;

hence v = 0. V by Def16; :: thesis: verum

end;then A1: ((x ") * x) * v = (x ") * (0. V) by Def15

.= 0. V by Th10 ;

assume x <> 0. F ; :: thesis: v = 0. V

then 0. V = (1. F) * v by A1, Def10;

hence v = 0. V by Def16; :: thesis: verum