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

Metamath Proof Explorer

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 ‘ 𝑅 ) )