Metamath Proof Explorer

Theorem idlnegcl

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

Ref Expression
Hypotheses idlnegcl.1 ⊢ G = 1 st ⁡ R
idlnegcl.2 ⊢ N = inv ⁡ G
Assertion idlnegcl ⊢ R ∈ RingOps ∧ I ∈ Idl ⁡ R ∧ A ∈ I → N ⁡ A ∈ I

Proof

Step Hyp Ref Expression
1 idlnegcl.1 ⊢ G = 1 st ⁡ R
2 idlnegcl.2 ⊢ N = inv ⁡ G
3 eqid ⊢ ran ⁡ G = ran ⁡ G
4 1 3 idlss ⊢ R ∈ RingOps ∧ I ∈ Idl ⁡ R → I ⊆ ran ⁡ G
5 ssel2 ⊢ I ⊆ ran ⁡ G ∧ A ∈ I → A ∈ ran ⁡ G
6 eqid ⊢ 2 nd ⁡ R = 2 nd ⁡ R
7 eqid ⊢ GId ⁡ 2 nd ⁡ R = GId ⁡ 2 nd ⁡ R
8 1 6 3 2 7 rngonegmn1l ⊢ R ∈ RingOps ∧ A ∈ ran ⁡ G → N ⁡ A = N ⁡ GId ⁡ 2 nd ⁡ R 2 nd ⁡ R A
9 5 8 sylan2 ⊢ R ∈ RingOps ∧ I ⊆ ran ⁡ G ∧ A ∈ I → N ⁡ A = N ⁡ GId ⁡ 2 nd ⁡ R 2 nd ⁡ R A
10 9 anassrs ⊢ R ∈ RingOps ∧ I ⊆ ran ⁡ G ∧ A ∈ I → N ⁡ A = N ⁡ GId ⁡ 2 nd ⁡ R 2 nd ⁡ R A
11 4 10 syldanl ⊢ R ∈ RingOps ∧ I ∈ Idl ⁡ R ∧ A ∈ I → N ⁡ A = N ⁡ GId ⁡ 2 nd ⁡ R 2 nd ⁡ R A
12 1 rneqi ⊢ ran ⁡ G = ran ⁡ 1 st ⁡ R
13 12 6 7 rngo1cl ⊢ R ∈ RingOps → GId ⁡ 2 nd ⁡ R ∈ ran ⁡ G
14 1 3 2 rngonegcl ⊢ R ∈ RingOps ∧ GId ⁡ 2 nd ⁡ R ∈ ran ⁡ G → N ⁡ GId ⁡ 2 nd ⁡ R ∈ ran ⁡ G
15 13 14 mpdan ⊢ R ∈ RingOps → N ⁡ GId ⁡ 2 nd ⁡ R ∈ ran ⁡ G
16 15 ad2antrr ⊢ R ∈ RingOps ∧ I ∈ Idl ⁡ R ∧ A ∈ I → N ⁡ GId ⁡ 2 nd ⁡ R ∈ ran ⁡ G
17 1 6 3 idllmulcl ⊢ R ∈ RingOps ∧ I ∈ Idl ⁡ R ∧ A ∈ I ∧ N ⁡ GId ⁡ 2 nd ⁡ R ∈ ran ⁡ G → N ⁡ GId ⁡ 2 nd ⁡ R 2 nd ⁡ R A ∈ I
18 17 anassrs ⊢ R ∈ RingOps ∧ I ∈ Idl ⁡ R ∧ A ∈ I ∧ N ⁡ GId ⁡ 2 nd ⁡ R ∈ ran ⁡ G → N ⁡ GId ⁡ 2 nd ⁡ R 2 nd ⁡ R A ∈ I
19 16 18 mpdan ⊢ R ∈ RingOps ∧ I ∈ Idl ⁡ R ∧ A ∈ I → N ⁡ GId ⁡ 2 nd ⁡ R 2 nd ⁡ R A ∈ I
20 11 19 eqeltrd ⊢ R ∈ RingOps ∧ I ∈ Idl ⁡ R ∧ A ∈ I → N ⁡ A ∈ I