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=1stR
ringneg.2 H=2ndR
ringneg.3 X=ranG
ringneg.4 N=invG
ringneg.5 U=GIdH
Assertion rngonegmn1l RRingOpsAXNA=NUHA

Proof

Step Hyp Ref Expression
1 ringneg.1 G=1stR
2 ringneg.2 H=2ndR
3 ringneg.3 X=ranG
4 ringneg.4 N=invG
5 ringneg.5 U=GIdH
6 1 rneqi ranG=ran1stR
7 3 6 eqtri X=ran1stR
8 7 2 5 rngo1cl RRingOpsUX
9 1 3 4 rngonegcl RRingOpsUXNUX
10 8 9 mpdan RRingOpsNUX
11 8 10 jca RRingOpsUXNUX
12 1 2 3 rngodir RRingOpsUXNUXAXUGNUHA=UHAGNUHA
13 12 3exp2 RRingOpsUXNUXAXUGNUHA=UHAGNUHA
14 13 imp42 RRingOpsUXNUXAXUGNUHA=UHAGNUHA
15 14 an32s RRingOpsAXUXNUXUGNUHA=UHAGNUHA
16 11 15 mpidan RRingOpsAXUGNUHA=UHAGNUHA
17 eqid GIdG=GIdG
18 1 3 4 17 rngoaddneg1 RRingOpsUXUGNU=GIdG
19 8 18 mpdan RRingOpsUGNU=GIdG
20 19 adantr RRingOpsAXUGNU=GIdG
21 20 oveq1d RRingOpsAXUGNUHA=GIdGHA
22 17 3 1 2 rngolz RRingOpsAXGIdGHA=GIdG
23 21 22 eqtrd RRingOpsAXUGNUHA=GIdG
24 2 7 5 rngolidm RRingOpsAXUHA=A
25 24 oveq1d RRingOpsAXUHAGNUHA=AGNUHA
26 16 23 25 3eqtr3rd RRingOpsAXAGNUHA=GIdG
27 1 2 3 rngocl RRingOpsNUXAXNUHAX
28 27 3expa RRingOpsNUXAXNUHAX
29 28 an32s RRingOpsAXNUXNUHAX
30 10 29 mpidan RRingOpsAXNUHAX
31 1 rngogrpo RRingOpsGGrpOp
32 3 17 4 grpoinvid1 GGrpOpAXNUHAXNA=NUHAAGNUHA=GIdG
33 31 32 syl3an1 RRingOpsAXNUHAXNA=NUHAAGNUHA=GIdG
34 30 33 mpd3an3 RRingOpsAXNA=NUHAAGNUHA=GIdG
35 26 34 mpbird RRingOpsAXNA=NUHA