Metamath Proof Explorer

Theorem ringlsmss2

Description: The product with an ideal of a ring is a subset of that ideal. (Contributed by Thierry Arnoux, 2-Jun-2024)

Ref Expression
Hypotheses ringlsmss.1 
|- B = ( Base ` R )
ringlsmss.2 
|- G = ( mulGrp ` R )
ringlsmss.3 
|- .X. = ( LSSum ` G )
ringlsmss2.1 
|- ( ph -> R e. Ring )
ringlsmss2.2 
|- ( ph -> E C_ B )
ringlsmss2.3 
|- ( ph -> I e. ( LIdeal ` R ) )
Assertion ringlsmss2 
|- ( ph -> ( E .X. I ) C_ I )

Proof

Step Hyp Ref Expression
1 ringlsmss.1 
 |-  B = ( Base ` R )
2 ringlsmss.2 
 |-  G = ( mulGrp ` R )
3 ringlsmss.3 
 |-  .X. = ( LSSum ` G )
4 ringlsmss2.1 
 |-  ( ph -> R e. Ring )
5 ringlsmss2.2 
 |-  ( ph -> E C_ B )
6 ringlsmss2.3 
 |-  ( ph -> I e. ( LIdeal ` R ) )
7 simpr 
 |-  ( ( ( ( ( ph /\ a e. ( E .X. I ) ) /\ e e. E ) /\ i e. I ) /\ a = ( e ( .r ` R ) i ) ) -> a = ( e ( .r ` R ) i ) )
8 4 ad2antrr 
 |-  ( ( ( ph /\ e e. E ) /\ i e. I ) -> R e. Ring )
9 6 ad2antrr 
 |-  ( ( ( ph /\ e e. E ) /\ i e. I ) -> I e. ( LIdeal ` R ) )
10 5 sselda 
 |-  ( ( ph /\ e e. E ) -> e e. B )
11 10 adantr 
 |-  ( ( ( ph /\ e e. E ) /\ i e. I ) -> e e. B )
12 simpr 
 |-  ( ( ( ph /\ e e. E ) /\ i e. I ) -> i e. I )
13 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
14 eqid 
 |-  ( .r ` R ) = ( .r ` R )
15 13 1 14 lidlmcl 
 |-  ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) /\ ( e e. B /\ i e. I ) ) -> ( e ( .r ` R ) i ) e. I )
16 8 9 11 12 15 syl22anc 
 |-  ( ( ( ph /\ e e. E ) /\ i e. I ) -> ( e ( .r ` R ) i ) e. I )
17 16 adantllr 
 |-  ( ( ( ( ph /\ a e. ( E .X. I ) ) /\ e e. E ) /\ i e. I ) -> ( e ( .r ` R ) i ) e. I )
18 17 adantr 
 |-  ( ( ( ( ( ph /\ a e. ( E .X. I ) ) /\ e e. E ) /\ i e. I ) /\ a = ( e ( .r ` R ) i ) ) -> ( e ( .r ` R ) i ) e. I )
19 7 18 eqeltrd 
 |-  ( ( ( ( ( ph /\ a e. ( E .X. I ) ) /\ e e. E ) /\ i e. I ) /\ a = ( e ( .r ` R ) i ) ) -> a e. I )
20 1 13 lidlss 
 |-  ( I e. ( LIdeal ` R ) -> I C_ B )
21 6 20 syl 
 |-  ( ph -> I C_ B )
22 1 14 2 3 5 21 elringlsm 
 |-  ( ph -> ( a e. ( E .X. I ) <-> E. e e. E E. i e. I a = ( e ( .r ` R ) i ) ) )
23 22 biimpa 
 |-  ( ( ph /\ a e. ( E .X. I ) ) -> E. e e. E E. i e. I a = ( e ( .r ` R ) i ) )
24 19 23 r19.29vva 
 |-  ( ( ph /\ a e. ( E .X. I ) ) -> a e. I )
25 24 ex 
 |-  ( ph -> ( a e. ( E .X. I ) -> a e. I ) )
26 25 ssrdv 
 |-  ( ph -> ( E .X. I ) C_ I )