Metamath Proof Explorer

Theorem idllmulcl

Description: An ideal is closed under multiplication on the left. (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 idllmulcl ⊢R∈RingOps∧I∈Idl⁡R∧A∈I∧B∈X→BHA∈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 simpl ⊢zHx∈I∧xHz∈I→zHx∈I
9 8 ralimi ⊢∀z∈XzHx∈I∧xHz∈I→∀z∈XzHx∈I
10 9 adantl ⊢∀y∈IxGy∈I∧∀z∈XzHx∈I∧xHz∈I→∀z∈XzHx∈I
11 10 ralimi ⊢∀x∈I∀y∈IxGy∈I∧∀z∈XzHx∈I∧xHz∈I→∀x∈I∀z∈XzHx∈I
12 7 11 syl ⊢R∈RingOps∧I∈Idl⁡R→∀x∈I∀z∈XzHx∈I
13 oveq2 ⊢x=A→zHx=zHA
14 13 eleq1d ⊢x=A→zHx∈I↔zHA∈I
15 oveq1 ⊢z=B→zHA=BHA
16 15 eleq1d ⊢z=B→zHA∈I↔BHA∈I
17 14 16 rspc2v ⊢A∈I∧B∈X→∀x∈I∀z∈XzHx∈I→BHA∈I
18 12 17 mpan9 ⊢R∈RingOps∧I∈Idl⁡R∧A∈I∧B∈X→BHA∈I