Metamath Proof Explorer

Theorem rngonegmn1r

Description: Negation in a ring is the same as right multiplication by -u 1 . (Contributed by Jeff Madsen, 19-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 rngonegmn1r 
|- ( ( R e. RingOps /\ A e. X ) -> ( N ` A ) = ( A H ( N ` U ) ) )

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 10 adantr 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( N ` U ) e. X )
12 8 adantr 
 |-  ( ( R e. RingOps /\ A e. X ) -> U e. X )
13 11 12 jca 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( ( N ` U ) e. X /\ U e. X ) )
14 1 2 3 rngodi 
 |-  ( ( R e. RingOps /\ ( A e. X /\ ( N ` U ) e. X /\ U e. X ) ) -> ( A H ( ( N ` U ) G U ) ) = ( ( A H ( N ` U ) ) G ( A H U ) ) )
15 14 3exp2 
 |-  ( R e. RingOps -> ( A e. X -> ( ( N ` U ) e. X -> ( U e. X -> ( A H ( ( N ` U ) G U ) ) = ( ( A H ( N ` U ) ) G ( A H U ) ) ) ) ) )
16 15 imp43 
 |-  ( ( ( R e. RingOps /\ A e. X ) /\ ( ( N ` U ) e. X /\ U e. X ) ) -> ( A H ( ( N ` U ) G U ) ) = ( ( A H ( N ` U ) ) G ( A H U ) ) )
17 13 16 mpdan 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( A H ( ( N ` U ) G U ) ) = ( ( A H ( N ` U ) ) G ( A H U ) ) )
18 eqid 
 |-  ( GId ` G ) = ( GId ` G )
19 1 3 4 18 rngoaddneg2 
 |-  ( ( R e. RingOps /\ U e. X ) -> ( ( N ` U ) G U ) = ( GId ` G ) )
20 8 19 mpdan 
 |-  ( R e. RingOps -> ( ( N ` U ) G U ) = ( GId ` G ) )
21 20 adantr 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( ( N ` U ) G U ) = ( GId ` G ) )
22 21 oveq2d 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( A H ( ( N ` U ) G U ) ) = ( A H ( GId ` G ) ) )
23 18 3 1 2 rngorz 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( A H ( GId ` G ) ) = ( GId ` G ) )
24 22 23 eqtrd 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( A H ( ( N ` U ) G U ) ) = ( GId ` G ) )
25 2 7 5 rngoridm 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( A H U ) = A )
26 25 oveq2d 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( ( A H ( N ` U ) ) G ( A H U ) ) = ( ( A H ( N ` U ) ) G A ) )
27 17 24 26 3eqtr3rd 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( ( A H ( N ` U ) ) G A ) = ( GId ` G ) )
28 1 2 3 rngocl 
 |-  ( ( R e. RingOps /\ A e. X /\ ( N ` U ) e. X ) -> ( A H ( N ` U ) ) e. X )
29 11 28 mpd3an3 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( A H ( N ` U ) ) e. X )
30 1 rngogrpo 
 |-  ( R e. RingOps -> G e. GrpOp )
31 3 18 4 grpoinvid2 
 |-  ( ( G e. GrpOp /\ A e. X /\ ( A H ( N ` U ) ) e. X ) -> ( ( N ` A ) = ( A H ( N ` U ) ) <-> ( ( A H ( N ` U ) ) G A ) = ( GId ` G ) ) )
32 30 31 syl3an1 
 |-  ( ( R e. RingOps /\ A e. X /\ ( A H ( N ` U ) ) e. X ) -> ( ( N ` A ) = ( A H ( N ` U ) ) <-> ( ( A H ( N ` U ) ) G A ) = ( GId ` G ) ) )
33 29 32 mpd3an3 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( ( N ` A ) = ( A H ( N ` U ) ) <-> ( ( A H ( N ` U ) ) G A ) = ( GId ` G ) ) )
34 27 33 mpbird 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( N ` A ) = ( A H ( N ` U ) ) )