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 ‘ 𝑅 ) ) ∧ 𝐴 ∈ 𝐼 ) → ( 𝑁 ‘ 𝐴 ) ∈ 𝐼 )