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 ⊢ B = Base R
ringlsmss.2 ⊢ G = mulGrp R
ringlsmss.3 ⊢ × ˙ = LSSum ⁡ G
ringlsmss2.1 ⊢ φ → R ∈ Ring
ringlsmss2.2 ⊢ φ → E ⊆ B
ringlsmss2.3 ⊢ φ → I ∈ LIdeal ⁡ R
Assertion ringlsmss2 ⊢ φ → E × ˙ I ⊆ I

Proof

Step Hyp Ref Expression
1 ringlsmss.1 ⊢ B = Base R
2 ringlsmss.2 ⊢ G = mulGrp R
3 ringlsmss.3 ⊢ × ˙ = LSSum ⁡ G
4 ringlsmss2.1 ⊢ φ → R ∈ Ring
5 ringlsmss2.2 ⊢ φ → E ⊆ B
6 ringlsmss2.3 ⊢ φ → I ∈ LIdeal ⁡ R
7 simpr ⊢ φ ∧ a ∈ E × ˙ I ∧ e ∈ E ∧ i ∈ I ∧ a = e ⋅ R i → a = e ⋅ R i
8 4 ad2antrr ⊢ φ ∧ e ∈ E ∧ i ∈ I → R ∈ Ring
9 6 ad2antrr ⊢ φ ∧ e ∈ E ∧ i ∈ I → I ∈ LIdeal ⁡ R
10 5 sselda ⊢ φ ∧ e ∈ E → e ∈ B
11 10 adantr ⊢ φ ∧ e ∈ E ∧ i ∈ I → e ∈ B
12 simpr ⊢ φ ∧ e ∈ E ∧ i ∈ I → i ∈ I
13 eqid ⊢ LIdeal ⁡ R = LIdeal ⁡ R
14 eqid ⊢ ⋅ R = ⋅ R
15 13 1 14 lidlmcl ⊢ R ∈ Ring ∧ I ∈ LIdeal ⁡ R ∧ e ∈ B ∧ i ∈ I → e ⋅ R i ∈ I
16 8 9 11 12 15 syl22anc ⊢ φ ∧ e ∈ E ∧ i ∈ I → e ⋅ R i ∈ I
17 16 adantllr ⊢ φ ∧ a ∈ E × ˙ I ∧ e ∈ E ∧ i ∈ I → e ⋅ R i ∈ I
18 17 adantr ⊢ φ ∧ a ∈ E × ˙ I ∧ e ∈ E ∧ i ∈ I ∧ a = e ⋅ R i → e ⋅ R i ∈ I
19 7 18 eqeltrd ⊢ φ ∧ a ∈ E × ˙ I ∧ e ∈ E ∧ i ∈ I ∧ a = e ⋅ R i → a ∈ I
20 1 13 lidlss ⊢ I ∈ LIdeal ⁡ R → I ⊆ B
21 6 20 syl ⊢ φ → I ⊆ B
22 1 14 2 3 5 21 elringlsm ⊢ φ → a ∈ E × ˙ I ↔ ∃ e ∈ E ∃ i ∈ I a = e ⋅ R i
23 22 biimpa ⊢ φ ∧ a ∈ E × ˙ I → ∃ e ∈ E ∃ i ∈ I a = e ⋅ R i
24 19 23 r19.29vva ⊢ φ ∧ a ∈ E × ˙ I → a ∈ I
25 24 ex ⊢ φ → a ∈ E × ˙ I → a ∈ I
26 25 ssrdv ⊢ φ → E × ˙ I ⊆ I