This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ringlsmss1

Description: The product of an ideal I of a commutative ring R with some set E is a subset of the ideal. (Contributed by Thierry Arnoux, 8-Jun-2024)

Ref Expression
Hypotheses ringlsmss.1 
|- B = ( Base ` R )
ringlsmss.2 
|- G = ( mulGrp ` R )
ringlsmss.3 
|- .X. = ( LSSum ` G )
ringlsmss1.1 
|- ( ph -> R e. CRing )
ringlsmss1.2 
|- ( ph -> E C_ B )
ringlsmss1.3 
|- ( ph -> I e. ( LIdeal ` R ) )
Assertion ringlsmss1 
|- ( ph -> ( I .X. E ) 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 ringlsmss1.1 
 |-  ( ph -> R e. CRing )
5 ringlsmss1.2 
 |-  ( ph -> E C_ B )
6 ringlsmss1.3 
 |-  ( ph -> I e. ( LIdeal ` R ) )
7 simpr 
 |-  ( ( ( ( ( ph /\ a e. ( I .X. E ) ) /\ i e. I ) /\ e e. E ) /\ a = ( i ( .r ` R ) e ) ) -> a = ( i ( .r ` R ) e ) )
8 4 ad2antrr 
 |-  ( ( ( ph /\ i e. I ) /\ e e. E ) -> R e. CRing )
9 5 sselda 
 |-  ( ( ph /\ e e. E ) -> e e. B )
10 9 adantlr 
 |-  ( ( ( ph /\ i e. I ) /\ e e. E ) -> e e. B )
11 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
12 1 11 lidlss 
 |-  ( I e. ( LIdeal ` R ) -> I C_ B )
13 6 12 syl 
 |-  ( ph -> I C_ B )
14 13 sselda 
 |-  ( ( ph /\ i e. I ) -> i e. B )
15 14 adantr 
 |-  ( ( ( ph /\ i e. I ) /\ e e. E ) -> i e. B )
16 eqid 
 |-  ( .r ` R ) = ( .r ` R )
17 1 16 crngcom 
 |-  ( ( R e. CRing /\ e e. B /\ i e. B ) -> ( e ( .r ` R ) i ) = ( i ( .r ` R ) e ) )
18 8 10 15 17 syl3anc 
 |-  ( ( ( ph /\ i e. I ) /\ e e. E ) -> ( e ( .r ` R ) i ) = ( i ( .r ` R ) e ) )
19 crngring 
 |-  ( R e. CRing -> R e. Ring )
20 4 19 syl 
 |-  ( ph -> R e. Ring )
21 20 ad2antrr 
 |-  ( ( ( ph /\ i e. I ) /\ e e. E ) -> R e. Ring )
22 6 ad2antrr 
 |-  ( ( ( ph /\ i e. I ) /\ e e. E ) -> I e. ( LIdeal ` R ) )
23 simplr 
 |-  ( ( ( ph /\ i e. I ) /\ e e. E ) -> i e. I )
24 11 1 16 lidlmcl 
 |-  ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) ) /\ ( e e. B /\ i e. I ) ) -> ( e ( .r ` R ) i ) e. I )
25 21 22 10 23 24 syl22anc 
 |-  ( ( ( ph /\ i e. I ) /\ e e. E ) -> ( e ( .r ` R ) i ) e. I )
26 18 25 eqeltrrd 
 |-  ( ( ( ph /\ i e. I ) /\ e e. E ) -> ( i ( .r ` R ) e ) e. I )
27 26 adantllr 
 |-  ( ( ( ( ph /\ a e. ( I .X. E ) ) /\ i e. I ) /\ e e. E ) -> ( i ( .r ` R ) e ) e. I )
28 27 adantr 
 |-  ( ( ( ( ( ph /\ a e. ( I .X. E ) ) /\ i e. I ) /\ e e. E ) /\ a = ( i ( .r ` R ) e ) ) -> ( i ( .r ` R ) e ) e. I )
29 7 28 eqeltrd 
 |-  ( ( ( ( ( ph /\ a e. ( I .X. E ) ) /\ i e. I ) /\ e e. E ) /\ a = ( i ( .r ` R ) e ) ) -> a e. I )
30 1 16 2 3 13 5 elringlsm 
 |-  ( ph -> ( a e. ( I .X. E ) <-> E. i e. I E. e e. E a = ( i ( .r ` R ) e ) ) )
31 30 biimpa 
 |-  ( ( ph /\ a e. ( I .X. E ) ) -> E. i e. I E. e e. E a = ( i ( .r ` R ) e ) )
32 29 31 r19.29vva 
 |-  ( ( ph /\ a e. ( I .X. E ) ) -> a e. I )
33 32 ex 
 |-  ( ph -> ( a e. ( I .X. E ) -> a e. I ) )
34 33 ssrdv 
 |-  ( ph -> ( I .X. E ) C_ I )