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 = AbsVal R
abvneg.b B = Base R
abvneg.p N = inv g R
Assertion abvneg F A X B F N X = F X

Proof

Step Hyp Ref Expression
1 abv0.a A = AbsVal R
2 abvneg.b B = Base R
3 abvneg.p N = inv g R
4 1 abvrcl F A R Ring
5 4 adantr F A X B R Ring
6 ringgrp R Ring R Grp
7 4 6 syl F A R Grp
8 2 3 grpinvcl R Grp X B N X B
9 7 8 sylan F A X B N X B
10 simpr F A X B X B
11 eqid 1 R = 1 R
12 eqid 0 R = 0 R
13 2 11 12 ring1eq0 R Ring N X B X B 1 R = 0 R N X = X
14 5 9 10 13 syl3anc F A X B 1 R = 0 R N X = X
15 14 imp F A X B 1 R = 0 R N X = X
16 15 fveq2d F A X B 1 R = 0 R F N X = F X
17 2 11 ringidcl R Ring 1 R B
18 4 17 syl F A 1 R B
19 2 3 grpinvcl R Grp 1 R B N 1 R B
20 7 18 19 syl2anc F A N 1 R B
21 1 2 abvcl F A N 1 R B F N 1 R
22 20 21 mpdan F A F N 1 R
23 22 recnd F A F N 1 R
24 23 sqvald F A F N 1 R 2 = F N 1 R F N 1 R
25 eqid R = R
26 1 2 25 abvmul F A N 1 R B N 1 R B F N 1 R R N 1 R = F N 1 R F N 1 R
27 20 20 26 mpd3an23 F A F N 1 R R N 1 R = F N 1 R F N 1 R
28 2 25 3 4 20 18 ringmneg2 F A N 1 R R N 1 R = N N 1 R R 1 R
29 2 25 11 3 4 18 ringnegl F A N 1 R R 1 R = N 1 R
30 29 fveq2d F A N N 1 R R 1 R = N N 1 R
31 2 3 grpinvinv R Grp 1 R B N N 1 R = 1 R
32 7 18 31 syl2anc F A N N 1 R = 1 R
33 28 30 32 3eqtrd F A N 1 R R N 1 R = 1 R
34 33 fveq2d F A F N 1 R R N 1 R = F 1 R
35 24 27 34 3eqtr2d F A F N 1 R 2 = F 1 R
36 35 adantr F A 1 R 0 R F N 1 R 2 = F 1 R
37 1 11 12 abv1z F A 1 R 0 R F 1 R = 1
38 36 37 eqtrd F A 1 R 0 R F N 1 R 2 = 1
39 sq1 1 2 = 1
40 38 39 syl6eqr F A 1 R 0 R F N 1 R 2 = 1 2
41 1 2 abvge0 F A N 1 R B 0 F N 1 R
42 20 41 mpdan F A 0 F N 1 R
43 1re 1
44 0le1 0 1
45 sq11 F N 1 R 0 F N 1 R 1 0 1 F N 1 R 2 = 1 2 F N 1 R = 1
46 43 44 45 mpanr12 F N 1 R 0 F N 1 R F N 1 R 2 = 1 2 F N 1 R = 1
47 22 42 46 syl2anc F A F N 1 R 2 = 1 2 F N 1 R = 1
48 47 biimpa F A F N 1 R 2 = 1 2 F N 1 R = 1
49 40 48 syldan F A 1 R 0 R F N 1 R = 1
50 49 adantlr F A X B 1 R 0 R F N 1 R = 1
51 50 oveq1d F A X B 1 R 0 R F N 1 R F X = 1 F X
52 simpl F A X B F A
53 20 adantr F A X B N 1 R B
54 1 2 25 abvmul F A N 1 R B X B F N 1 R R X = F N 1 R F X
55 52 53 10 54 syl3anc F A X B F N 1 R R X = F N 1 R F X
56 2 25 11 3 5 10 ringnegl F A X B N 1 R R X = N X
57 56 fveq2d F A X B F N 1 R R X = F N X
58 55 57 eqtr3d F A X B F N 1 R F X = F N X
59 58 adantr F A X B 1 R 0 R F N 1 R F X = F N X
60 51 59 eqtr3d F A X B 1 R 0 R 1 F X = F N X
61 1 2 abvcl F A X B F X
62 61 recnd F A X B F X
63 62 mulid2d F A X B 1 F X = F X
64 63 adantr F A X B 1 R 0 R 1 F X = F X
65 60 64 eqtr3d F A X B 1 R 0 R F N X = F X
66 16 65 pm2.61dane F A X B F N X = F X