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

Metamath Proof Explorer

Theorem elfrlmbasn0

Description: If the dimension of a free module over a ring is not 0, every element of its base set is not empty. (Contributed by AV, 10-Feb-2019)

Ref Expression
Hypotheses frlmfibas.f 
|- F = ( R freeLMod I )
frlmfibas.n 
|- N = ( Base ` R )
elfrlmbasn0.b 
|- B = ( Base ` F )
Assertion elfrlmbasn0 
|- ( ( I e. V /\ I =/= (/) ) -> ( X e. B -> X =/= (/) ) )

Proof

Step Hyp Ref Expression
1 frlmfibas.f 
 |-  F = ( R freeLMod I )
2 frlmfibas.n 
 |-  N = ( Base ` R )
3 elfrlmbasn0.b 
 |-  B = ( Base ` F )
4 1 2 3 frlmbasf 
 |-  ( ( I e. V /\ X e. B ) -> X : I --> N )
5 4 ex 
 |-  ( I e. V -> ( X e. B -> X : I --> N ) )
6 f0dom0 
 |-  ( X : I --> N -> ( I = (/) <-> X = (/) ) )
7 6 biimprd 
 |-  ( X : I --> N -> ( X = (/) -> I = (/) ) )
8 7 necon3d 
 |-  ( X : I --> N -> ( I =/= (/) -> X =/= (/) ) )
9 8 com12 
 |-  ( I =/= (/) -> ( X : I --> N -> X =/= (/) ) )
10 5 9 sylan9 
 |-  ( ( I e. V /\ I =/= (/) ) -> ( X e. B -> X =/= (/) ) )