Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  zrhpsgnodpm Structured version   Unicode version

Theorem zrhpsgnodpm 18497
 Description: The sign of an odd permutation embedded into a ring is the additive inverse of the multiplicative neutral element of the ring. (Contributed by SO, 9-Jul-2018.)
Hypotheses
Ref Expression
zrhpsgnevpm.y RHom
zrhpsgnevpm.s pmSgn
zrhpsgnevpm.o
zrhpsgnodpm.p
zrhpsgnodpm.i
Assertion
Ref Expression
zrhpsgnodpm pmEven

Proof of Theorem zrhpsgnodpm
StepHypRef Expression
1 eqid 2467 . . . . . 6
2 zrhpsgnevpm.s . . . . . 6 pmSgn
3 eqid 2467 . . . . . 6 mulGrpflds mulGrpflds
41, 2, 3psgnghm2 18486 . . . . 5 mulGrpflds
5 zrhpsgnodpm.p . . . . . 6
6 eqid 2467 . . . . . 6 mulGrpflds mulGrpflds
75, 6ghmf 16143 . . . . 5 mulGrpflds mulGrpflds
84, 7syl 16 . . . 4 mulGrpflds
983ad2ant2 1018 . . 3 pmEven mulGrpflds
10 eldifi 3631 . . . 4 pmEven
11103ad2ant3 1019 . . 3 pmEven
12 fvco3 5951 . . 3 mulGrpflds
139, 11, 12syl2anc 661 . 2 pmEven
141, 5, 2psgnodpm 18493 . . . 4 pmEven
15143adant1 1014 . . 3 pmEven
1615fveq2d 5876 . 2 pmEven
17 zrhpsgnevpm.y . . . . . . 7 RHom
1817zrhrhm 18418 . . . . . 6 ring RingHom
19 rhmghm 17246 . . . . . 6 ring RingHom ring
2018, 19syl 16 . . . . 5 ring
21 1z 10906 . . . . . 6
2221a1i 11 . . . . 5
23 zringbas 18364 . . . . . 6 ring
24 eqid 2467 . . . . . 6 ring ring
25 zrhpsgnodpm.i . . . . . 6
2623, 24, 25ghminv 16146 . . . . 5 ring ring
2720, 22, 26syl2anc 661 . . . 4 ring
28 ax-1cn 9562 . . . . . . . . 9
29 cnfldneg 18314 . . . . . . . . 9 fld
3028, 29ax-mp 5 . . . . . . . 8 fld
31 zringinvg 18388 . . . . . . . . 9 ring
3221, 31ax-mp 5 . . . . . . . 8 ring
3330, 32eqtri 2496 . . . . . . 7 fld ring
3433, 30eqtr3i 2498 . . . . . 6 ring
3534fveq2i 5875 . . . . 5 ring
3635a1i 11 . . . 4 ring
37 zrhpsgnevpm.o . . . . . 6
3817, 37zrh1 18419 . . . . 5
3938fveq2d 5876 . . . 4
4027, 36, 393eqtr3d 2516 . . 3