This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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. { (/) } ) ) )