rspcl

Description: The span of a set of ring elements is an ideal. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by Mario Carneiro, 2-Oct-2015)

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

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

Metamath Proof Explorer