Metamath Proof Explorer

Theorem rspvalint

Description: The ideal generated by a subset of a ring as intersection of ideals including the subset. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by AV, 30-Jun-2026)

Ref Expression
Hypotheses rspvalint.v ⊢ 𝐵 = ( Base ‘ 𝑅 )
rspvalint.i ⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
rspvalint.k ⊢ 𝐾 = ( RSpan ‘ 𝑅 )
Assertion rspvalint ( ( 𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵 ) → ( 𝐾 ‘ 𝑆 ) = ∩ { 𝑡 ∈ 𝐼 ∣ 𝑆 ⊆ 𝑡 } )

Proof

Step Hyp Ref Expression
1 rspvalint.v ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 rspvalint.i ⊢ 𝐼 = ( LIdeal ‘ 𝑅 )
3 rspvalint.k ⊢ 𝐾 = ( RSpan ‘ 𝑅 )
4 rspval ⊢ ( RSpan ‘ 𝑅 ) = ( LSpan ‘ ( ringLMod ‘ 𝑅 ) )
5 3 4 eqtri ⊢ 𝐾 = ( LSpan ‘ ( ringLMod ‘ 𝑅 ) )
6 5 fveq1i ⊢ ( 𝐾 ‘ 𝑆 ) = ( ( LSpan ‘ ( ringLMod ‘ 𝑅 ) ) ‘ 𝑆 )
7 6 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵 ) → ( 𝐾 ‘ 𝑆 ) = ( ( LSpan ‘ ( ringLMod ‘ 𝑅 ) ) ‘ 𝑆 ) )
8 rlmlmod ⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
9 rlmbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
10 1 9 eqtri ⊢ 𝐵 = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
11 10 sseq2i ⊢ ( 𝑆 ⊆ 𝐵 ↔ 𝑆 ⊆ ( Base ‘ ( ringLMod ‘ 𝑅 ) ) )
12 11 bilani ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵 ) → 𝑆 ⊆ ( Base ‘ ( ringLMod ‘ 𝑅 ) ) )
13 eqid ⊢ ( Base ‘ ( ringLMod ‘ 𝑅 ) ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
14 eqid ⊢ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
15 eqid ⊢ ( LSpan ‘ ( ringLMod ‘ 𝑅 ) ) = ( LSpan ‘ ( ringLMod ‘ 𝑅 ) )
16 13 14 15 lspval ⊢ ( ( ( ringLMod ‘ 𝑅 ) ∈ LMod ∧ 𝑆 ⊆ ( Base ‘ ( ringLMod ‘ 𝑅 ) ) ) → ( ( LSpan ‘ ( ringLMod ‘ 𝑅 ) ) ‘ 𝑆 ) = ∩ { 𝑡 ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) ∣ 𝑆 ⊆ 𝑡 } )
17 8 12 16 syl2an2r ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵 ) → ( ( LSpan ‘ ( ringLMod ‘ 𝑅 ) ) ‘ 𝑆 ) = ∩ { 𝑡 ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) ∣ 𝑆 ⊆ 𝑡 } )
18 lidlval ⊢ ( LIdeal ‘ 𝑅 ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
19 2 18 eqtr2i ⊢ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) = 𝐼
20 19 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵 ) → ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) = 𝐼 )
21 20 rabeqdv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵 ) → { 𝑡 ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) ∣ 𝑆 ⊆ 𝑡 } = { 𝑡 ∈ 𝐼 ∣ 𝑆 ⊆ 𝑡 } )
22 21 inteqd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵 ) → ∩ { 𝑡 ∈ ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) ) ∣ 𝑆 ⊆ 𝑡 } = ∩ { 𝑡 ∈ 𝐼 ∣ 𝑆 ⊆ 𝑡 } )
23 7 17 22 3eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ⊆ 𝐵 ) → ( 𝐾 ‘ 𝑆 ) = ∩ { 𝑡 ∈ 𝐼 ∣ 𝑆 ⊆ 𝑡 } )