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

Metamath Proof Explorer

Theorem idlnegcl

Description: An ideal is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses idlnegcl.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
idlnegcl.2 ⊢ 𝑁 = ( inv ‘ 𝐺 )
Assertion idlnegcl ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝐴 ∈ 𝐼 ) → ( 𝑁 ‘ 𝐴 ) ∈ 𝐼 )

Proof

Step Hyp Ref Expression
1 idlnegcl.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 idlnegcl.2 ⊢ 𝑁 = ( inv ‘ 𝐺 )
3 eqid ⊢ ran 𝐺 = ran 𝐺
4 1 3 idlss ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) → 𝐼 ⊆ ran 𝐺 )
5 ssel2 ⊢ ( ( 𝐼 ⊆ ran 𝐺 ∧ 𝐴 ∈ 𝐼 ) → 𝐴 ∈ ran 𝐺 )
6 eqid ⊢ ( 2nd ‘ 𝑅 ) = ( 2nd ‘ 𝑅 )
7 eqid ⊢ ( GId ‘ ( 2nd ‘ 𝑅 ) ) = ( GId ‘ ( 2nd ‘ 𝑅 ) )
8 1 6 3 2 7 rngonegmn1l ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ ran 𝐺 ) → ( 𝑁 ‘ 𝐴 ) = ( ( 𝑁 ‘ ( GId ‘ ( 2nd ‘ 𝑅 ) ) ) ( 2nd ‘ 𝑅 ) 𝐴 ) )
9 5 8 sylan2 ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐼 ⊆ ran 𝐺 ∧ 𝐴 ∈ 𝐼 ) ) → ( 𝑁 ‘ 𝐴 ) = ( ( 𝑁 ‘ ( GId ‘ ( 2nd ‘ 𝑅 ) ) ) ( 2nd ‘ 𝑅 ) 𝐴 ) )
10 9 anassrs ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ⊆ ran 𝐺 ) ∧ 𝐴 ∈ 𝐼 ) → ( 𝑁 ‘ 𝐴 ) = ( ( 𝑁 ‘ ( GId ‘ ( 2nd ‘ 𝑅 ) ) ) ( 2nd ‘ 𝑅 ) 𝐴 ) )
11 4 10 syldanl ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝐴 ∈ 𝐼 ) → ( 𝑁 ‘ 𝐴 ) = ( ( 𝑁 ‘ ( GId ‘ ( 2nd ‘ 𝑅 ) ) ) ( 2nd ‘ 𝑅 ) 𝐴 ) )
12 1 rneqi ⊢ ran 𝐺 = ran ( 1st ‘ 𝑅 )
13 12 6 7 rngo1cl ⊢ ( 𝑅 ∈ RingOps → ( GId ‘ ( 2nd ‘ 𝑅 ) ) ∈ ran 𝐺 )
14 1 3 2 rngonegcl ⊢ ( ( 𝑅 ∈ RingOps ∧ ( GId ‘ ( 2nd ‘ 𝑅 ) ) ∈ ran 𝐺 ) → ( 𝑁 ‘ ( GId ‘ ( 2nd ‘ 𝑅 ) ) ) ∈ ran 𝐺 )
15 13 14 mpdan ⊢ ( 𝑅 ∈ RingOps → ( 𝑁 ‘ ( GId ‘ ( 2nd ‘ 𝑅 ) ) ) ∈ ran 𝐺 )
16 15 ad2antrr ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝐴 ∈ 𝐼 ) → ( 𝑁 ‘ ( GId ‘ ( 2nd ‘ 𝑅 ) ) ) ∈ ran 𝐺 )
17 1 6 3 idllmulcl ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ 𝐼 ∧ ( 𝑁 ‘ ( GId ‘ ( 2nd ‘ 𝑅 ) ) ) ∈ ran 𝐺 ) ) → ( ( 𝑁 ‘ ( GId ‘ ( 2nd ‘ 𝑅 ) ) ) ( 2nd ‘ 𝑅 ) 𝐴 ) ∈ 𝐼 )
18 17 anassrs ⊢ ( ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝐴 ∈ 𝐼 ) ∧ ( 𝑁 ‘ ( GId ‘ ( 2nd ‘ 𝑅 ) ) ) ∈ ran 𝐺 ) → ( ( 𝑁 ‘ ( GId ‘ ( 2nd ‘ 𝑅 ) ) ) ( 2nd ‘ 𝑅 ) 𝐴 ) ∈ 𝐼 )
19 16 18 mpdan ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝐴 ∈ 𝐼 ) → ( ( 𝑁 ‘ ( GId ‘ ( 2nd ‘ 𝑅 ) ) ) ( 2nd ‘ 𝑅 ) 𝐴 ) ∈ 𝐼 )
20 11 19 eqeltrd ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝐴 ∈ 𝐼 ) → ( 𝑁 ‘ 𝐴 ) ∈ 𝐼 )