Metamath Proof Explorer


Theorem abvneg

Description: The absolute value of a negative is the same as that of the positive. (Contributed by Mario Carneiro, 8-Sep-2014)

Ref Expression
Hypotheses abv0.a A=AbsValR
abvneg.b B=BaseR
abvneg.p N=invgR
Assertion abvneg FAXBFNX=FX

Proof

Step Hyp Ref Expression
1 abv0.a A=AbsValR
2 abvneg.b B=BaseR
3 abvneg.p N=invgR
4 1 abvrcl FARRing
5 4 adantr FAXBRRing
6 ringgrp RRingRGrp
7 4 6 syl FARGrp
8 2 3 grpinvcl RGrpXBNXB
9 7 8 sylan FAXBNXB
10 simpr FAXBXB
11 eqid 1R=1R
12 eqid 0R=0R
13 2 11 12 ring1eq0 RRingNXBXB1R=0RNX=X
14 5 9 10 13 syl3anc FAXB1R=0RNX=X
15 14 imp FAXB1R=0RNX=X
16 15 fveq2d FAXB1R=0RFNX=FX
17 2 11 ringidcl RRing1RB
18 4 17 syl FA1RB
19 2 3 grpinvcl RGrp1RBN1RB
20 7 18 19 syl2anc FAN1RB
21 1 2 abvcl FAN1RBFN1R
22 20 21 mpdan FAFN1R
23 22 recnd FAFN1R
24 23 sqvald FAFN1R2=FN1RFN1R
25 eqid R=R
26 1 2 25 abvmul FAN1RBN1RBFN1RRN1R=FN1RFN1R
27 20 20 26 mpd3an23 FAFN1RRN1R=FN1RFN1R
28 2 25 3 4 20 18 ringmneg2 FAN1RRN1R=NN1RR1R
29 2 25 11 3 4 18 ringnegl FAN1RR1R=N1R
30 29 fveq2d FANN1RR1R=NN1R
31 2 3 grpinvinv RGrp1RBNN1R=1R
32 7 18 31 syl2anc FANN1R=1R
33 28 30 32 3eqtrd FAN1RRN1R=1R
34 33 fveq2d FAFN1RRN1R=F1R
35 24 27 34 3eqtr2d FAFN1R2=F1R
36 35 adantr FA1R0RFN1R2=F1R
37 1 11 12 abv1z FA1R0RF1R=1
38 36 37 eqtrd FA1R0RFN1R2=1
39 sq1 12=1
40 38 39 eqtr4di FA1R0RFN1R2=12
41 1 2 abvge0 FAN1RB0FN1R
42 20 41 mpdan FA0FN1R
43 1re 1
44 0le1 01
45 sq11 FN1R0FN1R101FN1R2=12FN1R=1
46 43 44 45 mpanr12 FN1R0FN1RFN1R2=12FN1R=1
47 22 42 46 syl2anc FAFN1R2=12FN1R=1
48 47 biimpa FAFN1R2=12FN1R=1
49 40 48 syldan FA1R0RFN1R=1
50 49 adantlr FAXB1R0RFN1R=1
51 50 oveq1d FAXB1R0RFN1RFX=1FX
52 simpl FAXBFA
53 20 adantr FAXBN1RB
54 1 2 25 abvmul FAN1RBXBFN1RRX=FN1RFX
55 52 53 10 54 syl3anc FAXBFN1RRX=FN1RFX
56 2 25 11 3 5 10 ringnegl FAXBN1RRX=NX
57 56 fveq2d FAXBFN1RRX=FNX
58 55 57 eqtr3d FAXBFN1RFX=FNX
59 58 adantr FAXB1R0RFN1RFX=FNX
60 51 59 eqtr3d FAXB1R0R1FX=FNX
61 1 2 abvcl FAXBFX
62 61 recnd FAXBFX
63 62 mulid2d FAXB1FX=FX
64 63 adantr FAXB1R0R1FX=FX
65 60 64 eqtr3d FAXB1R0RFNX=FX
66 16 65 pm2.61dane FAXBFNX=FX