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 e. LMod -> ( J =/= (/) <-> E. k W ~=m ( F freeLMod k ) ) )

Proof

Step Hyp Ref Expression
1 lmisfree.j 
 |-  J = ( LBasis ` W )
2 lmisfree.f 
 |-  F = ( Scalar ` W )
3 n0 
 |-  ( J =/= (/) <-> E. j j e. J )
4 vex 
 |-  j e. _V
5 4 enref 
 |-  j ~~ j
6 2 1 lbslcic 
 |-  ( ( W e. LMod /\ j e. J /\ j ~~ j ) -> W ~=m ( F freeLMod j ) )
7 5 6 mp3an3 
 |-  ( ( W e. LMod /\ j e. J ) -> W ~=m ( F freeLMod j ) )
8 oveq2 
 |-  ( k = j -> ( F freeLMod k ) = ( F freeLMod j ) )
9 8 breq2d 
 |-  ( k = j -> ( W ~=m ( F freeLMod k ) <-> W ~=m ( F freeLMod j ) ) )
10 4 9 spcev 
 |-  ( W ~=m ( F freeLMod j ) -> E. k W ~=m ( F freeLMod k ) )
11 7 10 syl 
 |-  ( ( W e. LMod /\ j e. J ) -> E. k W ~=m ( F freeLMod k ) )
12 11 ex 
 |-  ( W e. LMod -> ( j e. J -> E. k W ~=m ( F freeLMod k ) ) )
13 12 exlimdv 
 |-  ( W e. LMod -> ( E. j j e. J -> E. k W ~=m ( F freeLMod k ) ) )
14 3 13 syl5bi 
 |-  ( W e. LMod -> ( J =/= (/) -> E. k W ~=m ( F freeLMod k ) ) )
15 lmicsym 
 |-  ( W ~=m ( F freeLMod k ) -> ( F freeLMod k ) ~=m W )
16 lmiclcl 
 |-  ( W ~=m ( F freeLMod k ) -> W e. LMod )
17 2 lmodring 
 |-  ( W e. LMod -> F e. Ring )
18 vex 
 |-  k e. _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 e. Ring /\ k e. _V ) -> ran ( F unitVec k ) e. ( LBasis ` ( F freeLMod k ) ) )
23 17 18 22 sylancl 
 |-  ( W e. LMod -> ran ( F unitVec k ) e. ( LBasis ` ( F freeLMod k ) ) )
24 23 ne0d 
 |-  ( W e. LMod -> ( LBasis ` ( F freeLMod k ) ) =/= (/) )
25 16 24 syl 
 |-  ( W ~=m ( F freeLMod k ) -> ( LBasis ` ( F freeLMod k ) ) =/= (/) )
26 21 1 lmiclbs 
 |-  ( ( F freeLMod k ) ~=m W -> ( ( LBasis ` ( F freeLMod k ) ) =/= (/) -> J =/= (/) ) )
27 15 25 26 sylc 
 |-  ( W ~=m ( F freeLMod k ) -> J =/= (/) )
28 27 exlimiv 
 |-  ( E. k W ~=m ( F freeLMod k ) -> J =/= (/) )
29 14 28 impbid1 
 |-  ( W e. LMod -> ( J =/= (/) <-> E. k W ~=m ( F freeLMod k ) ) )