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 )

Metamath Proof Explorer

Theorem ringlsmss1

Proof