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 =/= (/) ) )