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

Metamath Proof Explorer

Theorem rspssid

Description: The span of a set of ring elements contains those elements. (Contributed by Stefan O'Rear, 3-Jan-2015)

	Ref	Expression
Hypotheses	rspcl.k	$⊢ K = RSpan (R)$
	rspcl.b	$⊢ B = {Base}_{R}$
Assertion	rspssid	$⊢ (R \in Ring \land G \subseteq B) \to G \subseteq K (G)$

Step	Hyp	Ref	Expression
1		rspcl.k	$⊢ K = RSpan (R)$
2		rspcl.b	$⊢ B = {Base}_{R}$
3		rlmlmod	$⊢ R \in Ring \to ringLMod (R) \in LMod$
4		rlmbas	$⊢ {Base}_{R} = {Base}_{ringLMod (R)}$
5	2 4	eqtri	$⊢ B = {Base}_{ringLMod (R)}$
6		rspval	$⊢ RSpan (R) = LSpan (ringLMod (R))$
7	1 6	eqtri	$⊢ K = LSpan (ringLMod (R))$
8	5 7	lspssid	$⊢ (ringLMod (R) \in LMod \land G \subseteq B) \to G \subseteq K (G)$
9	3 8	sylan	$⊢ (R \in Ring \land G \subseteq B) \to G \subseteq K (G)$