Theorem frlmiscvec

Description: Every free module is isomorphic to the free module of "column vectors" of the same dimension over the same (nonzero) ring. (Contributed by AV, 10-Mar-2019)

	Ref	Expression
Assertion	frlmiscvec	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑌 ) → ( 𝑅 freeLMod 𝐼 ) ≃𝑚 ( 𝑅 freeLMod ( 𝐼 × { ∅ } ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑌 ) → 𝐼 ∈ 𝑌 )
2		0ex	⊢ ∅ ∈ V
3		xpsneng	⊢ ( ( 𝐼 ∈ 𝑌 ∧ ∅ ∈ V ) → ( 𝐼 × { ∅ } ) ≈ 𝐼 )
4	3	ensymd	⊢ ( ( 𝐼 ∈ 𝑌 ∧ ∅ ∈ V ) → 𝐼 ≈ ( 𝐼 × { ∅ } ) )
5	1 2 4	sylancl	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑌 ) → 𝐼 ≈ ( 𝐼 × { ∅ } ) )
6		frlmisfrlm	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑌 ∧ 𝐼 ≈ ( 𝐼 × { ∅ } ) ) → ( 𝑅 freeLMod 𝐼 ) ≃𝑚 ( 𝑅 freeLMod ( 𝐼 × { ∅ } ) ) )
7	5 6	mpd3an3	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐼 ∈ 𝑌 ) → ( 𝑅 freeLMod 𝐼 ) ≃𝑚 ( 𝑅 freeLMod ( 𝐼 × { ∅ } ) ) )