Metamath Proof Explorer

Theorem lbslcic

Description: A module with a basis is isomorphic to a free module with the same cardinality. (Contributed by Stefan O'Rear, 26-Feb-2015)

Ref Expression
Hypotheses lbslcic.f 
|- F = ( Scalar ` W )
lbslcic.j 
|- J = ( LBasis ` W )
Assertion lbslcic 
|- ( ( W e. LMod /\ B e. J /\ I ~~ B ) -> W ~=m ( F freeLMod I ) )

Proof

Step Hyp Ref Expression
1 lbslcic.f 
 |-  F = ( Scalar ` W )
2 lbslcic.j 
 |-  J = ( LBasis ` W )
3 simp3 
 |-  ( ( W e. LMod /\ B e. J /\ I ~~ B ) -> I ~~ B )
4 bren 
 |-  ( I ~~ B <-> E. e e : I -1-1-onto-> B )
5 3 4 sylib 
 |-  ( ( W e. LMod /\ B e. J /\ I ~~ B ) -> E. e e : I -1-1-onto-> B )
6 eqid 
 |-  ( F freeLMod I ) = ( F freeLMod I )
7 eqid 
 |-  ( Base ` ( F freeLMod I ) ) = ( Base ` ( F freeLMod I ) )
8 eqid 
 |-  ( Base ` W ) = ( Base ` W )
9 eqid 
 |-  ( .s ` W ) = ( .s ` W )
10 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
11 eqid 
 |-  ( x e. ( Base ` ( F freeLMod I ) ) |-> ( W gsum ( x oF ( .s ` W ) e ) ) ) = ( x e. ( Base ` ( F freeLMod I ) ) |-> ( W gsum ( x oF ( .s ` W ) e ) ) )
12 simpl1 
 |-  ( ( ( W e. LMod /\ B e. J /\ I ~~ B ) /\ e : I -1-1-onto-> B ) -> W e. LMod )
13 relen 
 |-  Rel ~~
14 13 brrelex1i 
 |-  ( I ~~ B -> I e. _V )
15 14 3ad2ant3 
 |-  ( ( W e. LMod /\ B e. J /\ I ~~ B ) -> I e. _V )
16 15 adantr 
 |-  ( ( ( W e. LMod /\ B e. J /\ I ~~ B ) /\ e : I -1-1-onto-> B ) -> I e. _V )
17 1 a1i 
 |-  ( ( ( W e. LMod /\ B e. J /\ I ~~ B ) /\ e : I -1-1-onto-> B ) -> F = ( Scalar ` W ) )
18 f1ofo 
 |-  ( e : I -1-1-onto-> B -> e : I -onto-> B )
19 18 adantl 
 |-  ( ( ( W e. LMod /\ B e. J /\ I ~~ B ) /\ e : I -1-1-onto-> B ) -> e : I -onto-> B )
20 2 lbslinds 
 |-  J C_ ( LIndS ` W )
21 20 sseli 
 |-  ( B e. J -> B e. ( LIndS ` W ) )
22 21 3ad2ant2 
 |-  ( ( W e. LMod /\ B e. J /\ I ~~ B ) -> B e. ( LIndS ` W ) )
23 22 adantr 
 |-  ( ( ( W e. LMod /\ B e. J /\ I ~~ B ) /\ e : I -1-1-onto-> B ) -> B e. ( LIndS ` W ) )
24 f1of1 
 |-  ( e : I -1-1-onto-> B -> e : I -1-1-> B )
25 24 adantl 
 |-  ( ( ( W e. LMod /\ B e. J /\ I ~~ B ) /\ e : I -1-1-onto-> B ) -> e : I -1-1-> B )
26 f1linds 
 |-  ( ( W e. LMod /\ B e. ( LIndS ` W ) /\ e : I -1-1-> B ) -> e LIndF W )
27 12 23 25 26 syl3anc 
 |-  ( ( ( W e. LMod /\ B e. J /\ I ~~ B ) /\ e : I -1-1-onto-> B ) -> e LIndF W )
28 8 2 10 lbssp 
 |-  ( B e. J -> ( ( LSpan ` W ) ` B ) = ( Base ` W ) )
29 28 3ad2ant2 
 |-  ( ( W e. LMod /\ B e. J /\ I ~~ B ) -> ( ( LSpan ` W ) ` B ) = ( Base ` W ) )
30 29 adantr 
 |-  ( ( ( W e. LMod /\ B e. J /\ I ~~ B ) /\ e : I -1-1-onto-> B ) -> ( ( LSpan ` W ) ` B ) = ( Base ` W ) )
31 6 7 8 9 10 11 12 16 17 19 27 30 indlcim 
 |-  ( ( ( W e. LMod /\ B e. J /\ I ~~ B ) /\ e : I -1-1-onto-> B ) -> ( x e. ( Base ` ( F freeLMod I ) ) |-> ( W gsum ( x oF ( .s ` W ) e ) ) ) e. ( ( F freeLMod I ) LMIso W ) )
32 lmimcnv 
 |-  ( ( x e. ( Base ` ( F freeLMod I ) ) |-> ( W gsum ( x oF ( .s ` W ) e ) ) ) e. ( ( F freeLMod I ) LMIso W ) -> `' ( x e. ( Base ` ( F freeLMod I ) ) |-> ( W gsum ( x oF ( .s ` W ) e ) ) ) e. ( W LMIso ( F freeLMod I ) ) )
33 brlmici 
 |-  ( `' ( x e. ( Base ` ( F freeLMod I ) ) |-> ( W gsum ( x oF ( .s ` W ) e ) ) ) e. ( W LMIso ( F freeLMod I ) ) -> W ~=m ( F freeLMod I ) )
34 31 32 33 3syl 
 |-  ( ( ( W e. LMod /\ B e. J /\ I ~~ B ) /\ e : I -1-1-onto-> B ) -> W ~=m ( F freeLMod I ) )
35 5 34 exlimddv 
 |-  ( ( W e. LMod /\ B e. J /\ I ~~ B ) -> W ~=m ( F freeLMod I ) )