Metamath Proof Explorer

Theorem rngonegmn1l

Description: Negation in a ring is the same as left multiplication by -u 1 . (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses ringneg.1 
|- G = ( 1st ` R )
ringneg.2 
|- H = ( 2nd ` R )
ringneg.3 
|- X = ran G
ringneg.4 
|- N = ( inv ` G )
ringneg.5 
|- U = ( GId ` H )
Assertion rngonegmn1l 
|- ( ( R e. RingOps /\ A e. X ) -> ( N ` A ) = ( ( N ` U ) H A ) )

Proof

Step Hyp Ref Expression
1 ringneg.1 
 |-  G = ( 1st ` R )
2 ringneg.2 
 |-  H = ( 2nd ` R )
3 ringneg.3 
 |-  X = ran G
4 ringneg.4 
 |-  N = ( inv ` G )
5 ringneg.5 
 |-  U = ( GId ` H )
6 1 rneqi 
 |-  ran G = ran ( 1st ` R )
7 3 6 eqtri 
 |-  X = ran ( 1st ` R )
8 7 2 5 rngo1cl 
 |-  ( R e. RingOps -> U e. X )
9 1 3 4 rngonegcl 
 |-  ( ( R e. RingOps /\ U e. X ) -> ( N ` U ) e. X )
10 8 9 mpdan 
 |-  ( R e. RingOps -> ( N ` U ) e. X )
11 8 10 jca 
 |-  ( R e. RingOps -> ( U e. X /\ ( N ` U ) e. X ) )
12 1 2 3 rngodir 
 |-  ( ( R e. RingOps /\ ( U e. X /\ ( N ` U ) e. X /\ A e. X ) ) -> ( ( U G ( N ` U ) ) H A ) = ( ( U H A ) G ( ( N ` U ) H A ) ) )
13 12 3exp2 
 |-  ( R e. RingOps -> ( U e. X -> ( ( N ` U ) e. X -> ( A e. X -> ( ( U G ( N ` U ) ) H A ) = ( ( U H A ) G ( ( N ` U ) H A ) ) ) ) ) )
14 13 imp42 
 |-  ( ( ( R e. RingOps /\ ( U e. X /\ ( N ` U ) e. X ) ) /\ A e. X ) -> ( ( U G ( N ` U ) ) H A ) = ( ( U H A ) G ( ( N ` U ) H A ) ) )
15 14 an32s 
 |-  ( ( ( R e. RingOps /\ A e. X ) /\ ( U e. X /\ ( N ` U ) e. X ) ) -> ( ( U G ( N ` U ) ) H A ) = ( ( U H A ) G ( ( N ` U ) H A ) ) )
16 11 15 mpidan 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( ( U G ( N ` U ) ) H A ) = ( ( U H A ) G ( ( N ` U ) H A ) ) )
17 eqid 
 |-  ( GId ` G ) = ( GId ` G )
18 1 3 4 17 rngoaddneg1 
 |-  ( ( R e. RingOps /\ U e. X ) -> ( U G ( N ` U ) ) = ( GId ` G ) )
19 8 18 mpdan 
 |-  ( R e. RingOps -> ( U G ( N ` U ) ) = ( GId ` G ) )
20 19 adantr 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( U G ( N ` U ) ) = ( GId ` G ) )
21 20 oveq1d 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( ( U G ( N ` U ) ) H A ) = ( ( GId ` G ) H A ) )
22 17 3 1 2 rngolz 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( ( GId ` G ) H A ) = ( GId ` G ) )
23 21 22 eqtrd 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( ( U G ( N ` U ) ) H A ) = ( GId ` G ) )
24 2 7 5 rngolidm 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( U H A ) = A )
25 24 oveq1d 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( ( U H A ) G ( ( N ` U ) H A ) ) = ( A G ( ( N ` U ) H A ) ) )
26 16 23 25 3eqtr3rd 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( A G ( ( N ` U ) H A ) ) = ( GId ` G ) )
27 1 2 3 rngocl 
 |-  ( ( R e. RingOps /\ ( N ` U ) e. X /\ A e. X ) -> ( ( N ` U ) H A ) e. X )
28 27 3expa 
 |-  ( ( ( R e. RingOps /\ ( N ` U ) e. X ) /\ A e. X ) -> ( ( N ` U ) H A ) e. X )
29 28 an32s 
 |-  ( ( ( R e. RingOps /\ A e. X ) /\ ( N ` U ) e. X ) -> ( ( N ` U ) H A ) e. X )
30 10 29 mpidan 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( ( N ` U ) H A ) e. X )
31 1 rngogrpo 
 |-  ( R e. RingOps -> G e. GrpOp )
32 3 17 4 grpoinvid1 
 |-  ( ( G e. GrpOp /\ A e. X /\ ( ( N ` U ) H A ) e. X ) -> ( ( N ` A ) = ( ( N ` U ) H A ) <-> ( A G ( ( N ` U ) H A ) ) = ( GId ` G ) ) )
33 31 32 syl3an1 
 |-  ( ( R e. RingOps /\ A e. X /\ ( ( N ` U ) H A ) e. X ) -> ( ( N ` A ) = ( ( N ` U ) H A ) <-> ( A G ( ( N ` U ) H A ) ) = ( GId ` G ) ) )
34 30 33 mpd3an3 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( ( N ` A ) = ( ( N ` U ) H A ) <-> ( A G ( ( N ` U ) H A ) ) = ( GId ` G ) ) )
35 26 34 mpbird 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( N ` A ) = ( ( N ` U ) H A ) )