This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
idllmulcl.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
idllmulcl.3 ⊢ 𝑋 = ran 𝐺
Assertion idlrmulcl ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐻 𝐵 ) ∈ 𝐼 )

Proof

Step Hyp Ref Expression
1 idllmulcl.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 idllmulcl.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 idllmulcl.3 ⊢ 𝑋 = ran 𝐺
4 eqid ⊢ ( GId ‘ 𝐺 ) = ( GId ‘ 𝐺 )
5 1 2 3 4 isidl ⊢ ( 𝑅 ∈ RingOps → ( 𝐼 ∈ ( Idl ‘ 𝑅 ) ↔ ( 𝐼 ⊆ 𝑋 ∧ ( GId ‘ 𝐺 ) ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ) ) )
6 5 biimpa ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → ( 𝐼 ⊆ 𝑋 ∧ ( GId ‘ 𝐺 ) ∈ 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) ) )
7 6 simp3d ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) )
8 simpr ⊢ ( ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) → ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 )
9 8 ralimi ⊢ ( ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) → ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 )
10 9 adantl ⊢ ( ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) → ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 )
11 10 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) → ∀ 𝑥 ∈ 𝐼 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 )
12 7 11 syl ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → ∀ 𝑥 ∈ 𝐼 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 )
13 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐻 𝑧 ) = ( 𝐴 𝐻 𝑧 ) )
14 13 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ↔ ( 𝐴 𝐻 𝑧 ) ∈ 𝐼 ) )
15 oveq2 ⊢ ( 𝑧 = 𝐵 → ( 𝐴 𝐻 𝑧 ) = ( 𝐴 𝐻 𝐵 ) )
16 15 eleq1d ⊢ ( 𝑧 = 𝐵 → ( ( 𝐴 𝐻 𝑧 ) ∈ 𝐼 ↔ ( 𝐴 𝐻 𝐵 ) ∈ 𝐼 ) )
17 14 16 rspc2v ⊢ ( ( 𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝐼 ∀ 𝑧 ∈ 𝑋 ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 → ( 𝐴 𝐻 𝐵 ) ∈ 𝐼 ) )
18 12 17 mpan9 ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐻 𝐵 ) ∈ 𝐼 )