Metamath Proof Explorer

Theorem rspssp

Description: The ideal span of a set of elements in a ring is contained in any subring which contains those elements. (Contributed by Stefan O'Rear, 3-Jan-2015)

		Ref	Expression
	Hypotheses	rspcl.k	$⊢ K = RSpan (R)$
		rspssp.u	$⊢ U = LIdeal (R)$
	Assertion	rspssp	$⊢ (R \in Ring \land I \in U \land G \subseteq I) \to K (G) \subseteq I$

Proof

Step	Hyp	Ref	Expression
1		rspcl.k	$⊢ K = RSpan (R)$
2		rspssp.u	$⊢ U = LIdeal (R)$
3		rlmlmod	$⊢ R \in Ring \to ringLMod (R) \in LMod$
4		lidlval	$⊢ LIdeal (R) = LSubSp (ringLMod (R))$
5	2 4	eqtri	$⊢ U = LSubSp (ringLMod (R))$
6		rspval	$⊢ RSpan (R) = LSpan (ringLMod (R))$
7	1 6	eqtri	$⊢ K = LSpan (ringLMod (R))$
8	5 7	lspssp	$⊢ (ringLMod (R) \in LMod \land I \in U \land G \subseteq I) \to K (G) \subseteq I$
9	3 8	syl3an1	$⊢ (R \in Ring \land I \in U \land G \subseteq I) \to K (G) \subseteq I$