Theorem idllmulcl

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

	Ref	Expression
Hypotheses	idllmulcl.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
	idllmulcl.2	⊢ 𝐻 = ( 2nd ‘ 𝑅 )
	idllmulcl.3	⊢ 𝑋 = ran 𝐺
Assertion	idllmulcl	⊢ ( ( ( 𝑅 ∈ 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		simpl	⊢ ( ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) → ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 )
9	8	ralimi	⊢ ( ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) → ∀ 𝑧 ∈ 𝑋 ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 )
10	9	adantl	⊢ ( ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) → ∀ 𝑧 ∈ 𝑋 ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 )
11	10	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 𝐺 𝑦 ) ∈ 𝐼 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ∧ ( 𝑥 𝐻 𝑧 ) ∈ 𝐼 ) ) → ∀ 𝑥 ∈ 𝐼 ∀ 𝑧 ∈ 𝑋 ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 )
12	7 11	syl	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → ∀ 𝑥 ∈ 𝐼 ∀ 𝑧 ∈ 𝑋 ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 )
13		oveq2	⊢ ( 𝑥 = 𝐴 → ( 𝑧 𝐻 𝑥 ) = ( 𝑧 𝐻 𝐴 ) )
14	13	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 ↔ ( 𝑧 𝐻 𝐴 ) ∈ 𝐼 ) )
15		oveq1	⊢ ( 𝑧 = 𝐵 → ( 𝑧 𝐻 𝐴 ) = ( 𝐵 𝐻 𝐴 ) )
16	15	eleq1d	⊢ ( 𝑧 = 𝐵 → ( ( 𝑧 𝐻 𝐴 ) ∈ 𝐼 ↔ ( 𝐵 𝐻 𝐴 ) ∈ 𝐼 ) )
17	14 16	rspc2v	⊢ ( ( 𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝐼 ∀ 𝑧 ∈ 𝑋 ( 𝑧 𝐻 𝑥 ) ∈ 𝐼 → ( 𝐵 𝐻 𝐴 ) ∈ 𝐼 ) )
18	12 17	mpan9	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐵 𝐻 𝐴 ) ∈ 𝐼 )