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 ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lmodsn0.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
Assertion lmodsn0 ( 𝑊 ∈ LMod → 𝐵 ≠ ∅ )

Proof

Step Hyp Ref Expression
1 lmodsn0.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 lmodsn0.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
3 1 lmodfgrp ⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Grp )
4 2 grpbn0 ⊢ ( 𝐹 ∈ Grp → 𝐵 ≠ ∅ )
5 3 4 syl ⊢ ( 𝑊 ∈ LMod → 𝐵 ≠ ∅ )