Theorem rspssbasd

Description: The span of a set of ring elements is a set of ring elements. (Contributed by SN, 19-Jun-2025)

	Ref	Expression
Hypotheses	rspssbasd.k	|- K = ( RSpan ` R )
	rspssbasd.b	|- B = ( Base ` R )
	rspssbasd.r	|- ( ph -> R e. Ring )
	rspssbasd.g	|- ( ph -> G C_ B )
Assertion	rspssbasd	|- ( ph -> ( K ` G ) C_ B )

Proof

Step	Hyp	Ref	Expression
1		rspssbasd.k	|- K = ( RSpan ` R )
2		rspssbasd.b	|- B = ( Base ` R )
3		rspssbasd.r	|- ( ph -> R e. Ring )
4		rspssbasd.g	|- ( ph -> G C_ B )
5		eqid	|- ( LIdeal ` R ) = ( LIdeal ` R )
6	1 2 5	rspcl	|- ( ( R e. Ring /\ G C_ B ) -> ( K ` G ) e. ( LIdeal ` R ) )
7	3 4 6	syl2anc	|- ( ph -> ( K ` G ) e. ( LIdeal ` R ) )
8	2 5	lidlss	|- ( ( K ` G ) e. ( LIdeal ` R ) -> ( K ` G ) C_ B )
9	7 8	syl	|- ( ph -> ( K ` G ) C_ B )