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	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
	frlmfibas.n	⊢ 𝑁 = ( Base ‘ 𝑅 )
	elfrlmbasn0.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
Assertion	elfrlmbasn0	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐼 ≠ ∅ ) → ( 𝑋 ∈ 𝐵 → 𝑋 ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		frlmfibas.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2		frlmfibas.n	⊢ 𝑁 = ( Base ‘ 𝑅 )
3		elfrlmbasn0.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
4	1 2 3	frlmbasf	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 : 𝐼 ⟶ 𝑁 )
5	4	ex	⊢ ( 𝐼 ∈ 𝑉 → ( 𝑋 ∈ 𝐵 → 𝑋 : 𝐼 ⟶ 𝑁 ) )
6		f0dom0	⊢ ( 𝑋 : 𝐼 ⟶ 𝑁 → ( 𝐼 = ∅ ↔ 𝑋 = ∅ ) )
7	6	biimprd	⊢ ( 𝑋 : 𝐼 ⟶ 𝑁 → ( 𝑋 = ∅ → 𝐼 = ∅ ) )
8	7	necon3d	⊢ ( 𝑋 : 𝐼 ⟶ 𝑁 → ( 𝐼 ≠ ∅ → 𝑋 ≠ ∅ ) )
9	8	com12	⊢ ( 𝐼 ≠ ∅ → ( 𝑋 : 𝐼 ⟶ 𝑁 → 𝑋 ≠ ∅ ) )
10	5 9	sylan9	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐼 ≠ ∅ ) → ( 𝑋 ∈ 𝐵 → 𝑋 ≠ ∅ ) )