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 = 1 st ⁡ R
idllmulcl.2 ⊢ H = 2 nd ⁡ R
idllmulcl.3 ⊢ X = ran ⁡ G
Assertion idllmulcl ⊢ R ∈ RingOps ∧ I ∈ Idl ⁡ R ∧ A ∈ I ∧ B ∈ X → B H A ∈ 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 simpl ⊢ z H x ∈ I ∧ x H z ∈ I → z H x ∈ I
9 8 ralimi ⊢ ∀ z ∈ X z H x ∈ I ∧ x H z ∈ I → ∀ z ∈ X z H x ∈ I
10 9 adantl ⊢ ∀ y ∈ I x G y ∈ I ∧ ∀ z ∈ X z H x ∈ I ∧ x H z ∈ I → ∀ z ∈ X z H x ∈ 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 z H x ∈ I
12 7 11 syl ⊢ R ∈ RingOps ∧ I ∈ Idl ⁡ R → ∀ x ∈ I ∀ z ∈ X z H x ∈ I
13 oveq2 ⊢ x = A → z H x = z H A
14 13 eleq1d ⊢ x = A → z H x ∈ I ↔ z H A ∈ I
15 oveq1 ⊢ z = B → z H A = B H A
16 15 eleq1d ⊢ z = B → z H A ∈ I ↔ B H A ∈ I
17 14 16 rspc2v ⊢ A ∈ I ∧ B ∈ X → ∀ x ∈ I ∀ z ∈ X z H x ∈ I → B H A ∈ I
18 12 17 mpan9 ⊢ R ∈ RingOps ∧ I ∈ Idl ⁡ R ∧ A ∈ I ∧ B ∈ X → B H A ∈ I