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 𝐵 = ( Base ‘ 𝑅 )
ringlsmss.2 𝐺 = ( mulGrp ‘ 𝑅 )
ringlsmss.3 × = ( LSSum ‘ 𝐺 )
ringlsmss1.1 ( 𝜑𝑅 ∈ CRing )
ringlsmss1.2 ( 𝜑𝐸𝐵 )
ringlsmss1.3 ( 𝜑𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
Assertion ringlsmss1 ( 𝜑 → ( 𝐼 × 𝐸 ) ⊆ 𝐼 )

Proof

Step Hyp Ref Expression
1 ringlsmss.1 𝐵 = ( Base ‘ 𝑅 )
2 ringlsmss.2 𝐺 = ( mulGrp ‘ 𝑅 )
3 ringlsmss.3 × = ( LSSum ‘ 𝐺 )
4 ringlsmss1.1 ( 𝜑𝑅 ∈ CRing )
5 ringlsmss1.2 ( 𝜑𝐸𝐵 )
6 ringlsmss1.3 ( 𝜑𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
7 simpr ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐼 × 𝐸 ) ) ∧ 𝑖𝐼 ) ∧ 𝑒𝐸 ) ∧ 𝑎 = ( 𝑖 ( .r𝑅 ) 𝑒 ) ) → 𝑎 = ( 𝑖 ( .r𝑅 ) 𝑒 ) )
8 4 ad2antrr ( ( ( 𝜑𝑖𝐼 ) ∧ 𝑒𝐸 ) → 𝑅 ∈ CRing )
9 5 sselda ( ( 𝜑𝑒𝐸 ) → 𝑒𝐵 )
10 9 adantlr ( ( ( 𝜑𝑖𝐼 ) ∧ 𝑒𝐸 ) → 𝑒𝐵 )
11 eqid ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
12 1 11 lidlss ( 𝐼 ∈ ( LIdeal ‘ 𝑅 ) → 𝐼𝐵 )
13 6 12 syl ( 𝜑𝐼𝐵 )
14 13 sselda ( ( 𝜑𝑖𝐼 ) → 𝑖𝐵 )
15 14 adantr ( ( ( 𝜑𝑖𝐼 ) ∧ 𝑒𝐸 ) → 𝑖𝐵 )
16 eqid ( .r𝑅 ) = ( .r𝑅 )
17 1 16 crngcom ( ( 𝑅 ∈ CRing ∧ 𝑒𝐵𝑖𝐵 ) → ( 𝑒 ( .r𝑅 ) 𝑖 ) = ( 𝑖 ( .r𝑅 ) 𝑒 ) )
18 8 10 15 17 syl3anc ( ( ( 𝜑𝑖𝐼 ) ∧ 𝑒𝐸 ) → ( 𝑒 ( .r𝑅 ) 𝑖 ) = ( 𝑖 ( .r𝑅 ) 𝑒 ) )
19 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
20 4 19 syl ( 𝜑𝑅 ∈ Ring )
21 20 ad2antrr ( ( ( 𝜑𝑖𝐼 ) ∧ 𝑒𝐸 ) → 𝑅 ∈ Ring )
22 6 ad2antrr ( ( ( 𝜑𝑖𝐼 ) ∧ 𝑒𝐸 ) → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
23 simplr ( ( ( 𝜑𝑖𝐼 ) ∧ 𝑒𝐸 ) → 𝑖𝐼 )
24 11 1 16 lidlmcl ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( 𝑒𝐵𝑖𝐼 ) ) → ( 𝑒 ( .r𝑅 ) 𝑖 ) ∈ 𝐼 )
25 21 22 10 23 24 syl22anc ( ( ( 𝜑𝑖𝐼 ) ∧ 𝑒𝐸 ) → ( 𝑒 ( .r𝑅 ) 𝑖 ) ∈ 𝐼 )
26 18 25 eqeltrrd ( ( ( 𝜑𝑖𝐼 ) ∧ 𝑒𝐸 ) → ( 𝑖 ( .r𝑅 ) 𝑒 ) ∈ 𝐼 )
27 26 adantllr ( ( ( ( 𝜑𝑎 ∈ ( 𝐼 × 𝐸 ) ) ∧ 𝑖𝐼 ) ∧ 𝑒𝐸 ) → ( 𝑖 ( .r𝑅 ) 𝑒 ) ∈ 𝐼 )
28 27 adantr ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐼 × 𝐸 ) ) ∧ 𝑖𝐼 ) ∧ 𝑒𝐸 ) ∧ 𝑎 = ( 𝑖 ( .r𝑅 ) 𝑒 ) ) → ( 𝑖 ( .r𝑅 ) 𝑒 ) ∈ 𝐼 )
29 7 28 eqeltrd ( ( ( ( ( 𝜑𝑎 ∈ ( 𝐼 × 𝐸 ) ) ∧ 𝑖𝐼 ) ∧ 𝑒𝐸 ) ∧ 𝑎 = ( 𝑖 ( .r𝑅 ) 𝑒 ) ) → 𝑎𝐼 )
30 1 16 2 3 13 5 elringlsm ( 𝜑 → ( 𝑎 ∈ ( 𝐼 × 𝐸 ) ↔ ∃ 𝑖𝐼𝑒𝐸 𝑎 = ( 𝑖 ( .r𝑅 ) 𝑒 ) ) )
31 30 biimpa ( ( 𝜑𝑎 ∈ ( 𝐼 × 𝐸 ) ) → ∃ 𝑖𝐼𝑒𝐸 𝑎 = ( 𝑖 ( .r𝑅 ) 𝑒 ) )
32 29 31 r19.29vva ( ( 𝜑𝑎 ∈ ( 𝐼 × 𝐸 ) ) → 𝑎𝐼 )
33 32 ex ( 𝜑 → ( 𝑎 ∈ ( 𝐼 × 𝐸 ) → 𝑎𝐼 ) )
34 33 ssrdv ( 𝜑 → ( 𝐼 × 𝐸 ) ⊆ 𝐼 )