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 ∈ NzRing ∧ I ∈ Y ∧ I ≈ J → R freeLMod I ≃ 𝑚 R freeLMod J

Proof

Step Hyp Ref Expression
1 nzrring ⊢ R ∈ NzRing → R ∈ Ring
2 eqid ⊢ R freeLMod I = R freeLMod I
3 2 frlmlmod ⊢ R ∈ Ring ∧ I ∈ Y → R freeLMod I ∈ LMod
4 1 3 sylan ⊢ R ∈ NzRing ∧ I ∈ Y → R freeLMod I ∈ LMod
5 4 3adant3 ⊢ R ∈ NzRing ∧ I ∈ Y ∧ I ≈ J → R freeLMod I ∈ 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 ∈ Ring ∧ I ∈ Y → ran ⁡ R unitVec I ∈ LBasis ⁡ R freeLMod I
9 1 8 sylan ⊢ R ∈ NzRing ∧ I ∈ Y → ran ⁡ R unitVec I ∈ LBasis ⁡ R freeLMod I
10 9 3adant3 ⊢ R ∈ NzRing ∧ I ∈ Y ∧ I ≈ J → ran ⁡ R unitVec I ∈ LBasis ⁡ R freeLMod I
11 simp3 ⊢ R ∈ NzRing ∧ I ∈ Y ∧ I ≈ J → I ≈ J
12 11 ensymd ⊢ R ∈ NzRing ∧ I ∈ Y ∧ I ≈ J → J ≈ I
13 6 uvcendim ⊢ R ∈ NzRing ∧ I ∈ Y → I ≈ ran ⁡ R unitVec I
14 13 3adant3 ⊢ R ∈ NzRing ∧ I ∈ 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 ∈ NzRing ∧ I ∈ 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 ∈ LMod ∧ ran ⁡ R unitVec I ∈ LBasis ⁡ R freeLMod I ∧ J ≈ ran ⁡ R unitVec I → R freeLMod I ≃ 𝑚 Scalar ⁡ R freeLMod I freeLMod J
19 5 10 16 18 syl3anc ⊢ R ∈ NzRing ∧ I ∈ Y ∧ I ≈ J → R freeLMod I ≃ 𝑚 Scalar ⁡ R freeLMod I freeLMod J
20 2 frlmsca ⊢ R ∈ NzRing ∧ I ∈ Y → R = Scalar ⁡ R freeLMod I
21 20 3adant3 ⊢ R ∈ NzRing ∧ I ∈ Y ∧ I ≈ J → R = Scalar ⁡ R freeLMod I
22 21 oveq1d ⊢ R ∈ NzRing ∧ I ∈ Y ∧ I ≈ J → R freeLMod J = Scalar ⁡ R freeLMod I freeLMod J
23 19 22 breqtrrd ⊢ R ∈ NzRing ∧ I ∈ Y ∧ I ≈ J → R freeLMod I ≃ 𝑚 R freeLMod J