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\mathrm{freeLMod}I$$
	frlmfibas.n	$$⊢N={\mathrm{Base}}_R$$
	elfrlmbasn0.b	$$⊢B={\mathrm{Base}}_F$$
Assertion	elfrlmbasn0	$$⊢\left(I\in V\wedge I\ne \varnothing \right)\to \left(X\in B\to X\ne \varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		frlmfibas.f	$$⊢F=R\mathrm{freeLMod}I$$
2		frlmfibas.n	$$⊢N={\mathrm{Base}}_R$$
3		elfrlmbasn0.b	$$⊢B={\mathrm{Base}}_F$$
4	1 2 3	frlmbasf	$$⊢\left(I\in V\wedge X\in B\right)\to X:I⟶N$$
5	4	ex	$$⊢I\in V\to \left(X\in B\to X:I⟶N\right)$$
6		f0dom0	$$⊢X:I⟶N\to \left(I=\varnothing \leftrightarrow X=\varnothing \right)$$
7	6	biimprd	$$⊢X:I⟶N\to \left(X=\varnothing \to I=\varnothing \right)$$
8	7	necon3d	$$⊢X:I⟶N\to \left(I\ne \varnothing \to X\ne \varnothing \right)$$
9	8	com12	$$⊢I\ne \varnothing \to \left(X:I⟶N\to X\ne \varnothing \right)$$
10	5 9	sylan9	$$⊢\left(I\in V\wedge I\ne \varnothing \right)\to \left(X\in B\to X\ne \varnothing \right)$$