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 = 1 st ⁡ R
idllmulcl.2 ⊢ H = 2 nd ⁡ R
idllmulcl.3 ⊢ X = ran ⁡ G
Assertion idlrmulcl ⊢ R ∈ RingOps ∧ I ∈ Idl ⁡ R ∧ A ∈ I ∧ B ∈ X → A H B ∈ I

Proof

Step Hyp Ref Expression
1 idllmulcl.1 ⊢ G = 1 st ⁡ R
2 idllmulcl.2 ⊢ H = 2 nd ⁡ 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 ∈ I x G y ∈ I ∧ ∀ z ∈ X z H x ∈ I ∧ x H z ∈ I
6 5 biimpa ⊢ R ∈ RingOps ∧ I ∈ Idl ⁡ R → I ⊆ X ∧ GId ⁡ G ∈ I ∧ ∀ x ∈ I ∀ y ∈ I x G y ∈ I ∧ ∀ z ∈ X z H x ∈ I ∧ x H z ∈ I
7 6 simp3d ⊢ R ∈ RingOps ∧ I ∈ Idl ⁡ R → ∀ x ∈ I ∀ y ∈ I x G y ∈ I ∧ ∀ z ∈ X z H x ∈ I ∧ x H z ∈ I
8 simpr ⊢ z H x ∈ I ∧ x H z ∈ I → x H z ∈ I
9 8 ralimi ⊢ ∀ z ∈ X z H x ∈ I ∧ x H z ∈ I → ∀ z ∈ X x H z ∈ I
10 9 adantl ⊢ ∀ y ∈ I x G y ∈ I ∧ ∀ z ∈ X z H x ∈ I ∧ x H z ∈ I → ∀ z ∈ X x H z ∈ I
11 10 ralimi ⊢ ∀ x ∈ I ∀ y ∈ I x G y ∈ I ∧ ∀ z ∈ X z H x ∈ I ∧ x H z ∈ I → ∀ x ∈ I ∀ z ∈ X x H z ∈ I
12 7 11 syl ⊢ R ∈ RingOps ∧ I ∈ Idl ⁡ R → ∀ x ∈ I ∀ z ∈ X x H z ∈ I
13 oveq1 ⊢ x = A → x H z = A H z
14 13 eleq1d ⊢ x = A → x H z ∈ I ↔ A H z ∈ I
15 oveq2 ⊢ z = B → A H z = A H B
16 15 eleq1d ⊢ z = B → A H z ∈ I ↔ A H B ∈ I
17 14 16 rspc2v ⊢ A ∈ I ∧ B ∈ X → ∀ x ∈ I ∀ z ∈ X x H z ∈ I → A H B ∈ I
18 12 17 mpan9 ⊢ R ∈ RingOps ∧ I ∈ Idl ⁡ R ∧ A ∈ I ∧ B ∈ X → A H B ∈ I