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 \in NzRing \land I \in Y) \to (R freeLMod I) ≃_{𝑚} (R freeLMod (I \times \{\emptyset\}))$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (R \in NzRing \land I \in Y) \to I \in Y$
2		0ex	$⊢ \emptyset \in V$
3		xpsneng	$⊢ (I \in Y \land \emptyset \in V) \to (I \times \{\emptyset\}) \approx I$
4	3	ensymd	$⊢ (I \in Y \land \emptyset \in V) \to I \approx (I \times \{\emptyset\})$
5	1 2 4	sylancl	$⊢ (R \in NzRing \land I \in Y) \to I \approx (I \times \{\emptyset\})$
6		frlmisfrlm	$⊢ (R \in NzRing \land I \in Y \land I \approx (I \times \{\emptyset\})) \to (R freeLMod I) ≃_{𝑚} (R freeLMod (I \times \{\emptyset\}))$
7	5 6	mpd3an3	$⊢ (R \in NzRing \land I \in Y) \to (R freeLMod I) ≃_{𝑚} (R freeLMod (I \times \{\emptyset\}))$