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

Metamath Proof Explorer

Theorem clmring

Description: The scalar ring of a subcomplex module is a ring. (Contributed by Mario Carneiro, 16-Oct-2015)

		Ref	Expression
	Hypothesis	clm0.f	$⊢ F = Scalar (W)$
	Assertion	clmring	$⊢ W \in CMod \to F \in Ring$

Step	Hyp	Ref	Expression
1		clm0.f	$⊢ F = Scalar (W)$
2		clmlmod	$⊢ W \in CMod \to W \in LMod$
3	1	lmodring	$⊢ W \in LMod \to F \in Ring$
4	2 3	syl	$⊢ W \in CMod \to F \in Ring$