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 ⊢ 𝐵 = ( 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 ⊢ ( 𝜑 → ( 𝐼 × 𝐸 ) ⊆ 𝐼 )