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	|- ( ( R e. NzRing /\ I e. Y ) -> ( R freeLMod I ) ~=m ( R freeLMod ( I X. { (/) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( R e. NzRing /\ I e. Y ) -> I e. Y )
2		0ex	|- (/) e. _V
3		xpsneng	|- ( ( I e. Y /\ (/) e. _V ) -> ( I X. { (/) } ) ~~ I )
4	3	ensymd	|- ( ( I e. Y /\ (/) e. _V ) -> I ~~ ( I X. { (/) } ) )
5	1 2 4	sylancl	|- ( ( R e. NzRing /\ I e. Y ) -> I ~~ ( I X. { (/) } ) )
6		frlmisfrlm	|- ( ( R e. NzRing /\ I e. Y /\ I ~~ ( I X. { (/) } ) ) -> ( R freeLMod I ) ~=m ( R freeLMod ( I X. { (/) } ) ) )
7	5 6	mpd3an3	|- ( ( R e. NzRing /\ I e. Y ) -> ( R freeLMod I ) ~=m ( R freeLMod ( I X. { (/) } ) ) )