let K be Ring; :: thesis: for V being LeftMod of K holds
( V is trivial iff ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = (0). V )
let V be LeftMod of K; :: thesis: ( V is trivial iff ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = (0). V )
set X = the carrier of ((0). V);
reconsider W = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) as strict Subspace of V by Th3;
reconsider Z = (0). V as Subspace of W by VECTSP_4:39;
A1: now :: thesis: ( W <> Z implies not V is trivial )
assume W <> Z ; :: thesis: not V is trivial
then consider a being Vector of V such that
A2: not a in Z by VECTSP_4:32;
not a in the carrier of ((0). V) by A2;
then not a in {(0. V)} by VECTSP_4:def 3;
then a <> 0. V by TARSKI:def 1;
hence not V is trivial ; :: thesis: verum
end;
now :: thesis: ( not V is trivial implies W <> (0). V )
assume not V is trivial ; :: thesis: W <> (0). V
then consider a being Vector of V such that
A3: a <> 0. V ;
not a in {(0. V)} by A3, TARSKI:def 1;
then not a in the carrier of ((0). V) by VECTSP_4:def 3;
hence W <> (0). V ; :: thesis: verum
end;
hence ( V is trivial iff ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = (0). V ) by A1; :: thesis: verum