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 | |
|
ringneg.2 | |
||
ringneg.3 | |
||
ringneg.4 | |
||
ringneg.5 | |
||
Assertion | rngonegmn1l | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ringneg.1 | |
|
2 | ringneg.2 | |
|
3 | ringneg.3 | |
|
4 | ringneg.4 | |
|
5 | ringneg.5 | |
|
6 | 1 | rneqi | |
7 | 3 6 | eqtri | |
8 | 7 2 5 | rngo1cl | |
9 | 1 3 4 | rngonegcl | |
10 | 8 9 | mpdan | |
11 | 8 10 | jca | |
12 | 1 2 3 | rngodir | |
13 | 12 | 3exp2 | |
14 | 13 | imp42 | |
15 | 14 | an32s | |
16 | 11 15 | mpidan | |
17 | eqid | |
|
18 | 1 3 4 17 | rngoaddneg1 | |
19 | 8 18 | mpdan | |
20 | 19 | adantr | |
21 | 20 | oveq1d | |
22 | 17 3 1 2 | rngolz | |
23 | 21 22 | eqtrd | |
24 | 2 7 5 | rngolidm | |
25 | 24 | oveq1d | |
26 | 16 23 25 | 3eqtr3rd | |
27 | 1 2 3 | rngocl | |
28 | 27 | 3expa | |
29 | 28 | an32s | |
30 | 10 29 | mpidan | |
31 | 1 | rngogrpo | |
32 | 3 17 4 | grpoinvid1 | |
33 | 31 32 | syl3an1 | |
34 | 30 33 | mpd3an3 | |
35 | 26 34 | mpbird | |