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 ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
lmisfree.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
Assertion lmisfree ( 𝑊 ∈ LMod → ( 𝐽 ≠ ∅ ↔ ∃ 𝑘 𝑊 ≃𝑚 ( 𝐹 freeLMod 𝑘 ) ) )

Proof

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