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

Metamath Proof Explorer

Theorem lmodsn0

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

Ref Expression
Hypotheses lmodsn0.f ⊢ F = Scalar ⁡ W
lmodsn0.b ⊢ B = Base F
Assertion lmodsn0 ⊢ W ∈ LMod → B ≠ ∅

Proof

Step Hyp Ref Expression
1 lmodsn0.f ⊢ F = Scalar ⁡ W
2 lmodsn0.b ⊢ B = Base F
3 1 lmodfgrp ⊢ W ∈ LMod → F ∈ Grp
4 2 grpbn0 ⊢ F ∈ Grp → B ≠ ∅
5 3 4 syl ⊢ W ∈ LMod → B ≠ ∅