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 
|- B = ( Base ` R )
rspvalint.i 
|- I = ( LIdeal ` R )
rspvalint.k 
|- K = ( RSpan ` R )
Assertion rspvalint 
|- ( ( R e. Ring /\ S C_ B ) -> ( K ` S ) = |^| { t e. I | S C_ t } )

Proof

Step Hyp Ref Expression
1 rspvalint.v 
 |-  B = ( Base ` R )
2 rspvalint.i 
 |-  I = ( LIdeal ` R )
3 rspvalint.k 
 |-  K = ( RSpan ` R )
4 rspval 
 |-  ( RSpan ` R ) = ( LSpan ` ( ringLMod ` R ) )
5 3 4 eqtri 
 |-  K = ( LSpan ` ( ringLMod ` R ) )
6 5 fveq1i 
 |-  ( K ` S ) = ( ( LSpan ` ( ringLMod ` R ) ) ` S )
7 6 a1i 
 |-  ( ( R e. Ring /\ S C_ B ) -> ( K ` S ) = ( ( LSpan ` ( ringLMod ` R ) ) ` S ) )
8 rlmlmod 
 |-  ( R e. Ring -> ( ringLMod ` R ) e. LMod )
9 rlmbas 
 |-  ( Base ` R ) = ( Base ` ( ringLMod ` R ) )
10 1 9 eqtri 
 |-  B = ( Base ` ( ringLMod ` R ) )
11 10 sseq2i 
 |-  ( S C_ B <-> S C_ ( Base ` ( ringLMod ` R ) ) )
12 11 bilani 
 |-  ( ( R e. Ring /\ S C_ B ) -> S C_ ( Base ` ( ringLMod ` R ) ) )
13 eqid 
 |-  ( Base ` ( ringLMod ` R ) ) = ( Base ` ( ringLMod ` R ) )
14 eqid 
 |-  ( LSubSp ` ( ringLMod ` R ) ) = ( LSubSp ` ( ringLMod ` R ) )
15 eqid 
 |-  ( LSpan ` ( ringLMod ` R ) ) = ( LSpan ` ( ringLMod ` R ) )
16 13 14 15 lspval 
 |-  ( ( ( ringLMod ` R ) e. LMod /\ S C_ ( Base ` ( ringLMod ` R ) ) ) -> ( ( LSpan ` ( ringLMod ` R ) ) ` S ) = |^| { t e. ( LSubSp ` ( ringLMod ` R ) ) | S C_ t } )
17 8 12 16 syl2an2r 
 |-  ( ( R e. Ring /\ S C_ B ) -> ( ( LSpan ` ( ringLMod ` R ) ) ` S ) = |^| { t e. ( LSubSp ` ( ringLMod ` R ) ) | S C_ t } )
18 lidlval 
 |-  ( LIdeal ` R ) = ( LSubSp ` ( ringLMod ` R ) )
19 2 18 eqtr2i 
 |-  ( LSubSp ` ( ringLMod ` R ) ) = I
20 19 a1i 
 |-  ( ( R e. Ring /\ S C_ B ) -> ( LSubSp ` ( ringLMod ` R ) ) = I )
21 20 rabeqdv 
 |-  ( ( R e. Ring /\ S C_ B ) -> { t e. ( LSubSp ` ( ringLMod ` R ) ) | S C_ t } = { t e. I | S C_ t } )
22 21 inteqd 
 |-  ( ( R e. Ring /\ S C_ B ) -> |^| { t e. ( LSubSp ` ( ringLMod ` R ) ) | S C_ t } = |^| { t e. I | S C_ t } )
23 7 17 22 3eqtrd 
 |-  ( ( R e. Ring /\ S C_ B ) -> ( K ` S ) = |^| { t e. I | S C_ t } )