This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lmodbn0

Description: The base set of a left module is nonempty. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypothesis lmodbn0.b 
|- B = ( Base ` W )
Assertion lmodbn0 
|- ( W e. LMod -> B =/= (/) )

Proof

Step Hyp Ref Expression
1 lmodbn0.b 
 |-  B = ( Base ` W )
2 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
3 1 grpbn0 
 |-  ( W e. Grp -> B =/= (/) )
4 2 3 syl 
 |-  ( W e. LMod -> B =/= (/) )