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

Metamath Proof Explorer

Theorem rlmds

Description: Metric component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015)

		Ref	Expression
	Assertion	rlmds	$⊢ dist (R) = dist (ringLMod (R))$

Step	Hyp	Ref	Expression
1		rlmval	$⊢ ringLMod (R) = subringAlg (R) ({Base}_{R})$
2	1	a1i	$⊢ ⊤ \to ringLMod (R) = subringAlg (R) ({Base}_{R})$
3		ssidd	$⊢ ⊤ \to {Base}_{R} \subseteq {Base}_{R}$
4	2 3	srads	$⊢ ⊤ \to dist (R) = dist (ringLMod (R))$
5	4	mptru	$⊢ dist (R) = dist (ringLMod (R))$