Metamath Proof Explorer

Theorem frlmisfrlm

Description: A free module is isomorphic to a free module over the same (nonzero) ring, with the same cardinality. (Contributed by AV, 10-Mar-2019)

Ref Expression
Assertion frlmisfrlm 
|- ( ( R e. NzRing /\ I e. Y /\ I ~~ J ) -> ( R freeLMod I ) ~=m ( R freeLMod J ) )

Proof

Step Hyp Ref Expression
1 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
2 eqid 
 |-  ( R freeLMod I ) = ( R freeLMod I )
3 2 frlmlmod 
 |-  ( ( R e. Ring /\ I e. Y ) -> ( R freeLMod I ) e. LMod )
4 1 3 sylan 
 |-  ( ( R e. NzRing /\ I e. Y ) -> ( R freeLMod I ) e. LMod )
5 4 3adant3 
 |-  ( ( R e. NzRing /\ I e. Y /\ I ~~ J ) -> ( R freeLMod I ) e. LMod )
6 eqid 
 |-  ( R unitVec I ) = ( R unitVec I )
7 eqid 
 |-  ( LBasis ` ( R freeLMod I ) ) = ( LBasis ` ( R freeLMod I ) )
8 2 6 7 frlmlbs 
 |-  ( ( R e. Ring /\ I e. Y ) -> ran ( R unitVec I ) e. ( LBasis ` ( R freeLMod I ) ) )
9 1 8 sylan 
 |-  ( ( R e. NzRing /\ I e. Y ) -> ran ( R unitVec I ) e. ( LBasis ` ( R freeLMod I ) ) )
10 9 3adant3 
 |-  ( ( R e. NzRing /\ I e. Y /\ I ~~ J ) -> ran ( R unitVec I ) e. ( LBasis ` ( R freeLMod I ) ) )
11 simp3 
 |-  ( ( R e. NzRing /\ I e. Y /\ I ~~ J ) -> I ~~ J )
12 11 ensymd 
 |-  ( ( R e. NzRing /\ I e. Y /\ I ~~ J ) -> J ~~ I )
13 6 uvcendim 
 |-  ( ( R e. NzRing /\ I e. Y ) -> I ~~ ran ( R unitVec I ) )
14 13 3adant3 
 |-  ( ( R e. NzRing /\ I e. Y /\ I ~~ J ) -> I ~~ ran ( R unitVec I ) )
15 entr 
 |-  ( ( J ~~ I /\ I ~~ ran ( R unitVec I ) ) -> J ~~ ran ( R unitVec I ) )
16 12 14 15 syl2anc 
 |-  ( ( R e. NzRing /\ I e. Y /\ I ~~ J ) -> J ~~ ran ( R unitVec I ) )
17 eqid 
 |-  ( Scalar ` ( R freeLMod I ) ) = ( Scalar ` ( R freeLMod I ) )
18 17 7 lbslcic 
 |-  ( ( ( R freeLMod I ) e. LMod /\ ran ( R unitVec I ) e. ( LBasis ` ( R freeLMod I ) ) /\ J ~~ ran ( R unitVec I ) ) -> ( R freeLMod I ) ~=m ( ( Scalar ` ( R freeLMod I ) ) freeLMod J ) )
19 5 10 16 18 syl3anc 
 |-  ( ( R e. NzRing /\ I e. Y /\ I ~~ J ) -> ( R freeLMod I ) ~=m ( ( Scalar ` ( R freeLMod I ) ) freeLMod J ) )
20 2 frlmsca 
 |-  ( ( R e. NzRing /\ I e. Y ) -> R = ( Scalar ` ( R freeLMod I ) ) )
21 20 3adant3 
 |-  ( ( R e. NzRing /\ I e. Y /\ I ~~ J ) -> R = ( Scalar ` ( R freeLMod I ) ) )
22 21 oveq1d 
 |-  ( ( R e. NzRing /\ I e. Y /\ I ~~ J ) -> ( R freeLMod J ) = ( ( Scalar ` ( R freeLMod I ) ) freeLMod J ) )
23 19 22 breqtrrd 
 |-  ( ( R e. NzRing /\ I e. Y /\ I ~~ J ) -> ( R freeLMod I ) ~=m ( R freeLMod J ) )