lmiclcl

Description: Isomorphism implies the left side is a module. (Contributed by Stefan O'Rear, 25-Jan-2015)

		Ref	Expression
	Assertion	lmiclcl	$⊢ R ≃_{𝑚} S \to R \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		lmhmlmod1	$⊢ f \in (R LMHom S) \to R \in LMod$
6	4 5	syl	$⊢ f \in (R LMIso S) \to R \in LMod$
7	6	exlimiv	$⊢ \exists f f \in (R LMIso S) \to R \in LMod$
8	3 7	sylbi	$⊢ R ≃_{𝑚} S \to R \in LMod$

Metamath Proof Explorer