Theorem rngoidl

Description: A ring R is an R ideal. (Contributed by Jeff Madsen, 10-Jun-2010)

	Ref	Expression
Hypotheses	rngidl.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
	rngidl.2	⊢ 𝑋 = ran 𝐺
Assertion	rngoidl	⊢ ( 𝑅 ∈ RingOps → 𝑋 ∈ ( Idl ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		rngidl.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
2		rngidl.2	⊢ 𝑋 = ran 𝐺
3		ssidd	⊢ ( 𝑅 ∈ RingOps → 𝑋 ⊆ 𝑋 )
4		eqid	⊢ ( GId ‘ 𝐺 ) = ( GId ‘ 𝐺 )
5	1 2 4	rngo0cl	⊢ ( 𝑅 ∈ RingOps → ( GId ‘ 𝐺 ) ∈ 𝑋 )
6	1 2	rngogcl	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐺 𝑦 ) ∈ 𝑋 )
7	6	3expa	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐺 𝑦 ) ∈ 𝑋 )
8	7	ralrimiva	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐺 𝑦 ) ∈ 𝑋 )
9		eqid	⊢ ( 2nd ‘ 𝑅 ) = ( 2nd ‘ 𝑅 )
10	1 9 2	rngocl	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ 𝑋 )
11	10	3com23	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ 𝑋 )
12	1 9 2	rngocl	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ 𝑋 )
13	11 12	jca	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ 𝑋 ∧ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ 𝑋 ) )
14	13	3expa	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ 𝑋 ∧ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ 𝑋 ) )
15	14	ralrimiva	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ 𝑋 ∧ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ 𝑋 ) )
16	8 15	jca	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐺 𝑦 ) ∈ 𝑋 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ 𝑋 ∧ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ 𝑋 ) ) )
17	16	ralrimiva	⊢ ( 𝑅 ∈ RingOps → ∀ 𝑥 ∈ 𝑋 ( ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐺 𝑦 ) ∈ 𝑋 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ 𝑋 ∧ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ 𝑋 ) ) )
18	1 9 2 4	isidl	⊢ ( 𝑅 ∈ RingOps → ( 𝑋 ∈ ( Idl ‘ 𝑅 ) ↔ ( 𝑋 ⊆ 𝑋 ∧ ( GId ‘ 𝐺 ) ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐺 𝑦 ) ∈ 𝑋 ∧ ∀ 𝑧 ∈ 𝑋 ( ( 𝑧 ( 2nd ‘ 𝑅 ) 𝑥 ) ∈ 𝑋 ∧ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑧 ) ∈ 𝑋 ) ) ) ) )
19	3 5 17 18	mpbir3and	⊢ ( 𝑅 ∈ RingOps → 𝑋 ∈ ( Idl ‘ 𝑅 ) )