lmicrcl

Description: Isomorphism implies the right side is a module. (Contributed by Mario Carneiro, 6-May-2015)

		Ref	Expression
	Assertion	lmicrcl	$⊢ R ≃_{𝑚} S \to S \in LMod$

Step	Hyp	Ref	Expression
1		brlmic	$⊢ R ≃_{𝑚} S \leftrightarrow R LMIso S \neq \emptyset$
2		n0	$⊢ R LMIso S \neq \emptyset \leftrightarrow \exists f f \in (R LMIso S)$
3	1 2	bitri	$⊢ R ≃_{𝑚} S \leftrightarrow \exists f f \in (R LMIso S)$
4		lmimlmhm	$⊢ f \in (R LMIso S) \to f \in (R LMHom S)$
5		lmhmlmod2	$⊢ f \in (R LMHom S) \to S \in LMod$
6	4 5	syl	$⊢ f \in (R LMIso S) \to S \in LMod$
7	6	exlimiv	$⊢ \exists f f \in (R LMIso S) \to S \in LMod$
8	3 7	sylbi	$⊢ R ≃_{𝑚} S \to S \in LMod$

Metamath Proof Explorer