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 ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑌 ∧ 𝐼 ≈ 𝐽 ) → ( 𝑅 freeLMod 𝐼 ) ≃𝑚 ( 𝑅 freeLMod 𝐽 ) )

Proof

Step Hyp Ref Expression
1 nzrring ⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
2 eqid ⊢ ( 𝑅 freeLMod 𝐼 ) = ( 𝑅 freeLMod 𝐼 )
3 2 frlmlmod ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑌 ) → ( 𝑅 freeLMod 𝐼 ) ∈ LMod )
4 1 3 sylan ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑌 ) → ( 𝑅 freeLMod 𝐼 ) ∈ LMod )
5 4 3adant3 ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑌 ∧ 𝐼 ≈ 𝐽 ) → ( 𝑅 freeLMod 𝐼 ) ∈ LMod )
6 eqid ⊢ ( 𝑅 unitVec 𝐼 ) = ( 𝑅 unitVec 𝐼 )
7 eqid ⊢ ( LBasis ‘ ( 𝑅 freeLMod 𝐼 ) ) = ( LBasis ‘ ( 𝑅 freeLMod 𝐼 ) )
8 2 6 7 frlmlbs ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑌 ) → ran ( 𝑅 unitVec 𝐼 ) ∈ ( LBasis ‘ ( 𝑅 freeLMod 𝐼 ) ) )
9 1 8 sylan ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑌 ) → ran ( 𝑅 unitVec 𝐼 ) ∈ ( LBasis ‘ ( 𝑅 freeLMod 𝐼 ) ) )
10 9 3adant3 ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑌 ∧ 𝐼 ≈ 𝐽 ) → ran ( 𝑅 unitVec 𝐼 ) ∈ ( LBasis ‘ ( 𝑅 freeLMod 𝐼 ) ) )
11 simp3 ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑌 ∧ 𝐼 ≈ 𝐽 ) → 𝐼 ≈ 𝐽 )
12 11 ensymd ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑌 ∧ 𝐼 ≈ 𝐽 ) → 𝐽 ≈ 𝐼 )
13 6 uvcendim ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑌 ) → 𝐼 ≈ ran ( 𝑅 unitVec 𝐼 ) )
14 13 3adant3 ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑌 ∧ 𝐼 ≈ 𝐽 ) → 𝐼 ≈ ran ( 𝑅 unitVec 𝐼 ) )
15 entr ⊢ ( ( 𝐽 ≈ 𝐼 ∧ 𝐼 ≈ ran ( 𝑅 unitVec 𝐼 ) ) → 𝐽 ≈ ran ( 𝑅 unitVec 𝐼 ) )
16 12 14 15 syl2anc ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑌 ∧ 𝐼 ≈ 𝐽 ) → 𝐽 ≈ ran ( 𝑅 unitVec 𝐼 ) )
17 eqid ⊢ ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) = ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) )
18 17 7 lbslcic ⊢ ( ( ( 𝑅 freeLMod 𝐼 ) ∈ LMod ∧ ran ( 𝑅 unitVec 𝐼 ) ∈ ( LBasis ‘ ( 𝑅 freeLMod 𝐼 ) ) ∧ 𝐽 ≈ ran ( 𝑅 unitVec 𝐼 ) ) → ( 𝑅 freeLMod 𝐼 ) ≃𝑚 ( ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) freeLMod 𝐽 ) )
19 5 10 16 18 syl3anc ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑌 ∧ 𝐼 ≈ 𝐽 ) → ( 𝑅 freeLMod 𝐼 ) ≃𝑚 ( ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) freeLMod 𝐽 ) )
20 2 frlmsca ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑌 ) → 𝑅 = ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) )
21 20 3adant3 ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑌 ∧ 𝐼 ≈ 𝐽 ) → 𝑅 = ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) )
22 21 oveq1d ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑌 ∧ 𝐼 ≈ 𝐽 ) → ( 𝑅 freeLMod 𝐽 ) = ( ( Scalar ‘ ( 𝑅 freeLMod 𝐼 ) ) freeLMod 𝐽 ) )
23 19 22 breqtrrd ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑌 ∧ 𝐼 ≈ 𝐽 ) → ( 𝑅 freeLMod 𝐼 ) ≃𝑚 ( 𝑅 freeLMod 𝐽 ) )