Metamath Proof Explorer

Theorem idlrmulcl

Description: An ideal is closed under multiplication on the right. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses idllmulcl.1 ⊢G=1st⁡R
idllmulcl.2 ⊢H=2nd⁡R
idllmulcl.3 ⊢X=ran⁡G
Assertion idlrmulcl ⊢R∈RingOps∧I∈Idl⁡R∧A∈I∧B∈X→AHB∈I

Proof

Step Hyp Ref Expression
1 idllmulcl.1 ⊢G=1st⁡R
2 idllmulcl.2 ⊢H=2nd⁡R
3 idllmulcl.3 ⊢X=ran⁡G
4 eqid ⊢GId⁡G=GId⁡G
5 1 2 3 4 isidl ⊢R∈RingOps→I∈Idl⁡R↔I⊆X∧GId⁡G∈I∧∀x∈I∀y∈IxGy∈I∧∀z∈XzHx∈I∧xHz∈I
6 5 biimpa ⊢R∈RingOps∧I∈Idl⁡R→I⊆X∧GId⁡G∈I∧∀x∈I∀y∈IxGy∈I∧∀z∈XzHx∈I∧xHz∈I
7 6 simp3d ⊢R∈RingOps∧I∈Idl⁡R→∀x∈I∀y∈IxGy∈I∧∀z∈XzHx∈I∧xHz∈I
8 simpr ⊢zHx∈I∧xHz∈I→xHz∈I
9 8 ralimi ⊢∀z∈XzHx∈I∧xHz∈I→∀z∈XxHz∈I
10 9 adantl ⊢∀y∈IxGy∈I∧∀z∈XzHx∈I∧xHz∈I→∀z∈XxHz∈I
11 10 ralimi ⊢∀x∈I∀y∈IxGy∈I∧∀z∈XzHx∈I∧xHz∈I→∀x∈I∀z∈XxHz∈I
12 7 11 syl ⊢R∈RingOps∧I∈Idl⁡R→∀x∈I∀z∈XxHz∈I
13 oveq1 ⊢x=A→xHz=AHz
14 13 eleq1d ⊢x=A→xHz∈I↔AHz∈I
15 oveq2 ⊢z=B→AHz=AHB
16 15 eleq1d ⊢z=B→AHz∈I↔AHB∈I
17 14 16 rspc2v ⊢A∈I∧B∈X→∀x∈I∀z∈XxHz∈I→AHB∈I
18 12 17 mpan9 ⊢R∈RingOps∧I∈Idl⁡R∧A∈I∧B∈X→AHB∈I