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 | ⊢ ( 𝜑 → ( 𝐾 ‘ 𝐺 ) ⊆ 𝐵 ) | 
| 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 | ⊢ ( 𝜑 → ( 𝐾 ‘ 𝐺 ) ⊆ 𝐵 ) |