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	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
	rspssbasd.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rspssbasd.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	rspssbasd.g	⊢ ( 𝜑 → 𝐺 ⊆ 𝐵 )
Assertion	rspssbasd	⊢ ( 𝜑 → ( 𝐾 ‘ 𝐺 ) ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		rspssbasd.k	⊢ 𝐾 = ( RSpan ‘ 𝑅 )
2		rspssbasd.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		rspssbasd.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
4		rspssbasd.g	⊢ ( 𝜑 → 𝐺 ⊆ 𝐵 )
5		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
6	1 2 5	rspcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ⊆ 𝐵 ) → ( 𝐾 ‘ 𝐺 ) ∈ ( LIdeal ‘ 𝑅 ) )
7	3 4 6	syl2anc	⊢ ( 𝜑 → ( 𝐾 ‘ 𝐺 ) ∈ ( LIdeal ‘ 𝑅 ) )
8	2 5	lidlss	⊢ ( ( 𝐾 ‘ 𝐺 ) ∈ ( LIdeal ‘ 𝑅 ) → ( 𝐾 ‘ 𝐺 ) ⊆ 𝐵 )
9	7 8	syl	⊢ ( 𝜑 → ( 𝐾 ‘ 𝐺 ) ⊆ 𝐵 )