Metamath Proof Explorer

Theorem lmisfree

Description: A module has a basis iff it is isomorphic to a free module. In settings where isomorphic objects are not distinguished, it is common to define "free module" as any module with a basis; thus for instance lbsex might be described as "every vector space is free". (Contributed by Stefan O'Rear, 26-Feb-2015)

Ref Expression
Hypotheses lmisfree.j ⊢ J = LBasis ⁡ W
lmisfree.f ⊢ F = Scalar ⁡ W
Assertion lmisfree ⊢ W ∈ LMod → J ≠ ∅ ↔ ∃ k W ≃ 𝑚 F freeLMod k

Proof

Step Hyp Ref Expression
1 lmisfree.j ⊢ J = LBasis ⁡ W
2 lmisfree.f ⊢ F = Scalar ⁡ W
3 n0 ⊢ J ≠ ∅ ↔ ∃ j j ∈ J
4 vex ⊢ j ∈ V
5 4 enref ⊢ j ≈ j
6 2 1 lbslcic ⊢ W ∈ LMod ∧ j ∈ J ∧ j ≈ j → W ≃ 𝑚 F freeLMod j
7 5 6 mp3an3 ⊢ W ∈ LMod ∧ j ∈ J → W ≃ 𝑚 F freeLMod j
8 oveq2 ⊢ k = j → F freeLMod k = F freeLMod j
9 8 breq2d ⊢ k = j → W ≃ 𝑚 F freeLMod k ↔ W ≃ 𝑚 F freeLMod j
10 4 9 spcev ⊢ W ≃ 𝑚 F freeLMod j → ∃ k W ≃ 𝑚 F freeLMod k
11 7 10 syl ⊢ W ∈ LMod ∧ j ∈ J → ∃ k W ≃ 𝑚 F freeLMod k
12 11 ex ⊢ W ∈ LMod → j ∈ J → ∃ k W ≃ 𝑚 F freeLMod k
13 12 exlimdv ⊢ W ∈ LMod → ∃ j j ∈ J → ∃ k W ≃ 𝑚 F freeLMod k
14 3 13 biimtrid ⊢ W ∈ LMod → J ≠ ∅ → ∃ k W ≃ 𝑚 F freeLMod k
15 lmicsym ⊢ W ≃ 𝑚 F freeLMod k → F freeLMod k ≃ 𝑚 W
16 lmiclcl ⊢ W ≃ 𝑚 F freeLMod k → W ∈ LMod
17 2 lmodring ⊢ W ∈ LMod → F ∈ Ring
18 vex ⊢ k ∈ V
19 eqid ⊢ F freeLMod k = F freeLMod k
20 eqid ⊢ F unitVec k = F unitVec k
21 eqid ⊢ LBasis ⁡ F freeLMod k = LBasis ⁡ F freeLMod k
22 19 20 21 frlmlbs ⊢ F ∈ Ring ∧ k ∈ V → ran ⁡ F unitVec k ∈ LBasis ⁡ F freeLMod k
23 17 18 22 sylancl ⊢ W ∈ LMod → ran ⁡ F unitVec k ∈ LBasis ⁡ F freeLMod k
24 23 ne0d ⊢ W ∈ LMod → LBasis ⁡ F freeLMod k ≠ ∅
25 16 24 syl ⊢ W ≃ 𝑚 F freeLMod k → LBasis ⁡ F freeLMod k ≠ ∅
26 21 1 lmiclbs ⊢ F freeLMod k ≃ 𝑚 W → LBasis ⁡ F freeLMod k ≠ ∅ → J ≠ ∅
27 15 25 26 sylc ⊢ W ≃ 𝑚 F freeLMod k → J ≠ ∅
28 27 exlimiv ⊢ ∃ k W ≃ 𝑚 F freeLMod k → J ≠ ∅
29 14 28 impbid1 ⊢ W ∈ LMod → J ≠ ∅ ↔ ∃ k W ≃ 𝑚 F freeLMod k