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

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

Proof

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